SUCCESS 54.47 (total time) COMPLETED TRS trans(x10, refl()) -> x10, trans(trans(x10, x20), x30) -> trans(x10, trans(x20, x30)), trans(refl(), x10) -> x10, trans(congror1(x10), trans(orfalse2(), x31)) -> trans(orfalse2(), trans(x10, x31)), trans(congror1(x10), ortrue2()) -> ortrue2(), trans(congror1(x10), orfalse2()) -> trans(orfalse2(), x10), trans(congror1(x38), trans(congror2(x28), x39)) -> trans(congror2(x28), trans(congror1(x38), x39)), trans(congror1(x38), congror2(x28)) -> trans(congror2(x28), congror1(x38)), trans(congror1(x18), trans(congror1(x38), x39)) -> trans(congror1(trans(x18, x38)), x39), trans(congror1(x18), congror1(x38)) -> congror1(trans(x18, x38)), trans(congror2(x10), trans(congror1(x318), ortrue1())) -> trans(congror1(x318), ortrue1()), trans(congror2(x10), ortrue1()) -> ortrue1(), trans(congror2(x24), trans(congror2(x44), x35)) -> trans(congror2(trans(x24, x44)), x35), trans(congror2(x24), congror2(x44)) -> congror2(trans(x24, x44)), trans(ortrue2(), x10) -> ortrue2(), trans(ortrue1(), x10) -> ortrue1(), trans(orfalse1(), x10) -> trans(congror2(x10), orfalse1()), congror1(refl()) -> refl(), congror2(refl()) -> refl() STATISTICS total time: 54.47 termination: 44.70 external termination prover: ttt2fast calls to termination prover: 266 (yes: 219, timeouts: 0) time limit per call: 1.0