%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO658-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 : n001.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:36 PM UTC 2026
% Result : Unsatisfiable 19.95s 8.03s
% Output : Proof 19.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 22
% Syntax : Number of formulae : 423 ( 11 unt; 0 def)
% Number of atoms : 2492 ( 0 equ)
% Maximal formula atoms : 13 ( 5 avg)
% Number of connectives : 3089 (1020 ~;2069 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 8 ( 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 : 409 ( 2 sgn 54 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f33,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_134) ).
fof(f33_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(f27,axiom,
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_2))))
| ~ qtd2(f(suc(suc(B_2))),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_129) ).
fof(f27_nnf,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_2))))
| ~ qtd2(f(suc(suc(B_2))),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_2))))
| ~ qtd2(f(suc(suc(B_2))),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,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)],[f27_sk]) ).
cnf(f10,axiom,
qtd2(f(A),s(s(qtd1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_72) ).
fof(f10_nnf,plain,
! [A] : qtd2(f(A),s(s(qtd1))),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A] : qtd2(f(A),s(s(qtd1))),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
qtd2(f(X0),s(s(qtd1))),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p65,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c27,c10]) ).
cnf(p374,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[c33,p65]) ).
cnf(f20,axiom,
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(suc(B_5)))))
| ~ qtd2(f(suc(suc(suc(B_5)))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_151) ).
fof(f20_nnf,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(suc(B_5)))))
| ~ qtd2(f(suc(suc(suc(B_5)))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(suc(B_5)))))
| ~ qtd2(f(suc(suc(suc(B_5)))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(f17,axiom,
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(B_2))
| ~ qtd2(f(B_2),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_51) ).
fof(f17_nnf,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(B_2))
| ~ qtd2(f(B_2),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(B_2))
| ~ qtd2(f(B_2),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p52,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[c17,c10]) ).
cnf(p63,plain,
( qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[c20,p52]) ).
cnf(p380,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[status(thm)],[p374,p63]) ).
cnf(f2,axiom,
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(B_2)))
| ~ qtd2(f(suc(B_2)),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_104) ).
fof(f2_nnf,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(B_2)))
| ~ qtd2(f(suc(B_2)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(B_2)))
| ~ qtd2(f(suc(B_2)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p57,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[c2,c10]) ).
cnf(p1648,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[status(thm)],[p380,p57]) ).
cnf(p3720,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(factoring,[status(thm)],[p1648]) ).
cnf(f3,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_81) ).
fof(f3_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1)) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,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)],[f3_sk]) ).
cnf(p64,plain,
( iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p63,c3]) ).
cnf(p273,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p64,p57]) ).
cnf(f25,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16) ).
fof(f25_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(A_1)))) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(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)],[f25_sk]) ).
cnf(p142,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[c25,p65]) ).
cnf(p147,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p142,p57]) ).
cnf(p150,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p147]) ).
cnf(p274,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p273,p150]) ).
cnf(p1222,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p274]) ).
cnf(p1861,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1222]) ).
cnf(p1865,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p1861,p63]) ).
cnf(p1866,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1865]) ).
cnf(p1868,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1866]) ).
cnf(p6234,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[status(thm)],[p3720,p1868]) ).
cnf(p8602,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p6234]) ).
cnf(p8606,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p8602]) ).
cnf(p8609,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p8606]) ).
cnf(p8611,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p8609]) ).
cnf(p8613,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(resolution,[status(thm)],[p8611,p273]) ).
cnf(p8614,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(factoring,[status(thm)],[p8613]) ).
cnf(p8618,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(factoring,[status(thm)],[p8614]) ).
cnf(p8621,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(factoring,[status(thm)],[p8618]) ).
cnf(p8624,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0)))))))) ),
inference(factoring,[status(thm)],[p8621]) ).
cnf(f1,axiom,
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(suc(B_2)))))
| ~ qtd2(f(suc(suc(suc(B_2)))),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_75) ).
fof(f1_nnf,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(suc(B_2)))))
| ~ qtd2(f(suc(suc(suc(B_2)))),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [B_2] :
( qtd2(f(B_2),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(suc(B_2)))))
| ~ qtd2(f(suc(suc(suc(B_2)))),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd2(f(suc(suc(suc(X0)))),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p55,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[c1,c10]) ).
cnf(p8625,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p8624,p55]) ).
cnf(p8626,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| iLEQ(suc(suc(suc(suc(X0)))),suc(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p8625]) ).
cnf(f13,axiom,
( ~ qtd0(f(B_3),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(B_3)))))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_140) ).
fof(f13_nnf,plain,
! [A_1,B_3] :
( ~ qtd0(f(B_3),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(B_3)))))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A_1,B_3] :
( ~ qtd0(f(B_3),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(A_1)))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(B_3)))))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ~ qtd0(f(X1),f(suc(suc(X1))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X1)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p151,plain,
( ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c13]) ).
cnf(p770,plain,
( ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p151]) ).
cnf(p2483,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p770]) ).
cnf(p2486,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p2483]) ).
cnf(p2489,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p2486]) ).
cnf(p2490,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p2489]) ).
cnf(p8632,plain,
( ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8626,p2490]) ).
cnf(p8654,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8632,p65]) ).
cnf(p8655,plain,
( ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8654]) ).
cnf(p8657,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8655,p63]) ).
cnf(p8658,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8657]) ).
cnf(p8660,plain,
( ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8658]) ).
cnf(p8661,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8660,p57]) ).
cnf(p8662,plain,
( ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(suc(X0))))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8661]) ).
cnf(p8663,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8662,p55]) ).
cnf(p8664,plain,
( ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8663]) ).
cnf(f15,axiom,
( qtd0(f(B_3),f(suc(suc(B_3))))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_41) ).
fof(f15_nnf,plain,
! [A_1,B_3] :
( qtd0(f(B_3),f(suc(suc(B_3))))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A_1,B_3] :
( qtd0(f(B_3),f(suc(suc(B_3))))
| qtd0(f(A_1),f(suc(suc(A_1))))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(f(B_3),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(suc(suc(B_3))))
| ~ qtd0(s(qtd1),f(A_1))
| ~ qtd0(s(qtd1),f(suc(suc(A_1))))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( qtd0(f(X1),f(suc(suc(X1))))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p199,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| qtd0(f(X0),f(suc(suc(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(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c15]) ).
cnf(p893,plain,
( qtd0(f(X0),f(suc(suc(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(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p199]) ).
cnf(p1023,plain,
( qtd0(f(X0),f(suc(suc(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(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p893]) ).
cnf(p1026,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1023]) ).
cnf(p1027,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1026]) ).
cnf(p8631,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8626,p1027]) ).
cnf(p8639,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8631,p65]) ).
cnf(p8640,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8639]) ).
cnf(p8641,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8640,p63]) ).
cnf(p8642,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8641]) ).
cnf(p8644,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8642]) ).
cnf(p8645,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8644,p57]) ).
cnf(p8646,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8645]) ).
cnf(f11,axiom,
( qtd0(f(B_3),f(suc(B_3)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_142) ).
fof(f11_nnf,plain,
! [A_1,B_3] :
( qtd0(f(B_3),f(suc(B_3)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A_1,B_3] :
( qtd0(f(B_3),f(suc(B_3)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(B_3))
| ~ qtd0(s(qtd1),f(suc(B_3)))
| ~ qtd0(s(qtd1),f(suc(A_1)))
| ~ qtd0(s(qtd1),f(A_1))
| ~ iLEQ(suc(A_1),suc(B_3)) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p121,plain,
( 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(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c11]) ).
cnf(p125,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p121]) ).
cnf(p126,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p125]) ).
cnf(p8628,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8626,p126]) ).
cnf(p8633,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8628,p63]) ).
cnf(p8634,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8633]) ).
cnf(p8636,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8634]) ).
cnf(p8637,plain,
( qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8636,p57]) ).
cnf(p8638,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8637]) ).
cnf(p8647,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8646,p8638]) ).
cnf(p8648,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8647]) ).
cnf(p8651,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8648]) ).
cnf(p8653,plain,
( qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(suc(X0)))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8651]) ).
cnf(p8665,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8664,p8653]) ).
cnf(p8666,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8665]) ).
cnf(p8669,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8666]) ).
cnf(p8671,plain,
( ~ qtd0(f(suc(suc(suc(X0)))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8669]) ).
cnf(p8672,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(resolution,[status(thm)],[p8671,p8638]) ).
cnf(p8673,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8672]) ).
cnf(p8676,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8673]) ).
cnf(p8678,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(suc(X0)))),s(qtd1)) ),
inference(factoring,[status(thm)],[p8676]) ).
cnf(p8679,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p8678,c20]) ).
cnf(p8681,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p8679]) ).
cnf(p8683,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p8681]) ).
cnf(f6,axiom,
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_141) ).
fof(f6_nnf,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p56,plain,
( qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c6,p52]) ).
cnf(p378,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(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p374,p56]) ).
cnf(p1639,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| 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(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[status(thm)],[p378,p57]) ).
cnf(p2303,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(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p1639]) ).
cnf(p61,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)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[c3,p56]) ).
cnf(p211,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| 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))))) ),
inference(resolution,[status(thm)],[p61,p57]) ).
cnf(p213,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p211,p150]) ).
cnf(p951,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p213]) ).
cnf(p998,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p951]) ).
cnf(p999,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p998,p56]) ).
cnf(p1001,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p999]) ).
cnf(p1003,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1001]) ).
cnf(p2305,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| 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))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p2303,p1003]) ).
cnf(p4143,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| 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))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p2305]) ).
cnf(p5929,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))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p4143]) ).
cnf(p5932,plain,
( qtd2(f(X0),qtd1)
| 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(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p5929]) ).
cnf(p5936,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(suc(suc(suc(X0)))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p5932]) ).
cnf(p5937,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| 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))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(resolution,[status(thm)],[p5936,p211]) ).
cnf(p5939,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| 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))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(factoring,[status(thm)],[p5937]) ).
cnf(p5943,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))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0))))))) ),
inference(factoring,[status(thm)],[p5939]) ).
cnf(p5947,plain,
( qtd2(f(X0),qtd1)
| 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(suc(suc(suc(X0))))))) ),
inference(factoring,[status(thm)],[p5943]) ).
cnf(p5949,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(suc(suc(suc(X0))))))) ),
inference(factoring,[status(thm)],[p5947]) ).
cnf(p5950,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| 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)))) ),
inference(resolution,[status(thm)],[p5949,p55]) ).
cnf(p5951,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)))) ),
inference(factoring,[status(thm)],[p5950]) ).
cnf(p5960,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(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)],[p5951,p2490]) ).
cnf(p6885,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p5960,p65]) ).
cnf(p6886,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(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)],[p6885]) ).
cnf(p6887,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),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)],[p6886,p56]) ).
cnf(p6889,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),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)],[p6887]) ).
cnf(p6891,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(suc(X0)))))))
| ~ qtd0(s(qtd1),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)],[p6889]) ).
cnf(p6892,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(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)],[p6891,p57]) ).
cnf(p6893,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(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)],[p6892]) ).
cnf(p6897,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(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)],[p6893,p55]) ).
cnf(p6898,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(suc(X0))),f(suc(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)],[p6897]) ).
cnf(p5959,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(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)],[p5951,p1027]) ).
cnf(p5972,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p5959,p65]) ).
cnf(p5975,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(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)],[p5972]) ).
cnf(p5976,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(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))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p5975,p56]) ).
cnf(p5978,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(X0))),f(suc(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))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p5976]) ).
cnf(p5980,plain,
( qtd0(f(suc(suc(X0))),f(suc(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))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p5978]) ).
cnf(p5983,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd0(f(suc(suc(X0))),f(suc(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)],[p5980,p57]) ).
cnf(p5984,plain,
( qtd0(f(suc(suc(X0))),f(suc(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(factoring,[status(thm)],[p5983]) ).
cnf(p5956,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p5951,p126]) ).
cnf(p5961,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(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))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p5956,p56]) ).
cnf(p5963,plain,
( qtd2(f(X0),qtd1)
| 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))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p5961]) ).
cnf(p5965,plain,
( 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))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p5963]) ).
cnf(p5970,plain,
( qtd2(f(suc(suc(X0))),s(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(resolution,[status(thm)],[p5965,p57]) ).
cnf(p5971,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)],[p5970]) ).
cnf(p5985,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| qtd0(f(suc(suc(X0))),f(suc(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)],[p5984,p5971]) ).
cnf(p5986,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(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)],[p5985]) ).
cnf(p5991,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(suc(X0))),f(suc(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)],[p5986]) ).
cnf(p5993,plain,
( qtd0(f(suc(suc(X0))),f(suc(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)],[p5991]) ).
cnf(p6899,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(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(resolution,[status(thm)],[p6898,p5993]) ).
cnf(p6900,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)],[p6899]) ).
cnf(p6905,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)],[p6900]) ).
cnf(p6907,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)],[p6905]) ).
cnf(p6908,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)],[p6907,p5971]) ).
cnf(p6909,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)],[p6908]) ).
cnf(p6912,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)],[p6909]) ).
cnf(p6914,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p6912]) ).
cnf(p6915,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)],[p6914,c6]) ).
cnf(p6917,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p6915]) ).
cnf(p6921,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p6917]) ).
cnf(f30,axiom,
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_122) ).
fof(f30_nnf,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p54,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p52,c30]) ).
cnf(p376,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(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p374,p54]) ).
cnf(p1547,plain,
( qtd2(f(suc(X0)),s(qtd1))
| 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(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p376,p57]) ).
cnf(p1549,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(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1547]) ).
cnf(p59,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))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c3,p54]) ).
cnf(p109,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p59,p57]) ).
cnf(p172,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p150,p109]) ).
cnf(p470,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p172]) ).
cnf(p472,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p470]) ).
cnf(p473,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))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p472,p54]) ).
cnf(p477,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p473]) ).
cnf(p479,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p477]) ).
cnf(p1554,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| 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(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1549,p479]) ).
cnf(p2210,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))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1554]) ).
cnf(p2214,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))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2210]) ).
cnf(p2217,plain,
( qtd2(f(X0),qtd1)
| 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(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2214]) ).
cnf(p2219,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(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2217]) ).
cnf(p2220,plain,
( qtd2(f(suc(X0)),s(qtd1))
| 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))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[status(thm)],[p2219,p109]) ).
cnf(p2230,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(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(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p2220]) ).
cnf(p2234,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))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p2230]) ).
cnf(p2237,plain,
( qtd2(f(X0),qtd1)
| 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(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p2234]) ).
cnf(p2239,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(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p2237]) ).
cnf(p2242,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p2239,p55]) ).
cnf(p2251,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p2242]) ).
cnf(p2508,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p2490,p2251]) ).
cnf(p3699,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p2508,p65]) ).
cnf(p3700,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3699]) ).
cnf(p3701,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))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p3700,p54]) ).
cnf(p3704,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p3701]) ).
cnf(p3709,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p3704]) ).
cnf(p3710,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[status(thm)],[p3709,p57]) ).
cnf(p3711,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p3710]) ).
cnf(p3712,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p3711,p55]) ).
cnf(p3713,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(f(suc(X0)),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p3712]) ).
cnf(p2256,plain,
( qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p2251,p1027]) ).
cnf(p2276,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p2256,p65]) ).
cnf(p2277,plain,
( qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p2276]) ).
cnf(p2278,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(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)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p2277,p54]) ).
cnf(p2282,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(X0)),f(suc(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)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p2278]) ).
cnf(p2287,plain,
( qtd0(f(suc(X0)),f(suc(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)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p2282]) ).
cnf(p2290,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd0(f(suc(X0)),f(suc(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)],[p2287,p57]) ).
cnf(p2292,plain,
( qtd0(f(suc(X0)),f(suc(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(factoring,[status(thm)],[p2290]) ).
cnf(p2253,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p2251,p126]) ).
cnf(p2257,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(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)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p2253,p54]) ).
cnf(p2261,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p2257]) ).
cnf(p2266,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p2261]) ).
cnf(p2269,plain,
( qtd2(f(suc(X0)),s(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(resolution,[status(thm)],[p2266,p57]) ).
cnf(p2271,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)],[p2269]) ).
cnf(p2293,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p2292,p2271]) ).
cnf(p2297,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p2293]) ).
cnf(p2300,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p2297]) ).
cnf(p2302,plain,
( qtd0(f(suc(X0)),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p2300]) ).
cnf(p3714,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))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p3713,p2302]) ).
cnf(p3715,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))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p3714]) ).
cnf(p3718,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p3715]) ).
cnf(p3721,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p3718]) ).
cnf(p3722,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)],[p3721,p2271]) ).
cnf(p3723,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)],[p3722]) ).
cnf(p3726,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p3723]) ).
cnf(p3728,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p3726]) ).
cnf(p3729,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p3728,c30]) ).
cnf(p3732,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p3729]) ).
cnf(p3734,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p3732]) ).
cnf(f16,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_2)))))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_139) ).
fof(f16_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_2)))))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(suc(A_2)))))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p3744,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p3734,c16]) ).
cnf(p6997,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6921,p3744]) ).
cnf(p7303,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p6997]) ).
cnf(f9,axiom,
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(A_2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4) ).
fof(f9_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(A_2)))) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(suc(A_2)))) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(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)],[f9_sk]) ).
cnf(p6925,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(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)],[p6921,c9]) ).
cnf(p7245,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6925,p3734]) ).
cnf(p7248,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p7245]) ).
cnf(f26,axiom,
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(B_5))
| ~ qtd2(f(B_5),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_109) ).
fof(f26_nnf,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(B_5))
| ~ qtd2(f(B_5),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [B_5] :
( qtd2(f(B_5),qtd1)
| qtd0(qtd1,f(B_5))
| ~ qtd2(f(B_5),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p53,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p52,c26]) ).
cnf(p375,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p374,p53]) ).
cnf(p404,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p375,p57]) ).
cnf(p407,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p404]) ).
cnf(p58,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[c3,p53]) ).
cnf(p77,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p58,p57]) ).
cnf(p169,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p150,p77]) ).
cnf(p335,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p169]) ).
cnf(p337,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p335]) ).
cnf(p338,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p337,p53]) ).
cnf(p344,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p338]) ).
cnf(p350,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p344]) ).
cnf(p410,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| 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(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p407,p350]) ).
cnf(p916,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p410]) ).
cnf(p920,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p916]) ).
cnf(p923,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p920]) ).
cnf(p925,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p923]) ).
cnf(p926,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| 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(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p925,p77]) ).
cnf(p941,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p926]) ).
cnf(p945,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p941]) ).
cnf(p948,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p945]) ).
cnf(p950,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p948]) ).
cnf(p955,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p950,p55]) ).
cnf(p960,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p955]) ).
cnf(p961,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)],[p960,c26]) ).
cnf(p969,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p961]) ).
cnf(p972,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p969]) ).
cnf(p2506,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p2490,p972]) ).
cnf(p2516,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p2506,p65]) ).
cnf(p2517,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p2516,p53]) ).
cnf(p2531,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2517]) ).
cnf(p2533,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2531]) ).
cnf(p2538,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p2533,p57]) ).
cnf(p2544,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p2538]) ).
cnf(p2547,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p2544,p55]) ).
cnf(p2552,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p2547]) ).
cnf(p1044,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1027,p972]) ).
cnf(p1051,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p1044,p65]) ).
cnf(p1052,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1051,p53]) ).
cnf(p1068,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1052]) ).
cnf(p1070,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1068]) ).
cnf(p1075,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1070,p57]) ).
cnf(p1078,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1075]) ).
cnf(p974,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p972,p126]) ).
cnf(p977,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(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)],[p974,p53]) ).
cnf(p984,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p977]) ).
cnf(p988,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p984]) ).
cnf(p993,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p988,p57]) ).
cnf(p1094,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1078,p993]) ).
cnf(p1100,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1094]) ).
cnf(p1101,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1100]) ).
cnf(p1103,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(f(X0),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1101]) ).
cnf(p2553,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p2552,p1103]) ).
cnf(p2581,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2553]) ).
cnf(p2582,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2581]) ).
cnf(p2584,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p2582]) ).
cnf(p2600,plain,
( qtd2(f(X0),s(qtd1))
| 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)],[p2584,p993]) ).
cnf(p2621,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2600]) ).
cnf(p2622,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2621]) ).
cnf(p2624,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2622]) ).
cnf(p2625,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p2624,c26]) ).
cnf(p2629,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2625]) ).
cnf(p2631,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p2629]) ).
cnf(f7,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_87) ).
fof(f7_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p2632,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p2631,c7]) ).
cnf(f32,axiom,
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_93) ).
fof(f32_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(A_2)))
| ~ qtd0(qtd1,f(A_2)) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,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)],[f32_sk]) ).
cnf(p2633,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p2632,c32]) ).
cnf(p3822,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p3734,p2633]) ).
cnf(p7251,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p7248,p3822]) ).
cnf(p7256,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p7251]) ).
cnf(p7257,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p7256]) ).
cnf(p7258,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(suc(z))))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p7257,p2632]) ).
cnf(p7307,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p7303,p7258]) ).
cnf(p7310,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p7307]) ).
cnf(p7311,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p7310]) ).
cnf(p7312,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p7311,p2632]) ).
cnf(p8783,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8683,p7312]) ).
cnf(p8884,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8783]) ).
cnf(p8886,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8884,p3822]) ).
cnf(p8888,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8886]) ).
cnf(p8889,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8888]) ).
cnf(f8,axiom,
( qtd0(f(B_6),f(suc(suc(B_6))))
| qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_78) ).
fof(f8_nnf,plain,
! [A_2,B_6] :
( qtd0(f(B_6),f(suc(suc(B_6))))
| qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A_2,B_6] :
( qtd0(f(B_6),f(suc(suc(B_6))))
| qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( qtd0(f(X1),f(suc(suc(X1))))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p97,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c8]) ).
cnf(p712,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p97]) ).
cnf(p836,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p712]) ).
cnf(p840,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p836]) ).
cnf(p841,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p840]) ).
cnf(p3758,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p3734,p841]) ).
cnf(p6990,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6921,p3758]) ).
cnf(p7237,plain,
( qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p6990]) ).
cnf(p7242,plain,
( qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p7237,p2632]) ).
cnf(p8897,plain,
( qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8889,p7242]) ).
cnf(p8899,plain,
( qtd0(f(z),f(suc(suc(z))))
| ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8897]) ).
cnf(f28,axiom,
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(A_2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_55) ).
fof(f28_nnf,plain,
! [A_2,B_6] :
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [A_2,B_6] :
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(qtd1,f(B_6))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p186,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c28]) ).
cnf(p187,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p186]) ).
cnf(p198,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p187]) ).
cnf(p3741,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p3734,p198]) ).
cnf(p3896,plain,
( qtd0(f(z),f(suc(z)))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p3741,p2632]) ).
cnf(p8896,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8889,p3896]) ).
cnf(p8898,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8896]) ).
cnf(p8900,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(suc(z))))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8899,p8898]) ).
cnf(p8901,plain,
( qtd0(f(z),f(suc(suc(z))))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8900]) ).
cnf(f0,axiom,
( ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(f(B_6),f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(B_6))
| ~ qtd0(qtd1,f(suc(suc(suc(A_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_6)))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_167) ).
fof(f0_nnf,plain,
! [A_2,B_6] :
( ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(f(B_6),f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(B_6))
| ~ qtd0(qtd1,f(suc(suc(suc(A_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_6)))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A_2,B_6] :
( ~ qtd0(qtd1,f(suc(B_6)))
| ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(f(B_6),f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(B_6))
| ~ qtd0(qtd1,f(suc(suc(suc(A_2)))))
| ~ qtd0(qtd1,f(suc(suc(suc(B_6)))))
| ~ iLEQ(suc(A_2),suc(B_6))
| ~ qtd0(qtd1,f(A_2))
| ~ qtd0(f(A_2),f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(A_2))))
| ~ qtd0(qtd1,f(suc(suc(B_6))))
| ~ qtd0(qtd1,f(suc(A_2))) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(suc(X1))))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(suc(suc(X1)))))
| ~ iLEQ(suc(X0),suc(X1))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p37,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[c0]) ).
cnf(p433,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p37]) ).
cnf(p1852,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p433]) ).
cnf(p1933,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p1852]) ).
cnf(p1936,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p1933]) ).
cnf(p1942,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p1936]) ).
cnf(p3779,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p3734,p1942]) ).
cnf(p6999,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p6921,p3779]) ).
cnf(p7327,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(suc(X0))))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p6999]) ).
cnf(p8904,plain,
( ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8901,p7327]) ).
cnf(p8944,plain,
( ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8904]) ).
cnf(p8945,plain,
( ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8944,p2632]) ).
cnf(p8947,plain,
( qtd2(f(z),qtd1)
| ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8945,p8889]) ).
cnf(p8948,plain,
( ~ qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(suc(suc(z)))))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8947]) ).
cnf(p8950,plain,
( qtd2(f(z),qtd1)
| ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8948,p8683]) ).
cnf(p8951,plain,
( ~ qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p8950]) ).
cnf(p8954,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p8951,p8898]) ).
cnf(p8955,plain,
qtd2(f(z),qtd1),
inference(factoring,[status(thm)],[p8954]) ).
cnf(p8956,plain,
$false,
inference(resolution,[status(thm)],[p8955,c7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO658-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 03:26:39 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 19.95/8.03 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.95/8.03 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------