%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO681-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:32:23 PM UTC 2026
% Result : Unsatisfiable 0.24s 0.26s
% Output : Refutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 54
% Syntax : Number of formulae : 864 ( 14 unt; 24 def)
% Number of atoms : 3514 ( 0 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 3341 ( 691 ~;2626 |; 0 &)
% ( 24 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 10 ( 3 avg)
% Number of predicates : 28 ( 27 usr; 25 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 219 ( 0 sgn 219 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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/sandbox2/benchmark/theBenchmark.p',clause_658) ).
fof(f3,axiom,
! [X0] : 'LE'(f(X0),s(s(s(s('0'))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_556) ).
fof(f7,axiom,
! [X0] :
( ~ 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s('0')),f(X0))
| 'LE'(f(X0),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_300) ).
fof(f8,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/sandbox2/benchmark/theBenchmark.p',clause_415) ).
fof(f9,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_614) ).
fof(f10,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/sandbox2/benchmark/theBenchmark.p',clause_607) ).
fof(f14,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_486) ).
fof(f15,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_687) ).
fof(f16,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_528) ).
fof(f17,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_359) ).
fof(f18,axiom,
! [X0] :
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_497) ).
fof(f19,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_463) ).
fof(f22,axiom,
! [X0] :
( ~ 'LE'(f(suc(X0)),s(s('0')))
| 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X0),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_95) ).
fof(f24,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/sandbox2/benchmark/theBenchmark.p',clause_125) ).
fof(f25,axiom,
! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s('0'))
| 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_61) ).
fof(f26,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/sandbox2/benchmark/theBenchmark.p',clause_713) ).
fof(f27,axiom,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_560) ).
fof(f28,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/sandbox2/benchmark/theBenchmark.p',clause_103) ).
fof(f29,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/sandbox2/benchmark/theBenchmark.p',clause_563) ).
fof(f32,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/sandbox2/benchmark/theBenchmark.p',clause_283) ).
fof(f34,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/sandbox2/benchmark/theBenchmark.p',clause_457) ).
fof(f36,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))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_663) ).
fof(f38,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_131) ).
fof(f40,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_41) ).
fof(f42,axiom,
! [X0] :
( ~ 'LE'(f(X0),s(s('0')))
| 'E'(s('0'),f(X0))
| 'LE'(f(X0),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_44) ).
fof(f43,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/sandbox2/benchmark/theBenchmark.p',clause_550) ).
fof(f46,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/sandbox2/benchmark/theBenchmark.p',clause_383) ).
fof(f49,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_363) ).
fof(f51,axiom,
! [X0] :
( ~ 'LE'(f(suc(X0)),s('0'))
| 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_595) ).
fof(f52,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/sandbox2/benchmark/theBenchmark.p',clause_508) ).
fof(f55,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,[],[f24,f29]) ).
fof(f56,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,[],[f8,f46]) ).
fof(f57,plain,
! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X0)) ),
inference(forward_subsumption_resolution,[],[f1,f3]) ).
fof(f58,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0))
| 'E'(s(s(s('0'))),f(X0)) ),
inference(resolution,[],[f7,f57]) ).
fof(f59,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(X0))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(X0)) ),
inference(resolution,[],[f58,f42]) ).
fof(f60,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[],[f58,f22]) ).
fof(f61,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f52,f58]) ).
fof(f62,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(resolution,[],[f34,f57]) ).
fof(f63,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[],[f62,f42]) ).
fof(f64,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f62,f22]) ).
fof(f65,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f62,f52]) ).
fof(f66,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f10,f57]) ).
fof(f67,plain,
! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(resolution,[],[f43,f3]) ).
fof(f68,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(resolution,[],[f67,f7]) ).
fof(f69,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f67,f34]) ).
fof(f70,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f67,f10]) ).
fof(f71,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(X0)) ),
inference(resolution,[],[f68,f42]) ).
fof(f72,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[],[f68,f22]) ).
fof(f73,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f68,f52]) ).
fof(f74,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[],[f69,f42]) ).
fof(f75,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f69,f22]) ).
fof(f76,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f69,f52]) ).
fof(f77,plain,
! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f28,f3]) ).
fof(f78,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f77,f7]) ).
fof(f79,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f77,f34]) ).
fof(f80,plain,
! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f77,f10]) ).
fof(f81,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(X0)) ),
inference(resolution,[],[f78,f42]) ).
fof(f82,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[],[f78,f22]) ).
fof(f83,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f78,f52]) ).
fof(f84,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f66,f42]) ).
fof(f85,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f66,f22]) ).
fof(f86,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f66,f52]) ).
fof(f87,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(X0))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(X0)) ),
inference(resolution,[],[f59,f18]) ).
fof(f88,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(resolution,[],[f59,f51]) ).
fof(f89,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f59,f25]) ).
fof(f98,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(X0))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(resolution,[],[f9,f26]) ).
fof(f113,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X1))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
inference(duplicate_literal_removal,[],[f98]) ).
fof(f122,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(X0))) ),
inference(resolution,[],[f79,f42]) ).
fof(f123,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f79,f22]) ).
fof(f124,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f79,f52]) ).
fof(f135,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(resolution,[],[f15,f29]) ).
fof(f146,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X1))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
inference(duplicate_literal_removal,[],[f135]) ).
fof(f157,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f70,f42]) ).
fof(f158,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f70,f22]) ).
fof(f159,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f70,f52]) ).
fof(f173,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(X0))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0)) ),
inference(resolution,[],[f19,f46]) ).
fof(f178,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
inference(duplicate_literal_removal,[],[f173]) ).
fof(f192,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(X0))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(resolution,[],[f71,f18]) ).
fof(f193,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f71,f51]) ).
fof(f194,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f71,f25]) ).
fof(f206,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(resolution,[],[f14,f32]) ).
fof(f215,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
inference(duplicate_literal_removal,[],[f206]) ).
fof(f227,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(resolution,[],[f63,f18]) ).
fof(f228,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f63,f51]) ).
fof(f229,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f63,f25]) ).
fof(f239,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(resolution,[],[f49,f27]) ).
fof(f252,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X1)) ),
inference(duplicate_literal_removal,[],[f239]) ).
fof(f262,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f80,f42]) ).
fof(f263,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f80,f22]) ).
fof(f264,plain,
! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0))))))))
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f80,f52]) ).
fof(f279,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(resolution,[],[f40,f55]) ).
fof(f282,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(suc(X1)))) ),
inference(duplicate_literal_removal,[],[f279]) ).
fof(f297,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(X0))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f81,f18]) ).
fof(f298,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f81,f51]) ).
fof(f299,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f81,f25]) ).
fof(f315,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f16,f56]) ).
fof(f316,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(duplicate_literal_removal,[],[f315]) ).
fof(f332,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(resolution,[],[f60,f18]) ).
fof(f333,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f60,f51]) ).
fof(f334,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f60,f25]) ).
fof(f347,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f38,f36]) ).
fof(f354,plain,
! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X1))) ),
inference(duplicate_literal_removal,[],[f347]) ).
fof(f367,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f74,f18]) ).
fof(f368,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f74,f51]) ).
fof(f369,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f74,f25]) ).
fof(f370,plain,
! [X0] :
( ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(X0))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(resolution,[],[f113,f26]) ).
fof(f385,plain,
! [X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0))) ),
inference(duplicate_literal_removal,[],[f370]) ).
fof(f388,plain,
! [X0] :
( ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X0))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(resolution,[],[f146,f29]) ).
fof(f399,plain,
! [X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0))) ),
inference(duplicate_literal_removal,[],[f388]) ).
fof(f409,plain,
! [X0] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X0))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f178,f56]) ).
fof(f410,plain,
! [X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0)) ),
inference(duplicate_literal_removal,[],[f409]) ).
fof(f453,plain,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(resolution,[],[f215,f32]) ).
fof(f462,plain,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(duplicate_literal_removal,[],[f453]) ).
fof(f467,plain,
! [X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X0)))) ),
inference(resolution,[],[f252,f27]) ).
fof(f480,plain,
! [X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X0)) ),
inference(duplicate_literal_removal,[],[f467]) ).
fof(f485,plain,
! [X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) ),
inference(forward_subsumption_resolution,[],[f480,f385]) ).
fof(f502,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(z))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(z)) ),
inference(resolution,[],[f87,f17]) ).
fof(f504,definition,
( spl0_1
<=> 'E'(s(s(s('0'))),f(z)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f506,plain,
( 'E'(s(s(s('0'))),f(z))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f504]) ).
fof(f508,definition,
( spl0_2
<=> 'E'('0',f(z)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f509,plain,
( ~ 'E'('0',f(z))
| spl0_2 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f510,plain,
( 'E'('0',f(z))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f512,definition,
( spl0_3
<=> 'E'(s(s('0')),f(z)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f513,plain,
( ~ 'E'(s(s('0')),f(z))
| spl0_3 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( 'E'(s(s('0')),f(z))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f516,definition,
( spl0_4
<=> 'E'(s('0'),f(z)) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f517,plain,
( ~ 'E'(s('0'),f(z))
| spl0_4 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f519,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f502,f516,f512,f508,f504]) ).
fof(f552,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f84,f18]) ).
fof(f553,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f84,f51]) ).
fof(f554,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f84,f25]) ).
fof(f587,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f72,f18]) ).
fof(f588,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f72,f51]) ).
fof(f589,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f72,f25]) ).
fof(f596,plain,
! [X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(suc(X0)))) ),
inference(resolution,[],[f282,f55]) ).
fof(f599,plain,
! [X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X0)) ),
inference(duplicate_literal_removal,[],[f596]) ).
fof(f607,plain,
! [X0] :
( ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[],[f599,f399]) ).
fof(f625,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f122,f18]) ).
fof(f626,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f122,f51]) ).
fof(f627,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f122,f25]) ).
fof(f644,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(z))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z))) ),
inference(resolution,[],[f192,f17]) ).
fof(f652,plain,
! [X0] :
( ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X0)))) ),
inference(resolution,[],[f316,f56]) ).
fof(f653,plain,
! [X0] :
( ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0))) ),
inference(duplicate_literal_removal,[],[f652]) ).
fof(f661,plain,
! [X0] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0)) ),
inference(forward_subsumption_resolution,[],[f653,f410]) ).
fof(f679,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f64,f18]) ).
fof(f680,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f64,f51]) ).
fof(f681,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f64,f25]) ).
fof(f714,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(X0)))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f82,f18]) ).
fof(f715,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f82,f51]) ).
fof(f716,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f82,f25]) ).
fof(f733,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f157,f18]) ).
fof(f734,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f157,f51]) ).
fof(f735,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f157,f25]) ).
fof(f752,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z))) ),
inference(resolution,[],[f227,f17]) ).
fof(f757,plain,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0)))) ),
inference(resolution,[],[f354,f36]) ).
fof(f764,plain,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(duplicate_literal_removal,[],[f757]) ).
fof(f771,plain,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f764,f462]) ).
fof(f788,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(z))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f297,f17]) ).
fof(f805,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s('0'),f(suc(suc(X0)))) ),
inference(resolution,[],[f61,f18]) ).
fof(f806,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s('0'),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f61,f51]) ).
fof(f807,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s('0'),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f61,f25]) ).
fof(f824,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f75,f18]) ).
fof(f825,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f75,f51]) ).
fof(f826,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f75,f25]) ).
fof(f843,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(X0))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f262,f18]) ).
fof(f844,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f262,f51]) ).
fof(f845,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f262,f25]) ).
fof(f862,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z))) ),
inference(resolution,[],[f332,f17]) ).
fof(f879,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f367,f17]) ).
fof(f880,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f85,f18]) ).
fof(f881,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f85,f51]) ).
fof(f882,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f85,f25]) ).
fof(f883,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f73,f18]) ).
fof(f884,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f73,f51]) ).
fof(f885,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f73,f25]) ).
fof(f886,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(X0))))) ),
inference(resolution,[],[f65,f18]) ).
fof(f887,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f65,f51]) ).
fof(f888,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f65,f25]) ).
fof(f889,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(z))) ),
inference(resolution,[],[f88,f17]) ).
fof(f891,definition,
( spl0_5
<=> 'E'(s(s(s('0'))),f(suc(z))) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f892,plain,
( ~ 'E'(s(s(s('0'))),f(suc(z)))
| spl0_5 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f893,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f895,definition,
( spl0_6
<=> 'E'('0',f(suc(z))) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f896,plain,
( ~ 'E'('0',f(suc(z)))
| spl0_6 ),
inference(avatar_component_clause,[],[f895]) ).
fof(f897,plain,
( 'E'('0',f(suc(z)))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f895]) ).
fof(f899,definition,
( spl0_7
<=> 'E'(s(s('0')),f(suc(z))) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f900,plain,
( ~ 'E'(s(s('0')),f(suc(z)))
| spl0_7 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f901,plain,
( 'E'(s(s('0')),f(suc(z)))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f903,definition,
( spl0_8
<=> 'E'(s('0'),f(suc(z))) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f904,plain,
( ~ 'E'(s('0'),f(suc(z)))
| spl0_8 ),
inference(avatar_component_clause,[],[f903]) ).
fof(f906,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f889,f903,f899,f895,f891]) ).
fof(f915,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f86,f18]) ).
fof(f916,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f86,f51]) ).
fof(f917,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(X0))))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f86,f25]) ).
fof(f918,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f123,f18]) ).
fof(f919,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f123,f51]) ).
fof(f920,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f123,f25]) ).
fof(f921,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f552,f17]) ).
fof(f922,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f587,f17]) ).
fof(f923,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f625,f17]) ).
fof(f924,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(X0))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f83,f18]) ).
fof(f925,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f83,f51]) ).
fof(f926,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f83,f25]) ).
fof(f927,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f158,f18]) ).
fof(f928,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f158,f51]) ).
fof(f929,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f158,f25]) ).
fof(f930,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f679,f17]) ).
fof(f931,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[],[f76,f18]) ).
fof(f932,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f76,f51]) ).
fof(f933,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f76,f25]) ).
fof(f934,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f193,f17]) ).
fof(f936,definition,
( spl0_10
<=> 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f937,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_10 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f938,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f939,plain,
( spl0_10
| spl0_6
| spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f934,f903,f899,f895,f936]) ).
fof(f940,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f228,f17]) ).
fof(f941,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(X0)))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f263,f18]) ).
fof(f942,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f263,f51]) ).
fof(f943,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(X0))))))))) ),
inference(resolution,[],[f263,f25]) ).
fof(f944,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f714,f17]) ).
fof(f945,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s('0'),f(suc(suc(z)))) ),
inference(resolution,[],[f805,f17]) ).
fof(f946,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f733,f17]) ).
fof(f947,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(X0)))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f124,f18]) ).
fof(f948,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f124,f51]) ).
fof(f949,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(X0))))))))) ),
inference(resolution,[],[f124,f25]) ).
fof(f950,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f298,f17]) ).
fof(f951,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f333,f17]) ).
fof(f952,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f824,f17]) ).
fof(f953,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f880,f17]) ).
fof(f954,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f843,f17]) ).
fof(f955,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(z)))) ),
inference(resolution,[],[f89,f17]) ).
fof(f957,definition,
( spl0_11
<=> 'E'('0',f(suc(suc(z)))) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f958,plain,
( ~ 'E'('0',f(suc(suc(z))))
| spl0_11 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f959,plain,
( 'E'('0',f(suc(suc(z))))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f961,definition,
( spl0_12
<=> 'E'(s(s('0')),f(suc(suc(z)))) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f962,plain,
( ~ 'E'(s(s('0')),f(suc(suc(z))))
| spl0_12 ),
inference(avatar_component_clause,[],[f961]) ).
fof(f963,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f961]) ).
fof(f965,definition,
( spl0_13
<=> 'E'(s('0'),f(suc(suc(z)))) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f966,plain,
( ~ 'E'(s('0'),f(suc(suc(z))))
| spl0_13 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f967,plain,
( 'E'(s('0'),f(suc(suc(z))))
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f968,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_13 ),
inference(avatar_split_clause,[],[f955,f965,f961,f957,f936]) ).
fof(f975,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[],[f159,f18]) ).
fof(f976,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f159,f51]) ).
fof(f977,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(X0))))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(X0))))))))) ),
inference(resolution,[],[f159,f25]) ).
fof(f978,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f553,f17]) ).
fof(f979,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f368,f17]) ).
fof(f980,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f886,f17]) ).
fof(f981,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f883,f17]) ).
fof(f982,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(X0))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(X0))))))
| 'E'('0',f(X0))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[],[f264,f18]) ).
fof(f983,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(X0)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(X0)))))))
| 'E'('0',f(suc(X0)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(X0))))))))) ),
inference(resolution,[],[f264,f51]) ).
fof(f984,plain,
! [X0] :
( 'LE'(f(X0),'0')
| 'E'(s('0'),f(suc(suc(suc(suc(X0))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(X0))))))))
| 'E'('0',f(suc(suc(X0))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(X0)))))))))) ),
inference(resolution,[],[f264,f25]) ).
fof(f985,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f918,f17]) ).
fof(f986,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f680,f17]) ).
fof(f987,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f588,f17]) ).
fof(f988,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f229,f17]) ).
fof(f990,definition,
( spl0_14
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f991,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_14 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f992,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f994,definition,
( spl0_15
<=> 'E'(s(s('0')),f(suc(suc(suc(z))))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f995,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| spl0_15 ),
inference(avatar_component_clause,[],[f994]) ).
fof(f996,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f994]) ).
fof(f997,plain,
( spl0_14
| spl0_11
| spl0_15
| spl0_13 ),
inference(avatar_split_clause,[],[f988,f965,f994,f957,f990]) ).
fof(f998,plain,
( ~ 'E'('0',f(suc(z)))
| ~ 'E'('0',f(z))
| ~ spl0_11 ),
inference(resolution,[],[f959,f485]) ).
fof(f999,plain,
( ~ 'E'('0',f(z))
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f998,f897]) ).
fof(f1000,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f999,f510]) ).
fof(f1001,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f1000]) ).
fof(f1002,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f923,f509]) ).
fof(f1003,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f944,f509]) ).
fof(f1004,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f946,f509]) ).
fof(f1005,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f952,f509]) ).
fof(f1006,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f953,f509]) ).
fof(f1007,plain,
( 'E'(s('0'),f(z))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f954,f509]) ).
fof(f1008,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f980,f509]) ).
fof(f1009,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f981,f509]) ).
fof(f1010,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f985,f509]) ).
fof(f1011,plain,
( spl0_14
| spl0_7
| spl0_4
| spl0_2 ),
inference(avatar_split_clause,[],[f1002,f508,f516,f899,f990]) ).
fof(f1012,plain,
( spl0_14
| spl0_7
| spl0_8
| spl0_2 ),
inference(avatar_split_clause,[],[f1003,f508,f903,f899,f990]) ).
fof(f1013,plain,
( spl0_14
| spl0_12
| spl0_4
| spl0_2 ),
inference(avatar_split_clause,[],[f1004,f508,f516,f961,f990]) ).
fof(f1014,plain,
( spl0_14
| spl0_12
| spl0_8
| spl0_2 ),
inference(avatar_split_clause,[],[f1005,f508,f903,f961,f990]) ).
fof(f1015,plain,
( spl0_14
| spl0_15
| spl0_8
| spl0_2 ),
inference(avatar_split_clause,[],[f1006,f508,f903,f994,f990]) ).
fof(f1017,definition,
( spl0_16
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f1018,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_16 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1019,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1020,plain,
( spl0_16
| spl0_12
| spl0_4
| spl0_2 ),
inference(avatar_split_clause,[],[f1007,f508,f516,f961,f1017]) ).
fof(f1021,plain,
( spl0_14
| spl0_15
| spl0_13
| spl0_2 ),
inference(avatar_split_clause,[],[f1008,f508,f965,f994,f990]) ).
fof(f1022,plain,
( spl0_14
| spl0_12
| spl0_13
| spl0_2 ),
inference(avatar_split_clause,[],[f1009,f508,f965,f961,f990]) ).
fof(f1023,plain,
( spl0_16
| spl0_12
| spl0_8
| spl0_2 ),
inference(avatar_split_clause,[],[f1010,f508,f903,f961,f1017]) ).
fof(f1024,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s('0'),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f806,f17]) ).
fof(f1025,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f915,f17]) ).
fof(f1026,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f334,f17]) ).
fof(f1027,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f1026,f958]) ).
fof(f1029,definition,
( spl0_17
<=> 'E'(s('0'),f(suc(suc(suc(z))))) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f1030,plain,
( ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| spl0_17 ),
inference(avatar_component_clause,[],[f1029]) ).
fof(f1031,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f1029]) ).
fof(f1032,plain,
( spl0_14
| spl0_15
| spl0_17
| spl0_11 ),
inference(avatar_split_clause,[],[f1027,f957,f1029,f994,f990]) ).
fof(f1033,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f881,f17]) ).
fof(f1036,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ 'E'(s('0'),f(z))
| ~ spl0_13 ),
inference(resolution,[],[f967,f607]) ).
fof(f1038,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1036,f965,f903,f516]) ).
fof(f1039,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f554,f17]) ).
fof(f1040,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f887,f17]) ).
fof(f1042,plain,
( ~ 'E'(s('0'),f(suc(suc(z))))
| ~ 'E'(s('0'),f(suc(z)))
| ~ spl0_17 ),
inference(resolution,[],[f1031,f607]) ).
fof(f1043,plain,
( ~ 'E'(s('0'),f(suc(z)))
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1042,f967]) ).
fof(f1044,plain,
( ~ spl0_8
| ~ spl0_13
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1043,f1029,f965,f903]) ).
fof(f1045,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f681,f17]) ).
fof(f1046,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f807,f17]) ).
fof(f1047,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f1046,f958]) ).
fof(f1049,definition,
( spl0_18
<=> 'E'(s('0'),f(suc(suc(suc(suc(z)))))) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f1050,plain,
( ~ 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| spl0_18 ),
inference(avatar_component_clause,[],[f1049]) ).
fof(f1051,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f1049]) ).
fof(f1053,definition,
( spl0_19
<=> 'E'(s(s('0')),f(suc(suc(suc(suc(z)))))) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f1054,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| spl0_19 ),
inference(avatar_component_clause,[],[f1053]) ).
fof(f1055,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f1053]) ).
fof(f1056,plain,
( spl0_18
| spl0_16
| spl0_19
| spl0_11 ),
inference(avatar_split_clause,[],[f1047,f957,f1053,f1017,f1049]) ).
fof(f1058,plain,
( ~ 'E'(s('0'),f(suc(suc(suc(z)))))
| ~ 'E'(s('0'),f(suc(suc(z))))
| ~ spl0_18 ),
inference(resolution,[],[f1051,f607]) ).
fof(f1059,plain,
( ~ 'E'(s('0'),f(suc(suc(z))))
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1058,f1031]) ).
fof(f1060,plain,
( $false
| ~ spl0_13
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1059,f967]) ).
fof(f1061,plain,
( ~ spl0_13
| ~ spl0_17
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1060]) ).
fof(f1062,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f916,f17]) ).
fof(f1063,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f882,f17]) ).
fof(f1065,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ spl0_16 ),
inference(resolution,[],[f1019,f771]) ).
fof(f1066,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1065,f938]) ).
fof(f1067,plain,
( ~ spl0_14
| ~ spl0_10
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1066,f1017,f936,f990]) ).
fof(f1068,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f888,f17]) ).
fof(f1069,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1068,f1050]) ).
fof(f1070,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_11
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1069,f958]) ).
fof(f1072,definition,
( spl0_20
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f1073,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_20 ),
inference(avatar_component_clause,[],[f1072]) ).
fof(f1074,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f1072]) ).
fof(f1076,definition,
( spl0_21
<=> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z))))))) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f1077,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| spl0_21 ),
inference(avatar_component_clause,[],[f1076]) ).
fof(f1078,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f1076]) ).
fof(f1079,plain,
( spl0_20
| spl0_21
| spl0_11
| spl0_18 ),
inference(avatar_split_clause,[],[f1070,f1049,f957,f1076,f1072]) ).
fof(f1080,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f917,f17]) ).
fof(f1081,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1080,f1050]) ).
fof(f1082,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_11
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1081,f958]) ).
fof(f1084,definition,
( spl0_22
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f1085,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_22 ),
inference(avatar_component_clause,[],[f1084]) ).
fof(f1086,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f1084]) ).
fof(f1088,definition,
( spl0_23
<=> 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f1090,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1091,plain,
( spl0_22
| spl0_23
| spl0_11
| spl0_18 ),
inference(avatar_split_clause,[],[f1082,f1049,f957,f1088,f1084]) ).
fof(f1094,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ spl0_21 ),
inference(resolution,[],[f1078,f661]) ).
fof(f1095,plain,
( ~ spl0_15
| ~ spl0_19
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f1094,f1076,f1053,f994]) ).
fof(f1097,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_22 ),
inference(resolution,[],[f1086,f771]) ).
fof(f1098,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1097,f1019]) ).
fof(f1099,plain,
( ~ spl0_20
| ~ spl0_16
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1098,f1084,f1017,f1072]) ).
fof(f1100,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f626,f17]) ).
fof(f1101,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f924,f17]) ).
fof(f1102,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f927,f17]) ).
fof(f1103,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z))))) ),
inference(resolution,[],[f194,f17]) ).
fof(f1104,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f715,f17]) ).
fof(f1105,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f734,f17]) ).
fof(f1106,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f931,f17]) ).
fof(f1107,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f941,f17]) ).
fof(f1108,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f299,f17]) ).
fof(f1109,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f825,f17]) ).
fof(f1110,plain,
( 'E'(s('0'),f(suc(z)))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f844,f17]) ).
fof(f1111,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f947,f17]) ).
fof(f1112,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f369,f17]) ).
fof(f1113,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f884,f17]) ).
fof(f1114,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f919,f17]) ).
fof(f1115,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f975,f17]) ).
fof(f1116,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z)))))) ),
inference(resolution,[],[f589,f17]) ).
fof(f1117,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f627,f17]) ).
fof(f1118,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f925,f17]) ).
fof(f1119,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f928,f17]) ).
fof(f1120,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f982,f17]) ).
fof(f1121,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f716,f17]) ).
fof(f1122,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f735,f17]) ).
fof(f1123,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f932,f17]) ).
fof(f1124,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f942,f17]) ).
fof(f1125,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f826,f17]) ).
fof(f1126,plain,
( 'E'(s('0'),f(suc(suc(z))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f845,f17]) ).
fof(f1127,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f948,f17]) ).
fof(f1128,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z))))))) ),
inference(resolution,[],[f885,f17]) ).
fof(f1129,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1128,f1050]) ).
fof(f1130,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_11
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1129,f958]) ).
fof(f1131,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| spl0_11
| spl0_18
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1130,f1073]) ).
fof(f1132,plain,
( spl0_19
| spl0_11
| spl0_18
| spl0_20 ),
inference(avatar_split_clause,[],[f1131,f1072,f1049,f957,f1053]) ).
fof(f1136,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f920,f17]) ).
fof(f1137,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f976,f17]) ).
fof(f1138,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f926,f17]) ).
fof(f1139,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f929,f17]) ).
fof(f1140,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
inference(resolution,[],[f983,f17]) ).
fof(f1141,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z)))))))) ),
inference(resolution,[],[f933,f17]) ).
fof(f1142,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
inference(resolution,[],[f943,f17]) ).
fof(f1143,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
inference(resolution,[],[f949,f17]) ).
fof(f1144,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
inference(resolution,[],[f977,f17]) ).
fof(f1145,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1144,f1050]) ).
fof(f1146,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_11
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1145,f958]) ).
fof(f1148,definition,
( spl0_24
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z))))))))) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f1149,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_24 ),
inference(avatar_component_clause,[],[f1148]) ).
fof(f1150,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f1148]) ).
fof(f1151,plain,
( spl0_24
| spl0_23
| spl0_11
| spl0_18 ),
inference(avatar_split_clause,[],[f1146,f1049,f957,f1088,f1148]) ).
fof(f1152,plain,
( 'E'(s('0'),f(suc(suc(suc(suc(z))))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))) ),
inference(resolution,[],[f984,f17]) ).
fof(f1153,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1152,f1050]) ).
fof(f1154,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(suc(z))))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| spl0_11
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1153,f958]) ).
fof(f1156,definition,
( spl0_25
<=> 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z)))))))))) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f1158,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(suc(z))))))))))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f1156]) ).
fof(f1159,plain,
( spl0_25
| spl0_23
| spl0_11
| spl0_18 ),
inference(avatar_split_clause,[],[f1154,f1049,f957,f1088,f1156]) ).
fof(f1162,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ spl0_23 ),
inference(resolution,[],[f1090,f661]) ).
fof(f1163,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| ~ spl0_21
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1162,f1078]) ).
fof(f1164,plain,
( $false
| ~ spl0_19
| ~ spl0_21
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1163,f1055]) ).
fof(f1165,plain,
( ~ spl0_19
| ~ spl0_21
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1164]) ).
fof(f1169,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ spl0_24 ),
inference(resolution,[],[f1150,f771]) ).
fof(f1170,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ spl0_20
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1169,f1074]) ).
fof(f1177,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ spl0_25 ),
inference(resolution,[],[f1158,f771]) ).
fof(f1178,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| ~ spl0_22
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1177,f1086]) ).
fof(f1181,plain,
( ~ spl0_22
| ~ spl0_20
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f1170,f1148,f1072,f1084]) ).
fof(f1182,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1141,f1050]) ).
fof(f1183,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_18
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1182,f1077]) ).
fof(f1184,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_11
| spl0_18
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1183,f958]) ).
fof(f1185,plain,
( $false
| spl0_11
| spl0_18
| spl0_21
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1184,f1085]) ).
fof(f1186,plain,
( spl0_11
| spl0_18
| spl0_21
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f1185]) ).
fof(f1187,plain,
( ~ spl0_24
| ~ spl0_22
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1178,f1156,f1084,f1148]) ).
fof(f1188,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1143,f1050]) ).
fof(f1189,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_18
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1188,f1077]) ).
fof(f1190,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_11
| spl0_18
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1189,f958]) ).
fof(f1191,plain,
( $false
| spl0_11
| spl0_18
| spl0_21
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1190,f1149]) ).
fof(f1192,plain,
( spl0_11
| spl0_18
| spl0_21
| spl0_24 ),
inference(avatar_contradiction_clause,[],[f1191]) ).
fof(f1193,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f1138,f1050]) ).
fof(f1194,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_18
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1193,f1054]) ).
fof(f1195,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_11
| spl0_18
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1194,f958]) ).
fof(f1196,plain,
( $false
| spl0_11
| spl0_18
| spl0_19
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1195,f1085]) ).
fof(f1197,plain,
( spl0_11
| spl0_18
| spl0_19
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f1196]) ).
fof(f1198,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1045,f1030]) ).
fof(f1199,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1116,f1030]) ).
fof(f1200,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1136,f1030]) ).
fof(f1201,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1198,f1054]) ).
fof(f1202,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1199,f995]) ).
fof(f1203,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1200,f1054]) ).
fof(f1204,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_11
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1201,f958]) ).
fof(f1205,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_11
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1202,f958]) ).
fof(f1206,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_11
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1203,f958]) ).
fof(f1207,plain,
( $false
| spl0_11
| spl0_16
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1204,f1018]) ).
fof(f1208,plain,
( spl0_11
| spl0_16
| spl0_17
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f1207]) ).
fof(f1209,plain,
( $false
| spl0_11
| spl0_15
| spl0_16
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1205,f1018]) ).
fof(f1210,plain,
( spl0_11
| spl0_15
| spl0_16
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f1209]) ).
fof(f1211,plain,
( spl0_22
| spl0_11
| spl0_17
| spl0_19 ),
inference(avatar_split_clause,[],[f1206,f1053,f1029,f957,f1084]) ).
fof(f1212,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1039,f966]) ).
fof(f1213,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1108,f966]) ).
fof(f1214,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1112,f966]) ).
fof(f1215,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1126,f966]) ).
fof(f1216,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1212,f1054]) ).
fof(f1217,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_11
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1213,f958]) ).
fof(f1218,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1214,f995]) ).
fof(f1219,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1215,f1054]) ).
fof(f1220,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_11
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1216,f958]) ).
fof(f1221,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| spl0_11
| spl0_13
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1217,f1018]) ).
fof(f1222,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_11
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1218,f958]) ).
fof(f1223,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_11
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1219,f958]) ).
fof(f1224,plain,
( $false
| spl0_11
| spl0_13
| spl0_16
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1220,f1018]) ).
fof(f1225,plain,
( spl0_11
| spl0_13
| spl0_16
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f1224]) ).
fof(f1226,plain,
( spl0_12
| spl0_11
| spl0_13
| spl0_16 ),
inference(avatar_split_clause,[],[f1221,f1017,f965,f957,f961]) ).
fof(f1227,plain,
( $false
| spl0_11
| spl0_13
| spl0_15
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1222,f1018]) ).
fof(f1228,plain,
( spl0_11
| spl0_13
| spl0_15
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1227]) ).
fof(f1229,plain,
( spl0_22
| spl0_11
| spl0_13
| spl0_19 ),
inference(avatar_split_clause,[],[f1223,f1053,f965,f957,f1084]) ).
fof(f1240,plain,
( ~ 'E'(s(s('0')),f(suc(suc(suc(z)))))
| ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ spl0_19 ),
inference(resolution,[],[f1055,f661]) ).
fof(f1247,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ spl0_20 ),
inference(resolution,[],[f1074,f771]) ).
fof(f1248,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| ~ spl0_14
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1247,f992]) ).
fof(f1249,plain,
( $false
| ~ spl0_14
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1248,f1019]) ).
fof(f1250,plain,
( ~ spl0_14
| ~ spl0_16
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1249]) ).
fof(f1251,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1121,f1030]) ).
fof(f1252,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1251,f995]) ).
fof(f1253,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_11
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1252,f958]) ).
fof(f1254,plain,
( $false
| spl0_11
| spl0_15
| spl0_17
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1253,f1073]) ).
fof(f1255,plain,
( spl0_11
| spl0_15
| spl0_17
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1254]) ).
fof(f1256,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1117,f966]) ).
fof(f1257,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1256,f995]) ).
fof(f1258,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_11
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1257,f958]) ).
fof(f1259,plain,
( $false
| spl0_11
| spl0_13
| spl0_15
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1258,f1073]) ).
fof(f1260,plain,
( spl0_11
| spl0_13
| spl0_15
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1259]) ).
fof(f1261,plain,
( ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ spl0_15
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1240,f996]) ).
fof(f1262,plain,
( $false
| ~ spl0_12
| ~ spl0_15
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1261,f963]) ).
fof(f1263,plain,
( ~ spl0_12
| ~ spl0_15
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1262]) ).
fof(f1264,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1103,f966]) ).
fof(f1265,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1264,f962]) ).
fof(f1266,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_11
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1265,f958]) ).
fof(f1267,plain,
( $false
| spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f1266,f991]) ).
fof(f1268,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f1267]) ).
fof(f1269,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1122,f966]) ).
fof(f1270,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1269,f1054]) ).
fof(f1271,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_11
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1270,f958]) ).
fof(f1272,plain,
( $false
| spl0_11
| spl0_13
| spl0_19
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1271,f1073]) ).
fof(f1273,plain,
( spl0_11
| spl0_13
| spl0_19
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1272]) ).
fof(f1274,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1063,f1030]) ).
fof(f1275,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1139,f1030]) ).
fof(f1276,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1142,f1030]) ).
fof(f1277,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1274,f1077]) ).
fof(f1278,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1275,f1077]) ).
fof(f1279,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1276,f1077]) ).
fof(f1280,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_11
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1277,f958]) ).
fof(f1281,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_11
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1278,f958]) ).
fof(f1282,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_11
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1279,f958]) ).
fof(f1283,plain,
( spl0_20
| spl0_11
| spl0_17
| spl0_21 ),
inference(avatar_split_clause,[],[f1280,f1076,f1029,f957,f1072]) ).
fof(f1284,plain,
( $false
| spl0_11
| spl0_17
| spl0_21
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1281,f1085]) ).
fof(f1285,plain,
( spl0_11
| spl0_17
| spl0_21
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f1284]) ).
fof(f1286,plain,
( $false
| spl0_11
| spl0_17
| spl0_21
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1282,f1149]) ).
fof(f1287,plain,
( spl0_11
| spl0_17
| spl0_21
| spl0_24 ),
inference(avatar_contradiction_clause,[],[f1286]) ).
fof(f1288,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1125,f1030]) ).
fof(f1289,plain,
( 'E'('0',f(suc(suc(z))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1288,f1054]) ).
fof(f1290,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_11
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1289,f958]) ).
fof(f1291,plain,
( $false
| spl0_11
| spl0_17
| spl0_19
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1290,f1073]) ).
fof(f1292,plain,
( spl0_11
| spl0_17
| spl0_19
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1291]) ).
fof(f1293,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f940,f904]) ).
fof(f1294,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f951,f966]) ).
fof(f1295,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f979,f904]) ).
fof(f1296,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f987,f966]) ).
fof(f1297,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1100,f904]) ).
fof(f1298,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f1040,f896]) ).
fof(f1299,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f1123,f896]) ).
fof(f1300,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1033,f966]) ).
fof(f1301,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1104,f966]) ).
fof(f1302,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1119,f966]) ).
fof(f1303,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1062,f1077]) ).
fof(f1304,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1140,f1077]) ).
fof(f1305,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_8
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1293,f962]) ).
fof(f1306,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1294,f962]) ).
fof(f1307,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_8
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1295,f962]) ).
fof(f1308,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1296,f962]) ).
fof(f1309,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_8
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1297,f962]) ).
fof(f1310,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| spl0_6
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1298,f1018]) ).
fof(f1311,plain,
( spl0_20
| spl0_19
| spl0_17
| spl0_6 ),
inference(avatar_split_clause,[],[f1299,f895,f1029,f1053,f1072]) ).
fof(f1312,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_6
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1300,f896]) ).
fof(f1313,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1301,f962]) ).
fof(f1314,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_6
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1302,f896]) ).
fof(f1315,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_6
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1303,f896]) ).
fof(f1316,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(suc(z)))))))))
| spl0_6
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1304,f896]) ).
fof(f1317,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_6
| spl0_8
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1305,f896]) ).
fof(f1318,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_6
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1306,f896]) ).
fof(f1319,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_6
| spl0_8
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1307,f896]) ).
fof(f1320,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_6
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1308,f896]) ).
fof(f1321,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_6
| spl0_8
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1309,f896]) ).
fof(f1322,plain,
( spl0_19
| spl0_17
| spl0_6
| spl0_16 ),
inference(avatar_split_clause,[],[f1310,f1017,f895,f1029,f1053]) ).
fof(f1323,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| spl0_6
| spl0_13
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1312,f1018]) ).
fof(f1324,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_6
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1313,f896]) ).
fof(f1325,plain,
( spl0_20
| spl0_19
| spl0_6
| spl0_13 ),
inference(avatar_split_clause,[],[f1314,f965,f895,f1053,f1072]) ).
fof(f1326,plain,
( spl0_20
| spl0_17
| spl0_6
| spl0_21 ),
inference(avatar_split_clause,[],[f1315,f1076,f895,f1029,f1072]) ).
fof(f1327,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| spl0_6
| spl0_21
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f1316,f1149]) ).
fof(f1328,plain,
( $false
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1317,f937]) ).
fof(f1329,plain,
( spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(avatar_contradiction_clause,[],[f1328]) ).
fof(f1330,plain,
( $false
| spl0_6
| spl0_10
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1318,f937]) ).
fof(f1331,plain,
( spl0_6
| spl0_10
| spl0_12
| spl0_13 ),
inference(avatar_contradiction_clause,[],[f1330]) ).
fof(f1332,plain,
( $false
| spl0_6
| spl0_8
| spl0_12
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f1319,f991]) ).
fof(f1333,plain,
( spl0_6
| spl0_8
| spl0_12
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f1332]) ).
fof(f1334,plain,
( $false
| spl0_6
| spl0_12
| spl0_13
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f1320,f991]) ).
fof(f1335,plain,
( spl0_6
| spl0_12
| spl0_13
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f1334]) ).
fof(f1336,plain,
( $false
| spl0_6
| spl0_8
| spl0_12
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1321,f1018]) ).
fof(f1337,plain,
( spl0_6
| spl0_8
| spl0_12
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1336]) ).
fof(f1338,plain,
( spl0_19
| spl0_6
| spl0_13
| spl0_16 ),
inference(avatar_split_clause,[],[f1323,f1017,f965,f895,f1053]) ).
fof(f1339,plain,
( $false
| spl0_6
| spl0_12
| spl0_13
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1324,f1018]) ).
fof(f1340,plain,
( spl0_6
| spl0_12
| spl0_13
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1339]) ).
fof(f1341,plain,
( spl0_17
| spl0_6
| spl0_21
| spl0_24 ),
inference(avatar_split_clause,[],[f1327,f1148,f1076,f895,f1029]) ).
fof(f1342,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1025,f966]) ).
fof(f1343,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1101,f966]) ).
fof(f1344,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1115,f966]) ).
fof(f1345,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s('0'),f(suc(suc(z))))
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f945,f962]) ).
fof(f1346,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_2
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1342,f509]) ).
fof(f1347,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1343,f962]) ).
fof(f1348,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_2
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1344,f509]) ).
fof(f1349,plain,
( 'E'('0',f(z))
| 'E'(s('0'),f(suc(suc(z))))
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1345,f937]) ).
fof(f1350,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| spl0_2
| spl0_13
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1346,f1018]) ).
fof(f1351,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_2
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1347,f509]) ).
fof(f1352,plain,
( spl0_20
| spl0_19
| spl0_2
| spl0_13 ),
inference(avatar_split_clause,[],[f1348,f965,f508,f1053,f1072]) ).
fof(f1353,plain,
( 'E'(s('0'),f(suc(suc(z))))
| spl0_2
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1349,f509]) ).
fof(f1354,plain,
( spl0_19
| spl0_2
| spl0_13
| spl0_16 ),
inference(avatar_split_clause,[],[f1350,f1017,f965,f508,f1053]) ).
fof(f1355,plain,
( $false
| spl0_2
| spl0_12
| spl0_13
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1351,f1018]) ).
fof(f1356,plain,
( spl0_2
| spl0_12
| spl0_13
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1355]) ).
fof(f1357,plain,
( $false
| spl0_2
| spl0_10
| spl0_12
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1353,f966]) ).
fof(f1358,plain,
( spl0_2
| spl0_10
| spl0_12
| spl0_13 ),
inference(avatar_contradiction_clause,[],[f1357]) ).
fof(f1359,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(suc(z)))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1137,f1030]) ).
fof(f1360,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1359,f1077]) ).
fof(f1361,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_6
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1360,f896]) ).
fof(f1362,plain,
( $false
| spl0_6
| spl0_17
| spl0_21
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1361,f1085]) ).
fof(f1363,plain,
( spl0_6
| spl0_17
| spl0_21
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f1362]) ).
fof(f1370,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f879,f517]) ).
fof(f1371,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_4
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1370,f900]) ).
fof(f1372,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_2
| spl0_4
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1371,f509]) ).
fof(f1373,plain,
( $false
| spl0_2
| spl0_4
| spl0_7
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1372,f937]) ).
fof(f1374,plain,
( spl0_2
| spl0_4
| spl0_7
| spl0_10 ),
inference(avatar_contradiction_clause,[],[f1373]) ).
fof(f1386,plain,
( ~ 'E'(s(s('0')),f(suc(z)))
| ~ 'E'(s(s('0')),f(z))
| ~ spl0_12 ),
inference(resolution,[],[f963,f661]) ).
fof(f1388,plain,
( ~ 'E'(s(s('0')),f(z))
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1386,f901]) ).
fof(f1389,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1388,f514]) ).
fof(f1390,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f1389]) ).
fof(f1391,plain,
( 'E'(s(s('0')),f(z))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f788,f517]) ).
fof(f1392,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1391,f513]) ).
fof(f1393,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_2
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1392,f509]) ).
fof(f1394,plain,
( $false
| spl0_2
| spl0_3
| spl0_4
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1393,f937]) ).
fof(f1395,plain,
( spl0_2
| spl0_3
| spl0_4
| spl0_10 ),
inference(avatar_contradiction_clause,[],[f1394]) ).
fof(f1400,plain,
( ~ 'E'(s(s('0')),f(suc(suc(z))))
| ~ 'E'(s(s('0')),f(suc(z)))
| ~ spl0_15 ),
inference(resolution,[],[f996,f661]) ).
fof(f1402,plain,
( ~ 'E'(s(s('0')),f(suc(z)))
| ~ spl0_12
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1400,f963]) ).
fof(f1403,plain,
( $false
| ~ spl0_7
| ~ spl0_12
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1402,f901]) ).
fof(f1404,plain,
( ~ spl0_7
| ~ spl0_12
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f1403]) ).
fof(f1406,plain,
( ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ spl0_14 ),
inference(resolution,[],[f992,f771]) ).
fof(f1407,plain,
( ~ 'E'(s(s(s('0'))),f(suc(suc(z))))
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1406,f893]) ).
fof(f1410,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z)))
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f752,f517]) ).
fof(f1411,plain,
( 'E'(s(s('0')),f(z))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z)))
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f644,f517]) ).
fof(f1412,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z)))
| spl0_4
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1410,f900]) ).
fof(f1413,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z)))
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1411,f513]) ).
fof(f1414,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| spl0_2
| spl0_4
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1412,f509]) ).
fof(f1415,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| spl0_2
| spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1413,f509]) ).
fof(f1416,plain,
( $false
| spl0_2
| spl0_4
| spl0_5
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1414,f892]) ).
fof(f1417,plain,
( spl0_2
| spl0_4
| spl0_5
| spl0_7 ),
inference(avatar_contradiction_clause,[],[f1416]) ).
fof(f1418,plain,
( $false
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f1415,f892]) ).
fof(f1419,plain,
( spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(avatar_contradiction_clause,[],[f1418]) ).
fof(f1420,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z)))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f862,f904]) ).
fof(f1421,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(z)))
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1420,f900]) ).
fof(f1422,plain,
( 'E'(s(s(s('0'))),f(suc(z)))
| spl0_2
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1421,f509]) ).
fof(f1423,plain,
( $false
| spl0_2
| spl0_5
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1422,f892]) ).
fof(f1424,plain,
( spl0_2
| spl0_5
| spl0_7
| spl0_8 ),
inference(avatar_contradiction_clause,[],[f1423]) ).
fof(f1425,plain,
( ~ spl0_10
| ~ spl0_5
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1407,f990,f891,f936]) ).
fof(f1426,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f922,f904]) ).
fof(f1427,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1426,f900]) ).
fof(f1428,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_2
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1427,f509]) ).
fof(f1429,plain,
( $false
| spl0_2
| spl0_7
| spl0_8
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f1428,f937]) ).
fof(f1430,plain,
( spl0_2
| spl0_7
| spl0_8
| spl0_10 ),
inference(avatar_contradiction_clause,[],[f1429]) ).
fof(f1431,plain,
( 'E'(s(s('0')),f(suc(z)))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f950,f904]) ).
fof(f1432,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1431,f900]) ).
fof(f1433,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_6
| spl0_7
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1432,f896]) ).
fof(f1434,plain,
( $false
| spl0_6
| spl0_7
| spl0_8
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f1433,f991]) ).
fof(f1435,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f1434]) ).
fof(f1436,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f978,f904]) ).
fof(f1437,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1105,f904]) ).
fof(f1438,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_8
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1436,f995]) ).
fof(f1439,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_8
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1437,f995]) ).
fof(f1440,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_6
| spl0_8
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1438,f896]) ).
fof(f1441,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_6
| spl0_8
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1439,f896]) ).
fof(f1442,plain,
( spl0_14
| spl0_6
| spl0_8
| spl0_15 ),
inference(avatar_split_clause,[],[f1440,f994,f903,f895,f990]) ).
fof(f1443,plain,
( $false
| spl0_6
| spl0_8
| spl0_15
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1441,f1018]) ).
fof(f1444,plain,
( spl0_6
| spl0_8
| spl0_15
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1443]) ).
fof(f1445,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1102,f904]) ).
fof(f1446,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_8
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1445,f995]) ).
fof(f1447,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_2
| spl0_8
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1446,f509]) ).
fof(f1448,plain,
( $false
| spl0_2
| spl0_8
| spl0_15
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1447,f1018]) ).
fof(f1449,plain,
( spl0_2
| spl0_8
| spl0_15
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1448]) ).
fof(f1457,plain,
( ~ 'E'(s(s(s('0'))),f(z))
| ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ spl0_10 ),
inference(resolution,[],[f938,f771]) ).
fof(f1461,plain,
( ~ 'E'(s(s(s('0'))),f(suc(z)))
| ~ spl0_1
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1457,f506]) ).
fof(f1462,plain,
( $false
| ~ spl0_1
| ~ spl0_5
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1461,f893]) ).
fof(f1463,plain,
( ~ spl0_1
| ~ spl0_5
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f1462]) ).
fof(f1464,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s('0'),f(suc(suc(suc(z)))))
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1024,f995]) ).
fof(f1465,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1113,f1030]) ).
fof(f1466,plain,
( 'E'('0',f(suc(z)))
| 'E'(s('0'),f(suc(suc(suc(z)))))
| spl0_14
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1464,f991]) ).
fof(f1467,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1465,f995]) ).
fof(f1468,plain,
( 'E'(s('0'),f(suc(suc(suc(z)))))
| spl0_6
| spl0_14
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1466,f896]) ).
fof(f1469,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_6
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1467,f896]) ).
fof(f1470,plain,
( $false
| spl0_6
| spl0_14
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1468,f1030]) ).
fof(f1471,plain,
( spl0_6
| spl0_14
| spl0_15
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f1470]) ).
fof(f1472,plain,
( $false
| spl0_6
| spl0_15
| spl0_16
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1469,f1018]) ).
fof(f1473,plain,
( spl0_6
| spl0_15
| spl0_16
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f1472]) ).
fof(f1474,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f986,f966]) ).
fof(f1475,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1109,f966]) ).
fof(f1476,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1474,f995]) ).
fof(f1477,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1475,f995]) ).
fof(f1478,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(z)))))
| spl0_6
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1476,f896]) ).
fof(f1479,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_6
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1477,f896]) ).
fof(f1480,plain,
( $false
| spl0_6
| spl0_13
| spl0_14
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1478,f991]) ).
fof(f1481,plain,
( spl0_6
| spl0_13
| spl0_14
| spl0_15 ),
inference(avatar_contradiction_clause,[],[f1480]) ).
fof(f1482,plain,
( $false
| spl0_6
| spl0_13
| spl0_15
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1479,f1018]) ).
fof(f1483,plain,
( spl0_6
| spl0_13
| spl0_15
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1482]) ).
fof(f1484,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1106,f966]) ).
fof(f1485,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1484,f995]) ).
fof(f1486,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(z))))))
| spl0_2
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1485,f509]) ).
fof(f1487,plain,
( $false
| spl0_2
| spl0_13
| spl0_15
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1486,f1018]) ).
fof(f1488,plain,
( spl0_2
| spl0_13
| spl0_15
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f1487]) ).
fof(f1489,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1114,f966]) ).
fof(f1490,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1111,f966]) ).
fof(f1491,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1489,f995]) ).
fof(f1492,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1490,f995]) ).
fof(f1493,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_6
| spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1491,f896]) ).
fof(f1494,plain,
( 'E'('0',f(z))
| spl0_13
| spl0_15
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1492,f1073]) ).
fof(f1495,plain,
( $false
| spl0_6
| spl0_13
| spl0_15
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1493,f1073]) ).
fof(f1496,plain,
( spl0_6
| spl0_13
| spl0_15
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1495]) ).
fof(f1497,plain,
( spl0_2
| spl0_13
| spl0_15
| spl0_20 ),
inference(avatar_split_clause,[],[f1494,f1072,f994,f965,f508]) ).
fof(f1498,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1124,f966]) ).
fof(f1499,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f1120,f966]) ).
fof(f1500,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1498,f1054]) ).
fof(f1501,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1499,f1054]) ).
fof(f1502,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_6
| spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1500,f896]) ).
fof(f1503,plain,
( 'E'('0',f(z))
| spl0_13
| spl0_19
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1501,f1085]) ).
fof(f1504,plain,
( $false
| spl0_6
| spl0_13
| spl0_19
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1502,f1085]) ).
fof(f1505,plain,
( spl0_6
| spl0_13
| spl0_19
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f1504]) ).
fof(f1506,plain,
( spl0_2
| spl0_13
| spl0_19
| spl0_22 ),
inference(avatar_split_clause,[],[f1503,f1084,f1053,f965,f508]) ).
fof(f1507,plain,
( 'E'(s(s('0')),f(suc(suc(suc(suc(z))))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1127,f1030]) ).
fof(f1508,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1507,f1054]) ).
fof(f1509,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(suc(z))))))))
| spl0_6
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1508,f896]) ).
fof(f1510,plain,
( $false
| spl0_6
| spl0_17
| spl0_19
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f1509,f1085]) ).
fof(f1511,plain,
( spl0_6
| spl0_17
| spl0_19
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f1510]) ).
fof(f1512,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1118,f1030]) ).
fof(f1513,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1512,f995]) ).
fof(f1514,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_6
| spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1513,f896]) ).
fof(f1515,plain,
( $false
| spl0_6
| spl0_15
| spl0_17
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1514,f1073]) ).
fof(f1516,plain,
( spl0_6
| spl0_15
| spl0_17
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1515]) ).
fof(f1517,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f921,f517]) ).
fof(f1518,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_4
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1517,f962]) ).
fof(f1519,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_2
| spl0_4
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1518,f509]) ).
fof(f1520,plain,
( $false
| spl0_2
| spl0_4
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1519,f937]) ).
fof(f1521,plain,
( spl0_2
| spl0_4
| spl0_10
| spl0_12 ),
inference(avatar_contradiction_clause,[],[f1520]) ).
fof(f1522,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1107,f904]) ).
fof(f1523,plain,
( 'E'(s(s('0')),f(suc(suc(z))))
| 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f930,f904]) ).
fof(f1524,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_2
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1522,f509]) ).
fof(f1525,plain,
( 'E'('0',f(z))
| 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_8
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1523,f962]) ).
fof(f1526,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| spl0_2
| spl0_8
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1524,f1073]) ).
fof(f1527,plain,
( 'E'(s(s(s('0'))),f(suc(suc(z))))
| spl0_2
| spl0_8
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1525,f509]) ).
fof(f1528,plain,
( spl0_15
| spl0_2
| spl0_8
| spl0_20 ),
inference(avatar_split_clause,[],[f1526,f1072,f903,f508,f994]) ).
fof(f1529,plain,
( $false
| spl0_2
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1527,f937]) ).
fof(f1530,plain,
( spl0_2
| spl0_8
| spl0_10
| spl0_12 ),
inference(avatar_contradiction_clause,[],[f1529]) ).
fof(f1531,plain,
( 'E'(s(s('0')),f(suc(suc(suc(z)))))
| 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1110,f904]) ).
fof(f1532,plain,
( 'E'('0',f(suc(z)))
| 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_8
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1531,f995]) ).
fof(f1533,plain,
( 'E'(s(s(s('0'))),f(suc(suc(suc(suc(suc(z)))))))
| spl0_6
| spl0_8
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1532,f896]) ).
fof(f1534,plain,
( $false
| spl0_6
| spl0_8
| spl0_15
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f1533,f1073]) ).
fof(f1535,plain,
( spl0_6
| spl0_8
| spl0_15
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f1534]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f519]) ).
cnf(s2,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f906]) ).
cnf(s4,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_10 ),
inference(sat_conversion,[],[f939]) ).
cnf(s5,plain,
( spl0_10
| spl0_11
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f968]) ).
cnf(s6,plain,
( spl0_11
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f997]) ).
cnf(s7,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_11 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s8,plain,
( spl0_2
| spl0_4
| spl0_7
| spl0_14 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s9,plain,
( spl0_2
| spl0_7
| spl0_8
| spl0_14 ),
inference(sat_conversion,[],[f1012]) ).
cnf(s10,plain,
( spl0_2
| spl0_4
| spl0_12
| spl0_14 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s11,plain,
( spl0_2
| spl0_8
| spl0_12
| spl0_14 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s12,plain,
( spl0_2
| spl0_8
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s13,plain,
( spl0_2
| spl0_4
| spl0_12
| spl0_16 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s14,plain,
( spl0_2
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s15,plain,
( spl0_2
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f1022]) ).
cnf(s16,plain,
( spl0_2
| spl0_8
| spl0_12
| spl0_16 ),
inference(sat_conversion,[],[f1023]) ).
cnf(s17,plain,
( spl0_11
| spl0_14
| spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s18,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_13 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s19,plain,
( ~ spl0_8
| ~ spl0_13
| ~ spl0_17 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s20,plain,
( spl0_11
| spl0_16
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s21,plain,
( ~ spl0_13
| ~ spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s22,plain,
( ~ spl0_10
| ~ spl0_14
| ~ spl0_16 ),
inference(sat_conversion,[],[f1067]) ).
cnf(s23,plain,
( spl0_11
| spl0_18
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s24,plain,
( spl0_11
| spl0_18
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s25,plain,
( ~ spl0_15
| ~ spl0_19
| ~ spl0_21 ),
inference(sat_conversion,[],[f1095]) ).
cnf(s26,plain,
( ~ spl0_16
| ~ spl0_20
| ~ spl0_22 ),
inference(sat_conversion,[],[f1099]) ).
cnf(s27,plain,
( spl0_11
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1132]) ).
cnf(s28,plain,
( spl0_11
| spl0_18
| spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s29,plain,
( spl0_11
| spl0_18
| spl0_23
| spl0_25 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s30,plain,
( ~ spl0_19
| ~ spl0_21
| ~ spl0_23 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s33,plain,
( ~ spl0_20
| ~ spl0_22
| ~ spl0_24 ),
inference(sat_conversion,[],[f1181]) ).
cnf(s34,plain,
( spl0_11
| spl0_18
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s35,plain,
( ~ spl0_22
| ~ spl0_24
| ~ spl0_25 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s36,plain,
( spl0_11
| spl0_18
| spl0_21
| spl0_24 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s37,plain,
( spl0_11
| spl0_18
| spl0_19
| spl0_22 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s38,plain,
( spl0_11
| spl0_16
| spl0_17
| spl0_19 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s39,plain,
( spl0_11
| spl0_15
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s40,plain,
( spl0_11
| spl0_17
| spl0_19
| spl0_22 ),
inference(sat_conversion,[],[f1211]) ).
cnf(s41,plain,
( spl0_11
| spl0_13
| spl0_16
| spl0_19 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s42,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s43,plain,
( spl0_11
| spl0_13
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s44,plain,
( spl0_11
| spl0_13
| spl0_19
| spl0_22 ),
inference(sat_conversion,[],[f1229]) ).
cnf(s45,plain,
( ~ spl0_14
| ~ spl0_16
| ~ spl0_20 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s46,plain,
( spl0_11
| spl0_15
| spl0_17
| spl0_20 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s47,plain,
( spl0_11
| spl0_13
| spl0_15
| spl0_20 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s48,plain,
( ~ spl0_12
| ~ spl0_15
| ~ spl0_19 ),
inference(sat_conversion,[],[f1263]) ).
cnf(s50,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s51,plain,
( spl0_11
| spl0_13
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1273]) ).
cnf(s52,plain,
( spl0_11
| spl0_17
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s53,plain,
( spl0_11
| spl0_17
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s54,plain,
( spl0_11
| spl0_17
| spl0_21
| spl0_24 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s55,plain,
( spl0_11
| spl0_17
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s56,plain,
( spl0_6
| spl0_17
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s57,plain,
( spl0_6
| spl0_16
| spl0_17
| spl0_19 ),
inference(sat_conversion,[],[f1322]) ).
cnf(s58,plain,
( spl0_6
| spl0_13
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1325]) ).
cnf(s59,plain,
( spl0_6
| spl0_17
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s60,plain,
( spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(sat_conversion,[],[f1329]) ).
cnf(s61,plain,
( spl0_6
| spl0_10
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f1331]) ).
cnf(s62,plain,
( spl0_6
| spl0_8
| spl0_12
| spl0_14 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s63,plain,
( spl0_6
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f1335]) ).
cnf(s64,plain,
( spl0_6
| spl0_8
| spl0_12
| spl0_16 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s65,plain,
( spl0_6
| spl0_13
| spl0_16
| spl0_19 ),
inference(sat_conversion,[],[f1338]) ).
cnf(s66,plain,
( spl0_6
| spl0_12
| spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f1340]) ).
cnf(s67,plain,
( spl0_6
| spl0_17
| spl0_21
| spl0_24 ),
inference(sat_conversion,[],[f1341]) ).
cnf(s68,plain,
( spl0_2
| spl0_13
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f1352]) ).
cnf(s69,plain,
( spl0_2
| spl0_13
| spl0_16
| spl0_19 ),
inference(sat_conversion,[],[f1354]) ).
cnf(s70,plain,
( spl0_2
| spl0_12
| spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f1356]) ).
cnf(s71,plain,
( spl0_2
| spl0_10
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f1358]) ).
cnf(s73,plain,
( spl0_6
| spl0_17
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1363]) ).
cnf(s75,plain,
( spl0_2
| spl0_4
| spl0_7
| spl0_10 ),
inference(sat_conversion,[],[f1374]) ).
cnf(s77,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_12 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s78,plain,
( spl0_2
| spl0_3
| spl0_4
| spl0_10 ),
inference(sat_conversion,[],[f1395]) ).
cnf(s79,plain,
( ~ spl0_7
| ~ spl0_12
| ~ spl0_15 ),
inference(sat_conversion,[],[f1404]) ).
cnf(s81,plain,
( spl0_2
| spl0_4
| spl0_5
| spl0_7 ),
inference(sat_conversion,[],[f1417]) ).
cnf(s82,plain,
( spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s83,plain,
( spl0_2
| spl0_5
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f1424]) ).
cnf(s84,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_14 ),
inference(sat_conversion,[],[f1425]) ).
cnf(s85,plain,
( spl0_2
| spl0_7
| spl0_8
| spl0_10 ),
inference(sat_conversion,[],[f1430]) ).
cnf(s87,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_14 ),
inference(sat_conversion,[],[f1435]) ).
cnf(s88,plain,
( spl0_6
| spl0_8
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s89,plain,
( spl0_6
| spl0_8
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s90,plain,
( spl0_2
| spl0_8
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f1449]) ).
cnf(s91,plain,
( ~ spl0_1
| ~ spl0_5
| ~ spl0_10 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s92,plain,
( spl0_6
| spl0_14
| spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f1471]) ).
cnf(s93,plain,
( spl0_6
| spl0_15
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f1473]) ).
cnf(s94,plain,
( spl0_6
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s95,plain,
( spl0_6
| spl0_13
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f1483]) ).
cnf(s96,plain,
( spl0_2
| spl0_13
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s97,plain,
( spl0_6
| spl0_13
| spl0_15
| spl0_20 ),
inference(sat_conversion,[],[f1496]) ).
cnf(s98,plain,
( spl0_2
| spl0_13
| spl0_15
| spl0_20 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s99,plain,
( spl0_6
| spl0_13
| spl0_19
| spl0_22 ),
inference(sat_conversion,[],[f1505]) ).
cnf(s100,plain,
( spl0_2
| spl0_13
| spl0_19
| spl0_22 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s101,plain,
( spl0_6
| spl0_17
| spl0_19
| spl0_22 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s102,plain,
( spl0_6
| spl0_15
| spl0_17
| spl0_20 ),
inference(sat_conversion,[],[f1516]) ).
cnf(s103,plain,
( spl0_2
| spl0_4
| spl0_10
| spl0_12 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s104,plain,
( spl0_2
| spl0_8
| spl0_15
| spl0_20 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s105,plain,
( spl0_2
| spl0_8
| spl0_10
| spl0_12 ),
inference(sat_conversion,[],[f1530]) ).
cnf(s106,plain,
( spl0_6
| spl0_8
| spl0_15
| spl0_20 ),
inference(sat_conversion,[],[f1535]) ).
cnf(s109,plain,
( spl0_19
| spl0_13
| spl0_2 ),
inference(rat,[],[s26,s69,s68,s100]) ).
cnf(s116,plain,
( spl0_15
| ~ spl0_16
| spl0_13
| spl0_2 ),
inference(rat,[],[s45,s14,s98]) ).
cnf(s117,plain,
( ~ spl0_16
| spl0_13
| spl0_2 ),
inference(rat,[],[s22,s71,s15,s48,s116,s109]) ).
cnf(s118,plain,
( spl0_13
| spl0_2 ),
inference(rat,[],[s48,s70,s96,s117,s109]) ).
cnf(s119,plain,
( spl0_15
| ~ spl0_16
| spl0_8
| spl0_2 ),
inference(rat,[],[s45,s12,s104]) ).
cnf(s120,plain,
( ~ spl0_16
| ~ spl0_7
| spl0_8
| spl0_2 ),
inference(rat,[],[s22,s105,s11,s79,s119]) ).
cnf(s121,plain,
( ~ spl0_7
| spl0_8
| spl0_2 ),
inference(rat,[],[s79,s16,s90,s120]) ).
cnf(s122,plain,
( spl0_7
| spl0_8
| spl0_2 ),
inference(rat,[],[s84,s9,s85,s83]) ).
cnf(s123,plain,
( spl0_8
| spl0_2 ),
inference(rat,[],[s122,s121]) ).
cnf(s124,plain,
( spl0_7
| spl0_4
| spl0_2 ),
inference(rat,[],[s84,s81,s8,s75]) ).
cnf(s125,plain,
( spl0_12
| spl0_4
| spl0_2 ),
inference(rat,[],[s22,s103,s10,s13]) ).
cnf(s126,plain,
( spl0_4
| spl0_2
| spl0_1 ),
inference(rat,[],[s125,s77,s124,s1]) ).
cnf(s127,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s126,s18,s123,s118]) ).
cnf(s128,plain,
( spl0_22
| spl0_19
| spl0_13
| ~ spl0_2 ),
inference(rat,[],[s7,s99,s44]) ).
cnf(s129,plain,
( spl0_19
| ~ spl0_16
| spl0_13
| ~ spl0_2 ),
inference(rat,[],[s7,s58,s51,s26,s128]) ).
cnf(s130,plain,
( spl0_14
| spl0_15
| spl0_13
| ~ spl0_2 ),
inference(rat,[],[s7,s6,s94]) ).
cnf(s131,plain,
( ~ spl0_16
| ~ spl0_12
| spl0_13
| ~ spl0_2 ),
inference(rat,[],[s7,s47,s97,s45,s130,s48,s129]) ).
cnf(s132,plain,
( spl0_19
| spl0_16
| spl0_13
| ~ spl0_2 ),
inference(rat,[],[s7,s65,s41]) ).
cnf(s133,plain,
( ~ spl0_12
| spl0_13
| ~ spl0_2 ),
inference(rat,[],[s7,s95,s43,s48,s132,s131]) ).
cnf(s134,plain,
( spl0_11
| ~ spl0_16
| spl0_12
| spl0_13 ),
inference(rat,[],[s22,s50,s5]) ).
cnf(s135,plain,
( ~ spl0_16
| spl0_13
| ~ spl0_2 ),
inference(rat,[],[s22,s61,s63,s7,s134,s133]) ).
cnf(s136,plain,
( spl0_13
| ~ spl0_2 ),
inference(rat,[],[s7,s42,s66,s135,s133]) ).
cnf(s137,plain,
( spl0_19
| spl0_11
| ~ spl0_16
| spl0_17 ),
inference(rat,[],[s26,s40,s55]) ).
cnf(s139,plain,
( spl0_19
| spl0_6
| ~ spl0_16
| spl0_17 ),
inference(rat,[],[s26,s56,s101]) ).
cnf(s143,plain,
( spl0_21
| spl0_11
| spl0_17 ),
inference(rat,[],[s33,s52,s53,s54]) ).
cnf(s144,plain,
( spl0_11
| ~ spl0_16
| spl0_17 ),
inference(rat,[],[s45,s46,s17,s25,s143,s137]) ).
cnf(s145,plain,
( spl0_21
| spl0_6
| ~ spl0_16
| spl0_17 ),
inference(rat,[],[s26,s59,s73]) ).
cnf(s146,plain,
( spl0_6
| ~ spl0_16
| spl0_17 ),
inference(rat,[],[s45,s102,s92,s25,s145,s139]) ).
cnf(s147,plain,
( ~ spl0_16
| spl0_17
| ~ spl0_2 ),
inference(rat,[],[s146,s7,s144]) ).
cnf(s148,plain,
( spl0_11
| spl0_16
| spl0_17 ),
inference(rat,[],[s25,s143,s39,s38]) ).
cnf(s149,plain,
( spl0_21
| spl0_17
| spl0_6 ),
inference(rat,[],[s33,s59,s67,s73]) ).
cnf(s150,plain,
( spl0_6
| spl0_16
| spl0_17 ),
inference(rat,[],[s149,s25,s93,s57]) ).
cnf(s151,plain,
( spl0_17
| ~ spl0_2 ),
inference(rat,[],[s150,s7,s148,s147]) ).
cnf(s152,plain,
( spl0_19
| spl0_11
| ~ spl0_16
| spl0_18 ),
inference(rat,[],[s26,s37,s27]) ).
cnf(s153,plain,
( spl0_21
| spl0_11
| ~ spl0_16
| spl0_18 ),
inference(rat,[],[s26,s34,s23]) ).
cnf(s154,plain,
( spl0_23
| spl0_11
| spl0_18 ),
inference(rat,[],[s35,s24,s28,s29]) ).
cnf(s155,plain,
( spl0_11
| ~ spl0_16
| spl0_18 ),
inference(rat,[],[s154,s30,s153,s152]) ).
cnf(s156,plain,
( spl0_14
| ~ spl0_15
| spl0_6
| spl0_8 ),
inference(rat,[],[s79,s62,s87]) ).
cnf(s157,plain,
( ~ spl0_15
| spl0_6
| ~ spl0_16
| spl0_8 ),
inference(rat,[],[s79,s4,s60,s22,s156]) ).
cnf(s158,plain,
( spl0_6
| ~ spl0_16
| spl0_8 ),
inference(rat,[],[s45,s88,s106,s157]) ).
cnf(s159,plain,
( ~ spl0_16
| ~ spl0_2 ),
inference(rat,[],[s158,s7,s155,s19,s21,s151,s136]) ).
cnf(s160,plain,
( spl0_21
| spl0_11
| spl0_18 ),
inference(rat,[],[s33,s34,s36,s23]) ).
cnf(s161,plain,
( spl0_11
| ~ spl0_2 ),
inference(rat,[],[s160,s30,s20,s154,s21,s151,s136,s159]) ).
cnf(s162,plain,
( spl0_6
| spl0_8
| spl0_16 ),
inference(rat,[],[s84,s2,s4,s156,s79,s89,s64]) ).
cnf(s163,plain,
~ spl0_2,
inference(rat,[],[s162,s7,s161,s159,s19,s151,s136]) ).
cnf(s164,plain,
spl0_13,
inference(rat,[],[s118,s163]) ).
cnf(s165,plain,
spl0_8,
inference(rat,[],[s123,s163]) ).
cnf(s166,plain,
spl0_1,
inference(rat,[],[s127,s163]) ).
cnf(s167,plain,
~ spl0_4,
inference(rat,[],[s18,s164,s165]) ).
cnf(s169,plain,
spl0_7,
inference(rat,[],[s124,s163,s167]) ).
cnf(s170,plain,
spl0_12,
inference(rat,[],[s125,s163,s167]) ).
cnf(s172,plain,
~ spl0_3,
inference(rat,[],[s77,s169,s170]) ).
cnf(s173,plain,
spl0_5,
inference(rat,[],[s82,s167,s163,s172]) ).
cnf(s174,plain,
spl0_10,
inference(rat,[],[s78,s167,s163,s172]) ).
cnf(s175,plain,
$false,
inference(rat,[],[s91,s166,s174,s173]) ).
fof(f1536,plain,
$false,
inference(avatar_sat_refutation,[],[s175]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO681-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n014.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 18:04:15 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.24/0.26 % (2002920)Will run a generic schedule for satisfiability detection.
% 0.24/0.26 % (2002929)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=949113520:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.24/0.26 % (2002926)% WARNING: option uhcvi not known.
% 0.24/0.26 % (2002925)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=924620894_2999 on theBenchmark for (2999ds/0Mi)
% 0.24/0.26 % (2002930)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3462999919:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.24/0.26 % (2002927)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3245897196:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.24/0.26 % (2002928)dis+10_1_sil=32000:sp=arity:random_seed=2054431519:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.24/0.26 % (2002931)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3576587494:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.24/0.26 % (2002926)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3494038221:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.24/0.26 % (2002929) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2002920-2002929"...
% 0.24/0.26 % (2002929)...printing done.
% 0.24/0.26 % (2002929)Refutation found. Thanks to Tanya!
% 0.24/0.26 % SZS status Unsatisfiable for theBenchmark
% 0.24/0.26 % SZS output start Proof for theBenchmark
% See solution above
% 0.24/0.28 % (2002929)------------------------------
% 0.24/0.28 % (2002929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.24/0.28 % (2002929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.24/0.28 % (2002929)CaDiCaL version: 2.1.3
% 0.24/0.28 % (2002929)Termination reason: Refutation
% 0.24/0.28 % (2002929)Time elapsed: 0.024 s
% 0.24/0.28 % (2002929)Peak memory usage: 12 MB
% 0.24/0.28 % (2002929)Instructions burned: 89 (million)
% 0.24/0.28 % (2002920)Success in time 0.053 s
% 0.24/0.28 % Vampire exiting
%------------------------------------------------------------------------------