%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO688-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:28:39 PM UTC 2026
% Result : Unsatisfiable 8.72s 2.41s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 73
% Syntax : Number of formulae : 364 ( 35 unt; 15 def)
% Number of atoms : 4098 ( 0 equ)
% Maximal formula atoms : 25 ( 11 avg)
% Number of connectives : 7030 (3296 ~;3719 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 14 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 19 ( 18 usr; 16 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 701 ( 0 sgn 701 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_985) ).
fof(f92,axiom,
! [X0] : 'LE'(f(X0),s(s(s(s(s('0')))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_299) ).
fof(f125,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_743) ).
fof(f129,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_64) ).
fof(f135,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_773) ).
fof(f139,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_1123) ).
fof(f148,axiom,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_171) ).
fof(f153,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_1158) ).
fof(f169,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_269) ).
fof(f190,axiom,
! [X0] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1023) ).
fof(f213,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1074) ).
fof(f226,axiom,
! [X0] :
( ~ 'LE'(f(X0),s('0'))
| 'E'('0',f(X0))
| 'LE'(f(X0),'0') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_199) ).
fof(f279,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_237) ).
fof(f308,axiom,
! [X2,X0,X1] :
( ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_910) ).
fof(f335,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_699) ).
fof(f360,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_340) ).
fof(f366,axiom,
~ 'LE'(f(z),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_546) ).
fof(f384,axiom,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_813) ).
fof(f402,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_436) ).
fof(f410,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_191) ).
fof(f470,axiom,
! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_473) ).
fof(f471,axiom,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_912) ).
fof(f483,axiom,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_174) ).
fof(f502,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_1143) ).
fof(f535,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_160) ).
fof(f580,axiom,
! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_231) ).
fof(f581,axiom,
! [X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_106) ).
fof(f587,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_778) ).
fof(f590,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_207) ).
fof(f660,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_840) ).
fof(f678,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_915) ).
fof(f692,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_149) ).
fof(f708,axiom,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_709) ).
fof(f720,axiom,
! [X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_256) ).
fof(f756,axiom,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_694) ).
fof(f787,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_968) ).
fof(f809,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| '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_105) ).
fof(f852,axiom,
! [X0] :
( ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1089) ).
fof(f894,axiom,
! [X0] :
( ~ 'LE'(f(X0),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(X0))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_298) ).
fof(f913,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_748) ).
fof(f914,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_569) ).
fof(f932,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1016) ).
fof(f935,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'E'(f(X1),f(suc(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_514) ).
fof(f943,axiom,
! [X0] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_794) ).
fof(f976,axiom,
! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_483) ).
fof(f982,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_115) ).
fof(f1014,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_159) ).
fof(f1030,axiom,
! [X2,X0,X1] :
( ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_303) ).
fof(f1031,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_24) ).
fof(f1041,axiom,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_281) ).
fof(f1071,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_722) ).
fof(f1072,axiom,
! [X2,X0,X1] :
( ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_718) ).
fof(f1075,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_713) ).
fof(f1085,axiom,
! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_698) ).
fof(f1102,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_335) ).
fof(f1136,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_650) ).
fof(f1151,axiom,
! [X0] :
( ~ 'LE'(f(suc(X0)),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_297) ).
fof(f1160,axiom,
! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_249) ).
fof(f1172,definition,
( spl0_2
<=> ! [X0] :
( ~ 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f1173,plain,
( ! [X0] :
( ~ 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0)) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f1172]) ).
fof(f1176,definition,
( spl0_3
<=> ! [X2] :
( ~ 'LE'(f(X2),s('0'))
| 'LE'(f(X2),'0')
| 'E'('0',f(X2)) ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f1177,plain,
( ! [X2] :
( ~ 'LE'(f(X2),s('0'))
| 'LE'(f(X2),'0')
| 'E'('0',f(X2)) )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f1176]) ).
fof(f1183,definition,
( spl0_5
<=> ! [X1] :
( ~ 'LE'(f(X1),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(X1)) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f1184,plain,
( ! [X1] :
( ~ 'LE'(f(X1),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(X1)) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f1183]) ).
fof(f1194,definition,
( spl0_8
<=> ! [X1] :
( ~ 'LE'(f(suc(suc(X1))),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(suc(X1)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f1195,plain,
( ! [X1] :
( ~ 'LE'(f(suc(suc(X1))),s(s('0')))
| 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(suc(suc(X1)))) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1209,definition,
( spl0_12
<=> ! [X1] :
( ~ 'LE'(f(suc(X1)),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(suc(X1))) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f1210,plain,
( ! [X1] :
( ~ 'LE'(f(suc(X1)),s('0'))
| 'LE'(f(X1),'0')
| 'E'('0',f(suc(X1))) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f1209]) ).
fof(f1220,definition,
( spl0_15
<=> ! [X0] :
( ~ 'LE'(f(suc(X0)),s(s('0')))
| 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0))) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f1221,plain,
( ! [X0] :
( ~ 'LE'(f(suc(X0)),s(s('0')))
| 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0))) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1227,definition,
( spl0_17
<=> ! [X0] :
( ~ 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f1228,plain,
( ! [X0] :
( ~ 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X0)) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f1227]) ).
fof(f1245,definition,
( spl0_21
<=> 'LE'(f(z),'0') ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f1247,plain,
( ~ 'LE'(f(z),'0')
| spl0_21 ),
inference(avatar_component_clause,[],[f1245]) ).
fof(f1273,definition,
( spl0_28
<=> ! [X1] :
( ~ 'LE'(f(suc(suc(X1))),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X1)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f1274,plain,
( ! [X1] :
( ~ 'LE'(f(suc(suc(X1))),s(s(s('0'))))
| 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X1)))) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1281,definition,
( spl0_30
<=> ! [X2] :
( ~ 'LE'(f(suc(suc(X2))),s('0'))
| 'LE'(f(X2),'0')
| 'E'('0',f(suc(suc(X2)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f1282,plain,
( ! [X2] :
( ~ 'LE'(f(suc(suc(X2))),s('0'))
| 'LE'(f(X2),'0')
| 'E'('0',f(suc(suc(X2)))) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f1281]) ).
fof(f1289,definition,
( spl0_32
<=> ! [X2] :
( ~ 'LE'(f(suc(X2)),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X2))) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f1290,plain,
( ! [X2] :
( ~ 'LE'(f(suc(X2)),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(X2))) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1309,definition,
( spl0_37
<=> ! [X2] :
( ~ 'LE'(f(suc(X2)),s(s(s('0'))))
| 'LE'(f(X2),s(s('0')))
| 'E'(s(s('0')),f(suc(X2))) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f1310,plain,
( ! [X2] :
( ~ 'LE'(f(suc(X2)),s(s(s('0'))))
| 'LE'(f(X2),s(s('0')))
| 'E'(s(s('0')),f(suc(X2))) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1313,definition,
( spl0_38
<=> ! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s(s(s(s(s('0'))))))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f1314,plain,
( ! [X0] :
( ~ 'LE'(f(suc(suc(X0))),s(s(s(s(s('0'))))))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(suc(suc(X0)))) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f1313]) ).
fof(f1348,definition,
( spl0_46
<=> ! [X2] :
( ~ 'LE'(f(X2),s(s(s(s(s('0'))))))
| 'LE'(f(X2),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(X2)) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f1349,plain,
( ! [X2] :
( ~ 'LE'(f(X2),s(s(s(s(s('0'))))))
| 'LE'(f(X2),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(X2)) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f1348]) ).
fof(f1384,plain,
spl0_12,
inference(avatar_split_clause,[],[f1075,f1209]) ).
fof(f1386,definition,
( spl0_55
<=> ! [X1] :
( ~ 'LE'(f(suc(suc(X1))),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X1)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f1387,plain,
( ! [X1] :
( ~ 'LE'(f(suc(suc(X1))),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(suc(suc(X1)))) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f1386]) ).
fof(f1451,plain,
spl0_17,
inference(avatar_split_clause,[],[f1031,f1227]) ).
fof(f1474,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X2),f(suc(X2))) ),
inference(forward_subsumption_resolution,[],[f1014,f1136]) ).
fof(f1517,plain,
! [X2,X0,X1] :
( ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f976,f1072]) ).
fof(f1555,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(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(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f932,f935]) ).
fof(f1569,plain,
spl0_28,
inference(avatar_split_clause,[],[f914,f1273]) ).
fof(f1582,plain,
spl0_46,
inference(avatar_split_clause,[],[f894,f1348]) ).
fof(f1674,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) ),
inference(forward_subsumption_resolution,[],[f787,f1160]) ).
fof(f1747,plain,
spl0_15,
inference(avatar_split_clause,[],[f692,f1220]) ).
fof(f1775,plain,
spl0_30,
inference(avatar_split_clause,[],[f660,f1281]) ).
fof(f1825,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X2),f(suc(X2))) ),
inference(forward_subsumption_resolution,[],[f590,f1071]) ).
fof(f1833,plain,
spl0_38,
inference(avatar_split_clause,[],[f580,f1313]) ).
fof(f1871,plain,
spl0_8,
inference(avatar_split_clause,[],[f535,f1194]) ).
fof(f1904,plain,
spl0_2,
inference(avatar_split_clause,[],[f502,f1172]) ).
fof(f1921,plain,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f483,f756]) ).
fof(f1929,plain,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f471,f756]) ).
fof(f1930,plain,
! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f470,f1085]) ).
fof(f1979,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f410,f1102]) ).
fof(f1986,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X1))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f402,f913]) ).
fof(f2001,plain,
! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X2)) ),
inference(forward_subsumption_resolution,[],[f384,f1041]) ).
fof(f2017,plain,
~ spl0_21,
inference(avatar_split_clause,[],[f366,f1245]) ).
fof(f2023,plain,
! [X0] :
( ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f360,f852]) ).
fof(f2051,plain,
! [X2,X0,X1] :
( ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) ),
inference(forward_subsumption_resolution,[],[f335,f1030]) ).
fof(f2091,plain,
! [X0] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f279,f943]) ).
fof(f2131,plain,
spl0_3,
inference(avatar_split_clause,[],[f226,f1176]) ).
fof(f2150,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) ),
inference(forward_subsumption_resolution,[],[f213,f809]) ).
fof(f2190,plain,
spl0_32,
inference(avatar_split_clause,[],[f169,f1289]) ).
fof(f2203,plain,
spl0_5,
inference(avatar_split_clause,[],[f153,f1183]) ).
fof(f2217,plain,
spl0_55,
inference(avatar_split_clause,[],[f139,f1386]) ).
fof(f2220,plain,
spl0_37,
inference(avatar_split_clause,[],[f135,f1309]) ).
fof(f2225,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2))) ),
inference(forward_subsumption_resolution,[],[f129,f587]) ).
fof(f2229,plain,
! [X2,X0,X1] :
( ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X2)) ),
inference(forward_subsumption_resolution,[],[f125,f308]) ).
fof(f2316,plain,
! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X2))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1))) ),
inference(forward_subsumption_resolution,[],[f39,f1071]) ).
fof(f2380,plain,
( ! [X0] :
( 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1314,f92]) ).
fof(f2381,plain,
( ! [X2] :
( 'LE'(f(X2),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(X2)) )
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f1349,f92]) ).
fof(f2384,plain,
( ! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| iLEQ(suc(X0),suc(X0))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38 ),
inference(resolution,[],[f1930,f2380]) ).
fof(f2385,plain,
( ! [X0] :
( ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| iLEQ(suc(X0),suc(X0))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f2384,f2381]) ).
fof(f2388,plain,
! [X0] :
( 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(resolution,[],[f1151,f92]) ).
fof(f2390,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s(s('0')))))
| iLEQ(suc(X0),suc(X0))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f2388,f2385]) ).
fof(f2391,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s(s('0')))))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_38
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f2390]) ).
fof(f2950,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38 ),
inference(resolution,[],[f1986,f2380]) ).
fof(f2955,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2950,f2388]) ).
fof(f2956,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f2955,f2381]) ).
fof(f2958,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f2956,f2380]) ).
fof(f2963,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f2958,f2388]) ).
fof(f2964,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f2963,f2381]) ).
fof(f2966,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f2964,f2380]) ).
fof(f2971,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f2966,f2388]) ).
fof(f2972,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f2971,f2381]) ).
fof(f3419,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38 ),
inference(resolution,[],[f1474,f2380]) ).
fof(f3426,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X2)))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f3419,f2150]) ).
fof(f3429,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X2))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f3426,f2388]) ).
fof(f3430,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f3429,f2381]) ).
fof(f3432,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3430,f2380]) ).
fof(f3437,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| ~ 'E'(s(s(s(s('0')))),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f3432,f2381]) ).
fof(f3438,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s(s('0')))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f3437,f2388]) ).
fof(f3442,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s(s(s('0')))),f(X0))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3438,f2388]) ).
fof(f3444,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f3442,f2381]) ).
fof(f3447,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3444,f2391]) ).
fof(f3448,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f3447]) ).
fof(f3451,plain,
( ! [X0] :
( 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3448,f2391]) ).
fof(f3452,plain,
( ! [X0] :
( 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f3451]) ).
fof(f3455,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s(s(s('0')))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3452,f2972]) ).
fof(f3459,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s(s(s('0')))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f3455]) ).
fof(f3461,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X2),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f3459,f3444]) ).
fof(f3463,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3461,f2391]) ).
fof(f3464,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f3463]) ).
fof(f3467,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0')))))
| 'LE'(f(X0),s(s(s(s('0'))))) )
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3464,f2391]) ).
fof(f3468,plain,
( ! [X0] : 'LE'(f(X0),s(s(s(s('0')))))
| ~ spl0_38
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f3467]) ).
fof(f3470,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X0)) )
| ~ spl0_17
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3468,f1228]) ).
fof(f3471,plain,
( ! [X0] :
( 'E'(s(s(s('0'))),f(suc(X0)))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3468,f1290]) ).
fof(f3472,plain,
( ! [X0] :
( 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3468,f1387]) ).
fof(f3477,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X0))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3472,f190]) ).
fof(f3486,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3472,f678]) ).
fof(f3501,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2)))) )
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3472,f1555]) ).
fof(f3604,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X2)))) )
| ~ spl0_17
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3501,f3470]) ).
fof(f3619,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_17
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3486,f3470]) ).
fof(f3628,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_17
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3477,f3470]) ).
fof(f3651,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3604,f3471]) ).
fof(f3666,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X1))))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3619,f3471]) ).
fof(f3675,plain,
( ! [X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s(s(s('0'))))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3628,f3471]) ).
fof(f3729,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(s(s(s('0'))),f(X0))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46 ),
inference(resolution,[],[f3471,f148]) ).
fof(f3787,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f3729,f3470]) ).
fof(f3841,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3787,f3675]) ).
fof(f3846,plain,
( ! [X0] :
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3841,f1310]) ).
fof(f3847,plain,
( ! [X0] :
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0)))) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3841,f1274]) ).
fof(f3886,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3651,f3472]) ).
fof(f3889,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3886,f3470]) ).
fof(f3890,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(suc(X0))))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3889,f3471]) ).
fof(f3891,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3890,f3472]) ).
fof(f3894,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3891,f3470]) ).
fof(f3895,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3894,f3471]) ).
fof(f3954,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3666,f3472]) ).
fof(f3957,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3954,f3470]) ).
fof(f3958,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3957,f3471]) ).
fof(f3960,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f3958,f3471]) ).
fof(f3961,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3960,f3895]) ).
fof(f3963,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X0),s(s(s('0'))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f3961,f3470]) ).
fof(f4619,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f1674,f3472]) ).
fof(f4623,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f4619,f3470]) ).
fof(f4624,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ 'E'(s(s(s('0'))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X0))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f4623,f3471]) ).
fof(f4628,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(X0))
| ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f4624,f3471]) ).
fof(f4629,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s(s('0'))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f4628,f3470]) ).
fof(f5182,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s(s(s('0'))),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f4629,f3471]) ).
fof(f5184,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5182,f3470]) ).
fof(f5188,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5184,f3841]) ).
fof(f5197,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f5188]) ).
fof(f5204,plain,
( ! [X0] :
( 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5197,f3841]) ).
fof(f5213,plain,
( ! [X0] :
( 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f5204]) ).
fof(f5224,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5213,f3963]) ).
fof(f5227,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s(s('0'))))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),s(s(s('0'))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f5224]) ).
fof(f5231,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0'))))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X2),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5227,f5197]) ).
fof(f5236,plain,
( ! [X0,X1] :
( 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0'))))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X1),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5231,f3841]) ).
fof(f5245,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f5236]) ).
fof(f5252,plain,
( ! [X0] :
( 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0'))))
| 'LE'(f(X0),s(s(s('0')))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5245,f3841]) ).
fof(f5255,plain,
( ! [X0] :
( 'LE'(f(suc(suc(X0))),s(s(s('0'))))
| 'LE'(f(suc(suc(X0))),s(s(s('0'))))
| 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0)))) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5245,f3847]) ).
fof(f5256,plain,
( ! [X0] :
( 'LE'(f(suc(X0)),s(s(s('0'))))
| 'LE'(f(suc(X0)),s(s(s('0'))))
| 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5245,f3846]) ).
fof(f5257,plain,
( ! [X0] :
( 'LE'(f(suc(X0)),s(s(s('0'))))
| 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(X0))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f5256]) ).
fof(f5258,plain,
( ! [X0] :
( 'LE'(f(suc(suc(X0))),s(s(s('0'))))
| 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(suc(suc(X0)))) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f5255]) ).
fof(f5261,plain,
( ! [X0] : 'LE'(f(X0),s(s(s('0'))))
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f5252]) ).
fof(f5264,plain,
( ! [X0] :
( 'E'(s(s('0')),f(suc(X0)))
| 'LE'(f(X0),s(s('0'))) )
| ~ spl0_17
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5257,f1310]) ).
fof(f5265,plain,
( ! [X0] :
( 'E'(s(s('0')),f(suc(suc(X0))))
| 'LE'(f(X0),s(s('0'))) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5258,f1274]) ).
fof(f5266,plain,
( ! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'E'(s(s('0')),f(X0)) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5261,f1173]) ).
fof(f5278,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X1)) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5265,f982]) ).
fof(f5292,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X0))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5265,f1825]) ).
fof(f5295,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5265,f1979]) ).
fof(f5299,plain,
( ! [X0] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5265,f2091]) ).
fof(f5301,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X0))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5265,f2225]) ).
fof(f5302,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5265,f2316]) ).
fof(f5427,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5302,f5266]) ).
fof(f5428,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5301,f5266]) ).
fof(f5430,plain,
( ! [X0] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5299,f5266]) ).
fof(f5434,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5295,f5266]) ).
fof(f5437,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5292,f5266]) ).
fof(f5451,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X1)) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5278,f5266]) ).
fof(f5490,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5427,f5264]) ).
fof(f5491,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5428,f5264]) ).
fof(f5493,plain,
( ! [X0] :
( 'LE'(f(X0),s(s('0')))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5430,f5264]) ).
fof(f5497,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5434,f5264]) ).
fof(f5500,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5437,f5264]) ).
fof(f5514,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X1)) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5451,f5264]) ).
fof(f5525,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(s(s('0')),f(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X0),s(s('0')))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5500,f5491]) ).
fof(f5529,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s(s('0')),f(X1)) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5514,f5490]) ).
fof(f5534,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X2))))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(suc(X1))))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'(s(s('0')),f(suc(X2)))
| 'LE'(f(X0),s(s('0')))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X1)) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5529,f5497]) ).
fof(f5536,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| iLEQ(suc(X0),suc(X0))
| 'E'(s('0'),f(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5493,f1184]) ).
fof(f5537,plain,
( ! [X0] :
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0))) )
| ~ spl0_2
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5493,f1221]) ).
fof(f5793,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| 'LE'(f(X1),s(s('0')))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X2))
| ~ 'E'(s(s('0')),f(X0))
| 'LE'(f(X2),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5534,f5265]) ).
fof(f5796,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(suc(X2)))
| 'LE'(f(X1),s(s('0')))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X0))
| 'LE'(f(X2),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5793,f5266]) ).
fof(f5797,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s(s('0')),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X1),s(s('0')))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s(s('0')),f(X0))
| 'LE'(f(X2),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f5796,f5264]) ).
fof(f6095,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X0),s(s('0')))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(s(s('0')),f(X1))
| 'LE'(f(X2),s(s('0')))
| 'LE'(f(X1),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5797,f5265]) ).
fof(f6099,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X0),s(s('0')))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X2),s(s('0')))
| 'LE'(f(X1),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6095,f5266]) ).
fof(f6100,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X0),s(s('0')))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X2),s(s('0')))
| 'LE'(f(X1),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6099,f5264]) ).
fof(f6183,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X2),s(s('0')))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s(s('0')),f(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f5525,f5265]) ).
fof(f6187,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ 'E'(s(s('0')),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X2),s(s('0')))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6183,f5266]) ).
fof(f6188,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(suc(X0)))
| ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X2),s(s('0')))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6187,f5264]) ).
fof(f6233,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s(s('0')),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X2),s(s('0')))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s('0')))
| 'LE'(f(X0),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6188,f5264]) ).
fof(f6234,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X2),s(s('0')))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),s(s('0')))
| 'LE'(f(X0),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6233,f5266]) ).
fof(f6236,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X2),s(s('0')))
| ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X1),s(s('0')))
| 'LE'(f(X0),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6234,f6100]) ).
fof(f6242,plain,
( ! [X0,X1] :
( 'LE'(f(X0),s(s('0')))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X0),s(s('0')))
| 'LE'(f(X1),s(s('0')))
| 'LE'(f(X0),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6236,f5493]) ).
fof(f6253,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X0),s(s('0')))
| 'LE'(f(X1),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f6242]) ).
fof(f6266,plain,
( ! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'LE'(f(X0),s(s('0')))
| 'LE'(f(X0),s(s('0'))) )
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6253,f5493]) ).
fof(f6267,plain,
( ! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'LE'(f(X0),s(s('0')))
| 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6253,f5536]) ).
fof(f6270,plain,
( ! [X0] :
( 'LE'(f(suc(X0)),s(s('0')))
| 'LE'(f(suc(X0)),s(s('0')))
| 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0))) )
| ~ spl0_2
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6253,f5537]) ).
fof(f6273,plain,
( ! [X0] :
( 'LE'(f(suc(X0)),s(s('0')))
| 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(suc(X0))) )
| ~ spl0_2
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f6270]) ).
fof(f6276,plain,
( ! [X0] :
( 'LE'(f(X0),s(s('0')))
| 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f6267]) ).
fof(f6277,plain,
( ! [X0] : 'LE'(f(X0),s(s('0')))
| ~ spl0_2
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f6266]) ).
fof(f6283,plain,
( ! [X0] :
( 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6273,f1221]) ).
fof(f6284,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(s('0'),f(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6276,f1184]) ).
fof(f6286,plain,
( ! [X0] :
( 'E'(s('0'),f(suc(suc(X0))))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6277,f1195]) ).
fof(f6289,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6286,f708]) ).
fof(f6299,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6286,f1921]) ).
fof(f6300,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6286,f1929]) ).
fof(f6302,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0)) )
| ~ spl0_2
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6286,f2001]) ).
fof(f6303,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6286,f2023]) ).
fof(f6436,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6303,f6284]) ).
fof(f6437,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6302,f6284]) ).
fof(f6439,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6300,f6284]) ).
fof(f6440,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6299,f6284]) ).
fof(f6450,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6289,f6284]) ).
fof(f6491,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6436,f6283]) ).
fof(f6492,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X2))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6437,f6283]) ).
fof(f6494,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6439,f6283]) ).
fof(f6495,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| ~ iLEQ(suc(X0),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6440,f6283]) ).
fof(f6505,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6450,f6283]) ).
fof(f6513,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X1))))
| ~ 'E'(s('0'),f(suc(X2)))
| 'LE'(f(X0),s('0'))
| ~ 'E'(s('0'),f(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X2))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f6505,f6494]) ).
fof(f6515,plain,
( ! [X0] :
( iLEQ(suc(X0),suc(X0))
| 'LE'(f(X0),'0')
| 'E'('0',f(X0)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6491,f1177]) ).
fof(f7038,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(s('0'),f(X1))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X2),s('0'))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X2))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6492,f6286]) ).
fof(f7043,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(s('0'),f(suc(X1)))
| ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X2),s('0'))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X2))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7038,f6284]) ).
fof(f7044,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X2),s('0'))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X2))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7043,f6283]) ).
fof(f7074,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X1),s('0'))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6513,f6286]) ).
fof(f7079,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X1),s('0'))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'(s('0'),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7074,f6284]) ).
fof(f7080,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X1),s('0'))
| ~ 'E'(s('0'),f(X0))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7079,f6283]) ).
fof(f7142,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X2),s('0'))
| ~ 'E'(s('0'),f(X0))
| ~ iLEQ(suc(X0),suc(X2))
| 'LE'(f(X1),s('0'))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7044,f6286]) ).
fof(f7147,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X1))
| ~ 'E'(s('0'),f(suc(X0)))
| 'LE'(f(X2),s('0'))
| ~ iLEQ(suc(X0),suc(X2))
| 'LE'(f(X1),s('0'))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7142,f6284]) ).
fof(f7148,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X1))
| 'LE'(f(X2),s('0'))
| ~ iLEQ(suc(X0),suc(X2))
| 'LE'(f(X1),s('0'))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7147,f6283]) ).
fof(f7227,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'LE'(f(X1),s('0'))
| ~ 'E'(s('0'),f(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f6495,f6283]) ).
fof(f7229,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'LE'(f(X1),s('0'))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7227,f6284]) ).
fof(f7231,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(suc(X0)))
| ~ 'E'(s('0'),f(X0))
| 'LE'(f(X1),s('0'))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7229,f7080]) ).
fof(f7235,plain,
( ! [X2,X0,X1] :
( ~ 'E'(s('0'),f(X0))
| 'LE'(f(X1),s('0'))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s('0'))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7231,f6283]) ).
fof(f7237,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X1),s('0'))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X2),s('0'))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7235,f6284]) ).
fof(f7247,plain,
( ! [X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X1),s('0'))
| 'LE'(f(X1),s('0'))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7237,f6491]) ).
fof(f7256,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X0),s('0'))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7247]) ).
fof(f7274,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s('0'))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7256,f6491]) ).
fof(f7283,plain,
( ! [X0] :
( 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7274]) ).
fof(f7302,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X2),s('0'))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X0),s('0'))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7283,f7148]) ).
fof(f7309,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),s('0'))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X2),s('0'))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7302]) ).
fof(f7311,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X0),s('0'))
| 'LE'(f(X2),s('0'))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7309,f7283]) ).
fof(f7339,plain,
( ! [X0,X1] :
( 'LE'(f(X0),s('0'))
| 'LE'(f(X0),s('0'))
| ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X1),s('0'))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7311,f6491]) ).
fof(f7348,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X1),suc(X0))
| 'LE'(f(X0),s('0'))
| 'LE'(f(X1),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7339]) ).
fof(f7366,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| 'LE'(f(X0),s('0'))
| 'LE'(f(X0),s('0')) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7348,f6491]) ).
fof(f7367,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| 'LE'(f(X0),s('0'))
| 'LE'(f(X0),'0')
| 'E'('0',f(X0)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7348,f6515]) ).
fof(f7374,plain,
( ! [X0] :
( 'LE'(f(X0),s('0'))
| 'LE'(f(X0),'0')
| 'E'('0',f(X0)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7367]) ).
fof(f7375,plain,
( ! [X0] : 'LE'(f(X0),s('0'))
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7366]) ).
fof(f7384,plain,
( ! [X0] :
( 'LE'(f(X0),'0')
| 'E'('0',f(X0)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7374,f1177]) ).
fof(f7386,plain,
( ! [X0] :
( 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7375,f1282]) ).
fof(f7387,plain,
( ! [X0] :
( 'E'('0',f(suc(X0)))
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7375,f1210]) ).
fof(f7389,plain,
( ! [X0] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7386,f720]) ).
fof(f7393,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7386,f1517]) ).
fof(f7396,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7386,f2051]) ).
fof(f7397,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7386,f2229]) ).
fof(f7476,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0))) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7397,f7384]) ).
fof(f7477,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7396,f7384]) ).
fof(f7480,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7393,f7384]) ).
fof(f7484,plain,
( ! [X0] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7389,f7384]) ).
fof(f7515,plain,
( ! [X2,X0,X1] :
( ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| 'LE'(f(X0),'0')
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7476,f7387]) ).
fof(f7516,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2))) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7477,f7387]) ).
fof(f7519,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7480,f7387]) ).
fof(f7523,plain,
( ! [X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),'0')
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7484,f7387]) ).
fof(f7525,plain,
( ! [X2,X0,X1] :
( ~ 'E'('0',f(suc(suc(X2))))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| 'LE'(f(X0),'0')
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X2))
| 'E'(f(X1),f(suc(X1))) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7519,f7516]) ).
fof(f7527,plain,
( ! [X0] :
( 'LE'(f(X0),'0')
| iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7523,f581]) ).
fof(f7535,plain,
( ! [X0] :
( 'LE'(f(X0),'0')
| iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0)) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7527]) ).
fof(f7536,plain,
( ! [X0] :
( 'LE'(f(X0),'0')
| iLEQ(suc(X0),suc(X0))
| ~ 'E'('0',f(suc(X0))) )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7535,f7384]) ).
fof(f7537,plain,
( ! [X0] :
( iLEQ(suc(X0),suc(X0))
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7536,f7387]) ).
fof(f7732,plain,
( ! [X2,X0,X1] :
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7515,f7386]) ).
fof(f7735,plain,
( ! [X2,X0,X1] :
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7732,f7384]) ).
fof(f7736,plain,
( ! [X2,X0,X1] :
( ~ 'E'('0',f(suc(suc(X0))))
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7735,f7387]) ).
fof(f7737,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(X1))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X2),'0')
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7736,f7386]) ).
fof(f7740,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X2),'0')
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7737,f7384]) ).
fof(f7741,plain,
( ! [X2,X0,X1] :
( ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),'0')
| ~ iLEQ(suc(X2),suc(X0))
| 'LE'(f(X2),'0')
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7740,f7387]) ).
fof(f7750,plain,
( ! [X2,X0,X1] :
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7525,f7386]) ).
fof(f7753,plain,
( ! [X2,X0,X1] :
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X1)))
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7750,f7384]) ).
fof(f7754,plain,
( ! [X2,X0,X1] :
( ~ 'E'('0',f(suc(X0)))
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X1),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7753,f7387]) ).
fof(f7756,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ iLEQ(suc(X1),suc(X2))
| ~ 'E'('0',f(X1))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),'0')
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7754,f7387]) ).
fof(f7757,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X0),'0')
| 'E'(f(X1),f(suc(X1)))
| 'LE'(f(X2),'0')
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7756,f7384]) ).
fof(f7769,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),'0')
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X1),'0')
| 'LE'(f(X0),'0')
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7757,f7537]) ).
fof(f7776,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),'0')
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7769]) ).
fof(f7797,plain,
( ! [X0] :
( 'LE'(f(X0),'0')
| 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),'0')
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7776,f7537]) ).
fof(f7804,plain,
( ! [X0] :
( 'E'(f(X0),f(suc(X0)))
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7797]) ).
fof(f7829,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),'0')
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7804,f7741]) ).
fof(f7830,plain,
( ! [X2,X0,X1] :
( 'LE'(f(X0),'0')
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'(f(X2),f(suc(X2)))
| 'LE'(f(X2),'0')
| ~ iLEQ(suc(X1),suc(X2))
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7829]) ).
fof(f7832,plain,
( ! [X2,X0,X1] :
( ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X2),'0')
| 'LE'(f(X0),'0')
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f7830,f7804]) ).
fof(f7843,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),'0')
| 'LE'(f(X0),'0')
| 'LE'(f(X1),'0')
| 'LE'(f(X1),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7832,f7537]) ).
fof(f7850,plain,
( ! [X0,X1] :
( ~ iLEQ(suc(X0),suc(X1))
| 'LE'(f(X1),'0')
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7843]) ).
fof(f7871,plain,
( ! [X0] :
( 'LE'(f(X0),'0')
| 'LE'(f(X0),'0')
| 'LE'(f(X0),'0') )
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7850,f7537]) ).
fof(f7878,plain,
( ! [X0] : 'LE'(f(X0),'0')
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f7871]) ).
fof(f7889,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| spl0_21
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(resolution,[],[f7878,f1247]) ).
fof(f7890,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| spl0_21
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f7889]) ).
cnf(s53,plain,
spl0_12,
inference(sat_conversion,[],[f1384]) ).
cnf(s78,plain,
spl0_17,
inference(sat_conversion,[],[f1451]) ).
cnf(s142,plain,
spl0_28,
inference(sat_conversion,[],[f1569]) ).
cnf(s150,plain,
spl0_46,
inference(sat_conversion,[],[f1582]) ).
cnf(s252,plain,
spl0_15,
inference(sat_conversion,[],[f1747]) ).
cnf(s270,plain,
spl0_30,
inference(sat_conversion,[],[f1775]) ).
cnf(s303,plain,
spl0_38,
inference(sat_conversion,[],[f1833]) ).
cnf(s327,plain,
spl0_8,
inference(sat_conversion,[],[f1871]) ).
cnf(s348,plain,
spl0_2,
inference(sat_conversion,[],[f1904]) ).
cnf(s415,plain,
~ spl0_21,
inference(sat_conversion,[],[f2017]) ).
cnf(s489,plain,
spl0_3,
inference(sat_conversion,[],[f2131]) ).
cnf(s518,plain,
spl0_32,
inference(sat_conversion,[],[f2190]) ).
cnf(s529,plain,
spl0_5,
inference(sat_conversion,[],[f2203]) ).
cnf(s538,plain,
spl0_55,
inference(sat_conversion,[],[f2217]) ).
cnf(s541,plain,
spl0_37,
inference(sat_conversion,[],[f2220]) ).
cnf(s616,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_8
| ~ spl0_12
| ~ spl0_15
| ~ spl0_17
| spl0_21
| ~ spl0_28
| ~ spl0_30
| ~ spl0_32
| ~ spl0_37
| ~ spl0_38
| ~ spl0_46
| ~ spl0_55 ),
inference(sat_conversion,[],[f7890]) ).
cnf(s617,plain,
~ spl0_12,
inference(rat,[],[s616,s538,s150,s303,s541,s518,s270,s142,s415,s252,s327,s348,s489,s529,s78]) ).
cnf(s681,plain,
$false,
inference(rat,[],[s53,s617]) ).
fof(f7891,plain,
$false,
inference(avatar_sat_refutation,[],[s681]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO688-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 18:05:28 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/1.98 % (2642721)Input is clausal, will run a generic CNF schedule.
% 8.37/1.98 % (2642732)dis-21_1_sil=8000:lcm=predicate:random_seed=2558647683:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 8.37/1.98 % (2642727)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=283020222:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.37/1.98 % (2642732)Instruction limit reached!
% 8.37/1.98 % (2642732)------------------------------
% 8.37/1.98 % (2642732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.37/1.98 % (2642732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.98 % (2642732)CaDiCaL version: 2.1.3
% 8.37/1.98 % (2642732)Termination reason: Instruction limit
% 8.37/1.98 % (2642732)Termination phase: Saturation
% 8.37/1.98 % (2642732)Time elapsed: 0.028 s
% 8.37/1.98 % (2642732)Peak memory usage: 89 MB
% 8.37/1.98 % (2642732)Instructions burned: 118 (million)
% 8.37/1.98 % (2642731)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3312657362:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.37/1.98 % (2642729)lrs+10_1_sil=8000:sp=occurrence:random_seed=158699932:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.37/1.98 % (2642726)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3327988133:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.37/1.98 % (2642730)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1239491463:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.37/1.98 % (2642728)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2545777882:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.37/1.98 % (2642729)Refutation not found, incomplete strategy
% 8.37/1.98 % (2642729)------------------------------
% 8.37/1.98 % (2642729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.37/1.98 % (2642729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.98 % (2642729)CaDiCaL version: 2.1.3
% 8.37/1.98 % (2642729)Termination reason: Refutation not found, incomplete strategy
% 8.37/1.98 % (2642729)Time elapsed: 0.009 s
% 8.37/1.98 % (2642729)Peak memory usage: 88 MB
% 8.37/1.98 % (2642729)Instructions burned: 17 (million)
% 8.37/1.98 % (2642730)Refutation not found, incomplete strategy
% 8.37/1.98 % (2642730)------------------------------
% 8.37/1.98 % (2642730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.37/1.98 % (2642730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.98 % (2642730)CaDiCaL version: 2.1.3
% 8.37/1.98 % (2642730)Termination reason: Refutation not found, incomplete strategy
% 8.37/1.98 % (2642730)Time elapsed: 0.013 s
% 8.37/1.98 % (2642730)Peak memory usage: 88 MB
% 8.37/1.98 % (2642730)Instructions burned: 25 (million)
% 8.37/1.98 % (2642731)Instruction limit reached!
% 8.37/1.98 % (2642731)------------------------------
% 8.37/1.98 % (2642731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.37/1.98 % (2642731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.98 % (2642731)CaDiCaL version: 2.1.3
% 8.37/1.98 % (2642731)Termination reason: Instruction limit
% 8.37/1.98 % (2642731)Termination phase: Saturation
% 8.37/1.98 % (2642731)Time elapsed: 0.072 s
% 8.37/1.98 % (2642731)Peak memory usage: 89 MB
% 8.37/1.98 % (2642731)Instructions burned: 181 (million)
% 8.37/1.98 % (2642740)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2318384743:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.37/1.98 % (2642740)Refutation not found, incomplete strategy
% 8.37/1.98 % (2642740)------------------------------
% 8.37/1.98 % (2642740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.37/1.98 % (2642740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.37/1.98 % (2642740)CaDiCaL version: 2.1.3
% 8.37/1.98 % (2642740)Termination reason: Refutation not found, incomplete strategy
% 8.37/1.98 % (2642740)Time elapsed: 0.005 s
% 8.37/1.98 % (2642740)Peak memory usage: 88 MB
% 8.37/1.98 % (2642740)Instructions burned: 17 (million)
% 8.37/1.98 % (2642741)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2365547560:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 8.72/2.40 % (2642740)------------------------------
% 8.72/2.40 % (2642740)------------------------------
% 8.72/2.40 % (2642741)Refutation not found, incomplete strategy
% 8.72/2.40 % (2642741)------------------------------
% 8.72/2.40 % (2642741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642741)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642741)Termination reason: Refutation not found, incomplete strategy
% 8.72/2.40 % (2642741)Time elapsed: 0.026 s
% 8.72/2.40 % (2642741)Peak memory usage: 88 MB
% 8.72/2.40 % (2642741)Instructions burned: 50 (million)
% 8.72/2.40 % (2642729)------------------------------
% 8.72/2.40 % (2642729)------------------------------
% 8.72/2.40 % (2642730)------------------------------
% 8.72/2.40 % (2642730)------------------------------
% 8.72/2.40 % (2642744)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=916138239:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 8.72/2.40 % (2642744)Refutation not found, incomplete strategy
% 8.72/2.40 % (2642744)------------------------------
% 8.72/2.40 % (2642744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642744)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642744)Termination reason: Refutation not found, incomplete strategy
% 8.72/2.40 % (2642744)Time elapsed: 0.007 s
% 8.72/2.40 % (2642744)Peak memory usage: 88 MB
% 8.72/2.40 % (2642744)Instructions burned: 25 (million)
% 8.72/2.40 % (2642745)lrs+10_64_to=lpo:sil=8000:random_seed=2862983638:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 8.72/2.40 % (2642746)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2645217376:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 8.72/2.40 % (2642745)Instruction limit reached!
% 8.72/2.40 % (2642745)------------------------------
% 8.72/2.40 % (2642745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642745)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642745)Termination reason: Instruction limit
% 8.72/2.40 % (2642745)Termination phase: Saturation
% 8.72/2.40 % (2642745)Time elapsed: 0.071 s
% 8.72/2.40 % (2642745)Peak memory usage: 89 MB
% 8.72/2.40 % (2642745)Instructions burned: 126 (million)
% 8.72/2.40 % (2642744)------------------------------
% 8.72/2.40 % (2642744)------------------------------
% 8.72/2.40 % (2642741)------------------------------
% 8.72/2.40 % (2642741)------------------------------
% 8.72/2.40 % (2642746)Instruction limit reached!
% 8.72/2.40 % (2642746)------------------------------
% 8.72/2.40 % (2642746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642746)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642746)Termination reason: Instruction limit
% 8.72/2.40 % (2642746)Termination phase: Saturation
% 8.72/2.40 % (2642746)Time elapsed: 0.115 s
% 8.72/2.40 % (2642746)Peak memory usage: 90 MB
% 8.72/2.40 % (2642746)Instructions burned: 196 (million)
% 8.72/2.40 % (2642751)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3562667068:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 8.72/2.40 % (2642750)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2863234470:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 8.72/2.40 % (2642752)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=438924556:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 8.72/2.40 % (2642752)Refutation not found, incomplete strategy
% 8.72/2.40 % (2642752)------------------------------
% 8.72/2.40 % (2642752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642752)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642752)Termination reason: Refutation not found, incomplete strategy
% 8.72/2.40 % (2642752)Time elapsed: 0.018 s
% 8.72/2.40 % (2642752)Peak memory usage: 88 MB
% 8.72/2.40 % (2642752)Instructions burned: 33 (million)
% 8.72/2.40 % (2642753)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1207033738:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 8.72/2.40 % (2642750)Instruction limit reached!
% 8.72/2.40 % (2642750)------------------------------
% 8.72/2.40 % (2642750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642750)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642750)Termination reason: Instruction limit
% 8.72/2.40 % (2642750)Termination phase: Saturation
% 8.72/2.40 % (2642750)Time elapsed: 0.074 s
% 8.72/2.40 % (2642750)Peak memory usage: 89 MB
% 8.72/2.40 % (2642750)Instructions burned: 159 (million)
% 8.72/2.40 % (2642753)Refutation not found, incomplete strategy
% 8.72/2.40 % (2642753)------------------------------
% 8.72/2.40 % (2642753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642753)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642753)Termination reason: Refutation not found, incomplete strategy
% 8.72/2.40 % (2642753)Time elapsed: 0.045 s
% 8.72/2.40 % (2642753)Peak memory usage: 91 MB
% 8.72/2.40 % (2642753)Instructions burned: 86 (million)
% 8.72/2.40 % (2642758)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3492208992:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 8.72/2.40 % (2642752)------------------------------
% 8.72/2.40 % (2642752)------------------------------
% 8.72/2.40 % (2642758)Instruction limit reached!
% 8.72/2.40 % (2642758)------------------------------
% 8.72/2.40 % (2642758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642758)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642758)Termination reason: Instruction limit
% 8.72/2.40 % (2642758)Termination phase: Saturation
% 8.72/2.40 % (2642758)Time elapsed: 0.103 s
% 8.72/2.40 % (2642758)Peak memory usage: 89 MB
% 8.72/2.40 % (2642758)Instructions burned: 242 (million)
% 8.72/2.40 % (2642727)Refutation not found, incomplete strategy
% 8.72/2.40 % (2642727)------------------------------
% 8.72/2.40 % (2642727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.40 % (2642727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.40 % (2642727)CaDiCaL version: 2.1.3
% 8.72/2.40 % (2642727)Termination reason: Refutation not found, incomplete strategy
% 8.72/2.40 % (2642727)Time elapsed: 0.957 s
% 8.72/2.40 % (2642727)Peak memory usage: 144 MB
% 8.72/2.40 % (2642727)Instructions burned: 1522 (million)
% 8.72/2.40 % (2642753)------------------------------
% 8.72/2.40 % (2642753)------------------------------
% 8.72/2.40 % (2642760)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=534300873:cond=fast:i=5208:av=off_2988 on theBenchmark for (2988ds/5208Mi)
% 8.72/2.40 % (2642761)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2903286799:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 8.72/2.40 % (2642761)Refutation not found, incomplete strategy
% 8.72/2.41 % (2642761)------------------------------
% 8.72/2.41 % (2642761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.41 % (2642761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.41 % (2642761)CaDiCaL version: 2.1.3
% 8.72/2.41 % (2642761)Termination reason: Refutation not found, incomplete strategy
% 8.72/2.41 % (2642761)Time elapsed: 0.010 s
% 8.72/2.41 % (2642761)Peak memory usage: 88 MB
% 8.72/2.41 % (2642761)Instructions burned: 17 (million)
% 8.72/2.41 % (2642762)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2265831522:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 8.72/2.41 % (2642727)------------------------------
% 8.72/2.41 % (2642727)------------------------------
% 8.72/2.41 % (2642761)------------------------------
% 8.72/2.41 % (2642761)------------------------------
% 8.72/2.41 % (2642766)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1747793099:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 8.72/2.41 % (2642762)Instruction limit reached!
% 8.72/2.41 % (2642762)------------------------------
% 8.72/2.41 % (2642762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.41 % (2642762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.41 % (2642762)CaDiCaL version: 2.1.3
% 8.72/2.41 % (2642762)Termination reason: Instruction limit
% 8.72/2.41 % (2642762)Termination phase: Saturation
% 8.72/2.41 % (2642762)Time elapsed: 0.276 s
% 8.72/2.41 % (2642762)Peak memory usage: 92 MB
% 8.72/2.41 % (2642762)Instructions burned: 500 (million)
% 8.72/2.41 % (2642767)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=146440476:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 8.72/2.41 % (2642766)Instruction limit reached!
% 8.72/2.41 % (2642766)------------------------------
% 8.72/2.41 % (2642766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.41 % (2642766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.41 % (2642766)CaDiCaL version: 2.1.3
% 8.72/2.41 % (2642766)Termination reason: Instruction limit
% 8.72/2.41 % (2642766)Termination phase: Saturation
% 8.72/2.41 % (2642766)Time elapsed: 0.108 s
% 8.72/2.41 % (2642766)Peak memory usage: 90 MB
% 8.72/2.41 % (2642766)Instructions burned: 192 (million)
% 8.72/2.41 % (2642769)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1393723008:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 8.72/2.41 % (2642769)Instruction limit reached!
% 8.72/2.41 % (2642769)------------------------------
% 8.72/2.41 % (2642769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.41 % (2642769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.41 % (2642769)CaDiCaL version: 2.1.3
% 8.72/2.41 % (2642769)Termination reason: Instruction limit
% 8.72/2.41 % (2642769)Termination phase: Saturation
% 8.72/2.41 % (2642769)Time elapsed: 0.064 s
% 8.72/2.41 % (2642769)Peak memory usage: 88 MB
% 8.72/2.41 % (2642769)Instructions burned: 157 (million)
% 8.72/2.41 % (2642771)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3272060735:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 8.72/2.41 % (2642767)Instruction limit reached!
% 8.72/2.41 % (2642767)------------------------------
% 8.72/2.41 % (2642767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.41 % (2642767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.41 % (2642767)CaDiCaL version: 2.1.3
% 8.72/2.41 % (2642767)Termination reason: Instruction limit
% 8.72/2.41 % (2642767)Termination phase: Saturation
% 8.72/2.41 % (2642767)Time elapsed: 0.143 s
% 8.72/2.41 % (2642767)Peak memory usage: 91 MB
% 8.72/2.41 % (2642767)Instructions burned: 265 (million)
% 8.72/2.41 % (2642751)First to succeed.
% 8.72/2.41 % (2642751)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2642721"
% 8.72/2.41 % (2642773)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4078678069:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 8.72/2.41 % (2642775)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1948453487:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi)
% 8.72/2.41 % (2642726)Also succeeded, but the first one will report.
% 8.72/2.41 % (2642751)Refutation found. Thanks to Tanya!
% 8.72/2.41 % SZS status Unsatisfiable for theBenchmark
% 8.72/2.41 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/2.60 % (2642751)------------------------------
% 0.18/2.60 % (2642751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/2.60 % (2642751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/2.60 % (2642751)CaDiCaL version: 2.1.3
% 0.18/2.60 % (2642751)Termination reason: Refutation
% 0.18/2.60 % (2642751)Time elapsed: 1.048 s
% 0.18/2.60 % (2642751)Peak memory usage: 144 MB
% 0.18/2.60 % (2642751)Instructions burned: 3210 (million)
% 0.18/2.60 % (2642751)------------------------------
% 0.18/2.60 % (2642751)------------------------------
% 0.18/2.60 % (2642721)Success in time 1.993 s
% 0.18/2.60 % Vampire exiting
%------------------------------------------------------------------------------