SUCCESS
6.64 (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), congror2(x)) ->
 trans(congror2(x), congror1(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(ortrue2(), x) -> ortrue2(),
                                          trans(ortrue1(), x) -> ortrue1(),
                                             congror1(refl()) -> refl(),
                                             congror2(refl()) -> refl()



STATISTICS

number of inference steps: 34 

total time:   6.64
orient:       4.85
rewrite:      1.58
deduce:       0.17
termination:  4.77

termination checked internally with TTT2
calls to termination prover: 161 (yes: 104, timeouts: 0)
time limit per call:         0.7