%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO677-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 : n016.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:38 PM UTC 2026
% Result : Unsatisfiable 123.37s 103.19s
% Output : Proof 123.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 110
% Number of leaves : 30
% Syntax : Number of formulae : 463 ( 11 unt; 0 def)
% Number of atoms : 2183 ( 0 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 2470 ( 750 ~;1720 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 6 ( 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 : 472 ( 2 sgn 74 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f31,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(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_65) ).
fof(f31_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(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)],[f31]) ).
fof(f31_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1)) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(f14,axiom,
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_9))))
| ~ qtd2(f(suc(suc(B_9))),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18) ).
fof(f14_nnf,plain,
! [B_9] :
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_9))))
| ~ qtd2(f(suc(suc(B_9))),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [B_9] :
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_9))))
| ~ qtd2(f(suc(suc(B_9))),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f15,axiom,
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_4))
| ~ qtd2(f(B_4),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_61) ).
fof(f15_nnf,plain,
! [B_4] :
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_4))
| ~ qtd2(f(B_4),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [B_4] :
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_4))
| ~ qtd2(f(B_4),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,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)],[f15_sk]) ).
cnf(f17,axiom,
qtd2(f(A),s(s(s(s(qtd1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_113) ).
fof(f17_nnf,plain,
! [A] : qtd2(f(A),s(s(s(s(qtd1))))),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A] : qtd2(f(A),s(s(s(s(qtd1))))),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
qtd2(f(X0),s(s(s(s(qtd1))))),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p52,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[c15,c17]) ).
cnf(p63,plain,
( qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c14,p52]) ).
cnf(p74,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[c31,p63]) ).
cnf(f8,axiom,
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_4)))
| ~ qtd2(f(suc(B_4)),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13) ).
fof(f8_nnf,plain,
! [B_4] :
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_4)))
| ~ qtd2(f(suc(B_4)),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [B_4] :
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_4)))
| ~ qtd2(f(suc(B_4)),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,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)],[f8_sk]) ).
cnf(p65,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c8,c17]) ).
cnf(p452,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p74,p65]) ).
cnf(f21,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_140) ).
fof(f21_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_1)))) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_1)))) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(f2,axiom,
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(B_4))))
| ~ qtd2(f(suc(suc(B_4))),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_143) ).
fof(f2_nnf,plain,
! [B_4] :
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(B_4))))
| ~ qtd2(f(suc(suc(B_4))),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [B_4] :
( qtd2(f(B_4),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(B_4))))
| ~ qtd2(f(suc(suc(B_4))),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p53,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c2,c17]) ).
cnf(p100,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c21,p53]) ).
cnf(p119,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p100,p65]) ).
cnf(p120,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p119]) ).
cnf(p454,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p452,p120]) ).
cnf(p1944,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p454]) ).
cnf(p2169,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1944]) ).
cnf(p2170,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p2169,p63]) ).
cnf(p2171,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2170]) ).
cnf(p2173,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2171]) ).
cnf(p2174,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p2173,c14]) ).
cnf(p2177,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2174]) ).
cnf(p2179,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2177]) ).
cnf(f9,axiom,
( qtd0(f(B_5),f(suc(B_5)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(s(s(s(qtd1))),f(B_5))
| ~ iLEQ(suc(A_1),suc(B_5))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_5))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_51) ).
fof(f9_nnf,plain,
! [B_5,A_1] :
( qtd0(f(B_5),f(suc(B_5)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(s(s(s(qtd1))),f(B_5))
| ~ iLEQ(suc(A_1),suc(B_5))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_5))) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [B_5,A_1] :
( qtd0(f(B_5),f(suc(B_5)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(s(s(s(qtd1))),f(B_5))
| ~ iLEQ(suc(A_1),suc(B_5))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_5))) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p106,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(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(suc(X0))) ),
inference(factoring,[status(thm)],[c9]) ).
cnf(p290,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p106]) ).
cnf(p292,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p290]) ).
cnf(p297,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p292,p65]) ).
cnf(p2180,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p2179,p297]) ).
cnf(p2182,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p2180,p63]) ).
cnf(p2183,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2182]) ).
cnf(p2185,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2183]) ).
cnf(f29,axiom,
( ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(B_5))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_1))))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(s(s(s(qtd1))),f(B_5))
| ~ iLEQ(suc(A_1),suc(B_5))
| ~ qtd0(f(B_5),f(suc(B_5)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_5))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_121) ).
fof(f29_nnf,plain,
! [B_5,A_1] :
( ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(B_5))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_1))))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(s(s(s(qtd1))),f(B_5))
| ~ iLEQ(suc(A_1),suc(B_5))
| ~ qtd0(f(B_5),f(suc(B_5)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_5))) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [B_5,A_1] :
( ~ qtd0(s(s(s(qtd1))),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(B_5))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_1))))
| ~ qtd0(s(s(s(qtd1))),f(A_1))
| ~ qtd0(s(s(s(qtd1))),f(B_5))
| ~ iLEQ(suc(A_1),suc(B_5))
| ~ qtd0(f(B_5),f(suc(B_5)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_5))) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X1))))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p228,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[c29]) ).
cnf(p1138,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p228]) ).
cnf(p1140,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1138]) ).
cnf(p1141,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1140]) ).
cnf(p1146,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1141,p65]) ).
cnf(p2198,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p2185,p1146]) ).
cnf(p7849,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2198]) ).
cnf(p7879,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p7849,p2179]) ).
cnf(p8341,plain,
( qtd2(f(X0),s(s(qtd1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p7879]) ).
cnf(p8351,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8341]) ).
cnf(p8352,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p8351,p63]) ).
cnf(p8353,plain,
( qtd2(f(X0),s(s(qtd1)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8352]) ).
cnf(p8355,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8353]) ).
cnf(p8365,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p8355,p53]) ).
cnf(p8366,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8365]) ).
cnf(p8367,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p8366,c14]) ).
cnf(p8368,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8367]) ).
cnf(p8370,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8368]) ).
cnf(f11,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_97) ).
fof(f11_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_2)))) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_2)))) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p8374,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p8370,c11]) ).
cnf(f30,axiom,
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_9)))
| ~ qtd2(f(suc(B_9)),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_87) ).
fof(f30_nnf,plain,
! [B_9] :
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_9)))
| ~ qtd2(f(suc(B_9)),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [B_9] :
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_9)))
| ~ qtd2(f(suc(B_9)),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,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)],[f30_sk]) ).
cnf(p55,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)],[p52,c30]) ).
cnf(p73,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c31,p55]) ).
cnf(p186,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p73,p65]) ).
cnf(p187,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)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p186,c30]) ).
cnf(p443,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p187]) ).
cnf(p445,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p443]) ).
cnf(p447,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p445,p120]) ).
cnf(p521,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p447]) ).
cnf(p523,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p521,p55]) ).
cnf(p531,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p523]) ).
cnf(p533,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p531]) ).
cnf(p534,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)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p533,c30]) ).
cnf(p539,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p534]) ).
cnf(p541,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p539]) ).
cnf(p542,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p541,p297]) ).
cnf(p546,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p542,p55]) ).
cnf(p554,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p546]) ).
cnf(p556,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p554]) ).
cnf(p557,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p556,c30]) ).
cnf(p569,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p557]) ).
cnf(p571,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p569]) ).
cnf(p1154,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p1146,p571]) ).
cnf(p1279,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))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1154,p541]) ).
cnf(p2696,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))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1279]) ).
cnf(p2698,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2696]) ).
cnf(p2699,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))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p2698,p55]) ).
cnf(p2703,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))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p2699]) ).
cnf(p2705,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p2703]) ).
cnf(p2706,plain,
( qtd2(f(suc(X0)),s(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(resolution,[status(thm)],[p2705,p53]) ).
cnf(p2707,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)],[p2706]) ).
cnf(p2713,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)],[p2707,c30]) ).
cnf(p2715,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2713]) ).
cnf(p2717,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2715]) ).
cnf(p8516,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p8374,p2717]) ).
cnf(p8518,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p8516]) ).
cnf(f18,axiom,
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_9))
| ~ qtd2(f(B_9),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_73) ).
fof(f18_nnf,plain,
! [B_9] :
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_9))
| ~ qtd2(f(B_9),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [B_9] :
( qtd2(f(B_9),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_9))
| ~ qtd2(f(B_9),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,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)],[f18_sk]) ).
cnf(p54,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p52,c18]) ).
cnf(p72,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c31,p54]) ).
cnf(p95,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p72,p65]) ).
cnf(p96,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))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p95,c18]) ).
cnf(p137,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p96]) ).
cnf(p139,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p137]) ).
cnf(p149,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p139,p120]) ).
cnf(p250,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p149]) ).
cnf(p252,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p250,p54]) ).
cnf(p255,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p252]) ).
cnf(p262,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p255]) ).
cnf(p263,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))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p262,c18]) ).
cnf(p266,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p263]) ).
cnf(p268,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p266]) ).
cnf(p302,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p297,p268]) ).
cnf(p330,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))))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p302,p54]) ).
cnf(p375,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))))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p330]) ).
cnf(p377,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p375]) ).
cnf(p378,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))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p377,c18]) ).
cnf(p383,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p378]) ).
cnf(p386,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p383]) ).
cnf(p1149,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p1146,p386]) ).
cnf(p1203,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))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p1149,p268]) ).
cnf(p1603,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))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p1203]) ).
cnf(p1614,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p1603]) ).
cnf(p1616,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))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1614,p54]) ).
cnf(p1619,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))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1616]) ).
cnf(p1621,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1619]) ).
cnf(p1622,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p1621,p53]) ).
cnf(p1627,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p1622]) ).
cnf(p1628,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)],[p1627,c18]) ).
cnf(p1631,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p1628]) ).
cnf(p1633,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p1631]) ).
cnf(f26,axiom,
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_13))))
| ~ qtd2(f(suc(suc(B_13))),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_49) ).
fof(f26_nnf,plain,
! [B_13] :
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_13))))
| ~ qtd2(f(suc(suc(B_13))),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [B_13] :
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_13))))
| ~ qtd2(f(suc(suc(B_13))),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p1636,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1633,c26]) ).
cnf(f33,axiom,
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(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_84) ).
fof(f33_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2)) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p1696,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1636,c33]) ).
cnf(p2747,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p2717,p1696]) ).
cnf(p8522,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p8518,p2747]) ).
cnf(p18932,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p8522]) ).
cnf(p19555,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p18932]) ).
cnf(p19556,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19555,p1636]) ).
cnf(p19557,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19556]) ).
cnf(p19562,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19557]) ).
cnf(f5,axiom,
( qtd0(f(B_10),f(suc(B_10)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(B_10)))
| ~ iLEQ(suc(A_2),suc(B_10))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(B_10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_38) ).
fof(f5_nnf,plain,
! [B_10,A_2] :
( qtd0(f(B_10),f(suc(B_10)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(B_10)))
| ~ iLEQ(suc(A_2),suc(B_10))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(B_10)) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [B_10,A_2] :
( qtd0(f(B_10),f(suc(B_10)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(B_10)))
| ~ iLEQ(suc(A_2),suc(B_10))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(B_10)) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p78,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[c5]) ).
cnf(p192,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p78]) ).
cnf(p194,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p192]) ).
cnf(p1700,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1636,p194]) ).
cnf(p2748,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p2717,p1700]) ).
cnf(p19564,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19562,p2748]) ).
cnf(p21049,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19564]) ).
cnf(p21052,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p21049]) ).
cnf(p21054,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p21052]) ).
cnf(f0,axiom,
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_10))))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_2))))
| ~ qtd0(s(s(qtd1)),f(suc(B_10)))
| ~ iLEQ(suc(A_2),suc(B_10))
| ~ qtd0(f(B_10),f(suc(B_10)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(B_10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_24) ).
fof(f0_nnf,plain,
! [B_10,A_2] :
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_10))))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_2))))
| ~ qtd0(s(s(qtd1)),f(suc(B_10)))
| ~ iLEQ(suc(A_2),suc(B_10))
| ~ qtd0(f(B_10),f(suc(B_10)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(B_10)) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [B_10,A_2] :
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_10))))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(A_2))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_2))))
| ~ qtd0(s(s(qtd1)),f(suc(B_10)))
| ~ iLEQ(suc(A_2),suc(B_10))
| ~ qtd0(f(B_10),f(suc(B_10)))
| ~ qtd0(s(s(qtd1)),f(suc(A_2)))
| ~ qtd0(s(s(qtd1)),f(B_10)) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p40,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[c0]) ).
cnf(p286,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p40]) ).
cnf(p725,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p286]) ).
cnf(p727,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p725]) ).
cnf(p1709,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1636,p727]) ).
cnf(p2755,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p2717,p1709]) ).
cnf(p21071,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p21054,p2755]) ).
cnf(p28832,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p21071]) ).
cnf(p28835,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p28832]) ).
cnf(p28837,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p28835]) ).
cnf(p28838,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p28837,p19562]) ).
cnf(p28840,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p28838]) ).
cnf(p28843,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p28840]) ).
cnf(p28845,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p28843]) ).
cnf(p28846,plain,
( qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p28845,p8370]) ).
cnf(p28847,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p28846]) ).
cnf(p28848,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p28847,c26]) ).
cnf(p28849,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p28848]) ).
cnf(p28851,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p28849]) ).
cnf(f23,axiom,
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(suc(A_3)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_31) ).
fof(f23_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(suc(A_3)))) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(suc(A_3)))) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p28853,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p28851,c23]) ).
cnf(f24,axiom,
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(suc(B_13)))
| ~ qtd2(f(suc(B_13)),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_39) ).
fof(f24_nnf,plain,
! [B_13] :
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(suc(B_13)))
| ~ qtd2(f(suc(B_13)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [B_13] :
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(suc(B_13)))
| ~ qtd2(f(suc(B_13)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p1635,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1633,c24]) ).
cnf(p1666,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(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)],[p1635,c33]) ).
cnf(p2741,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(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)],[p2717,p1666]) ).
cnf(p8521,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)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p8518,p2741]) ).
cnf(p10534,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p8521]) ).
cnf(p10536,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p10534]) ).
cnf(p10537,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p10536,p1635]) ).
cnf(p10550,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p10537]) ).
cnf(p10552,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p10550]) ).
cnf(p10553,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p10552,c24]) ).
cnf(p10557,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p10553]) ).
cnf(p10570,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p10557]) ).
cnf(p1670,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ 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)],[p1635,p194]) ).
cnf(p2742,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ 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)],[p2717,p1670]) ).
cnf(p10572,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p10570,p2742]) ).
cnf(p10574,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p10572]) ).
cnf(p10576,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p10574]) ).
cnf(p1679,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(f(suc(X0)),f(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)],[p1635,p727]) ).
cnf(p2749,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(f(suc(X0)),f(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)],[p2717,p1679]) ).
cnf(p10593,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| ~ 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)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p10576,p2749]) ).
cnf(p16120,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| ~ 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)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p10593]) ).
cnf(p16121,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p16120]) ).
cnf(p16123,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p16121]) ).
cnf(p16124,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p16123,p10570]) ).
cnf(p16144,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p16124]) ).
cnf(p16146,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p16144]) ).
cnf(p16147,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p16146,p8370]) ).
cnf(p16148,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p16147]) ).
cnf(p16150,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)],[p16148,c24]) ).
cnf(p16152,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p16150]) ).
cnf(p16154,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p16152]) ).
cnf(p29120,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p28853,p16154]) ).
cnf(p29122,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p29120]) ).
cnf(f6,axiom,
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(B_13))
| ~ qtd2(f(B_13),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15) ).
fof(f6_nnf,plain,
! [B_13] :
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(B_13))
| ~ qtd2(f(B_13),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [B_13] :
( qtd2(f(B_13),s(qtd1))
| qtd0(s(qtd1),f(B_13))
| ~ qtd2(f(B_13),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p270,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p268,c6]) ).
cnf(p274,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(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)],[p270,c33]) ).
cnf(p283,plain,
( qtd0(f(X0),f(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(factoring,[status(thm)],[p274]) ).
cnf(p2726,plain,
( qtd0(f(X0),f(suc(X0)))
| 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)],[p2717,p283]) ).
cnf(p2767,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p2726,c6]) ).
cnf(p2857,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p2767]) ).
cnf(p2859,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p2857]) ).
cnf(p8520,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p8518,p2859]) ).
cnf(p8576,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p8520]) ).
cnf(p1634,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p1633,c6]) ).
cnf(p8577,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))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p8576,p1634]) ).
cnf(p8582,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p8577]) ).
cnf(p8584,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p8582]) ).
cnf(p8585,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)],[p8584,c6]) ).
cnf(p8594,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)],[p8585]) ).
cnf(p8596,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p8594]) ).
cnf(p387,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p386,c6]) ).
cnf(p397,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p387,p194]) ).
cnf(p408,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p397]) ).
cnf(p2728,plain,
( ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p2717,p408]) ).
cnf(p8601,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p8596,p2728]) ).
cnf(p8778,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p8601]) ).
cnf(p8780,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p8778]) ).
cnf(p8781,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p8780,c6]) ).
cnf(p8810,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p8781]) ).
cnf(p8812,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p8810]) ).
cnf(p1648,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p1634,p727]) ).
cnf(p2743,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p2717,p1648]) ).
cnf(p8830,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p8812,p2743]) ).
cnf(p9220,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p8830]) ).
cnf(p9222,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p9220]) ).
cnf(p9223,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p9222,p8596]) ).
cnf(p9227,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p9223]) ).
cnf(p9229,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p9227]) ).
cnf(p9230,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p9229,p8370]) ).
cnf(p9231,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p9230]) ).
cnf(p9232,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)],[p9231,c6]) ).
cnf(p9235,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p9232]) ).
cnf(p9237,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p9235]) ).
cnf(f35,axiom,
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_27) ).
fof(f35_nnf,plain,
! [B_16] :
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [B_16] :
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p9240,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p9237,c35]) ).
cnf(f36,axiom,
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_115) ).
fof(f36_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(A_3)) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p9291,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p9240,c36]) ).
cnf(p16183,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p16154,p9291]) ).
cnf(p29127,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p29122,p16183]) ).
cnf(p30330,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p29127]) ).
cnf(p30331,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30330]) ).
cnf(p30332,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p30331,p9240]) ).
cnf(p30339,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30332]) ).
cnf(p30341,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30339]) ).
cnf(f34,axiom,
( qtd0(f(B_14),f(suc(B_14)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(A_3),suc(B_14))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(s(qtd1),f(B_14))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(B_14))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_112) ).
fof(f34_nnf,plain,
! [B_14,A_3] :
( qtd0(f(B_14),f(suc(B_14)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(A_3),suc(B_14))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(s(qtd1),f(B_14))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(B_14))) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [B_14,A_3] :
( qtd0(f(B_14),f(suc(B_14)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(A_3),suc(B_14))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(s(qtd1),f(B_14))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(B_14))) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p257,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(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)],[c34]) ).
cnf(p281,plain,
( qtd0(f(X0),f(suc(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)],[p257]) ).
cnf(p282,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p281]) ).
cnf(p16161,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p16154,p282]) ).
cnf(p16295,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p16161,p9240]) ).
cnf(p30344,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p30341,p16295]) ).
cnf(p30370,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30344]) ).
cnf(p30379,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30370]) ).
cnf(p30381,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30379]) ).
cnf(f28,axiom,
( ~ iLEQ(suc(A_3),suc(B_14))
| ~ qtd0(s(qtd1),f(suc(suc(A_3))))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(f(B_14),f(suc(B_14)))
| ~ qtd0(s(qtd1),f(B_14))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(suc(B_14))))
| ~ qtd0(s(qtd1),f(suc(B_14))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_57) ).
fof(f28_nnf,plain,
! [B_14,A_3] :
( ~ iLEQ(suc(A_3),suc(B_14))
| ~ qtd0(s(qtd1),f(suc(suc(A_3))))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(f(B_14),f(suc(B_14)))
| ~ qtd0(s(qtd1),f(B_14))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(suc(B_14))))
| ~ qtd0(s(qtd1),f(suc(B_14))) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [B_14,A_3] :
( ~ iLEQ(suc(A_3),suc(B_14))
| ~ qtd0(s(qtd1),f(suc(suc(A_3))))
| ~ qtd0(s(qtd1),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(f(B_14),f(suc(B_14)))
| ~ qtd0(s(qtd1),f(B_14))
| ~ qtd0(s(qtd1),f(suc(A_3)))
| ~ qtd0(s(qtd1),f(suc(suc(B_14))))
| ~ qtd0(s(qtd1),f(suc(B_14))) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p212,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[c28]) ).
cnf(p827,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p212]) ).
cnf(p831,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p827]) ).
cnf(p853,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p831]) ).
cnf(p16170,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p16154,p853]) ).
cnf(p28915,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p28851,p16170]) ).
cnf(p29109,plain,
( ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p28915]) ).
cnf(p29112,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p29109,p9240]) ).
cnf(p30406,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p30381,p29112]) ).
cnf(p30414,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30406]) ).
cnf(p30423,plain,
( qtd2(f(X0),qtd1)
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30414]) ).
cnf(p30425,plain,
( ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30423]) ).
cnf(p30426,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p30425,p30341]) ).
cnf(p30427,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30426]) ).
cnf(p30430,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30427]) ).
cnf(p30432,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p30430]) ).
cnf(p30433,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p30432,c35]) ).
cnf(p30434,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p30433]) ).
cnf(p30436,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p30434]) ).
cnf(f37,axiom,
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(A_4))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(suc(A_4)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_114) ).
fof(f37_nnf,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(A_4))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(suc(A_4)))) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(qtd1,f(A_4))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(suc(A_4)))) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p30439,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p30436,c37]) ).
cnf(f12,axiom,
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2) ).
fof(f12_nnf,plain,
! [B_16] :
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [B_16] :
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p9239,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p9237,c12]) ).
cnf(p9266,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p9239,c36]) ).
cnf(p16177,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p16154,p9266]) ).
cnf(p29126,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p29122,p16177]) ).
cnf(p29530,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29126]) ).
cnf(p29531,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29530]) ).
cnf(p29532,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| 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)],[p29531,p9239]) ).
cnf(p29534,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29532]) ).
cnf(p29536,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29534]) ).
cnf(p16294,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p16161,p9239]) ).
cnf(p29540,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(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)],[p29536,p16294]) ).
cnf(p29564,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29540]) ).
cnf(p29567,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29564]) ).
cnf(p29569,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29567]) ).
cnf(p29111,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p29109,p9239]) ).
cnf(p29597,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ iLEQ(suc(suc(X0)),suc(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)],[p29569,p29111]) ).
cnf(p29601,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29597]) ).
cnf(p29604,plain,
( qtd2(f(X0),qtd1)
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29601]) ).
cnf(p29606,plain,
( ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29604]) ).
cnf(p29608,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)],[p29606,p29536]) ).
cnf(p29609,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)],[p29608]) ).
cnf(p29612,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29609]) ).
cnf(p29614,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p29612]) ).
cnf(p29615,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p29614,c12]) ).
cnf(p29617,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p29615]) ).
cnf(p29619,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p29617]) ).
cnf(p30512,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p30439,p29619]) ).
cnf(p30514,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p30512]) ).
cnf(f13,axiom,
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(B_16))
| ~ qtd2(f(B_16),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_145) ).
fof(f13_nnf,plain,
! [B_16] :
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(B_16))
| ~ qtd2(f(B_16),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [B_16] :
( qtd2(f(B_16),qtd1)
| qtd0(qtd1,f(B_16))
| ~ qtd2(f(B_16),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p9238,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p9237,c13]) ).
cnf(p9241,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p9238,c36]) ).
cnf(p16175,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p16154,p9241]) ).
cnf(p29125,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p29122,p16175]) ).
cnf(p29291,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p29125]) ).
cnf(p29293,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p29291]) ).
cnf(p29294,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p29293,p9238]) ).
cnf(p29297,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p29294]) ).
cnf(p29299,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p29297]) ).
cnf(p29300,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p29299,c13]) ).
cnf(p29308,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p29300]) ).
cnf(p29310,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p29308]) ).
cnf(p16293,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p16161,p9238]) ).
cnf(p29313,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p29310,p16293]) ).
cnf(p29316,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29313]) ).
cnf(p29318,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29316]) ).
cnf(p29110,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p29109,p9238]) ).
cnf(p29349,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p29318,p29110]) ).
cnf(p29373,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29349]) ).
cnf(p29374,plain,
( qtd2(f(X0),qtd1)
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29373]) ).
cnf(p29376,plain,
( ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29374]) ).
cnf(p29379,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)],[p29376,p29310]) ).
cnf(p29380,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29379]) ).
cnf(p29382,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29380]) ).
cnf(p29383,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p29382,c13]) ).
cnf(p29386,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29383]) ).
cnf(p29388,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p29386]) ).
cnf(f27,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_77) ).
fof(f27_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p29389,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p29388,c27]) ).
cnf(f22,axiom,
( iLEQ(suc(A_4),suc(A_4))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_150) ).
fof(f22_nnf,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4)) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p29390,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p29389,c22]) ).
cnf(p29651,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p29619,p29390]) ).
cnf(p30517,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p30514,p29651]) ).
cnf(p30525,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p30517]) ).
cnf(p30526,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p30525]) ).
cnf(p30527,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p30526,p29389]) ).
cnf(f16,axiom,
( qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_17))
| ~ iLEQ(suc(A_4),suc(B_17))
| ~ qtd0(qtd1,f(suc(B_17))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_0) ).
fof(f16_nnf,plain,
! [B_17,A_4] :
( qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_17))
| ~ iLEQ(suc(A_4),suc(B_17))
| ~ qtd0(qtd1,f(suc(B_17))) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [B_17,A_4] :
( qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(qtd1,f(A_4))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_17))
| ~ iLEQ(suc(A_4),suc(B_17))
| ~ qtd0(qtd1,f(suc(B_17))) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p144,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c16]) ).
cnf(p155,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p144]) ).
cnf(p157,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p155]) ).
cnf(p29624,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p29619,p157]) ).
cnf(p30529,plain,
( qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p30527,p29624]) ).
cnf(p30534,plain,
( qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p30529]) ).
cnf(p30535,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p30534,p29389]) ).
cnf(f19,axiom,
( ~ qtd0(qtd1,f(A_4))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_17))
| ~ qtd0(qtd1,f(suc(suc(A_4))))
| ~ qtd0(qtd1,f(suc(suc(B_17))))
| ~ iLEQ(suc(A_4),suc(B_17))
| ~ qtd0(qtd1,f(suc(B_17)))
| ~ qtd0(f(A_4),f(suc(A_4))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_48) ).
fof(f19_nnf,plain,
! [A_4,B_17] :
( ~ qtd0(qtd1,f(A_4))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_17))
| ~ qtd0(qtd1,f(suc(suc(A_4))))
| ~ qtd0(qtd1,f(suc(suc(B_17))))
| ~ iLEQ(suc(A_4),suc(B_17))
| ~ qtd0(qtd1,f(suc(B_17)))
| ~ qtd0(f(A_4),f(suc(A_4))) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A_4,B_17] :
( ~ qtd0(qtd1,f(A_4))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(qtd1,f(suc(A_4)))
| ~ qtd0(qtd1,f(B_17))
| ~ qtd0(qtd1,f(suc(suc(A_4))))
| ~ qtd0(qtd1,f(suc(suc(B_17))))
| ~ iLEQ(suc(A_4),suc(B_17))
| ~ qtd0(qtd1,f(suc(B_17)))
| ~ qtd0(f(A_4),f(suc(A_4))) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p158,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[c19]) ).
cnf(p505,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p158]) ).
cnf(p507,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p505]) ).
cnf(p509,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p507]) ).
cnf(p30540,plain,
( ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p30535,p509]) ).
cnf(p30561,plain,
( qtd2(f(z),qtd1)
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p30540,p29619]) ).
cnf(p30562,plain,
( ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p30561]) ).
cnf(p30563,plain,
( qtd2(f(z),qtd1)
| ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p30562,p30527]) ).
cnf(p30564,plain,
( ~ qtd0(qtd1,f(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p30563]) ).
cnf(p30566,plain,
( qtd2(f(z),qtd1)
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p30564,p30436]) ).
cnf(p30567,plain,
( ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p30566]) ).
cnf(p30568,plain,
qtd2(f(z),qtd1),
inference(resolution,[status(thm)],[p30567,p29389]) ).
cnf(p30569,plain,
$false,
inference(resolution,[status(thm)],[p30568,c27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO677-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.38 % Computer : n016.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Fri Sep 25 03:27:43 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 123.37/103.19 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 123.37/103.19 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------