%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYO660-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 : n004.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:42:55 PM UTC 2026
% Result : Unsatisfiable 0.15s 5.81s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 34
% Syntax : Number of formulae : 221 ( 9 unt; 0 def)
% Number of atoms : 1616 ( 0 equ)
% Maximal formula atoms : 25 ( 7 avg)
% Number of connectives : 2731 (1336 ~;1395 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 10 avg)
% Maximal term depth : 11 ( 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 : 463 ( 463 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [LE,B_2,E] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(B_2)))
| ~ 'LE'(f(suc(B_2)),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [LE] : ~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [LE,B_5,E] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(B_5))
| ~ 'LE'(f(B_5),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [LE,B_5,E] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(suc(B_5))))
| ~ 'LE'(f(suc(suc(B_5))),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [E,A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(A_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [E,A_1,B_3] :
( ~ 'E'(f(B_3),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(f(B_3),f(suc(suc(suc(B_3)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(B_3),f(suc(B_3)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(f(B_3),f(suc(suc(suc(suc(B_3))))))
| ~ 'E'(s('0'),f(suc(suc(suc(B_3)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(B_3))))))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(B_3)))))))
| ~ iLEQ(suc(A_1),suc(B_3))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(A_1))))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [E,A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(suc(suc(suc(A_2))))))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [LE,B_5,E] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(B_5)))
| ~ 'LE'(f(suc(B_5)),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [LE,B_5,E] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(suc(suc(B_5)))))
| ~ 'LE'(f(suc(suc(suc(B_5)))),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [LE,B_2,E] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(suc(suc(B_2)))))
| ~ 'LE'(f(suc(suc(suc(B_2)))),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [E,A_2,B_6] :
( 'E'(f(B_6),f(suc(suc(suc(B_6)))))
| 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(suc(B_6)))
| ~ 'E'(f(B_6),f(suc(B_6)))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(f(B_6),f(suc(suc(B_6))))
| ~ 'E'('0',f(B_6))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(suc(suc(suc(B_6)))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(B_6))))
| ~ 'E'('0',f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [LE,B_2,E] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(B_2))))))
| ~ 'LE'(f(suc(suc(suc(suc(B_2))))),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [E,A_2,B_6] :
( 'E'(f(B_6),f(suc(suc(suc(suc(B_6))))))
| 'E'(f(A_2),f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(B_6)))
| ~ 'E'(f(B_6),f(suc(B_6)))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(f(B_6),f(suc(suc(B_6))))
| ~ 'E'('0',f(B_6))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(suc(suc(suc(B_6)))))
| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(B_6))))
| ~ 'E'('0',f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [E,A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [LE,B_2,E] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(suc(B_2))))
| ~ 'LE'(f(suc(suc(B_2))),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [E,A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(A_2)))
| ~ 'E'('0',f(suc(suc(A_2)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [LE,B_5,E] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(suc(suc(suc(B_5))))))
| ~ 'LE'(f(suc(suc(suc(suc(B_5))))),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [E,A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [E,A_2,B_6] :
( ~ 'E'('0',f(suc(B_6)))
| ~ 'E'(f(B_6),f(suc(B_6)))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(f(B_6),f(suc(suc(B_6))))
| ~ 'E'(f(B_6),f(suc(suc(suc(suc(B_6))))))
| ~ 'E'('0',f(B_6))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(suc(suc(B_6)))))
| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(A_2)))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(B_6)))))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(B_6))))
| ~ 'E'('0',f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [E,A_2,B_6] :
( 'E'(f(B_6),f(suc(B_6)))
| 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(B_6)))
| ~ 'E'('0',f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'('0',f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [E,A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(A_2)))))))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A_1,B_3,E] :
( 'E'(f(B_3),f(suc(suc(suc(B_3)))))
| 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(B_3),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(B_3),f(suc(B_3)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(s('0'),f(suc(suc(suc(B_3)))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [LE,B_2,E] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(suc(B_2)))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(B_2)))))),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [LE,B_5,E] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(suc(suc(suc(suc(B_5)))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(B_5)))))),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [LE,B_2,E] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(B_2))
| ~ 'LE'(f(B_2),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A_1,B_3,E] :
( 'E'(f(B_3),f(suc(suc(suc(suc(B_3))))))
| 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(f(B_3),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(B_3),f(suc(suc(suc(B_3)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(B_3),f(suc(B_3)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(s('0'),f(suc(suc(suc(B_3)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(B_3))))))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [E,A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A_1,B_3,E] :
( 'E'(f(B_3),f(suc(B_3)))
| 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [E,A_2,B_6] :
( 'E'(f(B_6),f(suc(suc(B_6))))
| 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(B_6)))
| ~ 'E'(f(B_6),f(suc(B_6)))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(B_6))))
| ~ 'E'('0',f(suc(A_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [A_1,B_3,E] :
( 'E'(f(B_3),f(suc(suc(B_3))))
| 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(B_3),f(suc(B_3)))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [E,A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(A_2)))
| ~ 'E'('0',f(A_2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [E,A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [LE,A] : 'LE'(f(A),s(s('0'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [E,A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(A_1))))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,plain,
! [B_2] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(B_2)))
| ~ 'LE'(f(suc(B_2)),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f76,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)],[f75]) ).
fof(f79,plain,
! [LE] : ~ 'LE'(f(z),'0'),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f80,plain,
! [B_5] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(B_5))
| ~ 'LE'(f(B_5),s('0')) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f81,plain,
! [LE,X0,E] :
( 'LE'(f(X0),'0')
| 'E'('0',f(X0))
| ~ 'LE'(f(X0),s('0')) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
! [B_5] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(suc(B_5))))
| ~ 'LE'(f(suc(suc(B_5))),s('0')) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f83,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)],[f82]) ).
fof(f84,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(A_1)) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f85,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)],[f84]) ).
fof(f86,plain,
! [B_3] :
( ~ 'E'(f(B_3),f(suc(suc(B_3))))
| ! [A_1] :
( ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(f(B_3),f(suc(suc(suc(B_3)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(B_3),f(suc(B_3)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(f(B_3),f(suc(suc(suc(suc(B_3))))))
| ~ 'E'(s('0'),f(suc(suc(suc(B_3)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(B_3))))))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(B_3)))))))
| ~ iLEQ(suc(A_1),suc(B_3))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(A_1))))))) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f87,plain,
! [E,X0,X1] :
( ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(suc(suc(suc(X1))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X1)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X1))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X1)))))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f96,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(suc(suc(suc(A_2))))))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(A_2))) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f97,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f120,plain,
! [B_5] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(B_5)))
| ~ 'LE'(f(suc(B_5)),s('0')) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f121,plain,
! [LE,X0,E] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(X0)))
| ~ 'LE'(f(suc(X0)),s('0')) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f128,plain,
! [B_5] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(suc(suc(B_5)))))
| ~ 'LE'(f(suc(suc(suc(B_5)))),s('0')) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f129,plain,
! [LE,X0,E] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'LE'(f(suc(suc(suc(X0)))),s('0')) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [B_2] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(suc(suc(B_2)))))
| ~ 'LE'(f(suc(suc(suc(B_2)))),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f131,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'LE'(f(suc(suc(suc(X0)))),s(s('0'))) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f138,plain,
! [B_6] :
( 'E'(f(B_6),f(suc(suc(suc(B_6)))))
| ! [A_2] :
( 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(suc(B_6)))
| ~ 'E'(f(B_6),f(suc(B_6)))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(f(B_6),f(suc(suc(B_6))))
| ~ 'E'('0',f(B_6))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(suc(suc(suc(B_6)))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(B_6))))
| ~ 'E'('0',f(suc(A_2))) ) ),
inference(miniscoping,[status(thm)],[f33]) ).
fof(f139,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f142,plain,
! [B_2] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(B_2))))))
| ~ 'LE'(f(suc(suc(suc(suc(B_2))))),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f143,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'LE'(f(suc(suc(suc(suc(X0))))),s(s('0'))) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f144,plain,
! [B_6] :
( 'E'(f(B_6),f(suc(suc(suc(suc(B_6))))))
| ! [A_2] :
( 'E'(f(A_2),f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(B_6)))
| ~ 'E'(f(B_6),f(suc(B_6)))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(f(B_6),f(suc(suc(B_6))))
| ~ 'E'('0',f(B_6))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(suc(suc(suc(B_6)))))
| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(B_6))))
| ~ 'E'('0',f(suc(A_2))) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f145,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(suc(suc(suc(X1))))))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f150,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1)))) ),
inference(miniscoping,[status(thm)],[f39]) ).
fof(f151,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f152,plain,
! [B_2] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(suc(B_2))))
| ~ 'LE'(f(suc(suc(B_2))),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f153,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)],[f152]) ).
fof(f154,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(A_2)))
| ~ 'E'('0',f(suc(suc(A_2)))) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f155,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(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)],[f154]) ).
fof(f156,plain,
! [B_5] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(suc(suc(suc(B_5))))))
| ~ 'LE'(f(suc(suc(suc(suc(B_5))))),s('0')) ),
inference(miniscoping,[status(thm)],[f42]) ).
fof(f157,plain,
! [LE,X0,E] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'LE'(f(suc(suc(suc(suc(X0))))),s('0')) ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f158,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(A_2))) ),
inference(miniscoping,[status(thm)],[f43]) ).
fof(f159,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f170,plain,
! [B_6] :
( ~ 'E'('0',f(suc(B_6)))
| ~ 'E'(f(B_6),f(suc(B_6)))
| ! [A_2] :
( ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'(f(B_6),f(suc(suc(B_6))))
| ~ 'E'(f(B_6),f(suc(suc(suc(suc(B_6))))))
| ~ 'E'('0',f(B_6))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'(f(B_6),f(suc(suc(suc(B_6)))))
| ~ 'E'('0',f(suc(suc(suc(suc(B_6))))))
| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(suc(suc(B_6)))))
| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(A_2)))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(B_6)))))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(B_6))))
| ~ 'E'('0',f(suc(A_2))) ) ),
inference(miniscoping,[status(thm)],[f49]) ).
fof(f171,plain,
! [E,X0,X1] :
( ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X1)))))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f178,plain,
! [B_6] :
( 'E'(f(B_6),f(suc(B_6)))
| ! [A_2] :
( 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(B_6)))
| ~ 'E'('0',f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'('0',f(suc(A_2))) ) ),
inference(miniscoping,[status(thm)],[f53]) ).
fof(f179,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(suc(suc(A_2)))))
| ~ 'E'(f(A_2),f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(A_2))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(A_2)))))))
| ~ 'E'('0',f(A_2))
| ~ 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(A_2))) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f181,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f182,plain,
! [B_3] :
( 'E'(f(B_3),f(suc(suc(suc(B_3)))))
| ! [A_1] :
( 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(B_3),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(B_3),f(suc(B_3)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(s('0'),f(suc(suc(suc(B_3)))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f183,plain,
! [X0,X1,E] :
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(suc(X1)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f186,plain,
! [B_2] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(suc(B_2)))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(B_2)))))),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f57]) ).
fof(f187,plain,
! [LE,X0,E] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(X0)))))),s(s('0'))) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f190,plain,
! [B_5] :
( 'LE'(f(B_5),'0')
| 'E'('0',f(suc(suc(suc(suc(suc(B_5)))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(B_5)))))),s('0')) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f191,plain,
! [LE,X0,E] :
( 'LE'(f(X0),'0')
| 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'LE'(f(suc(suc(suc(suc(suc(X0)))))),s('0')) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f194,plain,
! [B_2] :
( 'LE'(f(B_2),s('0'))
| 'E'(s('0'),f(B_2))
| ~ 'LE'(f(B_2),s(s('0'))) ),
inference(miniscoping,[status(thm)],[f61]) ).
fof(f195,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)],[f194]) ).
fof(f200,plain,
! [B_3] :
( 'E'(f(B_3),f(suc(suc(suc(suc(B_3))))))
| ! [A_1] :
( 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(f(B_3),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(B_3),f(suc(suc(suc(B_3)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(B_3),f(suc(B_3)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(s('0'),f(suc(suc(suc(B_3)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(B_3))))))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ) ),
inference(miniscoping,[status(thm)],[f64]) ).
fof(f201,plain,
! [X0,X1,E] :
( 'E'(f(X1),f(suc(suc(suc(suc(X1))))))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(suc(X1)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X1))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1)))) ),
inference(miniscoping,[status(thm)],[f65]) ).
fof(f203,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f206,plain,
! [B_3] :
( 'E'(f(B_3),f(suc(B_3)))
| ! [A_1] :
( 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_3)) ) ),
inference(miniscoping,[status(thm)],[f67]) ).
fof(f207,plain,
! [X0,X1,E] :
( 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f208,plain,
! [B_6] :
( 'E'(f(B_6),f(suc(suc(B_6))))
| ! [A_2] :
( 'E'(f(A_2),f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(B_6)))
| ~ 'E'(f(B_6),f(suc(B_6)))
| ~ 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ 'E'('0',f(A_2))
| ~ 'E'('0',f(suc(suc(A_2))))
| ~ 'E'('0',f(suc(suc(B_6))))
| ~ 'E'('0',f(suc(A_2))) ) ),
inference(miniscoping,[status(thm)],[f68]) ).
fof(f209,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0))) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f210,plain,
! [B_3] :
( 'E'(f(B_3),f(suc(suc(B_3))))
| ! [A_1] :
( 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(B_3),f(suc(B_3)))
| ~ 'E'(s('0'),f(B_3))
| ~ 'E'(s('0'),f(suc(B_3)))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(suc(B_3))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ) ),
inference(miniscoping,[status(thm)],[f69]) ).
fof(f211,plain,
! [X0,X1,E] :
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f212,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| 'E'(f(A_2),f(suc(A_2)))
| ~ 'E'('0',f(suc(A_2)))
| ~ 'E'('0',f(A_2)) ),
inference(miniscoping,[status(thm)],[f70]) ).
fof(f213,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)],[f212]) ).
fof(f214,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(s('0'),f(suc(suc(A_1)))) ),
inference(miniscoping,[status(thm)],[f71]) ).
fof(f215,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(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)],[f214]) ).
fof(f218,plain,
! [A] : 'LE'(f(A),s(s('0'))),
inference(miniscoping,[status(thm)],[f73]) ).
fof(f219,plain,
! [LE,X0] : 'LE'(f(X0),s(s('0'))),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ 'E'(s('0'),f(suc(suc(suc(A_1)))))
| ~ 'E'(f(A_1),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(f(A_1),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(A_1))))))
| ~ 'E'(s('0'),f(suc(A_1)))
| ~ 'E'(f(A_1),f(suc(suc(suc(A_1)))))
| ~ 'E'(s('0'),f(A_1))
| ~ 'E'(s('0'),f(suc(suc(A_1))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(A_1))))))) ),
inference(miniscoping,[status(thm)],[f74]) ).
fof(f221,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f222,plain,
! [LE,E] :
( 'E'('0',f(z))
| ~ 'LE'(f(z),s('0')) ),
inference(resolution,[status(thm)],[f81,f79]) ).
fof(f223,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f76,f219]) ).
fof(f224,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f195,f219]) ).
fof(f225,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f153,f219]) ).
fof(f232,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(factoring,[status(thm)],[f87]) ).
fof(f241,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(duplicate_literals_removal,[status(thm)],[f232]) ).
fof(f242,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(suc(X0))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f131,f219]) ).
fof(f253,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(X0)))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f143,f219]) ).
fof(f264,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f187,f219]) ).
fof(f277,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f155,f213]) ).
fof(f278,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0))) ),
inference(factoring,[status(thm)],[f179]) ).
fof(f279,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f278]) ).
fof(f280,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f279,f213]) ).
fof(f281,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(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)],[f215,f85]) ).
fof(f283,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[f207]) ).
fof(f284,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f283]) ).
fof(f285,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)],[f284,f85]) ).
fof(f288,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f159,f277]) ).
fof(f289,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f203,f281]) ).
fof(f291,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f209,f280]) ).
fof(f292,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(factoring,[status(thm)],[f291]) ).
fof(f294,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f292]) ).
fof(f295,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f294,f277]) ).
fof(f296,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f295,f280]) ).
fof(f297,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f97,f296]) ).
fof(f298,plain,
! [X0,X1,E] :
( 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f211,f285]) ).
fof(f299,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(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))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[f298]) ).
fof(f300,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f299]) ).
fof(f301,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f300,f281]) ).
fof(f302,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f301,f285]) ).
fof(f303,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f151,f289]) ).
fof(f310,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f181,f296]) ).
fof(f312,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f221,f289]) ).
fof(f313,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f241,f312]) ).
fof(f342,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f139,f296]) ).
fof(f343,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(factoring,[status(thm)],[f342]) ).
fof(f346,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f343]) ).
fof(f347,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f346,f288]) ).
fof(f349,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f310,f351]) ).
fof(f350,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[f297,f351]) ).
fof(f351,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f347,f296]) ).
fof(f353,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f349,f280]) ).
fof(f354,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f350,f280]) ).
fof(f356,plain,
! [E,X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f354]) ).
fof(f357,plain,
! [X0,X1,E] :
( 'E'(f(X1),f(suc(suc(suc(X1)))))
| 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(suc(X1)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f183,f302]) ).
fof(f358,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(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))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[f357]) ).
fof(f359,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f358]) ).
fof(f360,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f359,f289]) ).
fof(f361,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f313,f362]) ).
fof(f362,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f360,f285]) ).
fof(f363,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f361,f302]) ).
fof(f364,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f363,f285]) ).
fof(f382,plain,
! [E,X0,X1] :
( 'E'(f(X1),f(suc(suc(suc(suc(X1))))))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f145,f296]) ).
fof(f386,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(factoring,[status(thm)],[f382]) ).
fof(f391,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f386]) ).
fof(f392,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f391,f354]) ).
fof(f393,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f392,f351]) ).
fof(f411,plain,
! [E,X0,X1] :
( ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(suc(suc(suc(X1))))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X1))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X1)))))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f171,f296]) ).
fof(f412,plain,
! [E,X0] :
( ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(resolution,[status(thm)],[f411,f356]) ).
fof(f424,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f412]) ).
fof(f425,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f424,f393]) ).
fof(f439,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f425,f351]) ).
fof(f446,plain,
! [E,X0] :
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(resolution,[status(thm)],[f439,f296]) ).
fof(f453,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f446]) ).
fof(f454,plain,
! [E,X0] :
( ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f453,f280]) ).
fof(f455,plain,
! [E,X0,LE] :
( 'LE'(f(X0),'0')
| ~ 'LE'(f(suc(suc(suc(suc(suc(X0)))))),s('0'))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'('0',f(suc(suc(suc(suc(X0))))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0))) ),
inference(resolution,[status(thm)],[f454,f191]) ).
fof(f460,plain,
! [E,LE] :
( ~ 'LE'(f(suc(suc(suc(suc(suc(z)))))),s('0'))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f455,f79]) ).
fof(f479,plain,
! [X0,X1,E] :
( 'E'(f(X1),f(suc(suc(suc(suc(X1))))))
| 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X1),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X1),f(suc(suc(suc(X1)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(suc(X1)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X1))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f201,f362]) ).
fof(f483,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(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(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[f479]) ).
fof(f490,plain,
! [X0,E] :
( 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f483]) ).
fof(f491,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f490,f303]) ).
fof(f492,plain,
! [E,X0] :
( 'E'(f(X0),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f491,f302]) ).
fof(f493,plain,
! [E,X0] :
( ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[f492,f364]) ).
fof(f494,plain,
! [E,X0] :
( ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(duplicate_literals_removal,[status(thm)],[f493]) ).
fof(f495,plain,
! [E,X0] :
( ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'(f(X0),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f494,f285]) ).
fof(f496,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[f495,f362]) ).
fof(f505,plain,
! [E,X0] :
( ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(duplicate_literals_removal,[status(thm)],[f496]) ).
fof(f506,plain,
! [E,X0] :
( ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f505,f302]) ).
fof(f524,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[f506,f264]) ).
fof(f529,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f524,f224]) ).
fof(f534,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(X0)))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f225]) ).
fof(f535,plain,
! [E] :
( ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))) ),
inference(resolution,[status(thm)],[f534,f460]) ).
fof(f574,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s('0'))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[status(thm)],[f535,f253]) ).
fof(f578,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s('0'))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f574,f242]) ).
fof(f582,plain,
! [E] :
( ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(backward_subsumption_resolution,[status(thm)],[f460,f583]) ).
fof(f583,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s('0'))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f223]) ).
fof(f584,plain,
! [E,LE] :
( 'LE'(f(z),'0')
| ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f582,f157]) ).
fof(f588,plain,
! [E,LE] :
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f584,f79]) ).
fof(f595,plain,
! [E] :
( ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f588,f534]) ).
fof(f628,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f595,f253]) ).
fof(f632,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f628,f242]) ).
fof(f636,plain,
! [E] :
( ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(backward_subsumption_resolution,[status(thm)],[f588,f637]) ).
fof(f637,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(suc(z))))),s('0'))
| ~ 'E'('0',f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f632,f223]) ).
fof(f638,plain,
! [E,LE] :
( 'LE'(f(z),'0')
| ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f636,f129]) ).
fof(f641,plain,
! [E,LE] :
( ~ 'LE'(f(suc(suc(suc(z)))),s('0'))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f638,f79]) ).
fof(f647,plain,
! [E] :
( ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f641,f534]) ).
fof(f675,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(z)))),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f647,f253]) ).
fof(f679,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(z)))),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f675,f242]) ).
fof(f683,plain,
! [E] :
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(backward_subsumption_resolution,[status(thm)],[f641,f684]) ).
fof(f684,plain,
! [E,LE] :
( 'LE'(f(suc(suc(suc(z)))),s('0'))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(suc(z))))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f679,f223]) ).
fof(f685,plain,
! [E,LE] :
( 'LE'(f(z),'0')
| ~ 'LE'(f(suc(suc(z))),s('0'))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f683,f83]) ).
fof(f687,plain,
! [E,LE] :
( ~ 'LE'(f(suc(suc(z))),s('0'))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f685,f79]) ).
fof(f690,plain,
! [E] :
( ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f687,f534]) ).
fof(f712,plain,
! [E,LE] :
( 'LE'(f(suc(suc(z))),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(resolution,[status(thm)],[f690,f253]) ).
fof(f716,plain,
! [E,LE] :
( 'LE'(f(suc(suc(z))),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f712,f242]) ).
fof(f720,plain,
! [E] :
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(backward_subsumption_resolution,[status(thm)],[f687,f721]) ).
fof(f721,plain,
! [E,LE] :
( 'LE'(f(suc(suc(z))),s('0'))
| ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z))) ),
inference(forward_subsumption_resolution,[status(thm)],[f716,f223]) ).
fof(f722,plain,
! [E,LE] :
( 'LE'(f(z),'0')
| ~ 'LE'(f(suc(z)),s('0'))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[f720,f121]) ).
fof(f723,plain,
! [E,LE] :
( ~ 'LE'(f(suc(z)),s('0'))
| ~ 'E'('0',f(z)) ),
inference(forward_subsumption_resolution,[status(thm)],[f722,f79]) ).
fof(f725,plain,
! [E] :
( ~ 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[f723,f534]) ).
fof(f737,plain,
! [E,LE] :
( 'LE'(f(suc(z)),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'('0',f(z)) ),
inference(resolution,[status(thm)],[f725,f253]) ).
fof(f741,plain,
! [E,LE] :
( 'LE'(f(suc(z)),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ 'E'('0',f(z)) ),
inference(forward_subsumption_resolution,[status(thm)],[f737,f223]) ).
fof(f745,plain,
! [E] : ~ 'E'('0',f(z)),
inference(backward_subsumption_resolution,[status(thm)],[f723,f746]) ).
fof(f746,plain,
! [E,LE] :
( 'LE'(f(suc(z)),s('0'))
| ~ 'E'('0',f(z)) ),
inference(forward_subsumption_resolution,[status(thm)],[f741,f242]) ).
fof(f747,plain,
! [LE] : ~ 'LE'(f(z),s('0')),
inference(backward_subsumption_resolution,[status(thm)],[f222,f745]) ).
fof(f748,plain,
! [E] :
( ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[status(thm)],[f747,f534]) ).
fof(f750,plain,
! [E,LE] :
( 'LE'(f(z),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(z))) ),
inference(resolution,[status(thm)],[f748,f253]) ).
fof(f754,plain,
! [E,LE] :
( 'LE'(f(z),s('0'))
| ~ 'E'(s('0'),f(suc(suc(suc(z))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f750,f223]) ).
fof(f759,plain,
! [LE] : 'LE'(f(z),s('0')),
inference(forward_subsumption_resolution,[status(thm)],[f754,f242]) ).
fof(f760,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f747,f759]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO660-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n004.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Mon Sep 21 12:08:11 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.15/5.40 % Drodi V4.1.1
% 0.15/5.81 % Refutation found
% 0.15/5.81 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/5.83 % Elapsed time: 0.443278 seconds
% 0.15/5.83 % CPU time: 3.259063 seconds
% 0.15/5.83 % Total memory used: 30.034 MB
% 0.15/5.83 % Net memory used: 27.395 MB
%------------------------------------------------------------------------------