SUCCESS
230.06 (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), z)) ->
 trans(congror2(x), trans(congror1(y), z)),
                   trans(congror1(y), congror2(x)) ->
 trans(congror2(x), congror1(y)),
 trans(congror2(x), trans(congror1(y), ortrue1())) ->
 trans(congror1(y), ortrue1()),
         trans(congror2(x), trans(congror2(y), z)) ->
 trans(congror2(trans(x, y)), z),
                   trans(congror2(x), congror2(y)) -> congror2(trans(x, y)),
                     trans(congror2(x), ortrue1()) -> ortrue1(),
                               trans(ortrue2(), x) -> ortrue2(),
                               trans(ortrue1(), x) -> ortrue1(),
                              trans(orfalse1(), x) ->
 trans(congror2(x), orfalse1()),
                                  congror1(refl()) -> refl(),
                                  congror2(refl()) -> refl()



STATISTICS

number of inference steps: 26 

total time:   230.06
orient:       223.66
rewrite:      5.83
deduce:       0.43
termination:  211.53

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