SUCCESS
53.47 (total time)


COMPLETED TRS

 
                                    trans(x0, refl()) -> x0,
                             trans(trans(x0, y0), z0) ->
 trans(x0, trans(y0, z0)),
                                    trans(refl(), x0) -> x0,
           trans(congror1(x0), trans(orfalse2(), z1)) ->
 trans(orfalse2(), trans(x0, z1)),
                       trans(congror1(x0), ortrue2()) -> ortrue2(),
                      trans(congror1(x0), orfalse2()) ->
 trans(orfalse2(), x0),
         trans(congror1(z8), trans(congror2(y8), z9)) ->
 trans(congror2(y8), trans(congror1(z8), z9)),
                    trans(congror1(z8), congror2(y8)) ->
 trans(congror2(y8), congror1(z8)),
         trans(congror1(x8), trans(congror1(z8), z9)) ->
 trans(congror1(trans(x8, z8)), z9),
                    trans(congror1(x8), congror1(z8)) ->
 congror1(trans(x8, z8)),
 trans(congror2(x0), trans(congror1(z18), ortrue1())) ->
 trans(congror1(z18), ortrue1()),
                       trans(congror2(x0), ortrue1()) -> ortrue1(),
         trans(congror2(y4), trans(congror2(w4), z5)) ->
 trans(congror2(trans(y4, w4)), z5),
                    trans(congror2(y4), congror2(w4)) ->
 congror2(trans(y4, w4)),
                                 trans(ortrue2(), x0) -> ortrue2(),
                                 trans(ortrue1(), x0) -> ortrue1(),
                                trans(orfalse1(), x0) ->
 trans(congror2(x0), orfalse1()),
                                     congror1(refl()) -> refl(),
                                     congror2(refl()) -> refl()



STATISTICS

total time:   53.47
termination:  43.78

external termination prover: ttt2fast
calls to termination prover: 262 (yes: 217, timeouts: 0)
time limit per call:         1.0