%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO647-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:28:30 PM UTC 2026
% Result : Unsatisfiable 13.71s 2.92s
% Output : Refutation 13.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 96
% Number of leaves : 7
% Syntax : Number of formulae : 116 ( 6 unt; 0 def)
% Number of atoms : 1826 ( 0 equ)
% Maximal formula atoms : 41 ( 15 avg)
% Number of connectives : 3223 (1513 ~;1710 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 21 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 1 con; 0-1 aty)
% Number of variables : 540 ( 540 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3293) ).
fof(f91,axiom,
! [X0] : 'E'('0',f(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6244) ).
fof(f101,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ 'E'('0',f(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4556) ).
fof(f113,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ iLEQ(suc(X2),suc(X4))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_433) ).
fof(f126,axiom,
! [X0] :
( ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6279) ).
fof(f501,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X4)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4547) ).
fof(f606,axiom,
! [X0] :
( ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| 'E'(f(X0),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6260) ).
fof(f734,plain,
! [X0] :
( ~ 'E'('0',f(suc(X0)))
| 'E'(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f126,f91]) ).
fof(f735,plain,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f734,f91]) ).
fof(f736,plain,
! [X0] :
( ~ 'E'('0',f(suc(X0)))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| 'E'(f(X0),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f606,f91]) ).
fof(f737,plain,
! [X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(X0))
| 'E'(f(X0),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f736,f91]) ).
fof(f738,plain,
! [X0] :
( ~ 'E'('0',f(X0))
| 'E'(f(X0),f(suc(suc(X0))))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f737,f735]) ).
fof(f739,plain,
! [X0] :
( iLEQ(suc(X0),suc(X0))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f738,f91]) ).
fof(f740,plain,
! [X0] :
( ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f11,f91]) ).
fof(f741,plain,
! [X0] :
( ~ 'E'('0',f(suc(suc(suc(X0)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f740,f739]) ).
fof(f742,plain,
! [X0] :
( ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f741,f91]) ).
fof(f743,plain,
! [X0] :
( ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f742,f735]) ).
fof(f744,plain,
! [X0] :
( ~ 'E'('0',f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f743,f91]) ).
fof(f745,plain,
! [X0] : iLEQ(suc(X0),suc(X0)),
inference(forward_subsumption_resolution,[],[f744,f91]) ).
fof(f746,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f101,f91]) ).
fof(f747,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f746,f91]) ).
fof(f748,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f747,f91]) ).
fof(f749,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f748,f91]) ).
fof(f750,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f749,f91]) ).
fof(f751,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f750,f91]) ).
fof(f752,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f751,f91]) ).
fof(f753,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f752,f91]) ).
fof(f754,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f753,f91]) ).
fof(f755,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f754,f91]) ).
fof(f756,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| 'E'(f(X5),f(suc(X5))) ),
inference(forward_subsumption_resolution,[],[f755,f91]) ).
fof(f757,plain,
! [X2,X3,X0,X1,X4,X5] :
( 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ iLEQ(suc(X4),suc(X2))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(forward_subsumption_resolution,[],[f756,f91]) ).
fof(f761,plain,
! [X2,X3,X0,X1,X4] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X4),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X4),f(suc(X4)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X0)) ),
inference(factoring,[],[f757]) ).
fof(f763,plain,
! [X2,X3,X0,X1,X4] :
( 'E'(f(X4),f(suc(X4)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X4),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f761,f735]) ).
fof(f767,plain,
! [X2,X3,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X2),suc(X3)) ),
inference(factoring,[],[f763]) ).
fof(f768,plain,
! [X2,X3,X0,X1] :
( 'E'(f(X3),f(suc(X3)))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X2),f(suc(X2)))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X2),suc(X3)) ),
inference(forward_subsumption_resolution,[],[f767,f735]) ).
fof(f770,plain,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[],[f768]) ).
fof(f773,plain,
! [X2,X0,X1] :
( 'E'(f(X2),f(suc(X2)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X1),f(suc(X1)))
| 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f770,f735]) ).
fof(f774,plain,
! [X0,X1] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X0),suc(X0))
| 'E'(f(X1),f(suc(X1))) ),
inference(factoring,[],[f773]) ).
fof(f776,plain,
! [X0,X1] :
( 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(X0))) ),
inference(forward_subsumption_resolution,[],[f774,f735]) ).
fof(f777,plain,
! [X0] :
( 'E'(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[],[f776]) ).
fof(f778,plain,
! [X0] : 'E'(f(X0),f(suc(X0))),
inference(forward_subsumption_resolution,[],[f777,f735]) ).
fof(f779,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ iLEQ(suc(X2),suc(X4))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f113,f778]) ).
fof(f780,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ iLEQ(suc(X2),suc(X4))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f779,f91]) ).
fof(f781,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ iLEQ(suc(X2),suc(X4))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f780,f91]) ).
fof(f782,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ iLEQ(suc(X2),suc(X4))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f781,f91]) ).
fof(f783,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ iLEQ(suc(X2),suc(X4))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f782,f778]) ).
fof(f784,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f783,f778]) ).
fof(f785,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ 'E'('0',f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f784,f91]) ).
fof(f786,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f785,f91]) ).
fof(f787,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f786,f778]) ).
fof(f788,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f787,f91]) ).
fof(f789,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f788,f778]) ).
fof(f790,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f789,f91]) ).
fof(f791,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f790,f91]) ).
fof(f792,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X4))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f791,f91]) ).
fof(f793,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f792,f91]) ).
fof(f794,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f793,f778]) ).
fof(f795,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f794,f91]) ).
fof(f796,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(X4)))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f795,f91]) ).
fof(f797,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f796,f91]) ).
fof(f798,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f797,f91]) ).
fof(f799,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f798,f91]) ).
fof(f800,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(X2))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f799,f91]) ).
fof(f801,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ 'E'('0',f(suc(X5)))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| 'E'(f(X5),f(suc(suc(X5))))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f800,f91]) ).
fof(f802,plain,
! [X2,X3,X0,X1,X4,X5] :
( 'E'(f(X5),f(suc(suc(X5))))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X1),suc(X5))
| ~ iLEQ(suc(X4),suc(X3))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X4),f(suc(suc(X4))))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f801,f91]) ).
fof(f803,plain,
! [X2,X3,X0,X1,X4] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X4),suc(X1))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X4),f(suc(suc(X4))))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2)))) ),
inference(factoring,[],[f802]) ).
fof(f808,plain,
! [X2,X3,X0,X1,X4] :
( 'E'(f(X4),f(suc(suc(X4))))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X4),suc(X1))
| 'E'(f(X3),f(suc(suc(X3))))
| 'E'(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X1),f(suc(suc(X1))))
| 'E'(f(X2),f(suc(suc(X2)))) ),
inference(forward_subsumption_resolution,[],[f803,f739]) ).
fof(f811,plain,
! [X2,X3,X0,X1] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X1),suc(X3))
| 'E'(f(X1),f(suc(suc(X1)))) ),
inference(factoring,[],[f808]) ).
fof(f813,plain,
! [X2,X3,X0,X1] :
( 'E'(f(X3),f(suc(suc(X3))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X2),suc(X0))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X3))
| 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f811,f739]) ).
fof(f817,plain,
! [X2,X0,X1] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X2),f(suc(suc(X2))))
| 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[],[f813]) ).
fof(f818,plain,
! [X2,X0,X1] :
( 'E'(f(X2),f(suc(suc(X2))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X2),suc(X1))
| 'E'(f(X0),f(suc(suc(X0))))
| 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f817,f739]) ).
fof(f820,plain,
! [X0,X1] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X0),suc(X0))
| 'E'(f(X1),f(suc(suc(X1)))) ),
inference(factoring,[],[f818]) ).
fof(f821,plain,
! [X0,X1] :
( 'E'(f(X1),f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X1))
| 'E'(f(X0),f(suc(suc(X0)))) ),
inference(forward_subsumption_resolution,[],[f820,f739]) ).
fof(f822,plain,
! [X0] :
( 'E'(f(X0),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[],[f821]) ).
fof(f823,plain,
! [X0] : 'E'(f(X0),f(suc(suc(X0)))),
inference(forward_subsumption_resolution,[],[f822,f739]) ).
fof(f824,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ 'E'(f(X0),f(suc(suc(X0))))
| ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X4)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f501,f91]) ).
fof(f825,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ 'E'(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X4)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f824,f823]) ).
fof(f826,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ 'E'('0',f(suc(suc(X2))))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X4)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f825,f778]) ).
fof(f827,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(X1))
| ~ 'E'('0',f(suc(suc(suc(X4)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f826,f91]) ).
fof(f828,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X4)))))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f827,f91]) ).
fof(f829,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(X3))))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f828,f91]) ).
fof(f830,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X3)))))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f829,f91]) ).
fof(f831,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X3),f(suc(X3)))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f830,f91]) ).
fof(f832,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'('0',f(suc(suc(suc(X5)))))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f831,f778]) ).
fof(f833,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ 'E'(f(X5),f(suc(X5)))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f832,f91]) ).
fof(f834,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'(f(X2),f(suc(suc(X2))))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f833,f778]) ).
fof(f835,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'('0',f(suc(X3)))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f834,f823]) ).
fof(f836,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ 'E'('0',f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f835,f91]) ).
fof(f837,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X2)))))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f836,f91]) ).
fof(f838,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'(f(X0),f(suc(X0)))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f837,f91]) ).
fof(f839,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(X4))))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f838,f778]) ).
fof(f840,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'(f(X2),f(suc(X2)))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f839,f91]) ).
fof(f841,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(X3))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f840,f778]) ).
fof(f842,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(X0))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f841,f91]) ).
fof(f843,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(X2)))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f842,f91]) ).
fof(f844,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(X5))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f843,f91]) ).
fof(f845,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'(f(X4),f(suc(X4)))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f844,f91]) ).
fof(f846,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(X5))))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f845,f778]) ).
fof(f847,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'(f(X5),f(suc(suc(X5))))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f846,f91]) ).
fof(f848,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f847,f823]) ).
fof(f849,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(suc(X1)))))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f848,f91]) ).
fof(f850,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(X5)))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f849,f91]) ).
fof(f851,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(X1)))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f850,f91]) ).
fof(f852,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(X0))))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f851,f91]) ).
fof(f853,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(suc(X1))))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f852,f91]) ).
fof(f854,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(X2))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f853,f91]) ).
fof(f855,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'(f(X4),f(suc(suc(X4))))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f854,f91]) ).
fof(f856,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'(f(X3),f(suc(suc(X3))))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f855,f823]) ).
fof(f857,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ 'E'('0',f(suc(X4)))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f856,f823]) ).
fof(f858,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ iLEQ(suc(X5),suc(X3))
| ~ 'E'(f(X1),f(suc(suc(X1)))) ),
inference(forward_subsumption_resolution,[],[f857,f91]) ).
fof(f859,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ iLEQ(suc(X5),suc(X3))
| ~ iLEQ(suc(X3),suc(X1))
| ~ iLEQ(suc(X2),suc(X5))
| ~ iLEQ(suc(X0),suc(X4))
| ~ iLEQ(suc(X1),suc(X0)) ),
inference(forward_subsumption_resolution,[],[f858,f823]) ).
fof(f860,plain,
! [X2,X3,X0,X1,X4] :
( ~ iLEQ(suc(X3),suc(X4))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X3)) ),
inference(resolution,[],[f859,f745]) ).
fof(f863,plain,
! [X2,X3,X0,X1] :
( ~ iLEQ(suc(X2),suc(X3))
| ~ iLEQ(suc(X1),suc(X2))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[],[f860,f745]) ).
fof(f866,plain,
! [X2,X0,X1] :
( ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(resolution,[],[f863,f745]) ).
fof(f869,plain,
! [X0,X1] : ~ iLEQ(suc(X0),suc(X1)),
inference(resolution,[],[f866,f745]) ).
fof(f872,plain,
$false,
inference(resolution,[],[f869,f745]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO647-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n004.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:00:37 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.76/2.25 % (600602)Input is clausal, will run a generic CNF schedule.
% 9.76/2.25 % (600612)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=596468939:s2a=on:i=180:gtg=position_2997 on theBenchmark for (2997ds/180Mi)
% 9.76/2.25 % (600609)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4202744449:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2997 on theBenchmark for (2997ds/137899Mi)
% 9.76/2.25 % (600608)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2179540907:i=132376:av=off_2997 on theBenchmark for (2997ds/132376Mi)
% 9.76/2.25 % (600607)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=1646504830:i=140167_2997 on theBenchmark for (2997ds/140167Mi)
% 9.76/2.25 % (600611)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2976946852:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2997 on theBenchmark for (2997ds/114Mi)
% 9.76/2.25 % (600610)lrs+10_1_sil=8000:sp=occurrence:random_seed=2436881755:i=107:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/107Mi)
% 9.76/2.25 % (600612)Instruction limit reached!
% 9.76/2.25 % (600612)------------------------------
% 9.76/2.25 % (600612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.76/2.25 % (600612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/2.25 % (600612)CaDiCaL version: 2.1.3
% 9.76/2.25 % (600612)Termination reason: Instruction limit
% 9.76/2.25 % (600612)Termination phase: Property scanning
% 9.76/2.25 % (600612)Time elapsed: 0.034 s
% 9.76/2.25 % (600612)Peak memory usage: 88 MB
% 9.76/2.25 % (600612)Instructions burned: 184 (million)
% 9.76/2.25 % (600610)Refutation not found, incomplete strategy
% 9.76/2.25 % (600610)------------------------------
% 9.76/2.25 % (600610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.76/2.25 % (600610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/2.25 % (600610)CaDiCaL version: 2.1.3
% 9.76/2.25 % (600610)Termination reason: Refutation not found, incomplete strategy
% 9.76/2.25 % (600610)Time elapsed: 0.010 s
% 9.76/2.25 % (600610)Peak memory usage: 90 MB
% 9.76/2.25 % (600610)Instructions burned: 22 (million)
% 9.76/2.25 % (600613)dis-21_1_sil=8000:lcm=predicate:random_seed=3189282074:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/117Mi)
% 9.76/2.25 % (600611)Refutation not found, incomplete strategy
% 9.76/2.25 % (600611)------------------------------
% 9.76/2.25 % (600611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.76/2.25 % (600611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/2.25 % (600611)CaDiCaL version: 2.1.3
% 9.76/2.25 % (600611)Termination reason: Refutation not found, incomplete strategy
% 9.76/2.25 % (600611)Time elapsed: 0.014 s
% 9.76/2.25 % (600611)Peak memory usage: 90 MB
% 9.76/2.25 % (600611)Instructions burned: 33 (million)
% 9.76/2.25 % (600613)Instruction limit reached!
% 9.76/2.25 % (600613)------------------------------
% 9.76/2.25 % (600613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.76/2.25 % (600613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/2.25 % (600613)CaDiCaL version: 2.1.3
% 9.76/2.25 % (600613)Termination reason: Instruction limit
% 9.76/2.25 % (600613)Termination phase: Property scanning
% 9.76/2.25 % (600613)Time elapsed: 0.042 s
% 9.76/2.25 % (600613)Peak memory usage: 88 MB
% 9.76/2.25 % (600613)Instructions burned: 117 (million)
% 9.76/2.25 % (600620)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=2533255047:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 9.76/2.25 % (600620)Refutation not found, incomplete strategy
% 9.76/2.25 % (600620)------------------------------
% 9.76/2.25 % (600620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.76/2.25 % (600620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.76/2.25 % (600620)CaDiCaL version: 2.1.3
% 9.76/2.25 % (600620)Termination reason: Refutation not found, incomplete strategy
% 9.76/2.25 % (600620)Time elapsed: 0.005 s
% 9.76/2.25 % (600620)Peak memory usage: 90 MB
% 9.76/2.25 % (600620)Instructions burned: 22 (million)
% 9.76/2.25 % (600622)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=337418022:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 13.71/2.92 % (600622)Refutation not found, incomplete strategy
% 13.71/2.92 % (600622)------------------------------
% 13.71/2.92 % (600622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600622)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600622)Termination reason: Refutation not found, incomplete strategy
% 13.71/2.92 % (600622)Time elapsed: 0.027 s
% 13.71/2.92 % (600622)Peak memory usage: 90 MB
% 13.71/2.92 % (600622)Instructions burned: 67 (million)
% 13.71/2.92 % (600610)------------------------------
% 13.71/2.92 % (600610)------------------------------
% 13.71/2.92 % (600611)------------------------------
% 13.71/2.92 % (600611)------------------------------
% 13.71/2.92 % (600620)------------------------------
% 13.71/2.92 % (600620)------------------------------
% 13.71/2.92 % (600627)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=68286400:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 13.71/2.92 % (600627)Instruction limit reached!
% 13.71/2.92 % (600627)------------------------------
% 13.71/2.92 % (600627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600627)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600627)Termination reason: Instruction limit
% 13.71/2.92 % (600627)Termination phase: Saturation
% 13.71/2.92 % (600627)Time elapsed: 0.042 s
% 13.71/2.92 % (600627)Peak memory usage: 90 MB
% 13.71/2.92 % (600627)Instructions burned: 198 (million)
% 13.71/2.92 % (600626)lrs+10_64_to=lpo:sil=8000:random_seed=91562826:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 13.71/2.92 % (600625)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=894505561:st=4:i=219:sd=3:ss=axioms_2993 on theBenchmark for (2993ds/219Mi)
% 13.71/2.92 % (600625)Refutation not found, incomplete strategy
% 13.71/2.92 % (600625)------------------------------
% 13.71/2.92 % (600625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600625)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600625)Termination reason: Refutation not found, incomplete strategy
% 13.71/2.92 % (600625)Time elapsed: 0.014 s
% 13.71/2.92 % (600625)Peak memory usage: 90 MB
% 13.71/2.92 % (600625)Instructions burned: 33 (million)
% 13.71/2.92 % (600626)Instruction limit reached!
% 13.71/2.92 % (600626)------------------------------
% 13.71/2.92 % (600626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600626)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600626)Termination reason: Instruction limit
% 13.71/2.92 % (600626)Termination phase: Saturation
% 13.71/2.92 % (600626)Time elapsed: 0.053 s
% 13.71/2.92 % (600626)Peak memory usage: 89 MB
% 13.71/2.92 % (600626)Instructions burned: 128 (million)
% 13.71/2.92 % (600622)------------------------------
% 13.71/2.92 % (600622)------------------------------
% 13.71/2.92 % (600631)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2058692079:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 13.71/2.92 % (600631)Instruction limit reached!
% 13.71/2.92 % (600631)------------------------------
% 13.71/2.92 % (600631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600631)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600631)Termination reason: Instruction limit
% 13.71/2.92 % (600631)Termination phase: Saturation
% 13.71/2.92 % (600631)Time elapsed: 0.032 s
% 13.71/2.92 % (600631)Peak memory usage: 90 MB
% 13.71/2.92 % (600631)Instructions burned: 161 (million)
% 13.71/2.92 % (600632)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1066229716:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 13.71/2.92 % (600635)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1242612003:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 13.71/2.92 % (600633)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=1150696633:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 13.71/2.92 % (600633)Refutation not found, incomplete strategy
% 13.71/2.92 % (600633)------------------------------
% 13.71/2.92 % (600633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600633)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600633)Termination reason: Refutation not found, incomplete strategy
% 13.71/2.92 % (600633)Time elapsed: 0.018 s
% 13.71/2.92 % (600633)Peak memory usage: 90 MB
% 13.71/2.92 % (600633)Instructions burned: 44 (million)
% 13.71/2.92 % (600635)Instruction limit reached!
% 13.71/2.92 % (600635)------------------------------
% 13.71/2.92 % (600635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600635)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600635)Termination reason: Instruction limit
% 13.71/2.92 % (600635)Termination phase: Saturation
% 13.71/2.92 % (600635)Time elapsed: 0.027 s
% 13.71/2.92 % (600635)Peak memory usage: 92 MB
% 13.71/2.92 % (600635)Instructions burned: 109 (million)
% 13.71/2.92 % (600625)------------------------------
% 13.71/2.92 % (600625)------------------------------
% 13.71/2.92 % (600639)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2557159401:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 13.71/2.92 % (600639)Instruction limit reached!
% 13.71/2.92 % (600639)------------------------------
% 13.71/2.92 % (600639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600639)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600639)Termination reason: Instruction limit
% 13.71/2.92 % (600639)Termination phase: Saturation
% 13.71/2.92 % (600639)Time elapsed: 0.046 s
% 13.71/2.92 % (600639)Peak memory usage: 90 MB
% 13.71/2.92 % (600639)Instructions burned: 243 (million)
% 13.71/2.92 % (600641)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3610819151:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 13.71/2.92 % (600643)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1369871351:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 13.71/2.92 % (600643)Refutation not found, incomplete strategy
% 13.71/2.92 % (600643)------------------------------
% 13.71/2.92 % (600643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600643)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600643)Termination reason: Refutation not found, incomplete strategy
% 13.71/2.92 % (600643)Time elapsed: 0.005 s
% 13.71/2.92 % (600643)Peak memory usage: 90 MB
% 13.71/2.92 % (600643)Instructions burned: 22 (million)
% 13.71/2.92 % (600633)------------------------------
% 13.71/2.92 % (600633)------------------------------
% 13.71/2.92 % (600646)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=975942267:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 13.71/2.92 % (600643)------------------------------
% 13.71/2.92 % (600643)------------------------------
% 13.71/2.92 % (600648)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1933604079:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 13.71/2.92 % (600648)Instruction limit reached!
% 13.71/2.92 % (600648)------------------------------
% 13.71/2.92 % (600648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600648)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600648)Termination reason: Instruction limit
% 13.71/2.92 % (600648)Termination phase: Saturation
% 13.71/2.92 % (600648)Time elapsed: 0.040 s
% 13.71/2.92 % (600648)Peak memory usage: 90 MB
% 13.71/2.92 % (600648)Instructions burned: 192 (million)
% 13.71/2.92 % (600646)Instruction limit reached!
% 13.71/2.92 % (600646)------------------------------
% 13.71/2.92 % (600646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600646)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600646)Termination reason: Instruction limit
% 13.71/2.92 % (600646)Termination phase: Saturation
% 13.71/2.92 % (600646)Time elapsed: 0.194 s
% 13.71/2.92 % (600646)Peak memory usage: 90 MB
% 13.71/2.92 % (600646)Instructions burned: 502 (million)
% 13.71/2.92 % (600650)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1827092:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 13.71/2.92 % (600650)Instruction limit reached!
% 13.71/2.92 % (600650)------------------------------
% 13.71/2.92 % (600650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600650)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600650)Termination reason: Instruction limit
% 13.71/2.92 % (600650)Termination phase: Saturation
% 13.71/2.92 % (600650)Time elapsed: 0.055 s
% 13.71/2.92 % (600650)Peak memory usage: 90 MB
% 13.71/2.92 % (600650)Instructions burned: 268 (million)
% 13.71/2.92 % (600651)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4037590889:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 13.71/2.92 % (600653)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=830403622:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 13.71/2.92 % (600651)Instruction limit reached!
% 13.71/2.92 % (600651)------------------------------
% 13.71/2.92 % (600651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/2.92 % (600651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/2.92 % (600651)CaDiCaL version: 2.1.3
% 13.71/2.92 % (600651)Termination reason: Instruction limit
% 13.71/2.92 % (600651)Termination phase: Saturation
% 13.71/2.92 % (600651)Time elapsed: 0.058 s
% 13.71/2.92 % (600651)Peak memory usage: 90 MB
% 13.71/2.92 % (600651)Instructions burned: 158 (million)
% 13.71/2.92 % (600656)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3530800290:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 13.71/2.92 % (600656)First to succeed.
% 13.71/2.92 % (600656)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-600602"
% 13.71/2.92 % (600656)Refutation found. Thanks to Tanya!
% 13.71/2.92 % SZS status Unsatisfiable for theBenchmark
% 13.71/2.92 % SZS output start Proof for theBenchmark
% See solution above
% 13.71/3.02 % (600656)------------------------------
% 13.71/3.02 % (600656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.71/3.02 % (600656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.71/3.02 % (600656)CaDiCaL version: 2.1.3
% 13.71/3.02 % (600656)Termination reason: Refutation
% 13.71/3.02 % (600656)Time elapsed: 0.076 s
% 13.71/3.02 % (600656)Peak memory usage: 91 MB
% 13.71/3.02 % (600656)Instructions burned: 197 (million)
% 13.71/3.02 % (600656)------------------------------
% 13.71/3.02 % (600656)------------------------------
% 13.71/3.02 % (600602)Success in time 2.264 s
% 13.71/3.02 % Vampire exiting
%------------------------------------------------------------------------------