%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYO681-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:51:44 PM UTC 2026
% Result : Unsatisfiable 1.92s 1.28s
% Output : CNFRefutation 1.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 54
% Syntax : Number of formulae : 276 ( 5 unt; 0 def)
% Number of atoms : 2068 ( 0 equ)
% Maximal formula atoms : 14 ( 7 avg)
% Number of connectives : 3521 (1729 ~;1792 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 10 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 429 ( 0 sgn 429 !; 0 ?; 312 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X0))
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_658) ).
fof(f2,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_592) ).
fof(f3,axiom,
! [X0] : 'LE'(f(X0),s(s(s(s('0'))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_556) ).
fof(f4,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_227) ).
fof(f5,axiom,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_80) ).
fof(f6,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_330) ).
fof(f7,axiom,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0))
| ~ 'LE'(f(X0),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_300) ).
fof(f8,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_415) ).
fof(f9,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_614) ).
fof(f10,axiom,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_607) ).
fof(f11,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_479) ).
fof(f12,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_723) ).
fof(f13,axiom,
! [X2,X0,X1] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_209) ).
fof(f14,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_486) ).
fof(f15,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_687) ).
fof(f16,axiom,
! [X2,X0,X1] :
( ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_528) ).
fof(f17,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_359) ).
fof(f18,axiom,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'('0',f(X0))
| ~ 'LE'(f(X0),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_497) ).
fof(f19,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_463) ).
fof(f20,axiom,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_534) ).
fof(f21,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_228) ).
fof(f22,axiom,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_95) ).
fof(f23,axiom,
! [X2,X0,X1] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_352) ).
fof(f24,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_125) ).
fof(f25,axiom,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_61) ).
fof(f26,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_713) ).
fof(f27,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_560) ).
fof(f28,axiom,
! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_103) ).
fof(f29,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_563) ).
fof(f30,axiom,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_450) ).
fof(f31,axiom,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_501) ).
fof(f32,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_283) ).
fof(f33,axiom,
! [X2,X0,X1] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_137) ).
fof(f34,axiom,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_457) ).
fof(f35,axiom,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_515) ).
fof(f36,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_663) ).
fof(f37,axiom,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_572) ).
fof(f38,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_131) ).
fof(f39,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_458) ).
fof(f40,axiom,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_41) ).
fof(f41,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_223) ).
fof(f42,axiom,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(X0))
| ~ 'LE'(f(X0),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_44) ).
fof(f43,axiom,
! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_550) ).
fof(f44,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_325) ).
fof(f45,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_291) ).
fof(f46,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_383) ).
fof(f47,axiom,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_473) ).
fof(f48,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_594) ).
fof(f49,axiom,
! [X2,X0,X1] :
( ~ 'E'('0',f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_363) ).
fof(f50,axiom,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_145) ).
fof(f51,axiom,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_595) ).
fof(f52,axiom,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_508) ).
fof(f53,axiom,
! [X2,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_671) ).
fof(f54,axiom,
! [X2,X0,X1] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_35) ).
tcf(c_103,plain,
! [X0: $i] :
( 'E'(s(s(s('0'))),f(X0))
| 'LE'(f(X0),s(s(s('0'))))
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_105,plain,
! [X0: $i] : 'LE'(f(X0),s(s(s(s('0'))))),
inference(cnf_transformation,[],[f3]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_109,plain,
! [X0: $i] :
( 'E'(s(s('0')),f(X0))
| 'LE'(f(X0),s(s('0')))
| ~ 'LE'(f(X0),s(s(s('0')))) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_110,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_112,plain,
! [X0: $i] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s(s(s('0')))) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0))) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_119,plain,
~ 'LE'(f(z),'0'),
inference(cnf_transformation,[],[f17]) ).
tcf(c_120,plain,
! [X0: $i] :
( 'E'('0',f(X0))
| 'LE'(f(X0),'0')
| ~ 'LE'(f(X0),s('0')) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_124,plain,
! [X0: $i] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s('0'))) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_126,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_127,plain,
! [X0: $i] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s('0')) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_128,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_129,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_130,plain,
! [X0: $i] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s(s(s(s('0'))))) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_131,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0))) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_134,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_136,plain,
! [X0: $i] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s(s('0')))) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_138,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_144,plain,
! [X0: $i] :
( 'E'(s('0'),f(X0))
| 'LE'(f(X0),s('0'))
| ~ 'LE'(f(X0),s(s('0'))) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_145,plain,
! [X0: $i] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s(s(s('0'))))) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_148,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_153,plain,
! [X0: $i] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s('0')) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_154,plain,
! [X0: $i] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s(s('0'))) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_186,plain,
! [X0: $i] :
( 'E'(s(s(s('0'))),f(X0))
| 'LE'(f(X0),s(s(s('0')))) ),
inference(global_subsumption_just,[status(thm)],[c_103,c_105,c_103]) ).
tcf(c_189,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(global_subsumption_just,[status(thm)],[c_129,c_128,c_129]) ).
tcf(c_192,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(global_subsumption_just,[status(thm)],[c_126,c_131,c_126]) ).
tcf(c_195,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_110,c_148,c_110]) ).
tcf(c_196,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(renaming,[status(thm)],[c_195]) ).
tcf(c_198,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_138,c_134,c_138]) ).
tcf(c_199,plain,
! [X0: $i] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(renaming,[status(thm)],[c_198]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(global_subsumption_just,[status(thm)],[c_141,c_111,c_141]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(global_subsumption_just,[status(thm)],[c_104,c_117,c_104]) ).
tcf(c_209,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2))) ),
inference(global_subsumption_just,[status(thm)],[c_114,c_121,c_114]) ).
tcf(c_210,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(renaming,[status(thm)],[c_209]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1))) ),
inference(global_subsumption_just,[status(thm)],[c_151,c_115,c_151]) ).
tcf(c_214,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(renaming,[status(thm)],[c_213]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2)) ),
inference(global_subsumption_just,[status(thm)],[c_106,c_116,c_106]) ).
tcf(c_216,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(renaming,[status(thm)],[c_215]) ).
tcf(c_219,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1))) ),
inference(global_subsumption_just,[status(thm)],[c_142,c_156,c_142]) ).
tcf(c_220,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(renaming,[status(thm)],[c_219]) ).
tcf(c_223,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1))) ),
inference(global_subsumption_just,[status(thm)],[c_118,c_125,c_118]) ).
tcf(c_224,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(renaming,[status(thm)],[c_223]) ).
tcf(c_225,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1))) ),
inference(global_subsumption_just,[status(thm)],[c_140,c_135,c_140]) ).
tcf(c_226,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(renaming,[status(thm)],[c_225]) ).
tcf(c_231,plain,
! [X0: $i] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_145,c_105]) ).
tcf(c_232,plain,
! [X0: $i] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_130,c_105]) ).
tcf(c_386,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_132,c_111]) ).
tcf(c_388,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_143,c_111]) ).
tcf(c_411,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_113,c_201]) ).
tcf(c_435,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_139,c_386]) ).
tcf(c_457,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_411,c_388]) ).
tcf(c_459,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_435,c_388]) ).
tcf(c_504,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_214,c_457]) ).
tcf(c_527,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_504,c_459]) ).
tcf(c_572,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_107,c_117]) ).
tcf(c_574,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_123,c_117]) ).
tcf(c_597,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_155,c_204]) ).
tcf(c_621,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_152,c_572]) ).
tcf(c_643,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_597,c_574]) ).
tcf(c_645,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_621,c_574]) ).
tcf(c_690,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_220,c_643]) ).
tcf(c_713,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_690,c_645]) ).
tcf(c_736,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_133,c_121]) ).
tcf(c_738,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_150,c_121]) ).
tcf(c_783,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_146,c_210]) ).
tcf(c_807,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_137,c_736]) ).
tcf(c_829,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_783,c_738]) ).
tcf(c_831,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_807,c_738]) ).
tcf(c_853,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_149,c_116]) ).
tcf(c_855,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_108,c_116]) ).
tcf(c_900,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_224,c_829]) ).
tcf(c_923,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_900,c_831]) ).
tcf(c_969,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_147,c_216]) ).
tcf(c_993,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_122,c_853]) ).
tcf(c_1015,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_969,c_855]) ).
tcf(c_1017,plain,
! [X0: $i,X1: $i,X2: $i] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_993,c_855]) ).
tcf(c_1062,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_226,c_1015]) ).
tcf(c_1085,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1062,c_1017]) ).
tcf(c_1297,plain,
( 'E'('0',f(z))
| 'LE'(f(z),'0')
| ~ 'LE'(f(z),s('0')) ),
inference(instantiation,[status(thm)],[c_120]) ).
tcf(c_1298,plain,
( 'LE'(f(z),'0')
| 'E'('0',f(suc(suc(z))))
| ~ 'LE'(f(suc(suc(z))),s('0')) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_1299,plain,
( 'LE'(f(z),'0')
| 'E'('0',f(suc(z)))
| ~ 'LE'(f(suc(z)),s('0')) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_1300,plain,
! [X0: $i,X1: $i] :
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(z),suc(X0))
| ~ iLEQ(suc(X1),suc(z))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(instantiation,[status(thm)],[c_527]) ).
tcf(c_1301,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_189]) ).
tcf(c_1309,plain,
! [X0: $i] :
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(suc(z)))
| ~ iLEQ(suc(X0),suc(z))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(instantiation,[status(thm)],[c_1300]) ).
tcf(c_1327,plain,
( ~ 'E'('0',f(z))
| ~ iLEQ(suc(z),suc(z))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_1309]) ).
tcf(c_1336,plain,
( 'LE'(f(z),s('0'))
| 'E'(s('0'),f(suc(suc(z))))
| ~ 'LE'(f(suc(suc(z))),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_1337,plain,
( 'E'(s('0'),f(z))
| 'LE'(f(z),s('0'))
| ~ 'LE'(f(z),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_1338,plain,
( 'LE'(f(z),s('0'))
| 'E'(s('0'),f(suc(z)))
| ~ 'LE'(f(suc(z)),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_1339,plain,
( 'LE'(f(suc(suc(z))),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ 'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_1340,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'LE'(f(suc(suc(z))),s('0'))
| ~ 'LE'(f(suc(suc(z))),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_1341,plain,
( 'LE'(f(suc(suc(z))),s('0'))
| 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'LE'(f(suc(suc(suc(z)))),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_1342,plain,
( 'LE'(f(suc(z)),s('0'))
| 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'LE'(f(suc(suc(suc(z)))),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_1343,plain,
( 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0'))
| ~ 'LE'(f(suc(z)),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_1344,plain,
( 'LE'(f(suc(z)),s('0'))
| 'E'(s('0'),f(suc(suc(z))))
| ~ 'LE'(f(suc(suc(z))),s(s('0'))) ),
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_1345,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ iLEQ(suc(X1),suc(suc(suc(z))))
| ~ iLEQ(suc(suc(suc(z))),suc(X0))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_713]) ).
tcf(c_1346,plain,
( iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_1348,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s('0'),f(z))
| ~ iLEQ(suc(z),suc(X0))
| ~ iLEQ(suc(X1),suc(z))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(instantiation,[status(thm)],[c_713]) ).
tcf(c_1349,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_1351,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(z)))
| ~ iLEQ(suc(X1),suc(suc(z)))
| ~ iLEQ(suc(suc(z)),suc(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_713]) ).
tcf(c_1352,plain,
( iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_192]) ).
tcf(c_1368,plain,
( 'LE'(f(suc(suc(z))),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'LE'(f(suc(suc(suc(z)))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_1369,plain,
( 'LE'(f(suc(suc(z))),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_1370,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'LE'(f(suc(suc(z))),s(s('0')))
| ~ 'LE'(f(suc(suc(z))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_109]) ).
tcf(c_1377,plain,
( 'LE'(f(z),s(s('0')))
| 'E'(s(s('0')),f(suc(z)))
| ~ 'LE'(f(suc(z)),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_1378,plain,
( 'LE'(f(z),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'LE'(f(suc(suc(z))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_1379,plain,
( 'E'(s(s('0')),f(z))
| 'LE'(f(z),s(s('0')))
| ~ 'LE'(f(z),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_109]) ).
tcf(c_1380,plain,
( 'LE'(f(suc(z)),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'LE'(f(suc(suc(z))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_1381,plain,
( 'LE'(f(suc(z)),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'LE'(f(suc(suc(suc(z)))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_1382,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'LE'(f(suc(z)),s(s('0')))
| ~ 'LE'(f(suc(z)),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_109]) ).
tcf(c_1386,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_1387,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_1388,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| ~ 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_109]) ).
tcf(c_1389,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_1390,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_1391,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| ~ 'LE'(f(suc(suc(suc(z)))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_109]) ).
tcf(c_1395,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(suc(suc(suc(z)))))
| ~ iLEQ(suc(suc(suc(suc(z)))),suc(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_923]) ).
tcf(c_1396,plain,
( iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_1398,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(suc(suc(suc(suc(z))))))
| ~ iLEQ(suc(suc(suc(suc(suc(z))))),suc(X0))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_923]) ).
tcf(c_1399,plain,
( iLEQ(suc(suc(suc(suc(suc(z))))),suc(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_1401,plain,
! [X0: $i,X1: $i] :
( ~ iLEQ(suc(z),suc(X0))
| ~ iLEQ(suc(X1),suc(z))
| ~ 'E'(s(s('0')),f(z))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(instantiation,[status(thm)],[c_923]) ).
tcf(c_1402,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'(s(s('0')),f(z))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_1404,plain,
! [X0: $i,X1: $i] :
( ~ iLEQ(suc(X1),suc(suc(z)))
| ~ iLEQ(suc(suc(z)),suc(X0))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_923]) ).
tcf(c_1405,plain,
( iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_1407,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X1),suc(suc(suc(z))))
| ~ iLEQ(suc(suc(suc(z))),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_923]) ).
tcf(c_1408,plain,
( iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_1424,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1425,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_1426,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_1430,plain,
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1431,plain,
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_1432,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_1433,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1434,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_1435,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'LE'(f(suc(suc(suc(z)))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_1445,plain,
( 'LE'(f(z),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1446,plain,
( 'LE'(f(z),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(z))) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_1447,plain,
( 'E'(s(s(s('0'))),f(z))
| 'LE'(f(z),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_1535,plain,
( 'LE'(f(suc(z)),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1536,plain,
( 'LE'(f(suc(z)),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_1537,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| 'LE'(f(suc(z)),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_1541,plain,
( 'LE'(f(suc(suc(z))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1542,plain,
( 'LE'(f(suc(suc(z))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_1543,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'LE'(f(suc(suc(z))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_1595,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ iLEQ(suc(X1),suc(suc(suc(suc(z)))))
| ~ iLEQ(suc(suc(suc(suc(z)))),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_1085]) ).
tcf(c_1596,plain,
( iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_1598,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(suc(suc(suc(suc(z))))))
| ~ iLEQ(suc(suc(suc(suc(suc(z))))),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_1085]) ).
tcf(c_1599,plain,
( iLEQ(suc(suc(suc(suc(suc(z))))),suc(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_1665,plain,
( 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))) ),
inference(instantiation,[status(thm)],[c_232]) ).
tcf(c_1666,plain,
( 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_1667,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s(s('0')))) ),
inference(instantiation,[status(thm)],[c_186]) ).
tcf(c_1668,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(suc(suc(suc(suc(suc(suc(z))))))))
| ~ iLEQ(suc(suc(suc(suc(suc(suc(suc(z))))))),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))) ),
inference(instantiation,[status(thm)],[c_1085]) ).
tcf(c_1669,plain,
( iLEQ(suc(suc(suc(suc(suc(suc(suc(z))))))),suc(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_1792,plain,
! [X0: $i,X1: $i] :
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(suc(suc(suc(suc(suc(z)))))))
| ~ iLEQ(suc(suc(suc(suc(suc(suc(z)))))),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
inference(instantiation,[status(thm)],[c_1085]) ).
tcf(c_1793,plain,
( iLEQ(suc(suc(suc(suc(suc(suc(z)))))),suc(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_1806,plain,
! [X0: $i,X1: $i] :
( ~ iLEQ(suc(X1),suc(suc(suc(z))))
| ~ iLEQ(suc(suc(suc(z))),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_1085]) ).
tcf(c_1807,plain,
( iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_1809,plain,
! [X0: $i,X1: $i] :
( ~ iLEQ(suc(X1),suc(suc(z)))
| ~ iLEQ(suc(suc(z)),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_1085]) ).
tcf(c_1810,plain,
( iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_1812,plain,
! [X0: $i,X1: $i] :
( ~ iLEQ(suc(z),suc(X0))
| ~ iLEQ(suc(X1),suc(z))
| ~ 'E'(s(s(s('0'))),f(z))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(instantiation,[status(thm)],[c_1085]) ).
tcf(c_1813,plain,
( iLEQ(suc(z),suc(z))
| ~ 'E'(s(s(s('0'))),f(z))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_1851,plain,
! [X0: $i] :
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z))
| ~ iLEQ(suc(X0),suc(z))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(instantiation,[status(thm)],[c_1348]) ).
tcf(c_1856,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s('0'),f(z))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_1851]) ).
tcf(c_1871,plain,
! [X0: $i] :
( ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X0),suc(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_1407]) ).
tcf(c_1875,plain,
( ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_1871]) ).
tcf(c_1937,plain,
! [X0: $i] :
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(X0))
| ~ 'E'(s(s('0')),f(z))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(instantiation,[status(thm)],[c_1401]) ).
tcf(c_1939,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s(s('0')),f(z))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_1937]) ).
tcf(c_1949,plain,
! [X0: $i] :
( ~ iLEQ(suc(z),suc(z))
| ~ iLEQ(suc(z),suc(X0))
| ~ 'E'(s(s(s('0'))),f(z))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(instantiation,[status(thm)],[c_1812]) ).
tcf(c_1951,plain,
( ~ iLEQ(suc(z),suc(z))
| ~ 'E'(s(s(s('0'))),f(z))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(instantiation,[status(thm)],[c_1949]) ).
tcf(c_1977,plain,
! [X0: $i] :
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ iLEQ(suc(X0),suc(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_1345]) ).
tcf(c_1987,plain,
! [X0: $i] :
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(z)))
| ~ iLEQ(suc(X0),suc(suc(z)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_1351]) ).
tcf(c_1993,plain,
( ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_1977]) ).
tcf(c_1998,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_1987]) ).
tcf(c_2026,plain,
! [X0: $i] :
( ~ 'E'(s(s(s('0'))),f(X0))
| ~ iLEQ(suc(X0),suc(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_1595]) ).
tcf(c_2083,plain,
! [X0: $i] :
( ~ iLEQ(suc(X0),suc(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_1806]) ).
tcf(c_2087,plain,
! [X0: $i] :
( ~ iLEQ(suc(X0),suc(suc(z)))
| ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_1809]) ).
tcf(c_2089,plain,
( ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_2087]) ).
tcf(c_2093,plain,
( ~ iLEQ(suc(suc(suc(z))),suc(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_2083]) ).
tcf(c_2140,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_2026]) ).
tcf(c_2328,plain,
! [X0: $i] :
( ~ iLEQ(suc(X0),suc(suc(z)))
| ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_1404]) ).
tcf(c_2336,plain,
! [X0: $i] :
( ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ iLEQ(suc(suc(suc(suc(suc(z))))),suc(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_1598]) ).
tcf(c_2344,plain,
( ~ iLEQ(suc(suc(z)),suc(suc(z)))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z))))) ),
inference(instantiation,[status(thm)],[c_2328]) ).
tcf(c_2414,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ iLEQ(suc(suc(suc(suc(suc(z))))),suc(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_2336]) ).
tcf(c_2470,plain,
! [X0: $i] :
( ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ iLEQ(suc(suc(suc(suc(suc(suc(z)))))),suc(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_1792]) ).
tcf(c_2479,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ iLEQ(suc(suc(suc(suc(suc(suc(z)))))),suc(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_2470]) ).
tcf(c_2486,plain,
! [X0: $i] :
( ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ iLEQ(suc(suc(suc(suc(suc(z))))),suc(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_1398]) ).
tcf(c_2548,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ iLEQ(suc(suc(suc(suc(suc(z))))),suc(suc(suc(suc(suc(z)))))) ),
inference(instantiation,[status(thm)],[c_2486]) ).
tcf(c_2581,plain,
! [X0: $i] :
( ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ iLEQ(suc(suc(suc(suc(suc(suc(suc(z))))))),suc(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_1668]) ).
tcf(c_2589,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ iLEQ(suc(suc(suc(suc(suc(suc(suc(z))))))),suc(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(instantiation,[status(thm)],[c_2581]) ).
tcf(c_2642,plain,
! [X0: $i] :
( ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_1395]) ).
tcf(c_2721,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ iLEQ(suc(suc(suc(suc(z)))),suc(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z))))))) ),
inference(instantiation,[status(thm)],[c_2642]) ).
tcf(c_2722,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_2721,c_2589,c_2548,c_2479,c_2414,c_2344,c_2140,c_2093,c_2089,c_1998,c_1993,c_1951,c_1939,c_1875,c_1856,c_1813,c_1810,c_1807,c_1793,c_1669,c_1665,c_1666,c_1667,c_1599,c_1596,c_1541,c_1542,c_1543,c_1535,c_1536,c_1537,c_1445,c_1446,c_1447,c_1433,c_1434,c_1435,c_1430,c_1431,c_1432,c_1424,c_1425,c_1426,c_1408,c_1405,c_1402,c_1399,c_1396,c_1389,c_1390,c_1391,c_1386,c_1387,c_1388,c_1380,c_1381,c_1382,c_1377,c_1378,c_1379,c_1368,c_1369,c_1370,c_1352,c_1349,c_1346,c_1342,c_1343,c_1344,c_1339,c_1340,c_1341,c_1336,c_1337,c_1338,c_1327,c_1301,c_1299,c_1298,c_1297,c_119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO681-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n010.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 03:23:30 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 1.92/1.28 % SZS status Started for theBenchmark.p
% 1.92/1.28 % SZS status Unsatisfiable for theBenchmark.p
% 1.92/1.28
% 1.92/1.28 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.92/1.28
% 1.92/1.28 % ------ iProver source info
% 1.92/1.28
% 1.92/1.28 % git: date: 2026-07-19 20:42:38 +0200
% 1.92/1.28 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.92/1.28 % git: non_committed_changes: false
% 1.92/1.28
% 1.92/1.28 % ------ Parsing...% successful
% 1.92/1.28
% 1.92/1.28
% 1.92/1.28 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.92/1.28
% 1.92/1.28 % ------ Preprocessing... sf_s rm: 33 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 1.92/1.28
% 1.92/1.28 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 1.92/1.28 % ------ Proving...
% 1.92/1.28 % ------ Problem Properties
% 1.92/1.28
% 1.92/1.28 %
% 1.92/1.28 % clauses 21
% 1.92/1.28 % conjectures 0
% 1.92/1.28 % EPR 0
% 1.92/1.28 % Horn 9
% 1.92/1.28 % unary 1
% 1.92/1.28 % binary 3
% 1.92/1.28 % lits 94
% 1.92/1.28 % lits eq 0
% 1.92/1.28 % fd_pure 0
% 1.92/1.28 % fd_pseudo 0
% 1.92/1.28 % fd_cond 0
% 1.92/1.28 % fd_pseudo_cond 0
% 1.92/1.28 % AC symbols 0
% 1.92/1.28
% 1.92/1.28 % ------ Schedule dynamic 5 is on
% 1.92/1.28
% 1.92/1.28 % ------ no conjectures: strip conj schedule
% 1.92/1.28
% 1.92/1.28 % ------ no equalities: superposition off
% 1.92/1.28
% 1.92/1.28 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 1.92/1.28
% 1.92/1.28
% 1.92/1.28 % ------
% 1.92/1.28 % Current options:
% 1.92/1.28 % ------
% 1.92/1.28
% 1.92/1.28
% 1.92/1.28 %
% 1.92/1.28
% 1.92/1.28 % ------ Proving...
% 1.92/1.28 %
% 1.92/1.28
% 1.92/1.28 % SZS status Unsatisfiable for theBenchmark.p
% 1.92/1.28
% 1.92/1.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.92/1.29
% 1.92/1.29
%------------------------------------------------------------------------------