%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYO688-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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 : Thu Sep 24 03:43:10 PM UTC 2026
% Result : Unsatisfiable 37.03s 10.32s
% Output : CNFRefutation 37.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 39
% Syntax : Number of formulae : 190 ( 11 unt; 0 def)
% Number of atoms : 1095 ( 0 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 1741 ( 836 ~; 905 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 9 avg)
% Maximal term depth : 6 ( 2 avg)
% 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 : 480 ( 480 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f92,axiom,
! [LE,A] : 'LE'(f(A),s(s(s(s(s('0')))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [A_5,B_94,E,B_95] :
( ~ 'E'('0',f(B_95))
| ~ 'E'('0',f(suc(B_95)))
| ~ 'E'('0',f(B_94))
| ~ iLEQ(suc(B_94),suc(B_95))
| ~ 'E'(f(A_5),f(suc(A_5)))
| ~ 'E'(f(B_94),f(suc(B_94)))
| ~ 'E'(f(B_95),f(suc(B_95)))
| ~ 'E'('0',f(suc(suc(A_5))))
| ~ 'E'('0',f(suc(A_5)))
| ~ 'E'('0',f(suc(suc(B_95))))
| ~ 'E'('0',f(suc(suc(B_94))))
| ~ 'E'('0',f(suc(B_94)))
| ~ 'E'('0',f(A_5))
| ~ iLEQ(suc(A_5),suc(B_94)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,axiom,
! [LE,B_74,E] :
( 'LE'(f(B_74),s(s('0')))
| 'E'(s(s('0')),f(suc(B_74)))
| ~ 'LE'(f(suc(B_74)),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [LE,B_56,E] :
( 'LE'(f(B_56),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(B_56))))
| ~ 'LE'(f(suc(suc(B_56))),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,axiom,
! [E,A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(A_2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,axiom,
! [LE,B_86,E] :
( 'LE'(f(B_86),s('0'))
| 'E'(s('0'),f(B_86))
| ~ 'LE'(f(B_86),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,axiom,
! [LE,B_56,E] :
( 'LE'(f(B_56),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(B_56)))
| ~ 'LE'(f(suc(B_56)),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,axiom,
! [E,A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ 'E'(s(s(s('0'))),f(A_2))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A_2)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,axiom,
! [E,B_33,B_32,A_1] :
( 'E'(f(B_32),f(suc(B_32)))
| 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))
| ~ 'E'(s(s(s(s('0')))),f(B_32))
| ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_32))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ 'E'(f(B_33),f(suc(B_33)))
| ~ iLEQ(suc(B_32),suc(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_33)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f226,axiom,
! [LE,B_93,E] :
( 'LE'(f(B_93),'0')
| 'E'('0',f(B_93))
| ~ 'LE'(f(B_93),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f279,axiom,
! [E,A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ 'E'(s(s('0')),f(A_3))
| ~ 'E'(f(A_3),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(suc(A_3)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f354,axiom,
! [E,A_1,B_32,B_33] :
( 'E'(f(B_33),f(suc(B_33)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))
| ~ 'E'(s(s(s(s('0')))),f(B_32))
| ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_32))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_32))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ iLEQ(suc(B_32),suc(B_33))
| ~ 'E'(f(B_32),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f360,axiom,
! [E,A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ 'E'(s('0'),f(A_4))
| ~ 'E'(f(A_4),f(suc(A_4)))
| ~ 'E'(s('0'),f(suc(A_4)))
| ~ 'E'(s('0'),f(suc(suc(A_4)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f366,axiom,
! [LE] : ~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f384,axiom,
! [E,B_88,A_4,B_87] :
( ~ iLEQ(suc(A_4),suc(B_87))
| ~ 'E'(s('0'),f(A_4))
| ~ 'E'(s('0'),f(suc(suc(B_88))))
| ~ 'E'(s('0'),f(suc(A_4)))
| ~ iLEQ(suc(B_87),suc(B_88))
| ~ 'E'(s('0'),f(B_87))
| ~ 'E'(s('0'),f(suc(B_87)))
| ~ 'E'(f(B_88),f(suc(B_88)))
| ~ 'E'(f(B_87),f(suc(B_87)))
| ~ 'E'(s('0'),f(suc(suc(B_87))))
| ~ 'E'(s('0'),f(suc(suc(A_4))))
| ~ 'E'(s('0'),f(suc(B_88)))
| ~ 'E'(f(A_4),f(suc(A_4)))
| ~ 'E'(s('0'),f(B_88)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f402,axiom,
! [E,B_33,A_1,B_32] :
( ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))
| ~ 'E'(s(s(s(s('0')))),f(B_32))
| ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_32))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_32))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ 'E'(f(B_33),f(suc(B_33)))
| ~ iLEQ(suc(B_32),suc(B_33))
| ~ 'E'(f(B_32),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A_1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_33)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f470,axiom,
! [E,A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f502,axiom,
! [LE,B_74,E] :
( 'LE'(f(B_74),s(s('0')))
| 'E'(s(s('0')),f(B_74))
| ~ 'LE'(f(B_74),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f535,axiom,
! [LE,B_86,E] :
( 'LE'(f(B_86),s('0'))
| 'E'(s('0'),f(suc(suc(B_86))))
| ~ 'LE'(f(suc(suc(B_86))),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f580,axiom,
! [LE,B_31,E] :
( 'LE'(f(B_31),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(B_31))))
| ~ 'LE'(f(suc(suc(B_31))),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f581,axiom,
! [E,A_5] :
( iLEQ(suc(A_5),suc(A_5))
| 'E'(f(A_5),f(suc(A_5)))
| ~ 'E'('0',f(suc(A_5)))
| ~ 'E'('0',f(A_5)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f587,axiom,
! [E,B_75,A_3,B_76] :
( 'E'(f(B_76),f(suc(B_76)))
| 'E'(f(B_75),f(suc(B_75)))
| 'E'(f(A_3),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(A_3))
| ~ 'E'(s(s('0')),f(B_75))
| ~ iLEQ(suc(A_3),suc(B_75))
| ~ iLEQ(suc(B_75),suc(B_76))
| ~ 'E'(s(s('0')),f(B_76))
| ~ 'E'(s(s('0')),f(suc(B_76)))
| ~ 'E'(s(s('0')),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(B_75))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f660,axiom,
! [LE,B_93,E] :
( 'LE'(f(B_93),'0')
| 'E'('0',f(suc(suc(B_93))))
| ~ 'LE'(f(suc(suc(B_93))),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f692,axiom,
! [LE,B_86,E] :
( 'LE'(f(B_86),s('0'))
| 'E'(s('0'),f(suc(B_86)))
| ~ 'LE'(f(suc(B_86)),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f720,axiom,
! [E,A_5] :
( iLEQ(suc(A_5),suc(A_5))
| ~ 'E'('0',f(A_5))
| ~ 'E'(f(A_5),f(suc(A_5)))
| ~ 'E'('0',f(suc(A_5)))
| ~ 'E'('0',f(suc(suc(A_5)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f756,axiom,
! [E,B_88,B_87,A_4] :
( 'E'(f(B_88),f(suc(B_88)))
| 'E'(f(B_87),f(suc(B_87)))
| 'E'(f(A_4),f(suc(A_4)))
| ~ iLEQ(suc(A_4),suc(B_87))
| ~ 'E'(s('0'),f(A_4))
| ~ 'E'(s('0'),f(suc(A_4)))
| ~ iLEQ(suc(B_87),suc(B_88))
| ~ 'E'(s('0'),f(B_87))
| ~ 'E'(s('0'),f(suc(B_87)))
| ~ 'E'(s('0'),f(suc(B_88)))
| ~ 'E'(s('0'),f(B_88)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f809,axiom,
! [B_32,B_33,E,A_1] :
( 'E'(f(B_33),f(suc(B_33)))
| 'E'(f(B_32),f(suc(B_32)))
| 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))
| ~ 'E'(s(s(s(s('0')))),f(B_32))
| ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_32))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ iLEQ(suc(B_32),suc(B_33)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f852,axiom,
! [E,A_4] :
( iLEQ(suc(A_4),suc(A_4))
| 'E'(f(A_4),f(suc(A_4)))
| ~ 'E'(s('0'),f(suc(A_4)))
| ~ 'E'(s('0'),f(A_4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f894,axiom,
! [LE,B_31,E] :
( 'LE'(f(B_31),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(B_31))
| ~ 'LE'(f(B_31),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f914,axiom,
! [LE,B_74,E] :
( 'LE'(f(B_74),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(B_74))))
| ~ 'LE'(f(suc(suc(B_74))),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f932,axiom,
! [E,B_58,A_2,B_57] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(B_57))))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A_2))))
| ~ 'E'(s(s(s('0'))),f(suc(B_58)))
| ~ 'E'(s(s(s('0'))),f(B_58))
| ~ 'E'(f(B_57),f(suc(B_57)))
| ~ 'E'(f(B_58),f(suc(B_58)))
| ~ 'E'(s(s(s('0'))),f(suc(B_57)))
| ~ 'E'(s(s(s('0'))),f(A_2))
| ~ iLEQ(suc(B_57),suc(B_58))
| ~ 'E'(s(s(s('0'))),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(B_57))
| ~ iLEQ(suc(A_2),suc(B_57))
| ~ 'E'(s(s(s('0'))),f(suc(suc(B_58)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f943,axiom,
! [E,A_3] :
( iLEQ(suc(A_3),suc(A_3))
| 'E'(f(A_3),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(A_3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f982,axiom,
! [E,B_75,A_3,B_76] :
( ~ 'E'(s(s('0')),f(A_3))
| ~ 'E'(f(B_75),f(suc(B_75)))
| ~ 'E'(s(s('0')),f(B_75))
| ~ iLEQ(suc(A_3),suc(B_75))
| ~ 'E'(s(s('0')),f(suc(suc(B_75))))
| ~ 'E'(f(A_3),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(suc(B_76))))
| ~ iLEQ(suc(B_75),suc(B_76))
| ~ 'E'(s(s('0')),f(suc(suc(A_3))))
| ~ 'E'(s(s('0')),f(B_76))
| ~ 'E'(f(B_76),f(suc(B_76)))
| ~ 'E'(s(s('0')),f(suc(B_76)))
| ~ 'E'(s(s('0')),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(B_75))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1030,axiom,
! [A_5,B_94,E,B_95] :
( 'E'(f(B_95),f(suc(B_95)))
| 'E'(f(B_94),f(suc(B_94)))
| 'E'(f(A_5),f(suc(A_5)))
| ~ 'E'('0',f(B_95))
| ~ 'E'('0',f(suc(B_95)))
| ~ 'E'('0',f(B_94))
| ~ iLEQ(suc(B_94),suc(B_95))
| ~ 'E'('0',f(suc(A_5)))
| ~ 'E'('0',f(suc(B_94)))
| ~ 'E'('0',f(A_5))
| ~ iLEQ(suc(A_5),suc(B_94)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1031,axiom,
! [LE,B_56,E] :
( 'LE'(f(B_56),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(B_56))
| ~ 'LE'(f(B_56),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1075,axiom,
! [LE,B_93,E] :
( 'LE'(f(B_93),'0')
| 'E'('0',f(suc(B_93)))
| ~ 'LE'(f(suc(B_93)),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1085,axiom,
! [E,A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(A_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1151,axiom,
! [LE,B_31,E] :
( 'LE'(f(B_31),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(B_31)))
| ~ 'LE'(f(suc(B_31)),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1160,axiom,
! [A_2,B_57,E,B_58] :
( 'E'(f(B_58),f(suc(B_58)))
| 'E'(f(B_57),f(suc(B_57)))
| 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(B_58)))
| ~ 'E'(s(s(s('0'))),f(B_58))
| ~ 'E'(s(s(s('0'))),f(suc(B_57)))
| ~ 'E'(s(s(s('0'))),f(A_2))
| ~ iLEQ(suc(B_57),suc(B_58))
| ~ 'E'(s(s(s('0'))),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(B_57))
| ~ iLEQ(suc(A_2),suc(B_57)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1350,plain,
! [A] : 'LE'(f(A),s(s(s(s(s('0')))))),
inference(miniscoping,[status(thm)],[f92]) ).
fof(f1351,plain,
! [LE,X0] : 'LE'(f(X0),s(s(s(s(s('0')))))),
inference(cnf_transformation,[status(thm)],[f1350]) ).
fof(f1416,plain,
! [B_95] :
( ~ 'E'('0',f(B_95))
| ~ 'E'('0',f(suc(B_95)))
| ! [B_94] :
( ~ 'E'('0',f(B_94))
| ~ iLEQ(suc(B_94),suc(B_95))
| ! [A_5] :
( ~ 'E'(f(A_5),f(suc(A_5)))
| ~ 'E'(f(B_94),f(suc(B_94)))
| ~ 'E'(f(B_95),f(suc(B_95)))
| ~ 'E'('0',f(suc(suc(A_5))))
| ~ 'E'('0',f(suc(A_5)))
| ~ 'E'('0',f(suc(suc(B_95))))
| ~ 'E'('0',f(suc(suc(B_94))))
| ~ 'E'('0',f(suc(B_94)))
| ~ 'E'('0',f(A_5))
| ~ iLEQ(suc(A_5),suc(B_94)) ) ) ),
inference(miniscoping,[status(thm)],[f125]) ).
fof(f1417,plain,
! [X0,X1,E,X2] :
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(thm)],[f1416]) ).
fof(f1436,plain,
! [B_74] :
( 'LE'(f(B_74),s(s('0')))
| 'E'(s(s('0')),f(suc(B_74)))
| ~ 'LE'(f(suc(B_74)),s(s(s('0')))) ),
inference(miniscoping,[status(thm)],[f135]) ).
fof(f1437,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s(s('0')))) ),
inference(cnf_transformation,[status(thm)],[f1436]) ).
fof(f1444,plain,
! [B_56] :
( 'LE'(f(B_56),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(B_56))))
| ~ 'LE'(f(suc(suc(B_56))),s(s(s(s('0'))))) ),
inference(miniscoping,[status(thm)],[f139]) ).
fof(f1445,plain,
! [LE,X0,E] :
( '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,[status(thm)],[f1444]) ).
fof(f1462,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(A_2)) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f1463,plain,
! [E,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)) ),
inference(cnf_transformation,[status(thm)],[f1462]) ).
fof(f1472,plain,
! [B_86] :
( 'LE'(f(B_86),s('0'))
| 'E'(s('0'),f(B_86))
| ~ 'LE'(f(B_86),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f1473,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(X0))
| ~ 'LE'(f(X0),s(s('0'))) ),
inference(cnf_transformation,[status(thm)],[f1472]) ).
fof(f1504,plain,
! [B_56] :
( 'LE'(f(B_56),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(B_56)))
| ~ 'LE'(f(suc(B_56)),s(s(s(s('0'))))) ),
inference(miniscoping,[status(thm)],[f169]) ).
fof(f1505,plain,
! [LE,X0,E] :
( '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,[status(thm)],[f1504]) ).
fof(f1546,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ 'E'(s(s(s('0'))),f(A_2))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A_2)))) ),
inference(miniscoping,[status(thm)],[f190]) ).
fof(f1547,plain,
! [E,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)))) ),
inference(cnf_transformation,[status(thm)],[f1546]) ).
fof(f1592,plain,
! [B_32] :
( 'E'(f(B_32),f(suc(B_32)))
| ! [A_1] :
( 'E'(f(A_1),f(suc(A_1)))
| ! [B_33] :
( ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))
| ~ 'E'(s(s(s(s('0')))),f(B_32))
| ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_32))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ 'E'(f(B_33),f(suc(B_33)))
| ~ iLEQ(suc(B_32),suc(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_33)))) ) ) ),
inference(miniscoping,[status(thm)],[f213]) ).
fof(f1593,plain,
! [E,X0,X1,X2] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(thm)],[f1592]) ).
fof(f1618,plain,
! [B_93] :
( 'LE'(f(B_93),'0')
| 'E'('0',f(B_93))
| ~ 'LE'(f(B_93),s('0')) ),
inference(miniscoping,[status(thm)],[f226]) ).
fof(f1619,plain,
! [LE,X0,E] :
( 'LE'(f(X0),'0')
| 'E'('0',f(X0))
| ~ 'LE'(f(X0),s('0')) ),
inference(cnf_transformation,[status(thm)],[f1618]) ).
fof(f1724,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ 'E'(s(s('0')),f(A_3))
| ~ 'E'(f(A_3),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(suc(A_3)))) ),
inference(miniscoping,[status(thm)],[f279]) ).
fof(f1725,plain,
! [E,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)))) ),
inference(cnf_transformation,[status(thm)],[f1724]) ).
fof(f1874,plain,
! [B_33] :
( 'E'(f(B_33),f(suc(B_33)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))
| ! [B_32] :
( ~ 'E'(s(s(s(s('0')))),f(B_32))
| ! [A_1] :
( ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_32))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_32))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ iLEQ(suc(B_32),suc(B_33))
| ~ 'E'(f(B_32),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A_1)))) ) ) ),
inference(miniscoping,[status(thm)],[f354]) ).
fof(f1875,plain,
! [E,X0,X1,X2] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(thm)],[f1874]) ).
fof(f1886,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ 'E'(s('0'),f(A_4))
| ~ 'E'(f(A_4),f(suc(A_4)))
| ~ 'E'(s('0'),f(suc(A_4)))
| ~ 'E'(s('0'),f(suc(suc(A_4)))) ),
inference(miniscoping,[status(thm)],[f360]) ).
fof(f1887,plain,
! [E,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)))) ),
inference(cnf_transformation,[status(thm)],[f1886]) ).
fof(f1898,plain,
! [LE] : ~ 'LE'(f(z),'0'),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f1933,plain,
! [A_4,B_87] :
( ~ iLEQ(suc(A_4),suc(B_87))
| ~ 'E'(s('0'),f(A_4))
| ! [B_88] :
( ~ 'E'(s('0'),f(suc(suc(B_88))))
| ~ 'E'(s('0'),f(suc(A_4)))
| ~ iLEQ(suc(B_87),suc(B_88))
| ~ 'E'(s('0'),f(B_87))
| ~ 'E'(s('0'),f(suc(B_87)))
| ~ 'E'(f(B_88),f(suc(B_88)))
| ~ 'E'(f(B_87),f(suc(B_87)))
| ~ 'E'(s('0'),f(suc(suc(B_87))))
| ~ 'E'(s('0'),f(suc(suc(A_4))))
| ~ 'E'(s('0'),f(suc(B_88)))
| ~ 'E'(f(A_4),f(suc(A_4)))
| ~ 'E'(s('0'),f(B_88)) ) ),
inference(miniscoping,[status(thm)],[f384]) ).
fof(f1934,plain,
! [E,X0,X1,X2] :
( ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f1933]) ).
fof(f1969,plain,
! [B_33] :
( ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))
| ! [B_32] :
( ~ 'E'(s(s(s(s('0')))),f(B_32))
| ! [A_1] :
( ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_32))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_32))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ 'E'(f(B_33),f(suc(B_33)))
| ~ iLEQ(suc(B_32),suc(B_33))
| ~ 'E'(f(B_32),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A_1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(B_33)))) ) ) ),
inference(miniscoping,[status(thm)],[f402]) ).
fof(f1970,plain,
! [E,X0,X1,X2] :
( ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(thm)],[f1969]) ).
fof(f2105,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(A_1)))) ),
inference(miniscoping,[status(thm)],[f470]) ).
fof(f2106,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(thm)],[f2105]) ).
fof(f2169,plain,
! [B_74] :
( 'LE'(f(B_74),s(s('0')))
| 'E'(s(s('0')),f(B_74))
| ~ 'LE'(f(B_74),s(s(s('0')))) ),
inference(miniscoping,[status(thm)],[f502]) ).
fof(f2170,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0))
| ~ 'LE'(f(X0),s(s(s('0')))) ),
inference(cnf_transformation,[status(thm)],[f2169]) ).
fof(f2235,plain,
! [B_86] :
( 'LE'(f(B_86),s('0'))
| 'E'(s('0'),f(suc(suc(B_86))))
| ~ 'LE'(f(suc(suc(B_86))),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f535]) ).
fof(f2236,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s(s('0'))) ),
inference(cnf_transformation,[status(thm)],[f2235]) ).
fof(f2325,plain,
! [B_31] :
( 'LE'(f(B_31),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(B_31))))
| ~ 'LE'(f(suc(suc(B_31))),s(s(s(s(s('0')))))) ),
inference(miniscoping,[status(thm)],[f580]) ).
fof(f2326,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s(s(s(s(s('0')))))) ),
inference(cnf_transformation,[status(thm)],[f2325]) ).
fof(f2327,plain,
! [A_5] :
( iLEQ(suc(A_5),suc(A_5))
| 'E'(f(A_5),f(suc(A_5)))
| ~ 'E'('0',f(suc(A_5)))
| ~ 'E'('0',f(A_5)) ),
inference(miniscoping,[status(thm)],[f581]) ).
fof(f2328,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(cnf_transformation,[status(thm)],[f2327]) ).
fof(f2339,plain,
! [B_76] :
( 'E'(f(B_76),f(suc(B_76)))
| ! [B_75] :
( 'E'(f(B_75),f(suc(B_75)))
| ! [A_3] :
( 'E'(f(A_3),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(A_3))
| ~ 'E'(s(s('0')),f(B_75))
| ~ iLEQ(suc(A_3),suc(B_75))
| ~ iLEQ(suc(B_75),suc(B_76))
| ~ 'E'(s(s('0')),f(B_76))
| ~ 'E'(s(s('0')),f(suc(B_76)))
| ~ 'E'(s(s('0')),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(B_75))) ) ) ),
inference(miniscoping,[status(thm)],[f587]) ).
fof(f2340,plain,
! [E,X0,X1,X2] :
( 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f2339]) ).
fof(f2485,plain,
! [B_93] :
( 'LE'(f(B_93),'0')
| 'E'('0',f(suc(suc(B_93))))
| ~ 'LE'(f(suc(suc(B_93))),s('0')) ),
inference(miniscoping,[status(thm)],[f660]) ).
fof(f2486,plain,
! [LE,X0,E] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(suc(X0))))
| ~ 'LE'(f(suc(suc(X0))),s('0')) ),
inference(cnf_transformation,[status(thm)],[f2485]) ).
fof(f2549,plain,
! [B_86] :
( 'LE'(f(B_86),s('0'))
| 'E'(s('0'),f(suc(B_86)))
| ~ 'LE'(f(suc(B_86)),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f692]) ).
fof(f2550,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s('0'))) ),
inference(cnf_transformation,[status(thm)],[f2549]) ).
fof(f2605,plain,
! [A_5] :
( iLEQ(suc(A_5),suc(A_5))
| ~ 'E'('0',f(A_5))
| ~ 'E'(f(A_5),f(suc(A_5)))
| ~ 'E'('0',f(suc(A_5)))
| ~ 'E'('0',f(suc(suc(A_5)))) ),
inference(miniscoping,[status(thm)],[f720]) ).
fof(f2606,plain,
! [E,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)))) ),
inference(cnf_transformation,[status(thm)],[f2605]) ).
fof(f2677,plain,
! [B_88] :
( 'E'(f(B_88),f(suc(B_88)))
| ! [B_87] :
( 'E'(f(B_87),f(suc(B_87)))
| ! [A_4] :
( 'E'(f(A_4),f(suc(A_4)))
| ~ iLEQ(suc(A_4),suc(B_87))
| ~ 'E'(s('0'),f(A_4))
| ~ 'E'(s('0'),f(suc(A_4)))
| ~ iLEQ(suc(B_87),suc(B_88))
| ~ 'E'(s('0'),f(B_87))
| ~ 'E'(s('0'),f(suc(B_87)))
| ~ 'E'(s('0'),f(suc(B_88)))
| ~ 'E'(s('0'),f(B_88)) ) ) ),
inference(miniscoping,[status(thm)],[f756]) ).
fof(f2678,plain,
! [E,X0,X1,X2] :
( 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f2677]) ).
fof(f2783,plain,
! [B_33] :
( 'E'(f(B_33),f(suc(B_33)))
| ! [B_32] :
( 'E'(f(B_32),f(suc(B_32)))
| ! [A_1] :
( 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_33)))
| ~ 'E'(s(s(s(s('0')))),f(B_32))
| ~ 'E'(s(s(s(s('0')))),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_32))
| ~ 'E'(s(s(s(s('0')))),f(suc(B_32)))
| ~ 'E'(s(s(s(s('0')))),f(B_33))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ iLEQ(suc(B_32),suc(B_33)) ) ) ),
inference(miniscoping,[status(thm)],[f809]) ).
fof(f2784,plain,
! [X0,X1,E,X2] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(thm)],[f2783]) ).
fof(f2869,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| 'E'(f(A_4),f(suc(A_4)))
| ~ 'E'(s('0'),f(suc(A_4)))
| ~ 'E'(s('0'),f(A_4)) ),
inference(miniscoping,[status(thm)],[f852]) ).
fof(f2870,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f2869]) ).
fof(f2953,plain,
! [B_31] :
( 'LE'(f(B_31),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(B_31))
| ~ 'LE'(f(B_31),s(s(s(s(s('0')))))) ),
inference(miniscoping,[status(thm)],[f894]) ).
fof(f2954,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(X0))
| ~ 'LE'(f(X0),s(s(s(s(s('0')))))) ),
inference(cnf_transformation,[status(thm)],[f2953]) ).
fof(f2993,plain,
! [B_74] :
( 'LE'(f(B_74),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(B_74))))
| ~ 'LE'(f(suc(suc(B_74))),s(s(s('0')))) ),
inference(miniscoping,[status(thm)],[f914]) ).
fof(f2994,plain,
! [LE,X0,E] :
( '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,[status(thm)],[f2993]) ).
fof(f3029,plain,
! [B_57] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(B_57))))
| ! [A_2] :
( ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(A_2))))
| ! [B_58] :
( ~ 'E'(s(s(s('0'))),f(suc(B_58)))
| ~ 'E'(s(s(s('0'))),f(B_58))
| ~ 'E'(f(B_57),f(suc(B_57)))
| ~ 'E'(f(B_58),f(suc(B_58)))
| ~ 'E'(s(s(s('0'))),f(suc(B_57)))
| ~ 'E'(s(s(s('0'))),f(A_2))
| ~ iLEQ(suc(B_57),suc(B_58))
| ~ 'E'(s(s(s('0'))),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(B_57))
| ~ iLEQ(suc(A_2),suc(B_57))
| ~ 'E'(s(s(s('0'))),f(suc(suc(B_58)))) ) ) ),
inference(miniscoping,[status(thm)],[f932]) ).
fof(f3030,plain,
! [E,X0,X1,X2] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(thm)],[f3029]) ).
fof(f3051,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| 'E'(f(A_3),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(A_3)) ),
inference(miniscoping,[status(thm)],[f943]) ).
fof(f3052,plain,
! [E,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)) ),
inference(cnf_transformation,[status(thm)],[f3051]) ).
fof(f3129,plain,
! [A_3] :
( ~ 'E'(s(s('0')),f(A_3))
| ! [B_75] :
( ~ 'E'(f(B_75),f(suc(B_75)))
| ~ 'E'(s(s('0')),f(B_75))
| ~ iLEQ(suc(A_3),suc(B_75))
| ~ 'E'(s(s('0')),f(suc(suc(B_75))))
| ~ 'E'(f(A_3),f(suc(A_3)))
| ! [B_76] :
( ~ 'E'(s(s('0')),f(suc(suc(B_76))))
| ~ iLEQ(suc(B_75),suc(B_76))
| ~ 'E'(s(s('0')),f(suc(suc(A_3))))
| ~ 'E'(s(s('0')),f(B_76))
| ~ 'E'(f(B_76),f(suc(B_76)))
| ~ 'E'(s(s('0')),f(suc(B_76)))
| ~ 'E'(s(s('0')),f(suc(A_3)))
| ~ 'E'(s(s('0')),f(suc(B_75))) ) ) ),
inference(miniscoping,[status(thm)],[f982]) ).
fof(f3130,plain,
! [E,X0,X1,X2] :
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f3129]) ).
fof(f3225,plain,
! [B_95] :
( 'E'(f(B_95),f(suc(B_95)))
| ! [B_94] :
( 'E'(f(B_94),f(suc(B_94)))
| ! [A_5] :
( 'E'(f(A_5),f(suc(A_5)))
| ~ 'E'('0',f(B_95))
| ~ 'E'('0',f(suc(B_95)))
| ~ 'E'('0',f(B_94))
| ~ iLEQ(suc(B_94),suc(B_95))
| ~ 'E'('0',f(suc(A_5)))
| ~ 'E'('0',f(suc(B_94)))
| ~ 'E'('0',f(A_5))
| ~ iLEQ(suc(A_5),suc(B_94)) ) ) ),
inference(miniscoping,[status(thm)],[f1030]) ).
fof(f3226,plain,
! [X0,X1,E,X2] :
( '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(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(thm)],[f3225]) ).
fof(f3227,plain,
! [B_56] :
( 'LE'(f(B_56),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(B_56))
| ~ 'LE'(f(B_56),s(s(s(s('0'))))) ),
inference(miniscoping,[status(thm)],[f1031]) ).
fof(f3228,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X0))
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(cnf_transformation,[status(thm)],[f3227]) ).
fof(f3315,plain,
! [B_93] :
( 'LE'(f(B_93),'0')
| 'E'('0',f(suc(B_93)))
| ~ 'LE'(f(suc(B_93)),s('0')) ),
inference(miniscoping,[status(thm)],[f1075]) ).
fof(f3316,plain,
! [LE,X0,E] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s('0')) ),
inference(cnf_transformation,[status(thm)],[f3315]) ).
fof(f3335,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(A_1)))
| ~ 'E'(s(s(s(s('0')))),f(A_1)) ),
inference(miniscoping,[status(thm)],[f1085]) ).
fof(f3336,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f3335]) ).
fof(f3467,plain,
! [B_31] :
( 'LE'(f(B_31),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(B_31)))
| ~ 'LE'(f(suc(B_31)),s(s(s(s(s('0')))))) ),
inference(miniscoping,[status(thm)],[f1151]) ).
fof(f3468,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s(s(s(s(s('0')))))) ),
inference(cnf_transformation,[status(thm)],[f3467]) ).
fof(f3485,plain,
! [B_58] :
( 'E'(f(B_58),f(suc(B_58)))
| ! [B_57] :
( 'E'(f(B_57),f(suc(B_57)))
| ! [A_2] :
( 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(suc(B_58)))
| ~ 'E'(s(s(s('0'))),f(B_58))
| ~ 'E'(s(s(s('0'))),f(suc(B_57)))
| ~ 'E'(s(s(s('0'))),f(A_2))
| ~ iLEQ(suc(B_57),suc(B_58))
| ~ 'E'(s(s(s('0'))),f(suc(A_2)))
| ~ 'E'(s(s(s('0'))),f(B_57))
| ~ iLEQ(suc(A_2),suc(B_57)) ) ) ),
inference(miniscoping,[status(thm)],[f1160]) ).
fof(f3486,plain,
! [X0,X1,E,X2] :
( 'E'(f(X2),f(suc(X2)))
| '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(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(thm)],[f3485]) ).
fof(f3504,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2606,f2328]) ).
fof(f3505,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2954,f1351]) ).
fof(f3509,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1887,f2870]) ).
fof(f3510,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3468,f1351]) ).
fof(f3512,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2326,f1351]) ).
fof(f3513,plain,
! [E,X0] :
( 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(forward_subsumption_resolution,[status(thm)],[f1725,f3052]) ).
fof(f3514,plain,
! [E,X0] :
( 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(forward_subsumption_resolution,[status(thm)],[f1547,f1463]) ).
fof(f3518,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2106,f3336]) ).
fof(f4822,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[f3226]) ).
fof(f4873,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4822]) ).
fof(f4874,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4873,f2328]) ).
fof(f5190,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(factoring,[status(thm)],[f2678]) ).
fof(f5199,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f5190]) ).
fof(f5200,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5199,f2870]) ).
fof(f5560,plain,
! [X0,X1,E,X2] :
( ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1417,f4874]) ).
fof(f5571,plain,
! [E,X0] :
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(resolution,[status(thm)],[f5560,f3504]) ).
fof(f5692,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f5571]) ).
fof(f5693,plain,
! [E,X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5692,f4874]) ).
fof(f6035,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(factoring,[status(thm)],[f2340]) ).
fof(f6052,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f6035]) ).
fof(f6053,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f6052,f3052]) ).
fof(f6507,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[f1593]) ).
fof(f6524,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ iLEQ(suc(X1),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(duplicate_literals_removal,[status(thm)],[f6507]) ).
fof(f6525,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f6524,f3336]) ).
fof(f6766,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[f3486]) ).
fof(f6795,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f6766]) ).
fof(f6796,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6795,f1463]) ).
fof(f7237,plain,
! [E,X0,X1,X2] :
( 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1875,f6525]) ).
fof(f7274,plain,
! [E,X0,X1,X2] :
( ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1934,f5200]) ).
fof(f7366,plain,
! [E,X0] :
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(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))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(resolution,[status(thm)],[f7274,f3509]) ).
fof(f7495,plain,
! [E,X0] :
( ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f7366]) ).
fof(f7496,plain,
! [E,X0] :
( ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7495,f5200]) ).
fof(f7768,plain,
! [E,X0,X1,X2] :
( ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1970,f7237]) ).
fof(f7817,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[f7768,f3518]) ).
fof(f7908,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ),
inference(duplicate_literals_removal,[status(thm)],[f7817]) ).
fof(f8038,plain,
! [X0,E] :
( ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[f2784,f7908]) ).
fof(f8044,plain,
! [X0,E] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f8038]) ).
fof(f8045,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8044,f3518]) ).
fof(f8055,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s(s('0')))))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0))) ),
inference(resolution,[status(thm)],[f8045,f3512]) ).
fof(f8058,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s(s('0')))))
| ~ 'E'(s(s(s(s('0')))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8055,f3510]) ).
fof(f8066,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1445,f8069]) ).
fof(f8067,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1505,f8069]) ).
fof(f8068,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f3228,f8069]) ).
fof(f8069,plain,
! [LE,X0] : 'LE'(f(X0),s(s(s(s('0'))))),
inference(forward_subsumption_resolution,[status(thm)],[f8058,f3505]) ).
fof(f8345,plain,
! [E,X0,X1,X2] :
( ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3130,f6053]) ).
fof(f8366,plain,
! [E,X0] :
( ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(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(X0)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[status(thm)],[f8345,f3513]) ).
fof(f8410,plain,
! [E,X0] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f8366]) ).
fof(f8411,plain,
! [E,X0] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8410,f6053]) ).
fof(f8540,plain,
! [E,X0,X1,X2] :
( ~ '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(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3030,f6796]) ).
fof(f8547,plain,
! [E,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))))
| ~ 'E'(s(s(s('0'))),f(suc(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))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[f8540,f3514]) ).
fof(f8587,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(duplicate_literals_removal,[status(thm)],[f8547]) ).
fof(f8588,plain,
! [E,X0] :
( ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8587,f6796]) ).
fof(f8633,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(resolution,[status(thm)],[f8588,f8066]) ).
fof(f8636,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8633,f8068]) ).
fof(f8641,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[f2994,f8653]) ).
fof(f8642,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1437,f8653]) ).
fof(f8643,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2170,f8653]) ).
fof(f8653,plain,
! [LE,X0] : 'LE'(f(X0),s(s(s('0')))),
inference(forward_subsumption_resolution,[status(thm)],[f8636,f8067]) ).
fof(f8660,plain,
! [LE,X0,E] :
( ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| 'LE'(f(X0),s(s('0'))) ),
inference(resolution,[status(thm)],[f8641,f8411]) ).
fof(f8661,plain,
! [LE,X0,E] :
( ~ 'E'(s(s('0')),f(X0))
| 'LE'(f(X0),s(s('0'))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8660,f8642]) ).
fof(f8665,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[f2236,f8671]) ).
fof(f8666,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f2550,f8671]) ).
fof(f8667,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1473,f8671]) ).
fof(f8671,plain,
! [LE,X0] : 'LE'(f(X0),s(s('0'))),
inference(forward_subsumption_resolution,[status(thm)],[f8661,f8643]) ).
fof(f8676,plain,
! [LE,X0,E] :
( ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'LE'(f(X0),s('0')) ),
inference(resolution,[status(thm)],[f8665,f7496]) ).
fof(f8677,plain,
! [LE,X0,E] :
( ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X0),s('0')) ),
inference(forward_subsumption_resolution,[status(thm)],[f8676,f8667]) ).
fof(f8681,plain,
! [E,X0,LE] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(suc(X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[f2486,f8685]) ).
fof(f8682,plain,
! [E,X0,LE] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f3316,f8685]) ).
fof(f8683,plain,
! [E,X0,LE] :
( 'LE'(f(X0),'0')
| 'E'('0',f(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1619,f8685]) ).
fof(f8685,plain,
! [LE,X0] : 'LE'(f(X0),s('0')),
inference(forward_subsumption_resolution,[status(thm)],[f8677,f8666]) ).
fof(f8689,plain,
! [LE,X0,E] :
( ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
inference(resolution,[status(thm)],[f8681,f5693]) ).
fof(f8690,plain,
! [LE,X0,E] :
( ~ 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
inference(forward_subsumption_resolution,[status(thm)],[f8689,f8683]) ).
fof(f8692,plain,
! [LE,X0] : 'LE'(f(X0),'0'),
inference(forward_subsumption_resolution,[status(thm)],[f8690,f8682]) ).
fof(f8693,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f1898,f8692]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO688-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n013.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 12:08:26 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.14/5.66 % Drodi V4.1.1
% 37.03/10.32 % Refutation found
% 37.03/10.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 37.03/10.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 37.03/10.35 % Elapsed time: 4.965745 seconds
% 37.03/10.35 % CPU time: 37.367857 seconds
% 37.03/10.35 % Total memory used: 224.340 MB
% 37.03/10.35 % Net memory used: 208.747 MB
%------------------------------------------------------------------------------