%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO683-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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 : Fri Sep 25 03:48:39 PM UTC 2026
% Result : Unsatisfiable 79.49s 81.45s
% Output : Proof 79.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 18
% Syntax : Number of formulae : 207 ( 11 unt; 0 def)
% Number of atoms : 1046 ( 0 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 1506 ( 667 ~; 839 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 284 ( 2 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f10,axiom,
( ~ iLEQ(suc(B_250),suc(B_251))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(B_249))
| ~ iLEQ(suc(B_248),suc(B_249))
| ~ qtd0(s(s(qtd1)),f(suc(B_250)))
| ~ qtd0(s(s(qtd1)),f(suc(B_248)))
| ~ qtd0(s(s(qtd1)),f(B_251))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_249),suc(B_250))
| ~ qtd0(s(s(qtd1)),f(suc(B_251)))
| ~ qtd0(s(s(qtd1)),f(B_248))
| ~ iLEQ(suc(A_2),suc(B_248))
| ~ qtd0(s(s(qtd1)),f(B_250))
| ~ qtd0(s(s(qtd1)),f(suc(B_249))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_563) ).
fof(f10_nnf,plain,
! [B_249,B_250,A_2,B_248,B_251] :
( ~ iLEQ(suc(B_250),suc(B_251))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(B_249))
| ~ iLEQ(suc(B_248),suc(B_249))
| ~ qtd0(s(s(qtd1)),f(suc(B_250)))
| ~ qtd0(s(s(qtd1)),f(suc(B_248)))
| ~ qtd0(s(s(qtd1)),f(B_251))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_249),suc(B_250))
| ~ qtd0(s(s(qtd1)),f(suc(B_251)))
| ~ qtd0(s(s(qtd1)),f(B_248))
| ~ iLEQ(suc(A_2),suc(B_248))
| ~ qtd0(s(s(qtd1)),f(B_250))
| ~ qtd0(s(s(qtd1)),f(suc(B_249))) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [B_249,B_250,A_2,B_248,B_251] :
( ~ iLEQ(suc(B_250),suc(B_251))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(B_249))
| ~ iLEQ(suc(B_248),suc(B_249))
| ~ qtd0(s(s(qtd1)),f(suc(B_250)))
| ~ qtd0(s(s(qtd1)),f(suc(B_248)))
| ~ qtd0(s(s(qtd1)),f(B_251))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ iLEQ(suc(B_249),suc(B_250))
| ~ qtd0(s(s(qtd1)),f(suc(B_251)))
| ~ qtd0(s(s(qtd1)),f(B_248))
| ~ iLEQ(suc(A_2),suc(B_248))
| ~ qtd0(s(s(qtd1)),f(B_250))
| ~ qtd0(s(s(qtd1)),f(suc(B_249))) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ~ iLEQ(suc(X1),suc(X4))
| ~ qtd0(s(s(qtd1)),f(X2))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X3),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(suc(X3)))
| ~ qtd0(s(s(qtd1)),f(X4))
| ~ qtd0(s(s(qtd1)),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X4)))
| ~ qtd0(s(s(qtd1)),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p76,plain,
( ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X2))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X3),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(suc(X3)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X2)))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(qtd1)),f(X3))
| ~ iLEQ(suc(X2),suc(X3))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[c10]) ).
cnf(p1232,plain,
( ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(suc(X2)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(qtd1)),f(X2))
| ~ iLEQ(suc(X0),suc(X2))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p76]) ).
cnf(p3763,plain,
( ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1232]) ).
cnf(p3774,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3763]) ).
cnf(p3782,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3774]) ).
cnf(p3784,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3782]) ).
cnf(p3786,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3784]) ).
cnf(p3788,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3786]) ).
cnf(p3798,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3788]) ).
cnf(p3799,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3798]) ).
cnf(p3800,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3799]) ).
cnf(f4,axiom,
( ~ iLEQ(suc(A_1),suc(B_159))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_160)))
| ~ iLEQ(suc(B_161),suc(B_162))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_161)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(B_159),suc(B_160))
| ~ qtd0(s(s(s(qtd1))),f(B_160))
| ~ qtd0(s(s(s(qtd1))),f(B_161))
| ~ qtd0(s(s(s(qtd1))),f(B_159))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_162)))
| ~ iLEQ(suc(B_160),suc(B_161))
| ~ qtd0(s(s(s(qtd1))),f(B_162))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_159))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_560) ).
fof(f4_nnf,plain,
! [B_159,B_162,B_160,B_161,A_1] :
( ~ iLEQ(suc(A_1),suc(B_159))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_160)))
| ~ iLEQ(suc(B_161),suc(B_162))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_161)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(B_159),suc(B_160))
| ~ qtd0(s(s(s(qtd1))),f(B_160))
| ~ qtd0(s(s(s(qtd1))),f(B_161))
| ~ qtd0(s(s(s(qtd1))),f(B_159))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_162)))
| ~ iLEQ(suc(B_160),suc(B_161))
| ~ qtd0(s(s(s(qtd1))),f(B_162))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_159))) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [B_159,B_162,B_160,B_161,A_1] :
( ~ iLEQ(suc(A_1),suc(B_159))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_160)))
| ~ iLEQ(suc(B_161),suc(B_162))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_161)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ iLEQ(suc(B_159),suc(B_160))
| ~ qtd0(s(s(s(qtd1))),f(B_160))
| ~ qtd0(s(s(s(qtd1))),f(B_161))
| ~ qtd0(s(s(s(qtd1))),f(B_159))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_162)))
| ~ iLEQ(suc(B_160),suc(B_161))
| ~ qtd0(s(s(s(qtd1))),f(B_162))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_159))) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( ~ iLEQ(suc(X4),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X4)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X2)))
| ~ iLEQ(suc(X3),suc(X1))
| ~ qtd0(s(s(s(qtd1))),f(suc(X3)))
| ~ qtd0(s(s(s(qtd1))),f(X4))
| ~ iLEQ(suc(X0),suc(X2))
| ~ qtd0(s(s(s(qtd1))),f(X2))
| ~ qtd0(s(s(s(qtd1))),f(X3))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X3))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p19,plain,
( ~ iLEQ(suc(X3),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X3)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X2)))
| ~ qtd0(s(s(s(qtd1))),f(X3))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ qtd0(s(s(s(qtd1))),f(X2))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X1),suc(X2))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[c4]) ).
cnf(p283,plain,
( ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X2))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p19]) ).
cnf(p2798,plain,
( ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p283]) ).
cnf(p3310,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2798]) ).
cnf(p3313,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3310]) ).
cnf(p3315,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3313]) ).
cnf(p3317,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3315]) ).
cnf(p3327,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3317]) ).
cnf(p3329,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3327]) ).
cnf(p3330,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3329]) ).
cnf(p3331,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3330]) ).
cnf(f7,axiom,
( qtd2(f(B_158),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_158)))
| ~ qtd2(f(suc(B_158)),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_443) ).
fof(f7_nnf,plain,
! [B_158] :
( qtd2(f(B_158),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_158)))
| ~ qtd2(f(suc(B_158)),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [B_158] :
( qtd2(f(B_158),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_158)))
| ~ qtd2(f(suc(B_158)),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(f2,axiom,
qtd2(f(A),s(s(s(s(qtd1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_451) ).
fof(f2_nnf,plain,
! [A] : qtd2(f(A),s(s(s(s(qtd1))))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] : qtd2(f(A),s(s(s(s(qtd1))))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
qtd2(f(X0),s(s(s(s(qtd1))))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p65,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c7,c2]) ).
cnf(p3339,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p3331,p65]) ).
cnf(f11,axiom,
( qtd2(f(B_158),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_158))
| ~ qtd2(f(B_158),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_539) ).
fof(f11_nnf,plain,
! [B_158] :
( qtd2(f(B_158),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_158))
| ~ qtd2(f(B_158),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [B_158] :
( qtd2(f(B_158),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_158))
| ~ qtd2(f(B_158),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p64,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[c11,c2]) ).
cnf(f5,axiom,
( qtd2(f(B_247),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_247)))
| ~ qtd2(f(suc(B_247)),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_476) ).
fof(f5_nnf,plain,
! [B_247] :
( qtd2(f(B_247),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_247)))
| ~ qtd2(f(suc(B_247)),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [B_247] :
( qtd2(f(B_247),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_247)))
| ~ qtd2(f(suc(B_247)),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p67,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p64,c5]) ).
cnf(p3344,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p3339,p67]) ).
cnf(f12,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_59) ).
fof(f12_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1)) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p73,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p67,c12]) ).
cnf(p180,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p73,p65]) ).
cnf(p183,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p180,c5]) ).
cnf(p305,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p183]) ).
cnf(p337,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p305]) ).
cnf(p3389,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p3344,p337]) ).
cnf(p3582,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p3389]) ).
cnf(p3584,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p3582]) ).
cnf(p3588,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p3584,c5]) ).
cnf(p3589,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3588]) ).
cnf(p3591,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3589]) ).
cnf(p3803,plain,
( qtd2(f(X0),s(s(qtd1)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p3800,p3591]) ).
cnf(f6,axiom,
( qtd2(f(B_247),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_247))
| ~ qtd2(f(B_247),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_97) ).
fof(f6_nnf,plain,
! [B_247] :
( qtd2(f(B_247),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_247))
| ~ qtd2(f(B_247),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [B_247] :
( qtd2(f(B_247),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_247))
| ~ qtd2(f(B_247),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p66,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p64,c6]) ).
cnf(p3343,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p3339,p66]) ).
cnf(p71,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p66,c12]) ).
cnf(p125,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p71,p65]) ).
cnf(p128,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p125,c6]) ).
cnf(p234,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p128]) ).
cnf(p236,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p234]) ).
cnf(p3360,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p3343,p236]) ).
cnf(p3489,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p3360]) ).
cnf(p3491,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p3489]) ).
cnf(p3492,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p3491,c6]) ).
cnf(p3502,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p3492]) ).
cnf(p3504,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p3502]) ).
cnf(f13,axiom,
( qtd2(f(B_291),s(qtd1))
| qtd0(s(qtd1),f(suc(B_291)))
| ~ qtd2(f(suc(B_291)),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_222) ).
fof(f13_nnf,plain,
! [B_291] :
( qtd2(f(B_291),s(qtd1))
| qtd0(s(qtd1),f(suc(B_291)))
| ~ qtd2(f(suc(B_291)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [B_291] :
( qtd2(f(B_291),s(qtd1))
| qtd0(s(qtd1),f(suc(B_291)))
| ~ qtd2(f(suc(B_291)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p3506,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p3504,c13]) ).
cnf(p3814,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p3803,p3506]) ).
cnf(f3,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_29) ).
fof(f3_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2)) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p3541,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p3506,c3]) ).
cnf(p3615,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p3591,p3541]) ).
cnf(p3632,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p3615,c13]) ).
cnf(p3650,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3632]) ).
cnf(p3652,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3650]) ).
cnf(p3843,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p3814,p3652]) ).
cnf(p4352,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p3843]) ).
cnf(p4354,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p4352]) ).
cnf(p4361,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p4354,c13]) ).
cnf(p4362,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p4361]) ).
cnf(p4364,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p4362]) ).
cnf(f17,axiom,
( ~ iLEQ(suc(B_292),suc(B_293))
| ~ iLEQ(suc(B_293),suc(B_294))
| ~ qtd0(s(qtd1),f(suc(B_293)))
| ~ qtd0(s(qtd1),f(A_3))
| ~ iLEQ(suc(B_294),suc(B_295))
| ~ qtd0(s(qtd1),f(B_293))
| ~ iLEQ(suc(A_3),suc(B_292))
| ~ qtd0(s(qtd1),f(B_292))
| ~ qtd0(s(qtd1),f(B_294))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(B_292)))
| ~ qtd0(s(qtd1),f(suc(B_295)))
| ~ qtd0(s(qtd1),f(B_295))
| ~ qtd0(s(qtd1),f(suc(B_294))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_151) ).
fof(f17_nnf,plain,
! [B_294,B_295,B_292,A_3,B_293] :
( ~ iLEQ(suc(B_292),suc(B_293))
| ~ iLEQ(suc(B_293),suc(B_294))
| ~ qtd0(s(qtd1),f(suc(B_293)))
| ~ qtd0(s(qtd1),f(A_3))
| ~ iLEQ(suc(B_294),suc(B_295))
| ~ qtd0(s(qtd1),f(B_293))
| ~ iLEQ(suc(A_3),suc(B_292))
| ~ qtd0(s(qtd1),f(B_292))
| ~ qtd0(s(qtd1),f(B_294))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(B_292)))
| ~ qtd0(s(qtd1),f(suc(B_295)))
| ~ qtd0(s(qtd1),f(B_295))
| ~ qtd0(s(qtd1),f(suc(B_294))) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [B_294,B_295,B_292,A_3,B_293] :
( ~ iLEQ(suc(B_292),suc(B_293))
| ~ iLEQ(suc(B_293),suc(B_294))
| ~ qtd0(s(qtd1),f(suc(B_293)))
| ~ qtd0(s(qtd1),f(A_3))
| ~ iLEQ(suc(B_294),suc(B_295))
| ~ qtd0(s(qtd1),f(B_293))
| ~ iLEQ(suc(A_3),suc(B_292))
| ~ qtd0(s(qtd1),f(B_292))
| ~ qtd0(s(qtd1),f(B_294))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(B_292)))
| ~ qtd0(s(qtd1),f(suc(B_295)))
| ~ qtd0(s(qtd1),f(B_295))
| ~ qtd0(s(qtd1),f(suc(B_294))) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( ~ iLEQ(suc(X2),suc(X4))
| ~ iLEQ(suc(X4),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X4)))
| ~ qtd0(s(qtd1),f(X3))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(s(qtd1),f(X4))
| ~ iLEQ(suc(X3),suc(X2))
| ~ qtd0(s(qtd1),f(X2))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X3)))
| ~ qtd0(s(qtd1),f(suc(X2)))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p185,plain,
( ~ iLEQ(suc(X1),suc(X3))
| ~ iLEQ(suc(X3),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X3)))
| ~ qtd0(s(qtd1),f(X2))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X2)))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[c17]) ).
cnf(p2077,plain,
( ~ iLEQ(suc(X0),suc(X2))
| ~ iLEQ(suc(X2),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X2)))
| ~ qtd0(s(qtd1),f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p185]) ).
cnf(p2102,plain,
( ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2077]) ).
cnf(p2116,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2102]) ).
cnf(p2119,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2116]) ).
cnf(p2121,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2119]) ).
cnf(p2145,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2121]) ).
cnf(p2147,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2145]) ).
cnf(p2149,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2147]) ).
cnf(p2150,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2149]) ).
cnf(p2169,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2150]) ).
cnf(p4368,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p4364,p2169]) ).
cnf(f14,axiom,
( qtd2(f(B_291),s(qtd1))
| qtd0(s(qtd1),f(B_291))
| ~ qtd2(f(B_291),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_44) ).
fof(f14_nnf,plain,
! [B_291] :
( qtd2(f(B_291),s(qtd1))
| qtd0(s(qtd1),f(B_291))
| ~ qtd2(f(B_291),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [B_291] :
( qtd2(f(B_291),s(qtd1))
| qtd0(s(qtd1),f(B_291))
| ~ qtd2(f(B_291),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p3505,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p3504,c14]) ).
cnf(p3813,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p3803,p3505]) ).
cnf(p275,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p236,c14]) ).
cnf(p277,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p275,c3]) ).
cnf(p279,plain,
( ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p277]) ).
cnf(p3594,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p3591,p279]) ).
cnf(p3626,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p3594,c14]) ).
cnf(p3636,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p3626]) ).
cnf(p3639,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p3636]) ).
cnf(p3825,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p3813,p3639]) ).
cnf(p3878,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p3825]) ).
cnf(p3892,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p3878]) ).
cnf(p3893,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p3892,c14]) ).
cnf(p3895,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p3893]) ).
cnf(p3897,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p3895]) ).
cnf(f9,axiom,
( qtd2(f(B_309),qtd1)
| qtd0(qtd1,f(suc(B_309)))
| ~ qtd2(f(suc(B_309)),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_547) ).
fof(f9_nnf,plain,
! [B_309] :
( qtd2(f(B_309),qtd1)
| qtd0(qtd1,f(suc(B_309)))
| ~ qtd2(f(suc(B_309)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [B_309] :
( qtd2(f(B_309),qtd1)
| qtd0(qtd1,f(suc(B_309)))
| ~ qtd2(f(suc(B_309)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p3903,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p3897,c9]) ).
cnf(p4578,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p4368,p3903]) ).
cnf(f1,axiom,
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_398) ).
fof(f1_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p4104,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p3903,c1]) ).
cnf(p4568,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p4364,p4104]) ).
cnf(p4603,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p4578,p4568]) ).
cnf(p4653,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p4603]) ).
cnf(p4657,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p4653]) ).
cnf(p4659,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p4657]) ).
cnf(p4660,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p4659,c9]) ).
cnf(p4661,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p4660]) ).
cnf(p4665,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p4661]) ).
cnf(f15,axiom,
( ~ qtd0(qtd1,f(A_4))
| ~ iLEQ(suc(B_312),suc(B_313))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ iLEQ(suc(A_4),suc(B_310))
| ~ iLEQ(suc(B_310),suc(B_311))
| ~ iLEQ(suc(B_311),suc(B_312))
| ~ qtd0(qtd1,f(B_313))
| ~ qtd0(qtd1,f(suc(B_312)))
| ~ qtd0(qtd1,f(B_312))
| ~ qtd0(qtd1,f(B_310))
| ~ qtd0(qtd1,f(suc(B_313)))
| ~ qtd0(qtd1,f(B_311))
| ~ qtd0(qtd1,f(suc(B_311)))
| ~ qtd0(qtd1,f(suc(B_310))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_442) ).
fof(f15_nnf,plain,
! [B_310,B_311,B_313,B_312,A_4] :
( ~ qtd0(qtd1,f(A_4))
| ~ iLEQ(suc(B_312),suc(B_313))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ iLEQ(suc(A_4),suc(B_310))
| ~ iLEQ(suc(B_310),suc(B_311))
| ~ iLEQ(suc(B_311),suc(B_312))
| ~ qtd0(qtd1,f(B_313))
| ~ qtd0(qtd1,f(suc(B_312)))
| ~ qtd0(qtd1,f(B_312))
| ~ qtd0(qtd1,f(B_310))
| ~ qtd0(qtd1,f(suc(B_313)))
| ~ qtd0(qtd1,f(B_311))
| ~ qtd0(qtd1,f(suc(B_311)))
| ~ qtd0(qtd1,f(suc(B_310))) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [B_310,B_311,B_313,B_312,A_4] :
( ~ qtd0(qtd1,f(A_4))
| ~ iLEQ(suc(B_312),suc(B_313))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ iLEQ(suc(A_4),suc(B_310))
| ~ iLEQ(suc(B_310),suc(B_311))
| ~ iLEQ(suc(B_311),suc(B_312))
| ~ qtd0(qtd1,f(B_313))
| ~ qtd0(qtd1,f(suc(B_312)))
| ~ qtd0(qtd1,f(B_312))
| ~ qtd0(qtd1,f(B_310))
| ~ qtd0(qtd1,f(suc(B_313)))
| ~ qtd0(qtd1,f(B_311))
| ~ qtd0(qtd1,f(suc(B_311)))
| ~ qtd0(qtd1,f(suc(B_310))) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ~ qtd0(qtd1,f(X4))
| ~ iLEQ(suc(X3),suc(X2))
| ~ qtd0(qtd1,f(suc(X4)))
| ~ iLEQ(suc(X4),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ iLEQ(suc(X1),suc(X3))
| ~ qtd0(qtd1,f(X2))
| ~ qtd0(qtd1,f(suc(X3)))
| ~ qtd0(qtd1,f(X3))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p130,plain,
( ~ qtd0(qtd1,f(X3))
| ~ iLEQ(suc(X2),suc(X1))
| ~ qtd0(qtd1,f(suc(X3)))
| ~ iLEQ(suc(X3),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X2))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ qtd0(qtd1,f(X2))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c15]) ).
cnf(p447,plain,
( ~ qtd0(qtd1,f(X2))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(qtd1,f(suc(X2)))
| ~ iLEQ(suc(X2),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p130]) ).
cnf(p485,plain,
( ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p447]) ).
cnf(p496,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p485]) ).
cnf(p501,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p496]) ).
cnf(p503,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p501]) ).
cnf(p526,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p503]) ).
cnf(p527,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p526]) ).
cnf(p528,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p527]) ).
cnf(p529,plain,
( ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p528]) ).
cnf(p547,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p529]) ).
cnf(p4668,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p4665,p547]) ).
cnf(f16,axiom,
( qtd2(f(B_309),qtd1)
| qtd0(qtd1,f(B_309))
| ~ qtd2(f(B_309),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_89) ).
fof(f16_nnf,plain,
! [B_309] :
( qtd2(f(B_309),qtd1)
| qtd0(qtd1,f(B_309))
| ~ qtd2(f(B_309),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [B_309] :
( qtd2(f(B_309),qtd1)
| qtd0(qtd1,f(B_309))
| ~ qtd2(f(B_309),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p3902,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p3897,c16]) ).
cnf(p3904,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p3902,c1]) ).
cnf(p4565,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p4364,p3904]) ).
cnf(p4594,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p4565,c16]) ).
cnf(p4621,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p4594]) ).
cnf(p4623,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p4621]) ).
cnf(p4577,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p4368,p3902]) ).
cnf(p4625,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p4623,p4577]) ).
cnf(p4630,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p4625]) ).
cnf(p4632,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p4630]) ).
cnf(p4633,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p4632,c16]) ).
cnf(p4635,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p4633]) ).
cnf(p4644,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p4635]) ).
cnf(f8,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_287) ).
fof(f8_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p4645,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p4644,c8]) ).
cnf(p5098,plain,
( ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p4668,p4645]) ).
cnf(f0,axiom,
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_469) ).
fof(f0_nnf,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4646,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p4645,c0]) ).
cnf(p5096,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p4665,p4646]) ).
cnf(p5102,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p5098,p5096]) ).
cnf(p5103,plain,
qtd2(f(z),qtd1),
inference(factoring,[status(thm)],[p5102]) ).
cnf(p5104,plain,
$false,
inference(resolution,[status(thm)],[p5103,c8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO683-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/20.43 % CPULimit : 300
% 0.07/20.43 % WCLimit : 300
% 0.07/20.43 % DateTime : Fri Sep 25 03:25:55 UTC 2026
% 0.07/20.43 % CPUTime :
% 0.07/20.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 79.49/81.45 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 79.49/81.45 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------