%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO685-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 : Tue Sep 29 02:28:38 PM UTC 2026
% Result : Unsatisfiable 0.65s 0.71s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 85
% Syntax : Number of formulae : 521 ( 12 unt; 38 def)
% Number of atoms : 1686 ( 0 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 2014 ( 849 ~;1127 |; 0 &)
% ( 38 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 42 ( 41 usr; 39 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 153 ( 0 sgn 153 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_143) ).
fof(f2,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_130) ).
fof(f3,axiom,
! [X0] :
( ~ 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s('0')),f(X0))
| 'LE'(f(X0),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_125) ).
fof(f4,axiom,
! [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))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_61) ).
fof(f5,axiom,
! [X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_169) ).
fof(f6,axiom,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_208) ).
fof(f7,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_28) ).
fof(f8,axiom,
! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'LE'(f(X0),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_97) ).
fof(f9,axiom,
! [X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_74) ).
fof(f10,axiom,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_190) ).
fof(f11,axiom,
! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_79) ).
fof(f12,axiom,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X0))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_55) ).
fof(f13,axiom,
! [X0] :
( ~ 'LE'(f(X0),s(s('0')))
| 'E'(s('0'),f(X0))
| 'LE'(f(X0),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_184) ).
fof(f14,axiom,
! [X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ iLEQ(suc(X1),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(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_94) ).
fof(f15,axiom,
! [X0] :
( ~ 'LE'(f(suc(X0)),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_191) ).
fof(f16,axiom,
! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_93) ).
fof(f17,axiom,
! [X0] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_40) ).
fof(f18,axiom,
! [X0] :
( ~ 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(X0))
| 'LE'(f(X0),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_95) ).
fof(f19,axiom,
! [X0] :
( ~ 'LE'(f(suc(X0)),s(s(s('0'))))
| 'E'(s(s('0')),f(suc(X0)))
| 'LE'(f(X0),s(s('0'))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_86) ).
fof(f20,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_96) ).
fof(f21,axiom,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_175) ).
fof(f22,axiom,
! [X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_49) ).
fof(f23,axiom,
! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'LE'(f(X0),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_52) ).
fof(f24,axiom,
! [X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_154) ).
fof(f25,axiom,
! [X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_36) ).
fof(f26,axiom,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_194) ).
fof(f27,axiom,
! [X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_181) ).
fof(f28,axiom,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_31) ).
fof(f29,axiom,
! [X0] :
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_168) ).
fof(f30,axiom,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_192) ).
fof(f31,axiom,
! [X0] :
( ~ 'LE'(f(suc(X0)),s(s('0')))
| 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X0),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30) ).
fof(f32,axiom,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_87) ).
fof(f33,axiom,
! [X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_105) ).
fof(f34,axiom,
! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s(s('0')))
| 'E'(s('0'),f(suc(suc(X0))))
| 'LE'(f(X0),s('0')) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_116) ).
fof(f35,axiom,
! [X0] :
( ~ 'LE'(f(X0),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(X0))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_113) ).
fof(f36,axiom,
! [X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_44) ).
fof(f37,axiom,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_34) ).
fof(f38,axiom,
! [X0] :
( ~ 'LE'(f(suc(X0)),s(s(s(s('0')))))
| 'E'(s(s(s('0'))),f(suc(X0)))
| 'LE'(f(X0),s(s(s('0')))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_111) ).
fof(f39,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19) ).
fof(f40,axiom,
! [X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_115) ).
fof(f41,axiom,
! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s('0'))
| 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_11) ).
fof(f42,axiom,
! [X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_9) ).
fof(f43,axiom,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_73) ).
fof(f44,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_204) ).
fof(f45,axiom,
! [X0] : 'LE'(f(X0),s(s(s(s(s('0')))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_53) ).
fof(f46,axiom,
! [X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ iLEQ(suc(X1),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(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_183) ).
fof(f47,axiom,
! [X0] :
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_173) ).
fof(f48,plain,
! [X0] :
( 'E'(s(s(s(s('0')))),f(X0))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(forward_subsumption_resolution,[],[f35,f45]) ).
fof(f49,plain,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f36,f39]) ).
fof(f50,plain,
! [X0] :
( 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(forward_subsumption_resolution,[],[f15,f45]) ).
fof(f51,plain,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f4,f44]) ).
fof(f52,plain,
! [X0] :
( 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(forward_subsumption_resolution,[],[f16,f45]) ).
fof(f53,plain,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f17,f1]) ).
fof(f54,plain,
! [X0] :
( iLEQ(suc(X0),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(forward_subsumption_resolution,[],[f10,f7]) ).
fof(f55,plain,
! [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(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f11,f2]) ).
fof(f56,plain,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[],[f26,f5]) ).
fof(f57,plain,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f27,f5]) ).
fof(f58,plain,
! [X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[],[f12,f32]) ).
fof(f59,plain,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[],[f30,f32]) ).
fof(f60,plain,
! [X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(forward_subsumption_resolution,[],[f33,f57]) ).
fof(f61,plain,
! [X0,X1] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(forward_subsumption_resolution,[],[f60,f56]) ).
fof(f64,plain,
! [X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(factoring,[],[f61]) ).
fof(f65,plain,
! [X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0))) ),
inference(duplicate_literal_removal,[],[f64]) ).
fof(f67,plain,
! [X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f65,f49]) ).
fof(f68,plain,
! [X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f24,f40]) ).
fof(f69,plain,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f25,f40]) ).
fof(f70,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[],[f21,f59]) ).
fof(f71,plain,
! [X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[],[f70,f58]) ).
fof(f72,plain,
! [X0] :
( ~ 'E'(s('0'),f(suc(suc(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(X0)) ),
inference(factoring,[],[f71]) ).
fof(f76,plain,
! [X0] :
( ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s('0'),f(X0)) ),
inference(duplicate_literal_removal,[],[f72]) ).
fof(f77,plain,
! [X0] :
( ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[],[f76,f51]) ).
fof(f78,plain,
! [X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[],[f6,f22]) ).
fof(f79,plain,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[],[f28,f22]) ).
fof(f80,plain,
! [X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f9,f69]) ).
fof(f81,plain,
! [X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f80,f68]) ).
fof(f83,plain,
! [X0] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(factoring,[],[f81]) ).
fof(f85,plain,
! [X0] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literal_removal,[],[f83]) ).
fof(f87,plain,
! [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,[],[f85,f53]) ).
fof(f88,plain,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),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(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0)) ),
inference(forward_subsumption_resolution,[],[f14,f37]) ).
fof(f89,plain,
! [X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ '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(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0)) ),
inference(forward_subsumption_resolution,[],[f42,f37]) ).
fof(f90,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f43,f79]) ).
fof(f91,plain,
! [X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f90,f78]) ).
fof(f94,plain,
! [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'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[],[f91]) ).
fof(f95,plain,
! [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))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(duplicate_literal_removal,[],[f94]) ).
fof(f97,plain,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(forward_subsumption_resolution,[],[f95,f54]) ).
fof(f98,plain,
! [X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ iLEQ(suc(X1),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(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f46,f88]) ).
fof(f99,plain,
! [X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),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(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X1)) ),
inference(forward_subsumption_resolution,[],[f98,f89]) ).
fof(f103,plain,
! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(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(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0)) ),
inference(factoring,[],[f99]) ).
fof(f107,plain,
! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0))) ),
inference(duplicate_literal_removal,[],[f103]) ).
fof(f108,plain,
! [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,[],[f107,f55]) ).
fof(f112,plain,
! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(resolution,[],[f108,f52]) ).
fof(f116,plain,
! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(forward_subsumption_resolution,[],[f112,f48]) ).
fof(f117,plain,
! [X0] : 'LE'(f(X0),s(s(s(s('0'))))),
inference(forward_subsumption_resolution,[],[f116,f50]) ).
fof(f118,plain,
! [X0] :
( 'E'(s(s(s('0'))),f(X0))
| 'LE'(f(X0),s(s(s('0')))) ),
inference(resolution,[],[f117,f18]) ).
fof(f119,plain,
! [X0] :
( 'E'(s(s(s('0'))),f(suc(X0)))
| 'LE'(f(X0),s(s(s('0')))) ),
inference(resolution,[],[f117,f38]) ).
fof(f120,plain,
! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f117,f23]) ).
fof(f123,plain,
! [X0] :
( 'LE'(f(suc(X0)),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(resolution,[],[f119,f97]) ).
fof(f126,plain,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(X0))
| 'LE'(f(suc(X0)),s(s(s('0')))) ),
inference(forward_subsumption_resolution,[],[f123,f118]) ).
fof(f127,plain,
! [X0] :
( 'LE'(f(suc(X0)),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) ),
inference(resolution,[],[f126,f118]) ).
fof(f130,plain,
! [X0] :
( 'E'(s(s('0')),f(suc(suc(X0))))
| 'LE'(f(suc(X0)),s(s(s('0'))))
| 'LE'(f(X0),s(s('0'))) ),
inference(resolution,[],[f127,f8]) ).
fof(f132,plain,
! [X0] :
( 'E'(s(s('0')),f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'LE'(f(X0),s(s('0'))) ),
inference(resolution,[],[f120,f3]) ).
fof(f133,plain,
! [X0] :
( 'E'(s(s('0')),f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'LE'(f(X0),s(s('0'))) ),
inference(resolution,[],[f120,f19]) ).
fof(f134,plain,
! [X0] :
( 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| 'LE'(f(X0),s(s('0'))) ),
inference(resolution,[],[f120,f8]) ).
fof(f142,plain,
! [X0] :
( 'LE'(f(suc(X0)),s(s('0')))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[],[f133,f87]) ).
fof(f150,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[],[f134,f87]) ).
fof(f157,plain,
! [X0] :
( 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0)))))))
| 'LE'(f(X0),s('0')) ),
inference(resolution,[],[f150,f31]) ).
fof(f158,plain,
! [X0] :
( 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0))))))))
| 'LE'(f(X0),s('0')) ),
inference(resolution,[],[f150,f34]) ).
fof(f162,plain,
! [X0] :
( 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0)))))))
| 'LE'(f(X0),s('0')) ),
inference(resolution,[],[f142,f34]) ).
fof(f214,plain,
! [X0] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0)))))))
| 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(resolution,[],[f162,f77]) ).
fof(f217,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[],[f214,f157]) ).
fof(f221,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(resolution,[],[f158,f77]) ).
fof(f235,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(X0)))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| 'E'('0',f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f217,f41]) ).
fof(f238,definition,
( spl0_1
<=> 'E'(s(s('0')),f(suc(z))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f239,plain,
( 'E'(s(s('0')),f(suc(z)))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( ~ 'E'(s(s('0')),f(suc(z)))
| spl0_1 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f242,definition,
( spl0_2
<=> 'E'('0',f(z)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f246,definition,
( spl0_3
<=> 'E'(s(s('0')),f(z)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f248,plain,
( ~ 'E'(s(s('0')),f(z))
| spl0_3 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f250,definition,
( spl0_4
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f251,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_4 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f252,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f255,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'LE'(f(z),s(s('0')))
| spl0_1 ),
inference(resolution,[],[f240,f133]) ).
fof(f259,definition,
( spl0_5
<=> 'LE'(f(suc(z)),s(s('0'))) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f261,plain,
( 'LE'(f(suc(z)),s(s('0')))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f263,definition,
( spl0_6
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f264,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_6 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f265,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f268,definition,
( spl0_7
<=> 'LE'(f(z),s(s('0'))) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f270,plain,
( 'LE'(f(z),s(s('0')))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f272,definition,
( spl0_8
<=> 'LE'(f(z),s(s(s('0')))) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f274,plain,
( 'LE'(f(z),s(s(s('0'))))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f276,plain,
( spl0_7
| spl0_6
| spl0_1 ),
inference(avatar_split_clause,[],[f255,f238,f263,f268]) ).
fof(f283,definition,
( spl0_9
<=> 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f284,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_9 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f285,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f289,definition,
( spl0_10
<=> 'LE'(f(z),s('0')) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f291,plain,
( 'LE'(f(z),s('0'))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl0_11
<=> 'E'(s('0'),f(z)) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f297,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'E'('0',f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f221,f47]) ).
fof(f298,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(X0)))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| 'E'('0',f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f221,f29]) ).
fof(f301,plain,
( ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(z))
| ~ spl0_9 ),
inference(resolution,[],[f285,f97]) ).
fof(f305,definition,
( spl0_12
<=> 'E'(s(s(s('0'))),f(z)) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f307,plain,
( ~ 'E'(s(s(s('0'))),f(z))
| spl0_12 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f309,definition,
( spl0_13
<=> 'E'(s(s(s('0'))),f(suc(z))) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f311,plain,
( ~ 'E'(s(s(s('0'))),f(suc(z)))
| spl0_13 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
( ~ spl0_12
| ~ spl0_13
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f301,f283,f309,f305]) ).
fof(f317,plain,
( 'LE'(f(z),s(s(s('0'))))
| spl0_12 ),
inference(resolution,[],[f307,f118]) ).
fof(f318,plain,
( spl0_8
| spl0_12 ),
inference(avatar_split_clause,[],[f317,f305,f272]) ).
fof(f321,plain,
( 'E'(s(s('0')),f(z))
| 'LE'(f(z),s(s('0')))
| ~ spl0_8 ),
inference(resolution,[],[f274,f3]) ).
fof(f329,definition,
( spl0_14
<=> 'E'(s(s('0')),f(suc(suc(z)))) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f330,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f333,definition,
( spl0_15
<=> 'E'('0',f(suc(z))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f334,plain,
( ~ 'E'('0',f(suc(z)))
| spl0_15 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f337,definition,
( spl0_16
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f338,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_16 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f339,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f341,plain,
( 'E'('0',f(z))
| 'LE'(f(z),'0')
| ~ spl0_10 ),
inference(resolution,[],[f291,f47]) ).
fof(f342,plain,
( 'E'('0',f(z))
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f341,f20]) ).
fof(f343,plain,
( spl0_2
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f342,f289,f242]) ).
fof(f348,definition,
( spl0_17
<=> 'E'(s(s('0')),f(suc(suc(suc(z))))) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f349,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f350,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| spl0_17 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f352,definition,
( spl0_18
<=> 'E'('0',f(suc(suc(z)))) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f353,plain,
( ~ 'E'('0',f(suc(suc(z))))
| spl0_18 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f354,plain,
( 'E'('0',f(suc(suc(z))))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,definition,
( spl0_19
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f357,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_19 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f358,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f370,definition,
( spl0_20
<=> 'LE'(f(suc(suc(z))),s(s('0'))) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f371,plain,
( ~ 'LE'(f(suc(suc(z))),s(s('0')))
| spl0_20 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f372,plain,
( 'LE'(f(suc(suc(z))),s(s('0')))
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f375,definition,
( spl0_21
<=> 'LE'(f(suc(z)),s(s(s('0')))) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f377,plain,
( 'LE'(f(suc(z)),s(s(s('0'))))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f386,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'LE'(f(suc(z)),s(s('0')))
| spl0_1 ),
inference(resolution,[],[f240,f132]) ).
fof(f387,plain,
( spl0_5
| spl0_6
| spl0_1 ),
inference(avatar_split_clause,[],[f386,f238,f263,f259]) ).
fof(f392,definition,
( spl0_22
<=> 'LE'(f(suc(z)),s('0')) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f393,plain,
( ~ 'LE'(f(suc(z)),s('0'))
| spl0_22 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f394,plain,
( 'LE'(f(suc(z)),s('0'))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f396,definition,
( spl0_23
<=> 'E'(s('0'),f(suc(z))) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f418,definition,
( spl0_24
<=> 'LE'(f(suc(suc(suc(z)))),s(s('0'))) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f420,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f423,definition,
( spl0_25
<=> 'LE'(f(suc(suc(z))),s(s(s('0')))) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f424,plain,
( ~ 'LE'(f(suc(suc(z))),s(s(s('0'))))
| spl0_25 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f425,plain,
( 'LE'(f(suc(suc(z))),s(s(s('0'))))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f441,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(z))
| 'E'('0',f(z))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f297,f20]) ).
fof(f442,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| 'E'('0',f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f235,f20]) ).
fof(f449,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f298,f20]) ).
fof(f461,plain,
( 'LE'(f(z),s(s(s('0'))))
| spl0_13 ),
inference(resolution,[],[f311,f119]) ).
fof(f462,plain,
( 'LE'(f(suc(z)),s(s(s('0'))))
| spl0_13 ),
inference(resolution,[],[f311,f118]) ).
fof(f463,plain,
( spl0_21
| spl0_13 ),
inference(avatar_split_clause,[],[f462,f309,f375]) ).
fof(f476,plain,
( 'E'('0',f(suc(z)))
| 'LE'(f(z),'0')
| ~ spl0_22 ),
inference(resolution,[],[f394,f29]) ).
fof(f479,plain,
( 'LE'(f(z),'0')
| spl0_15
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f476,f334]) ).
fof(f480,plain,
( $false
| spl0_15
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f479,f20]) ).
fof(f481,plain,
( spl0_15
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f480]) ).
fof(f485,definition,
( spl0_26
<=> 'E'(s(s('0')),f(suc(suc(suc(suc(z)))))) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f486,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f487,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| spl0_26 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f489,definition,
( spl0_27
<=> 'E'(s('0'),f(suc(suc(z)))) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f490,plain,
( 'E'(s('0'),f(suc(suc(z))))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( ~ 'E'(s('0'),f(suc(suc(z))))
| spl0_27 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f493,definition,
( spl0_28
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f494,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_28 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f495,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f507,definition,
( spl0_29
<=> 'LE'(f(suc(suc(suc(suc(z))))),s(s('0'))) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f508,plain,
( ~ 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_29 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f509,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f512,definition,
( spl0_30
<=> 'LE'(f(suc(suc(suc(z)))),s(s(s('0')))) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f513,plain,
( ~ 'LE'(f(suc(suc(suc(z)))),s(s(s('0'))))
| spl0_30 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s(s('0'))))
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f582,plain,
( 'LE'(f(suc(z)),s(s(s('0'))))
| spl0_9 ),
inference(resolution,[],[f284,f119]) ).
fof(f583,plain,
( 'LE'(f(suc(suc(z))),s(s(s('0'))))
| spl0_9 ),
inference(resolution,[],[f284,f118]) ).
fof(f584,plain,
( spl0_25
| spl0_9 ),
inference(avatar_split_clause,[],[f583,f283,f423]) ).
fof(f586,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ spl0_19 ),
inference(resolution,[],[f358,f97]) ).
fof(f589,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f586,f252]) ).
fof(f590,plain,
( ~ spl0_16
| ~ spl0_4
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f589,f356,f250,f337]) ).
fof(f594,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0'))))
| spl0_16 ),
inference(resolution,[],[f338,f119]) ).
fof(f595,plain,
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0'))))
| spl0_16 ),
inference(resolution,[],[f338,f118]) ).
fof(f596,plain,
( 'LE'(f(suc(suc(z))),s(s(s('0'))))
| spl0_6 ),
inference(resolution,[],[f264,f119]) ).
fof(f597,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s(s('0'))))
| spl0_6 ),
inference(resolution,[],[f264,f118]) ).
fof(f598,plain,
( spl0_30
| spl0_6 ),
inference(avatar_split_clause,[],[f597,f263,f512]) ).
fof(f599,plain,
( spl0_25
| spl0_6 ),
inference(avatar_split_clause,[],[f596,f263,f423]) ).
fof(f600,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s(s('0'))))
| spl0_4 ),
inference(resolution,[],[f251,f119]) ).
fof(f601,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0'))))
| spl0_4 ),
inference(resolution,[],[f251,f118]) ).
fof(f602,plain,
( spl0_30
| spl0_4 ),
inference(avatar_split_clause,[],[f600,f250,f512]) ).
fof(f603,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'LE'(f(z),s('0'))
| ~ spl0_20 ),
inference(resolution,[],[f372,f34]) ).
fof(f604,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'LE'(f(suc(z)),s('0'))
| ~ spl0_20 ),
inference(resolution,[],[f372,f31]) ).
fof(f605,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'LE'(f(suc(suc(z))),s('0'))
| ~ spl0_20 ),
inference(resolution,[],[f372,f13]) ).
fof(f606,plain,
( 'LE'(f(suc(suc(z))),s('0'))
| ~ spl0_20
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f605,f491]) ).
fof(f607,plain,
( 'LE'(f(suc(z)),s('0'))
| ~ spl0_20
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f604,f491]) ).
fof(f610,plain,
( spl0_22
| ~ spl0_20
| spl0_27 ),
inference(avatar_split_clause,[],[f607,f489,f370,f392]) ).
fof(f612,plain,
( 'LE'(f(z),s('0'))
| ~ spl0_20
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f603,f491]) ).
fof(f614,plain,
( spl0_10
| ~ spl0_20
| spl0_27 ),
inference(avatar_split_clause,[],[f612,f489,f370,f289]) ).
fof(f627,plain,
( 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0')
| ~ spl0_20
| spl0_27 ),
inference(resolution,[],[f606,f41]) ).
fof(f632,plain,
( 'LE'(f(z),'0')
| spl0_18
| ~ spl0_20
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f627,f353]) ).
fof(f633,plain,
( $false
| spl0_18
| ~ spl0_20
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f632,f20]) ).
fof(f634,plain,
( spl0_18
| ~ spl0_20
| spl0_27 ),
inference(avatar_contradiction_clause,[],[f633]) ).
fof(f648,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| spl0_20 ),
inference(resolution,[],[f371,f150]) ).
fof(f651,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'LE'(f(z),s(s('0')))
| ~ spl0_25 ),
inference(resolution,[],[f425,f8]) ).
fof(f653,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'LE'(f(suc(suc(z))),s(s('0')))
| ~ spl0_25 ),
inference(resolution,[],[f425,f3]) ).
fof(f657,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| spl0_20
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f653,f371]) ).
fof(f658,plain,
( spl0_14
| spl0_20
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f657,f423,f370,f329]) ).
fof(f659,plain,
( ~ 'E'(s(s('0')),f(z))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ spl0_14 ),
inference(resolution,[],[f330,f87]) ).
fof(f670,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(z))),s(s('0')))
| spl0_16 ),
inference(resolution,[],[f594,f8]) ).
fof(f671,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| spl0_16 ),
inference(resolution,[],[f594,f19]) ).
fof(f672,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_16 ),
inference(resolution,[],[f594,f3]) ).
fof(f673,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_16
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f672,f487]) ).
fof(f674,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| spl0_16
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f671,f487]) ).
fof(f675,plain,
( 'LE'(f(suc(suc(z))),s(s('0')))
| spl0_16
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f670,f487]) ).
fof(f676,plain,
( spl0_29
| spl0_16
| spl0_26 ),
inference(avatar_split_clause,[],[f673,f485,f337,f507]) ).
fof(f677,plain,
( spl0_24
| spl0_16
| spl0_26 ),
inference(avatar_split_clause,[],[f674,f485,f337,f418]) ).
fof(f678,plain,
( $false
| spl0_16
| spl0_20
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f675,f371]) ).
fof(f679,plain,
( spl0_16
| spl0_20
| spl0_26 ),
inference(avatar_contradiction_clause,[],[f678]) ).
fof(f681,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ spl0_14
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f648,f330]) ).
fof(f686,plain,
( ~ spl0_17
| spl0_19
| ~ spl0_14
| spl0_20 ),
inference(avatar_split_clause,[],[f681,f370,f329,f356,f348]) ).
fof(f697,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| 'LE'(f(suc(suc(z))),s(s('0')))
| spl0_17 ),
inference(resolution,[],[f350,f133]) ).
fof(f699,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| spl0_17 ),
inference(resolution,[],[f350,f132]) ).
fof(f700,plain,
( spl0_24
| spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f699,f348,f337,f418]) ).
fof(f701,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_17
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f697,f371]) ).
fof(f702,plain,
( spl0_16
| spl0_17
| spl0_20 ),
inference(avatar_split_clause,[],[f701,f370,f348,f337]) ).
fof(f712,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_30 ),
inference(resolution,[],[f513,f120]) ).
fof(f713,plain,
( spl0_16
| spl0_30 ),
inference(avatar_split_clause,[],[f712,f512,f337]) ).
fof(f729,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| spl0_26 ),
inference(resolution,[],[f487,f133]) ).
fof(f731,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_26 ),
inference(resolution,[],[f487,f132]) ).
fof(f732,plain,
( spl0_29
| spl0_19
| spl0_26 ),
inference(avatar_split_clause,[],[f731,f485,f356,f507]) ).
fof(f734,plain,
( spl0_24
| spl0_19
| spl0_26 ),
inference(avatar_split_clause,[],[f729,f485,f356,f418]) ).
fof(f740,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'LE'(f(suc(z)),s(s('0')))
| ~ spl0_30 ),
inference(resolution,[],[f514,f8]) ).
fof(f741,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'LE'(f(suc(suc(z))),s(s('0')))
| ~ spl0_30 ),
inference(resolution,[],[f514,f19]) ).
fof(f742,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| ~ spl0_30 ),
inference(resolution,[],[f514,f3]) ).
fof(f745,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(z))),s(s('0')))
| spl0_4 ),
inference(resolution,[],[f601,f8]) ).
fof(f746,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| spl0_4 ),
inference(resolution,[],[f601,f19]) ).
fof(f747,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_4 ),
inference(resolution,[],[f601,f3]) ).
fof(f755,plain,
( ~ spl0_26
| spl0_18
| ~ spl0_27
| ~ spl0_17
| spl0_28 ),
inference(avatar_split_clause,[],[f442,f493,f348,f489,f352,f485]) ).
fof(f757,definition,
( spl0_31
<=> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z))))))) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f758,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f759,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| spl0_31 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f761,definition,
( spl0_32
<=> 'E'(s('0'),f(suc(suc(suc(z))))) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f762,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f765,definition,
( spl0_33
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f767,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f765]) ).
fof(f771,plain,
( spl0_29
| spl0_26
| spl0_4 ),
inference(avatar_split_clause,[],[f747,f250,f485,f507]) ).
fof(f772,plain,
( spl0_24
| spl0_26
| spl0_4 ),
inference(avatar_split_clause,[],[f746,f250,f485,f418]) ).
fof(f773,plain,
( spl0_20
| spl0_26
| spl0_4 ),
inference(avatar_split_clause,[],[f745,f250,f485,f370]) ).
fof(f774,plain,
( spl0_24
| spl0_17
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f742,f512,f348,f418]) ).
fof(f775,plain,
( spl0_20
| spl0_17
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f741,f512,f348,f370]) ).
fof(f781,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(z))
| ~ spl0_27 ),
inference(resolution,[],[f490,f77]) ).
fof(f797,plain,
( ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ spl0_26 ),
inference(resolution,[],[f486,f87]) ).
fof(f805,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'LE'(f(suc(z)),s('0'))
| ~ spl0_24 ),
inference(resolution,[],[f420,f34]) ).
fof(f806,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'LE'(f(suc(suc(z))),s('0'))
| ~ spl0_24 ),
inference(resolution,[],[f420,f31]) ).
fof(f814,definition,
( spl0_35
<=> 'LE'(f(suc(suc(z))),s('0')) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f815,plain,
( ~ 'LE'(f(suc(suc(z))),s('0'))
| spl0_35 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f816,plain,
( 'LE'(f(suc(suc(z))),s('0'))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f817,plain,
( spl0_35
| spl0_32
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f806,f418,f761,f814]) ).
fof(f820,plain,
( ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(z)))
| ~ spl0_32 ),
inference(resolution,[],[f762,f77]) ).
fof(f822,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ spl0_27
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f820,f490]) ).
fof(f825,plain,
( ~ spl0_23
| ~ spl0_27
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f822,f761,f489,f396]) ).
fof(f829,plain,
( spl0_22
| spl0_32
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f805,f418,f761,f392]) ).
fof(f832,plain,
( spl0_7
| spl0_3
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f321,f272,f246,f268]) ).
fof(f833,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f659,f329,f246,f238]) ).
fof(f834,plain,
( spl0_21
| spl0_9 ),
inference(avatar_split_clause,[],[f582,f283,f375]) ).
fof(f836,plain,
( ~ spl0_11
| ~ spl0_23
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f781,f489,f396,f293]) ).
fof(f841,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'LE'(f(z),s(s('0')))
| spl0_3 ),
inference(resolution,[],[f248,f132]) ).
fof(f842,plain,
( spl0_7
| spl0_9
| spl0_3 ),
inference(avatar_split_clause,[],[f841,f246,f283,f268]) ).
fof(f868,plain,
( 'E'(s('0'),f(suc(z)))
| 'LE'(f(z),s('0'))
| ~ spl0_5 ),
inference(resolution,[],[f261,f31]) ).
fof(f873,plain,
( spl0_10
| spl0_23
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f868,f259,f396,f289]) ).
fof(f874,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'LE'(f(z),s(s('0')))
| ~ spl0_21 ),
inference(resolution,[],[f377,f19]) ).
fof(f875,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'LE'(f(suc(z)),s(s('0')))
| ~ spl0_21 ),
inference(resolution,[],[f377,f3]) ).
fof(f881,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ spl0_6 ),
inference(resolution,[],[f265,f97]) ).
fof(f890,plain,
( 'E'('0',f(suc(suc(z))))
| 'LE'(f(z),'0')
| ~ spl0_35 ),
inference(resolution,[],[f816,f41]) ).
fof(f895,plain,
( 'LE'(f(z),'0')
| spl0_18
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f890,f353]) ).
fof(f896,plain,
( $false
| spl0_18
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f895,f20]) ).
fof(f897,plain,
( spl0_18
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f896]) ).
fof(f972,definition,
( spl0_41
<=> 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f973,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f972]) ).
fof(f980,definition,
( spl0_43
<=> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f981,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f982,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_43 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f985,plain,
( 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s(s('0'))))
| spl0_28 ),
inference(resolution,[],[f494,f119]) ).
fof(f1023,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_43 ),
inference(resolution,[],[f981,f87]) ).
fof(f1025,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_26
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f1023,f486]) ).
fof(f1028,plain,
( ~ spl0_31
| ~ spl0_26
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f1025,f980,f485,f757]) ).
fof(f1035,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_31 ),
inference(resolution,[],[f759,f133]) ).
fof(f1042,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(z))),s('0'))
| ~ spl0_29 ),
inference(resolution,[],[f509,f34]) ).
fof(f1058,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ spl0_29
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f1042,f815]) ).
fof(f1060,plain,
( spl0_41
| ~ spl0_29
| spl0_35 ),
inference(avatar_split_clause,[],[f1058,f814,f507,f972]) ).
fof(f1076,plain,
( ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ spl0_41 ),
inference(resolution,[],[f973,f77]) ).
fof(f1078,plain,
( ~ 'E'(s('0'),f(suc(suc(z))))
| ~ spl0_32
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f1076,f762]) ).
fof(f1079,plain,
( $false
| ~ spl0_27
| ~ spl0_32
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f1078,f490]) ).
fof(f1080,plain,
( ~ spl0_27
| ~ spl0_32
| ~ spl0_41 ),
inference(avatar_contradiction_clause,[],[f1079]) ).
fof(f1082,plain,
( spl0_29
| spl0_28
| spl0_31 ),
inference(avatar_split_clause,[],[f1035,f757,f493,f507]) ).
fof(f1083,plain,
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0'))))
| spl0_19 ),
inference(resolution,[],[f357,f119]) ).
fof(f1084,plain,
( 'LE'(f(suc(suc(suc(suc(suc(suc(z))))))),s(s(s('0'))))
| spl0_19 ),
inference(resolution,[],[f357,f118]) ).
fof(f1107,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| spl0_29 ),
inference(resolution,[],[f508,f150]) ).
fof(f1109,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_19 ),
inference(resolution,[],[f1083,f19]) ).
fof(f1111,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_19
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f1109,f759]) ).
fof(f1120,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| spl0_16 ),
inference(resolution,[],[f595,f8]) ).
fof(f1121,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_16 ),
inference(resolution,[],[f595,f19]) ).
fof(f1129,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_26
| spl0_29 ),
inference(forward_subsumption_resolution,[],[f1107,f486]) ).
fof(f1134,plain,
( ~ spl0_31
| spl0_33
| ~ spl0_26
| spl0_29 ),
inference(avatar_split_clause,[],[f1129,f507,f485,f765,f757]) ).
fof(f1139,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ spl0_31 ),
inference(resolution,[],[f758,f87]) ).
fof(f1155,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ spl0_33 ),
inference(resolution,[],[f767,f97]) ).
fof(f1158,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_19 ),
inference(resolution,[],[f1084,f8]) ).
fof(f1162,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_19
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1158,f982]) ).
fof(f1166,plain,
( ~ spl0_19
| ~ spl0_28
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1155,f765,f493,f356]) ).
fof(f1170,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_28 ),
inference(resolution,[],[f985,f8]) ).
fof(f1174,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_28
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1170,f982]) ).
fof(f1176,plain,
( $false
| spl0_28
| spl0_29
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1174,f508]) ).
fof(f1177,plain,
( spl0_28
| spl0_29
| spl0_43 ),
inference(avatar_contradiction_clause,[],[f1176]) ).
fof(f1178,plain,
( spl0_8
| spl0_13 ),
inference(avatar_split_clause,[],[f461,f309,f272]) ).
fof(f1184,plain,
( ~ spl0_13
| ~ spl0_9
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f881,f263,f283,f309]) ).
fof(f1185,plain,
( spl0_7
| spl0_1
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f874,f375,f238,f268]) ).
fof(f1193,plain,
( ~ spl0_17
| ~ spl0_14
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f797,f485,f329,f348]) ).
fof(f1194,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f449,f490]) ).
fof(f1197,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ spl0_26
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f1139,f486]) ).
fof(f1198,plain,
( spl0_7
| spl0_14
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f651,f423,f329,f268]) ).
fof(f1201,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(z)))
| 'E'('0',f(suc(z)))
| ~ spl0_26
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1194,f486]) ).
fof(f1204,plain,
( ~ spl0_17
| ~ spl0_26
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f1197,f757,f485,f348]) ).
fof(f1205,plain,
( spl0_15
| ~ spl0_23
| ~ spl0_17
| spl0_28
| ~ spl0_26
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f1201,f489,f485,f493,f348,f396,f333]) ).
fof(f1208,plain,
( spl0_29
| spl0_31
| spl0_16 ),
inference(avatar_split_clause,[],[f1121,f337,f757,f507]) ).
fof(f1209,plain,
( spl0_24
| spl0_31
| spl0_16 ),
inference(avatar_split_clause,[],[f1120,f337,f757,f418]) ).
fof(f1213,plain,
( spl0_5
| spl0_1
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f875,f375,f238,f259]) ).
fof(f1214,plain,
( spl0_5
| spl0_17
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f740,f512,f348,f259]) ).
fof(f1218,definition,
( spl0_48
<=> 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0')))) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f1220,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0'))))
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f1218]) ).
fof(f1230,plain,
( ~ 'E'('0',f(z))
| ~ 'E'('0',f(suc(z)))
| ~ spl0_18 ),
inference(resolution,[],[f354,f67]) ).
fof(f1272,plain,
( ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ spl0_17 ),
inference(resolution,[],[f349,f87]) ).
fof(f1282,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ spl0_4 ),
inference(resolution,[],[f252,f97]) ).
fof(f1285,plain,
( ~ spl0_9
| ~ spl0_6
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f1282,f250,f263,f283]) ).
fof(f1289,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0'))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| spl0_31 ),
inference(resolution,[],[f759,f130]) ).
fof(f1293,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| 'LE'(f(suc(suc(suc(suc(z))))),s(s('0')))
| spl0_31 ),
inference(resolution,[],[f759,f133]) ).
fof(f1297,plain,
( spl0_29
| spl0_28
| spl0_31 ),
inference(avatar_split_clause,[],[f1293,f757,f493,f507]) ).
fof(f1299,plain,
( spl0_24
| spl0_48
| spl0_31 ),
inference(avatar_split_clause,[],[f1289,f757,f1218,f418]) ).
fof(f1301,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_28 ),
inference(resolution,[],[f495,f97]) ).
fof(f1329,plain,
( spl0_29
| spl0_19
| spl0_31 ),
inference(avatar_split_clause,[],[f1111,f757,f356,f507]) ).
fof(f1330,plain,
( spl0_29
| spl0_19
| spl0_43 ),
inference(avatar_split_clause,[],[f1162,f980,f356,f507]) ).
fof(f1332,definition,
( spl0_49
<=> 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0')))) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f1334,plain,
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0'))))
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1337,plain,
( ~ spl0_16
| ~ spl0_19
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f1301,f493,f356,f337]) ).
fof(f1339,plain,
( ~ spl0_15
| ~ spl0_2
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f1230,f352,f242,f333]) ).
fof(f1344,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ spl0_16 ),
inference(resolution,[],[f339,f97]) ).
fof(f1347,plain,
( 'E'(s('0'),f(z))
| 'LE'(f(z),s('0'))
| ~ spl0_7 ),
inference(resolution,[],[f270,f13]) ).
fof(f1348,plain,
( 'LE'(f(suc(suc(suc(suc(suc(z)))))),s(s(s('0'))))
| spl0_19 ),
inference(resolution,[],[f357,f119]) ).
fof(f1350,plain,
( spl0_49
| spl0_19 ),
inference(avatar_split_clause,[],[f1348,f356,f1332]) ).
fof(f1357,plain,
( 'E'(s('0'),f(suc(z)))
| 'LE'(f(suc(z)),s('0'))
| ~ spl0_5 ),
inference(resolution,[],[f261,f13]) ).
fof(f1358,plain,
( 'E'(s('0'),f(suc(z)))
| ~ spl0_5
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1357,f393]) ).
fof(f1359,plain,
( spl0_23
| ~ spl0_5
| spl0_22 ),
inference(avatar_split_clause,[],[f1358,f392,f259,f396]) ).
fof(f1372,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_25 ),
inference(resolution,[],[f424,f120]) ).
fof(f1373,plain,
( $false
| spl0_4
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f1372,f251]) ).
fof(f1374,plain,
( spl0_4
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f1373]) ).
fof(f1376,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'LE'(f(suc(z)),s(s('0')))
| ~ spl0_25 ),
inference(resolution,[],[f425,f19]) ).
fof(f1382,plain,
( 'LE'(f(suc(suc(suc(suc(z))))),s(s(s('0'))))
| ~ spl0_6 ),
inference(resolution,[],[f265,f126]) ).
fof(f1383,plain,
( spl0_48
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1382,f263,f1218]) ).
fof(f1406,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| ~ spl0_48 ),
inference(resolution,[],[f1220,f19]) ).
fof(f1483,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| ~ spl0_49 ),
inference(resolution,[],[f1334,f8]) ).
fof(f1486,plain,
( 'LE'(f(suc(suc(suc(z)))),s(s('0')))
| spl0_31
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1483,f759]) ).
fof(f1490,plain,
( spl0_24
| spl0_26
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f1406,f1218,f485,f418]) ).
fof(f1491,plain,
( spl0_24
| spl0_31
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f1486,f1332,f757,f418]) ).
fof(f1493,plain,
( ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1272,f239]) ).
fof(f1494,plain,
( ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(z))
| 'E'('0',f(z))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f441,f357]) ).
fof(f1495,plain,
( spl0_10
| spl0_11
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1347,f268,f293,f289]) ).
fof(f1496,plain,
( spl0_5
| spl0_14
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1376,f423,f329,f259]) ).
fof(f1497,plain,
( ~ spl0_6
| ~ spl0_4
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1344,f337,f250,f263]) ).
fof(f1499,plain,
( ~ spl0_14
| ~ spl0_1
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1493,f348,f238,f329]) ).
fof(f1500,plain,
( ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(z))
| 'E'('0',f(z))
| ~ spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1494,f349]) ).
fof(f1502,plain,
( spl0_2
| ~ spl0_11
| ~ spl0_23
| ~ spl0_14
| ~ spl0_17
| spl0_19 ),
inference(avatar_split_clause,[],[f1500,f356,f348,f329,f396,f293,f242]) ).
cnf(s4,plain,
( spl0_1
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f276]) ).
cnf(s8,plain,
( ~ spl0_9
| ~ spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f312]) ).
cnf(s9,plain,
( spl0_8
| spl0_12 ),
inference(sat_conversion,[],[f318]) ).
cnf(s13,plain,
( spl0_2
| ~ spl0_10 ),
inference(sat_conversion,[],[f343]) ).
cnf(s20,plain,
( spl0_1
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f387]) ).
cnf(s34,plain,
( spl0_13
| spl0_21 ),
inference(sat_conversion,[],[f463]) ).
cnf(s37,plain,
( spl0_15
| ~ spl0_22 ),
inference(sat_conversion,[],[f481]) ).
cnf(s58,plain,
( spl0_9
| spl0_25 ),
inference(sat_conversion,[],[f584]) ).
cnf(s60,plain,
( ~ spl0_4
| ~ spl0_16
| ~ spl0_19 ),
inference(sat_conversion,[],[f590]) ).
cnf(s62,plain,
( spl0_6
| spl0_30 ),
inference(sat_conversion,[],[f598]) ).
cnf(s63,plain,
( spl0_6
| spl0_25 ),
inference(sat_conversion,[],[f599]) ).
cnf(s64,plain,
( spl0_4
| spl0_30 ),
inference(sat_conversion,[],[f602]) ).
cnf(s66,plain,
( ~ spl0_20
| spl0_22
| spl0_27 ),
inference(sat_conversion,[],[f610]) ).
cnf(s69,plain,
( spl0_10
| ~ spl0_20
| spl0_27 ),
inference(sat_conversion,[],[f614]) ).
cnf(s71,plain,
( spl0_18
| ~ spl0_20
| spl0_27 ),
inference(sat_conversion,[],[f634]) ).
cnf(s77,plain,
( spl0_14
| spl0_20
| ~ spl0_25 ),
inference(sat_conversion,[],[f658]) ).
cnf(s78,plain,
( spl0_16
| spl0_26
| spl0_29 ),
inference(sat_conversion,[],[f676]) ).
cnf(s79,plain,
( spl0_16
| spl0_24
| spl0_26 ),
inference(sat_conversion,[],[f677]) ).
cnf(s80,plain,
( spl0_16
| spl0_20
| spl0_26 ),
inference(sat_conversion,[],[f679]) ).
cnf(s83,plain,
( ~ spl0_14
| ~ spl0_17
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f686]) ).
cnf(s87,plain,
( spl0_16
| spl0_17
| spl0_24 ),
inference(sat_conversion,[],[f700]) ).
cnf(s88,plain,
( spl0_16
| spl0_17
| spl0_20 ),
inference(sat_conversion,[],[f702]) ).
cnf(s89,plain,
( spl0_16
| spl0_30 ),
inference(sat_conversion,[],[f713]) ).
cnf(s94,plain,
( spl0_19
| spl0_26
| spl0_29 ),
inference(sat_conversion,[],[f732]) ).
cnf(s96,plain,
( spl0_19
| spl0_24
| spl0_26 ),
inference(sat_conversion,[],[f734]) ).
cnf(s104,plain,
( ~ spl0_17
| spl0_18
| ~ spl0_26
| ~ spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f755]) ).
cnf(s106,plain,
( spl0_4
| spl0_26
| spl0_29 ),
inference(sat_conversion,[],[f771]) ).
cnf(s107,plain,
( spl0_4
| spl0_24
| spl0_26 ),
inference(sat_conversion,[],[f772]) ).
cnf(s108,plain,
( spl0_4
| spl0_20
| spl0_26 ),
inference(sat_conversion,[],[f773]) ).
cnf(s109,plain,
( spl0_17
| spl0_24
| ~ spl0_30 ),
inference(sat_conversion,[],[f774]) ).
cnf(s110,plain,
( spl0_17
| spl0_20
| ~ spl0_30 ),
inference(sat_conversion,[],[f775]) ).
cnf(s116,plain,
( ~ spl0_24
| spl0_32
| spl0_35 ),
inference(sat_conversion,[],[f817]) ).
cnf(s119,plain,
( ~ spl0_23
| ~ spl0_27
| ~ spl0_32 ),
inference(sat_conversion,[],[f825]) ).
cnf(s123,plain,
( spl0_22
| ~ spl0_24
| spl0_32 ),
inference(sat_conversion,[],[f829]) ).
cnf(s126,plain,
( spl0_3
| spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f832]) ).
cnf(s127,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_14 ),
inference(sat_conversion,[],[f833]) ).
cnf(s128,plain,
( spl0_9
| spl0_21 ),
inference(sat_conversion,[],[f834]) ).
cnf(s132,plain,
( ~ spl0_11
| ~ spl0_23
| ~ spl0_27 ),
inference(sat_conversion,[],[f836]) ).
cnf(s135,plain,
( spl0_3
| spl0_7
| spl0_9 ),
inference(sat_conversion,[],[f842]) ).
cnf(s142,plain,
( ~ spl0_5
| spl0_10
| spl0_23 ),
inference(sat_conversion,[],[f873]) ).
cnf(s143,plain,
( spl0_18
| ~ spl0_35 ),
inference(sat_conversion,[],[f897]) ).
cnf(s159,plain,
( ~ spl0_26
| ~ spl0_31
| ~ spl0_43 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s166,plain,
( ~ spl0_29
| spl0_35
| spl0_41 ),
inference(sat_conversion,[],[f1060]) ).
cnf(s170,plain,
( ~ spl0_27
| ~ spl0_32
| ~ spl0_41 ),
inference(sat_conversion,[],[f1080]) ).
cnf(s172,plain,
( spl0_28
| spl0_29
| spl0_31 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s177,plain,
( ~ spl0_26
| spl0_29
| ~ spl0_31
| spl0_33 ),
inference(sat_conversion,[],[f1134]) ).
cnf(s186,plain,
( ~ spl0_19
| ~ spl0_28
| ~ spl0_33 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s188,plain,
( spl0_28
| spl0_29
| spl0_43 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s191,plain,
( spl0_8
| spl0_13 ),
inference(sat_conversion,[],[f1178]) ).
cnf(s197,plain,
( ~ spl0_6
| ~ spl0_9
| ~ spl0_13 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s198,plain,
( spl0_1
| spl0_7
| ~ spl0_21 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s206,plain,
( ~ spl0_14
| ~ spl0_17
| ~ spl0_26 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s207,plain,
( spl0_7
| spl0_14
| ~ spl0_25 ),
inference(sat_conversion,[],[f1198]) ).
cnf(s212,plain,
( ~ spl0_17
| ~ spl0_26
| ~ spl0_31 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s213,plain,
( spl0_15
| ~ spl0_17
| ~ spl0_23
| ~ spl0_26
| ~ spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s219,plain,
( spl0_16
| spl0_29
| spl0_31 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s220,plain,
( spl0_16
| spl0_24
| spl0_31 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s225,plain,
( spl0_1
| spl0_5
| ~ spl0_21 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s226,plain,
( spl0_5
| spl0_17
| ~ spl0_30 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s239,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_9 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s241,plain,
( spl0_28
| spl0_29
| spl0_31 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s243,plain,
( spl0_24
| spl0_31
| spl0_48 ),
inference(sat_conversion,[],[f1299]) ).
cnf(s251,plain,
( spl0_19
| spl0_29
| spl0_31 ),
inference(sat_conversion,[],[f1329]) ).
cnf(s253,plain,
( spl0_19
| spl0_29
| spl0_43 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s257,plain,
( ~ spl0_16
| ~ spl0_19
| ~ spl0_28 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s259,plain,
( ~ spl0_2
| ~ spl0_15
| ~ spl0_18 ),
inference(sat_conversion,[],[f1339]) ).
cnf(s261,plain,
( spl0_19
| spl0_49 ),
inference(sat_conversion,[],[f1350]) ).
cnf(s262,plain,
( ~ spl0_5
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f1359]) ).
cnf(s263,plain,
( spl0_4
| spl0_25 ),
inference(sat_conversion,[],[f1374]) ).
cnf(s264,plain,
( ~ spl0_6
| spl0_48 ),
inference(sat_conversion,[],[f1383]) ).
cnf(s281,plain,
( spl0_24
| spl0_26
| ~ spl0_48 ),
inference(sat_conversion,[],[f1490]) ).
cnf(s282,plain,
( spl0_24
| spl0_31
| ~ spl0_49 ),
inference(sat_conversion,[],[f1491]) ).
cnf(s283,plain,
( ~ spl0_7
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s284,plain,
( spl0_5
| spl0_14
| ~ spl0_25 ),
inference(sat_conversion,[],[f1496]) ).
cnf(s285,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s286,plain,
( ~ spl0_1
| ~ spl0_14
| ~ spl0_17 ),
inference(sat_conversion,[],[f1499]) ).
cnf(s288,plain,
( spl0_2
| ~ spl0_11
| ~ spl0_14
| ~ spl0_17
| spl0_19
| ~ spl0_23 ),
inference(sat_conversion,[],[f1502]) ).
cnf(s289,plain,
( spl0_5
| spl0_1 ),
inference(rat,[],[s197,s34,s128,s225,s20]) ).
cnf(s290,plain,
( spl0_20
| spl0_4 ),
inference(rat,[],[s206,s77,s108,s110,s263,s64]) ).
cnf(s292,plain,
( ~ spl0_17
| ~ spl0_14
| ~ spl0_11
| ~ spl0_23
| spl0_2 ),
inference(rat,[],[s60,s80,s288,s206,s290,s69,s132,s13]) ).
cnf(s293,plain,
( spl0_17
| spl0_20 ),
inference(rat,[],[s285,s62,s88,s110,s290]) ).
cnf(s294,plain,
( ~ spl0_11
| ~ spl0_23
| spl0_2 ),
inference(rat,[],[s239,s58,s63,s77,s292,s293,s290,s69,s132,s13]) ).
cnf(s295,plain,
( spl0_7
| spl0_1 ),
inference(rat,[],[s197,s34,s128,s4,s198]) ).
cnf(s296,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s294,s283,s142,s13,s289,s295]) ).
cnf(s297,plain,
( ~ spl0_6
| spl0_20 ),
inference(rat,[],[s77,s206,s58,s80,s239,s285,s290,s293]) ).
cnf(s298,plain,
spl0_20,
inference(rat,[],[s60,s80,s83,s206,s77,s63,s297,s293,s290]) ).
cnf(s300,plain,
( spl0_27
| ~ spl0_2 ),
inference(rat,[],[s259,s37,s71,s66,s298]) ).
cnf(s301,plain,
( spl0_26
| spl0_16
| ~ spl0_48
| spl0_35
| ~ spl0_27 ),
inference(rat,[],[s170,s116,s166,s281,s78]) ).
cnf(s302,plain,
( spl0_29
| ~ spl0_31
| ~ spl0_26 ),
inference(rat,[],[s186,s253,s188,s159,s177]) ).
cnf(s303,plain,
( spl0_29
| ~ spl0_26
| spl0_16 ),
inference(rat,[],[s302,s219]) ).
cnf(s304,plain,
( spl0_16
| ~ spl0_48
| spl0_35
| ~ spl0_27 ),
inference(rat,[],[s212,s109,s220,s116,s170,s166,s303,s301,s89]) ).
cnf(s305,plain,
( spl0_26
| spl0_4
| spl0_35
| ~ spl0_27 ),
inference(rat,[],[s170,s166,s116,s106,s107]) ).
cnf(s306,plain,
( ~ spl0_17
| ~ spl0_6
| spl0_18
| ~ spl0_27 ),
inference(rat,[],[s170,s116,s166,s282,s251,s261,s257,s104,s212,s305,s285,s304,s264,s143]) ).
cnf(s307,plain,
( ~ spl0_6
| spl0_18
| ~ spl0_27 ),
inference(rat,[],[s257,s241,s251,s302,s166,s170,s116,s109,s306,s305,s64,s285,s304,s264,s143]) ).
cnf(s308,plain,
( spl0_26
| spl0_16
| spl0_35
| ~ spl0_27 ),
inference(rat,[],[s170,s116,s166,s79,s78]) ).
cnf(s309,plain,
( spl0_16
| spl0_18
| ~ spl0_27 ),
inference(rat,[],[s212,s109,s243,s116,s170,s166,s303,s308,s304,s143,s62,s307]) ).
cnf(s310,plain,
( spl0_26
| spl0_19
| spl0_35
| ~ spl0_27 ),
inference(rat,[],[s170,s166,s116,s94,s96]) ).
cnf(s311,plain,
( spl0_24
| ~ spl0_26
| ~ spl0_49
| ~ spl0_30 ),
inference(rat,[],[s212,s282,s109]) ).
cnf(s312,plain,
( spl0_19
| spl0_18
| ~ spl0_27 ),
inference(rat,[],[s251,s302,s166,s170,s116,s311,s310,s261,s143,s62,s307]) ).
cnf(s313,plain,
( spl0_18
| ~ spl0_27 ),
inference(rat,[],[s172,s302,s166,s170,s116,s109,s104,s305,s257,s60,s312,s309,s62,s307,s143]) ).
cnf(s314,plain,
( spl0_16
| spl0_24 ),
inference(rat,[],[s212,s87,s79,s220]) ).
cnf(s315,plain,
( spl0_26
| spl0_24 ),
inference(rat,[],[s60,s96,s107,s314]) ).
cnf(s316,plain,
( ~ spl0_4
| spl0_24 ),
inference(rat,[],[s311,s261,s62,s60,s285,s314,s315]) ).
cnf(s317,plain,
spl0_1,
inference(rat,[],[s257,s261,s213,s311,s109,s64,s316,s315,s314,s123,s119,s262,s37,s259,s313,s300,s296,s289]) ).
cnf(s318,plain,
( spl0_25
| ~ spl0_4 ),
inference(rat,[],[s239,s58,s63]) ).
cnf(s319,plain,
( spl0_5
| ~ spl0_25
| ~ spl0_30 ),
inference(rat,[],[s286,s284,s226,s317]) ).
cnf(s320,plain,
( ~ spl0_5
| spl0_23
| ~ spl0_18 ),
inference(rat,[],[s259,s13,s37,s142,s262]) ).
cnf(s321,plain,
spl0_25,
inference(rat,[],[s318,s263]) ).
cnf(s322,plain,
( spl0_3
| spl0_7 ),
inference(rat,[],[s8,s9,s191,s126,s135]) ).
cnf(s323,plain,
spl0_7,
inference(rat,[],[s322,s127,s207,s317,s321]) ).
cnf(s324,plain,
( spl0_16
| ~ spl0_27 ),
inference(rat,[],[s259,s37,s13,s123,s283,s119,s132,s320,s319,s314,s89,s313,s323,s321]) ).
cnf(s325,plain,
( spl0_30
| ~ spl0_16 ),
inference(rat,[],[s285,s62,s64]) ).
cnf(s326,plain,
~ spl0_27,
inference(rat,[],[s257,s261,s213,s311,s109,s315,s123,s37,s259,s13,s283,s119,s132,s320,s319,s325,s324,s313,s323,s321]) ).
cnf(s327,plain,
spl0_10,
inference(rat,[],[s69,s298,s326]) ).
cnf(s330,plain,
~ spl0_2,
inference(rat,[],[s300,s326]) ).
cnf(s331,plain,
$false,
inference(rat,[],[s13,s327,s330]) ).
fof(f1503,plain,
$false,
inference(avatar_sat_refutation,[],[s331]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO685-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.18 % Computer : n009.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 18:05:15 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.22 Running first-order theorem proving
% 0.06/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.65/0.71 % (3303506)Input is clausal, will run a generic CNF schedule.
% 0.65/0.71 % (3303516)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=198873908:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.65/0.71 % (3303516)First to succeed.
% 0.65/0.71 % (3303516)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3303506"
% 0.65/0.71 % (3303514)lrs+10_1_sil=8000:sp=occurrence:random_seed=137733479:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.65/0.71 % (3303512)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1500884880:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.65/0.71 % (3303511)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3906536028:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.65/0.71 % (3303513)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1931373215:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.65/0.71 % (3303515)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3963166285:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.65/0.71 % (3303514)Refutation not found, incomplete strategy
% 0.65/0.71 % (3303514)------------------------------
% 0.65/0.71 % (3303514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.65/0.71 % (3303515)Refutation not found, incomplete strategy
% 0.65/0.71 % (3303515)------------------------------
% 0.65/0.71 % (3303515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.65/0.71 % (3303514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.71 % (3303514)CaDiCaL version: 2.1.3
% 0.65/0.71 % (3303514)Termination reason: Refutation not found, incomplete strategy
% 0.65/0.71 % (3303514)Time elapsed: 0.001 s
% 0.65/0.71 % (3303515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.65/0.71 % (3303515)CaDiCaL version: 2.1.3
% 0.65/0.71 % (3303514)Peak memory usage: 86 MB
% 0.65/0.71 % (3303515)Termination reason: Refutation not found, incomplete strategy
% 0.65/0.71 % (3303515)Time elapsed: 0.001 s
% 0.65/0.71 % (3303515)Peak memory usage: 86 MB
% 0.65/0.71 % (3303517)dis-21_1_sil=8000:lcm=predicate:random_seed=3489779124:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 0.65/0.71 % (3303517)Also succeeded, but the first one will report.
% 0.65/0.71 % (3303516)Refutation found. Thanks to Tanya!
% 0.65/0.71 % SZS status Unsatisfiable for theBenchmark
% 0.65/0.71 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.90 % (3303516)------------------------------
% 0.19/0.90 % (3303516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/0.90 % (3303516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.90 % (3303516)CaDiCaL version: 2.1.3
% 0.19/0.90 % (3303516)Termination reason: Refutation
% 0.19/0.90 % (3303516)Time elapsed: 0.023 s
% 0.19/0.90 % (3303516)Peak memory usage: 90 MB
% 0.19/0.90 % (3303516)Instructions burned: 71 (million)
% 0.19/0.90 % (3303516)------------------------------
% 0.19/0.90 % (3303516)------------------------------
% 0.19/0.90 % (3303506)Success in time 0.295 s
% 0.19/0.90 % Vampire exiting
%------------------------------------------------------------------------------