SUCCESS 1637.00 (total time) COMPLETED TRS trans(x, refl()) -> x, trans(trans(x, y), z) -> trans(x, trans(y, z)), trans(refl(), x) -> x, trans(CongrOr1(x), trans(CongrOr1(y), z)) -> trans(CongrOr1(trans(x, y)), z), trans(CongrOr1(x), trans(OrFalse2(), y)) -> trans(OrFalse2(), trans(x, y)), trans(CongrOr1(x), CongrOr1(y)) -> CongrOr1(trans(x, y)), trans(CongrOr1(x), OrTrue2()) -> OrTrue2(), trans(CongrOr1(x), OrFalse2()) -> trans(OrFalse2(), x), trans(CongrOr1(y), trans(CongrOr2(x), trans(OrFalse2(), z))) -> trans(CongrOr2(x), trans(OrFalse2(), trans(y, z))), trans(CongrOr1(y), trans(CongrOr2(x), CongrOr1(z))) -> trans(CongrOr2(x), CongrOr1(trans(y, z))), trans(CongrOr1(y), trans(CongrOr2(x), OrTrue2())) -> trans(CongrOr2(x), OrTrue2()), trans(CongrOr1(y), trans(CongrOr2(x), OrFalse2())) -> trans(CongrOr2(x), trans(OrFalse2(), y)), trans(CongrOr1(y), trans(OrTrue2(), x)) -> trans(OrTrue2(), x), trans(CongrOr1(y), CongrOr2(x)) -> trans(CongrOr2(x), CongrOr1(y)), trans(CongrOr1(z), trans(CongrOr2(x), trans(OrTrue2(), y))) -> trans(CongrOr2(x), trans(OrTrue2(), y)), trans(CongrOr2(x), trans(CongrOr1(y), z)) -> trans(CongrOr1(y), trans(CongrOr2(x), z)), trans(CongrOr2(x), trans(CongrOr2(y), z)) -> trans(CongrOr2(trans(x, y)), z), trans(CongrOr2(x), trans(OrFalse1(), y)) -> trans(OrFalse1(), trans(x, y)), trans(CongrOr2(x), CongrOr2(y)) -> CongrOr2(trans(x, y)), trans(CongrOr2(x), OrTrue1()) -> OrTrue1(), trans(CongrOr2(x), OrFalse1()) -> trans(OrFalse1(), x), trans(CongrOr2(y), trans(OrTrue1(), x)) -> trans(OrTrue1(), x), trans(CongrAnd1(x), trans(CongrAnd1(y), z)) -> trans(CongrAnd1(trans(x, y)), z), trans(CongrAnd1(x), trans(AndTrue2(), y)) -> trans(AndTrue2(), trans(x, y)), trans(CongrAnd1(x), CongrAnd1(y)) -> CongrAnd1(trans(x, y)), trans(CongrAnd1(x), AndFalse2()) -> AndFalse2(), trans(CongrAnd1(x), AndTrue2()) -> trans(AndTrue2(), x), trans(CongrAnd1(y), trans(CongrAnd2(x), trans(AndTrue2(), z))) -> trans(CongrAnd2(x), trans(AndTrue2(), trans(y, z))), trans(CongrAnd1(y), trans(CongrAnd2(x), CongrAnd1(z))) -> trans(CongrAnd2(x), CongrAnd1(trans(y, z))), trans(CongrAnd1(y), trans(CongrAnd2(x), AndFalse2())) -> trans(CongrAnd2(x), AndFalse2()), trans(CongrAnd1(y), trans(CongrAnd2(x), AndTrue2())) -> trans(CongrAnd2(x), trans(AndTrue2(), y)), trans(CongrAnd1(y), trans(AndFalse2(), x)) -> trans(AndFalse2(), x), trans(CongrAnd1(y), CongrAnd2(x)) -> trans(CongrAnd2(x), CongrAnd1(y)), trans(CongrAnd1(z), trans(CongrAnd2(x), trans(AndFalse2(), y))) -> trans(CongrAnd2(x), trans(AndFalse2(), y)), trans(CongrAnd2(x), trans(CongrAnd1(y), z)) -> trans(CongrAnd1(y), trans(CongrAnd2(x), z)), trans(CongrAnd2(x), trans(CongrAnd2(y), z)) -> trans(CongrAnd2(trans(x, y)), z), trans(CongrAnd2(x), trans(AndTrue1(), y)) -> trans(AndTrue1(), trans(x, y)), trans(CongrAnd2(x), CongrAnd2(y)) -> CongrAnd2(trans(x, y)), trans(CongrAnd2(x), AndFalse1()) -> AndFalse1(), trans(CongrAnd2(x), AndTrue1()) -> trans(AndTrue1(), x), trans(CongrAnd2(y), trans(AndFalse1(), x)) -> trans(AndFalse1(), x), trans(CongrNot(x), trans(CongrNot(y), z)) -> trans(CongrNot(trans(x, y)), z), trans(CongrNot(x), CongrNot(y)) -> CongrNot(trans(x, y)), CongrOr1(refl()) -> refl(), CongrOr2(refl()) -> refl(), CongrAnd1(refl()) -> refl(), CongrAnd2(refl()) -> refl(), CongrNot(refl()) -> refl() STATISTICS number of inference steps: 65 total time: 1637.00 orient: 1618.40 rewrite: 16.62 deduce: 1.32 termination: 1555.94 external termination prover: ./ttt2micro calls to termination prover: 2668 (yes: 1693, timeouts: 0) time limit per call: 5.0