%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO685-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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:48:39 PM UTC 2026
% Result : Unsatisfiable 65.37s 42.56s
% Output : Proof 65.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 133
% Number of leaves : 37
% Syntax : Number of formulae : 617 ( 11 unt; 0 def)
% Number of atoms : 2928 ( 0 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 3299 ( 988 ~;2311 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 633 ( 2 sgn 92 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f45,axiom,
( ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(A_1))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(B_6)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(B_6))))
| ~ iLEQ(suc(A_1),suc(B_6))
| ~ qtd0(s(s(s(s(qtd1)))),f(B_6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_183) ).
fof(f45_nnf,plain,
! [B_6,A_1] :
( ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(A_1))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(B_6)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(B_6))))
| ~ iLEQ(suc(A_1),suc(B_6))
| ~ qtd0(s(s(s(s(qtd1)))),f(B_6)) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [B_6,A_1] :
( ~ qtd0(f(B_6),f(suc(B_6)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(A_1))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(B_6)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(B_6))))
| ~ iLEQ(suc(A_1),suc(B_6))
| ~ qtd0(s(s(s(s(qtd1)))),f(B_6)) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(X1))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X1))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p383,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(factoring,[status(thm)],[c45]) ).
cnf(p1708,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(factoring,[status(thm)],[p383]) ).
cnf(p1723,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(factoring,[status(thm)],[p1708]) ).
cnf(p1726,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(factoring,[status(thm)],[p1723]) ).
cnf(f22,axiom,
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(B_11))))
| ~ qtd2(f(suc(suc(B_11))),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_52) ).
fof(f22_nnf,plain,
! [B_11] :
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(B_11))))
| ~ qtd2(f(suc(suc(B_11))),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [B_11] :
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(B_11))))
| ~ qtd2(f(suc(suc(B_11))),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(f34,axiom,
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(B_5))
| ~ qtd2(f(B_5),s(s(s(s(s(qtd1)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_113) ).
fof(f34_nnf,plain,
! [B_5] :
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(B_5))
| ~ qtd2(f(B_5),s(s(s(s(s(qtd1)))))) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [B_5] :
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(B_5))
| ~ qtd2(f(B_5),s(s(s(s(s(qtd1)))))) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(X0))
| ~ qtd2(f(X0),s(s(s(s(s(qtd1)))))) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(f44,axiom,
qtd2(f(A),s(s(s(s(s(qtd1)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_53) ).
fof(f44_nnf,plain,
! [A] : qtd2(f(A),s(s(s(s(s(qtd1)))))),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [A] : qtd2(f(A),s(s(s(s(s(qtd1)))))),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
qtd2(f(X0),s(s(s(s(s(qtd1)))))),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p47,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(resolution,[status(thm)],[c34,c44]) ).
cnf(p57,plain,
( qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c22,p47]) ).
cnf(p1729,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(suc(X0))))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1726,p57]) ).
cnf(f1,axiom,
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_130) ).
fof(f1_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1)) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1)) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p62,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p57,c1]) ).
cnf(f14,axiom,
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(s(s(s(s(qtd1)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_191) ).
fof(f14_nnf,plain,
! [B_5] :
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(s(s(s(s(qtd1)))))) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [B_5] :
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(B_5)))
| ~ qtd2(f(suc(B_5)),s(s(s(s(s(qtd1)))))) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(s(s(s(qtd1)))))) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p63,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c14,c44]) ).
cnf(p436,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p62,p63]) ).
cnf(p664,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p436,c22]) ).
cnf(p1450,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p664]) ).
cnf(p1452,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1450]) ).
cnf(f10,axiom,
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(A_1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_79) ).
fof(f10_nnf,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(A_1)))) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A_1] :
( iLEQ(suc(A_1),suc(A_1))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(A_1)))) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(f15,axiom,
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(s(s(s(s(qtd1)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_93) ).
fof(f15_nnf,plain,
! [B_5] :
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(s(s(s(s(qtd1)))))) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [B_5] :
( qtd2(f(B_5),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(suc(B_5))))
| ~ qtd2(f(suc(suc(B_5))),s(s(s(s(s(qtd1)))))) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(s(s(s(s(qtd1)))))) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p75,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[c15,c44]) ).
cnf(p89,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0))) ),
inference(resolution,[status(thm)],[c10,p75]) ).
cnf(p117,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(s(qtd1)))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p89,p63]) ).
cnf(p119,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p117]) ).
cnf(p1453,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1452,p119]) ).
cnf(p1643,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1453]) ).
cnf(p1644,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1643,p57]) ).
cnf(p1645,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1644]) ).
cnf(p1647,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1645]) ).
cnf(p1649,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1647,c22]) ).
cnf(p1656,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1649]) ).
cnf(p1658,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1656]) ).
cnf(p3308,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(suc(X0)))))) ),
inference(resolution,[status(thm)],[p1729,p1658]) ).
cnf(p7932,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p3308]) ).
cnf(p8047,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(suc(X0)))))) ),
inference(factoring,[status(thm)],[p7932]) ).
cnf(p8049,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p8047,p75]) ).
cnf(p8057,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p8049,p63]) ).
cnf(p8058,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p8057]) ).
cnf(f36,axiom,
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(B_6)))
| ~ iLEQ(suc(A_1),suc(B_6))
| ~ qtd0(s(s(s(s(qtd1)))),f(B_6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_34) ).
fof(f36_nnf,plain,
! [B_6,A_1] :
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(B_6)))
| ~ iLEQ(suc(A_1),suc(B_6))
| ~ qtd0(s(s(s(s(qtd1)))),f(B_6)) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [B_6,A_1] :
( qtd0(f(B_6),f(suc(B_6)))
| qtd0(f(A_1),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_1))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(A_1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(B_6)))
| ~ iLEQ(suc(A_1),suc(B_6))
| ~ qtd0(s(s(s(s(qtd1)))),f(B_6)) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(X1))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X1)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p307,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(factoring,[status(thm)],[c36]) ).
cnf(p437,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(factoring,[status(thm)],[p307]) ).
cnf(p439,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(factoring,[status(thm)],[p437]) ).
cnf(p442,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p439,p57]) ).
cnf(p1664,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1658,p442]) ).
cnf(p1686,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1664]) ).
cnf(p1688,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1686]) ).
cnf(p1691,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1688,p63]) ).
cnf(p1692,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1691,c22]) ).
cnf(p1705,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1692]) ).
cnf(p1707,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1705]) ).
cnf(p8059,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p8058,p1707]) ).
cnf(p8060,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8059]) ).
cnf(p8063,plain,
( qtd2(f(suc(suc(X0))),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8060]) ).
cnf(p8064,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p8063,c22]) ).
cnf(p8065,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8064]) ).
cnf(p8067,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p8065]) ).
cnf(f9,axiom,
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(s(qtd1))),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_190) ).
fof(f9_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| ~ qtd0(s(s(s(qtd1))),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ qtd0(s(s(s(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(s(s(s(qtd1))),f(A_2))
| ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_2)))) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p8071,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p8067,c9]) ).
cnf(f37,axiom,
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_11)))
| ~ qtd2(f(suc(B_11)),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_111) ).
fof(f37_nnf,plain,
! [B_11] :
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_11)))
| ~ qtd2(f(suc(B_11)),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [B_11] :
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(B_11)))
| ~ qtd2(f(suc(B_11)),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p54,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd0(s(s(s(s(qtd1)))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p47,c37]) ).
cnf(p1728,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p1726,p54]) ).
cnf(p56,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p54,c1]) ).
cnf(p149,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p56,p63]) ).
cnf(p155,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p149,c37]) ).
cnf(p683,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p155]) ).
cnf(p685,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p683]) ).
cnf(p688,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p685,p119]) ).
cnf(p841,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p688]) ).
cnf(p842,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p841,p54]) ).
cnf(p856,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p842]) ).
cnf(p858,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p856]) ).
cnf(p859,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p858,c37]) ).
cnf(p870,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p859]) ).
cnf(p872,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p870]) ).
cnf(p1789,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0))))) ),
inference(resolution,[status(thm)],[p1728,p872]) ).
cnf(p3790,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p1789]) ).
cnf(p3792,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(suc(X0))))) ),
inference(factoring,[status(thm)],[p3790]) ).
cnf(p3795,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p3792,p75]) ).
cnf(p3796,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p3795,p63]) ).
cnf(p3797,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p3796]) ).
cnf(p441,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p439,p54]) ).
cnf(p881,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p872,p441]) ).
cnf(p1050,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p881]) ).
cnf(p1052,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1050]) ).
cnf(p1055,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1052,p63]) ).
cnf(p1056,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1055,c37]) ).
cnf(p1065,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1056]) ).
cnf(p1067,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1065]) ).
cnf(p3798,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p3797,p1067]) ).
cnf(p3804,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3798]) ).
cnf(p3806,plain,
( qtd2(f(suc(X0)),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3804]) ).
cnf(p3807,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p3806,c37]) ).
cnf(p3809,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3807]) ).
cnf(p3811,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p3809]) ).
cnf(p8114,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p8071,p3811]) ).
cnf(p8117,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p8114]) ).
cnf(f17,axiom,
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_11))
| ~ qtd2(f(B_11),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_95) ).
fof(f17_nnf,plain,
! [B_11] :
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_11))
| ~ qtd2(f(B_11),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [B_11] :
( qtd2(f(B_11),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_11))
| ~ qtd2(f(B_11),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd2(f(X0),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p53,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(resolution,[status(thm)],[p47,c17]) ).
cnf(p1727,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0))))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p1726,p53]) ).
cnf(p55,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p53,c1]) ).
cnf(p101,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p55,p63]) ).
cnf(p102,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p101,c17]) ).
cnf(p158,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p102]) ).
cnf(p160,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p158]) ).
cnf(p164,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p160,p119]) ).
cnf(p300,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p164]) ).
cnf(p301,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(s(s(qtd1)))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p300,p53]) ).
cnf(p368,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(s(qtd1)))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p301]) ).
cnf(p370,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p368]) ).
cnf(p371,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p370,c17]) ).
cnf(p379,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p371]) ).
cnf(p396,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p379]) ).
cnf(p1753,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1727,p396]) ).
cnf(p1938,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1753]) ).
cnf(p1940,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p1938]) ).
cnf(p1945,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1940,p75]) ).
cnf(p1946,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1945,p63]) ).
cnf(p1947,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p1946]) ).
cnf(p440,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p439,p53]) ).
cnf(p459,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p440,p396]) ).
cnf(p580,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p459]) ).
cnf(p585,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(suc(X0))) ),
inference(factoring,[status(thm)],[p580]) ).
cnf(p589,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p585,p63]) ).
cnf(p590,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(resolution,[status(thm)],[p589,c17]) ).
cnf(p598,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p590]) ).
cnf(p601,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p598]) ).
cnf(p1948,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p1947,p601]) ).
cnf(p1961,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p1948]) ).
cnf(p1963,plain,
( qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p1961]) ).
cnf(p1964,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p1963,c17]) ).
cnf(p1967,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p1964]) ).
cnf(p1969,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(factoring,[status(thm)],[p1967]) ).
cnf(f7,axiom,
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_97) ).
fof(f7_nnf,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(B_16))))
| ~ qtd2(f(suc(suc(B_16))),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1972,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd0(s(s(s(qtd1))),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1969,c7]) ).
cnf(f6,axiom,
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(A_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_28) ).
fof(f6_nnf,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A_2] :
( iLEQ(suc(A_2),suc(A_2))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(A_2)) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p2001,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p1972,c6]) ).
cnf(p3819,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p3811,p2001]) ).
cnf(p8125,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p8117,p3819]) ).
cnf(p11616,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p8125]) ).
cnf(p13847,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p11616]) ).
cnf(p13848,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p13847,p1972]) ).
cnf(p13849,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p13848]) ).
cnf(p13851,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p13849]) ).
cnf(p13856,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p13851,c7]) ).
cnf(p13869,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p13856]) ).
cnf(p13871,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p13869]) ).
cnf(f42,axiom,
( ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_2))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(B_12))))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_12)))
| ~ qtd0(f(B_12),f(suc(B_12)))
| ~ qtd0(s(s(s(qtd1))),f(A_2))
| ~ qtd0(s(s(s(qtd1))),f(B_12))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ iLEQ(suc(A_2),suc(B_12)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_73) ).
fof(f42_nnf,plain,
! [A_2,B_12] :
( ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_2))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(B_12))))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_12)))
| ~ qtd0(f(B_12),f(suc(B_12)))
| ~ qtd0(s(s(s(qtd1))),f(A_2))
| ~ qtd0(s(s(s(qtd1))),f(B_12))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ iLEQ(suc(A_2),suc(B_12)) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [A_2,B_12] :
( ~ qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(A_2))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(B_12))))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_12)))
| ~ qtd0(f(B_12),f(suc(B_12)))
| ~ qtd0(s(s(s(qtd1))),f(A_2))
| ~ qtd0(s(s(s(qtd1))),f(B_12))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ iLEQ(suc(A_2),suc(B_12)) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p358,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c42]) ).
cnf(p1629,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p358]) ).
cnf(p1630,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1629]) ).
cnf(p1632,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p1630]) ).
cnf(p13882,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p13871,p1632]) ).
cnf(p15163,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p13882,p3811]) ).
cnf(p15164,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p15163,p1972]) ).
cnf(p19155,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p15164]) ).
cnf(p19157,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p19155]) ).
cnf(f21,axiom,
( qtd0(f(B_12),f(suc(B_12)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_12)))
| ~ qtd0(s(s(s(qtd1))),f(A_2))
| ~ qtd0(s(s(s(qtd1))),f(B_12))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ iLEQ(suc(A_2),suc(B_12)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_49) ).
fof(f21_nnf,plain,
! [A_2,B_12] :
( qtd0(f(B_12),f(suc(B_12)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_12)))
| ~ qtd0(s(s(s(qtd1))),f(A_2))
| ~ qtd0(s(s(s(qtd1))),f(B_12))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ iLEQ(suc(A_2),suc(B_12)) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [A_2,B_12] :
( qtd0(f(B_12),f(suc(B_12)))
| qtd0(f(A_2),f(suc(A_2)))
| ~ qtd0(s(s(s(qtd1))),f(suc(B_12)))
| ~ qtd0(s(s(s(qtd1))),f(A_2))
| ~ qtd0(s(s(s(qtd1))),f(B_12))
| ~ qtd0(s(s(s(qtd1))),f(suc(A_2)))
| ~ iLEQ(suc(A_2),suc(B_12)) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X1)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X1))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p151,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c21]) ).
cnf(p241,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p151]) ).
cnf(p243,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p241]) ).
cnf(p13876,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p13871,p243]) ).
cnf(p13888,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p13876,p3811]) ).
cnf(p13889,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p13888,p1972]) ).
cnf(p13894,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p13889]) ).
cnf(p13896,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p13894]) ).
cnf(p19159,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p19157,p13896]) ).
cnf(p19171,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p19159]) ).
cnf(p19172,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p19171]) ).
cnf(p19174,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(suc(X0))))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p19172]) ).
cnf(p19175,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p19174,p8067]) ).
cnf(p19176,plain,
( qtd2(f(suc(suc(X0))),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p19175]) ).
cnf(p19177,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p19176,c7]) ).
cnf(p19181,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p19177]) ).
cnf(p19183,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p19181]) ).
cnf(f16,axiom,
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_3)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_40) ).
fof(f16_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_3)))) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_3)))) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p19186,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19183,c16]) ).
cnf(f18,axiom,
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_86) ).
fof(f18_nnf,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(B_16)))
| ~ qtd2(f(suc(B_16)),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p398,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p396,c18]) ).
cnf(p414,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p398,c6]) ).
cnf(p651,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p414]) ).
cnf(p3814,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p3811,p651]) ).
cnf(p3938,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p3814,c18]) ).
cnf(p4228,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p3938]) ).
cnf(p4230,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p4228]) ).
cnf(p8126,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p8117,p4230]) ).
cnf(p8658,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p8126]) ).
cnf(p1971,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd0(s(s(s(qtd1))),f(suc(X0))) ),
inference(resolution,[status(thm)],[p1969,c18]) ).
cnf(p8659,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p8658,p1971]) ).
cnf(p8676,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p8659]) ).
cnf(p8678,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p8676]) ).
cnf(p8679,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p8678,c18]) ).
cnf(p8693,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p8679]) ).
cnf(p8695,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p8693]) ).
cnf(p8706,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p8695,p1632]) ).
cnf(p9615,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p8706,p3811]) ).
cnf(p9651,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p9615,p1971]) ).
cnf(p11201,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p9651]) ).
cnf(p11203,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p11201]) ).
cnf(p8700,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p8695,p243]) ).
cnf(p8708,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p8700,p3811]) ).
cnf(p8709,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p8708,p1971]) ).
cnf(p8733,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p8709]) ).
cnf(p8735,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p8733]) ).
cnf(p8736,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p8735,c18]) ).
cnf(p8752,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p8736]) ).
cnf(p8754,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p8752]) ).
cnf(p11204,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p11203,p8754]) ).
cnf(p11205,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p11204]) ).
cnf(p11212,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p11205]) ).
cnf(p11213,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p11212,p8067]) ).
cnf(p11214,plain,
( qtd2(f(suc(X0)),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p11213]) ).
cnf(p11215,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p11214,c18]) ).
cnf(p11222,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p11215]) ).
cnf(p11224,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p11222]) ).
cnf(p19437,plain,
( qtd2(f(X0),s(s(qtd1)))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19186,p11224]) ).
cnf(p19439,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19437]) ).
cnf(f2,axiom,
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_16))
| ~ qtd2(f(B_16),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_125) ).
fof(f2_nnf,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_16))
| ~ qtd2(f(B_16),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [B_16] :
( qtd2(f(B_16),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_16))
| ~ qtd2(f(B_16),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| ~ qtd2(f(X0),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p397,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p396,c2]) ).
cnf(p406,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p397,c6]) ).
cnf(p427,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p406]) ).
cnf(p3813,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p3811,p427]) ).
cnf(p3861,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p3813,c2]) ).
cnf(p3976,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p3861]) ).
cnf(p3978,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p3976]) ).
cnf(p8121,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p8117,p3978]) ).
cnf(p8166,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p8121]) ).
cnf(p1970,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(s(s(s(qtd1))),f(X0)) ),
inference(resolution,[status(thm)],[p1969,c2]) ).
cnf(p8167,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(resolution,[status(thm)],[p8166,p1970]) ).
cnf(p8274,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p8167]) ).
cnf(p8280,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(s(qtd1)))) ),
inference(factoring,[status(thm)],[p8274]) ).
cnf(p8281,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p8280,c2]) ).
cnf(p8296,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p8281]) ).
cnf(p8298,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p8296]) ).
cnf(p8313,plain,
( ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p8298,p1632]) ).
cnf(p8641,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p8313,p3811]) ).
cnf(p8643,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p8641,p1970]) ).
cnf(p9161,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p8643]) ).
cnf(p9163,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p9161]) ).
cnf(p8307,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| ~ qtd0(s(s(s(qtd1))),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p8298,p243]) ).
cnf(p8377,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p8307,p3811]) ).
cnf(p8380,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p8377,p1970]) ).
cnf(p8442,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p8380]) ).
cnf(p8444,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p8442]) ).
cnf(p8445,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p8444,c2]) ).
cnf(p8462,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p8445]) ).
cnf(p8464,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p8462]) ).
cnf(p9164,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p9163,p8464]) ).
cnf(p9170,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p9164]) ).
cnf(p9172,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| ~ qtd0(s(s(s(qtd1))),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p9170]) ).
cnf(p9177,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p9172,p8067]) ).
cnf(p9178,plain,
( qtd2(f(X0),s(s(s(qtd1))))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p9177]) ).
cnf(p9179,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p9178,c2]) ).
cnf(p9182,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p9179]) ).
cnf(p9184,plain,
( qtd2(f(X0),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(factoring,[status(thm)],[p9182]) ).
cnf(f33,axiom,
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_20))))
| ~ qtd2(f(suc(suc(B_20))),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_116) ).
fof(f33_nnf,plain,
! [B_20] :
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_20))))
| ~ qtd2(f(suc(suc(B_20))),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [B_20] :
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(B_20))))
| ~ qtd2(f(suc(suc(B_20))),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,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)],[f33_sk]) ).
cnf(p9187,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(s(s(qtd1)),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p9184,c33]) ).
cnf(f0,axiom,
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(A_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_143) ).
fof(f0_nnf,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(A_3)) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A_3] :
( iLEQ(suc(A_3),suc(A_3))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(A_3)) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p9253,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p9187,c0]) ).
cnf(p11255,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11224,p9253]) ).
cnf(p19444,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19439,p11255]) ).
cnf(p22721,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19444]) ).
cnf(p22734,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p22721]) ).
cnf(p22735,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p22734,p9187]) ).
cnf(p22736,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p22735]) ).
cnf(p22739,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p22736]) ).
cnf(f8,axiom,
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_17))))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(A_3),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_3))))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_74) ).
fof(f8_nnf,plain,
! [B_17,A_3] :
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_17))))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(A_3),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_3))))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17))) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [B_17,A_3] :
( ~ qtd0(s(s(qtd1)),f(suc(suc(B_17))))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ qtd0(f(B_17),f(suc(B_17)))
| ~ qtd0(f(A_3),f(suc(A_3)))
| ~ iLEQ(suc(A_3),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(suc(A_3))))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17))) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X1))))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p65,plain,
( ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[c8]) ).
cnf(p455,plain,
( ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p65]) ).
cnf(p700,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p455]) ).
cnf(p702,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p700]) ).
cnf(p11236,plain,
( ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11224,p702]) ).
cnf(p11392,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(suc(X0))))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11236,p9187]) ).
cnf(p19279,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19183,p11392]) ).
cnf(p20505,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19279]) ).
cnf(p22751,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p22739,p20505]) ).
cnf(p23786,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p22751]) ).
cnf(p23789,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p23786]) ).
cnf(p23791,plain,
( ~ qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p23789]) ).
cnf(f39,axiom,
( qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ iLEQ(suc(A_3),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_115) ).
fof(f39_nnf,plain,
! [B_17,A_3] :
( qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ iLEQ(suc(A_3),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17))) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [B_17,A_3] :
( qtd0(f(B_17),f(suc(B_17)))
| qtd0(f(A_3),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(A_3))
| ~ iLEQ(suc(A_3),suc(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(A_3)))
| ~ qtd0(s(s(qtd1)),f(B_17))
| ~ qtd0(s(s(qtd1)),f(suc(B_17))) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X1)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p329,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[c39]) ).
cnf(p334,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p329]) ).
cnf(p336,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(factoring,[status(thm)],[p334]) ).
cnf(p11231,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11224,p336]) ).
cnf(p11292,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11231,p9187]) ).
cnf(p22750,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p22739,p11292]) ).
cnf(p23767,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p22750]) ).
cnf(p23770,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p23767]) ).
cnf(p23775,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p23770]) ).
cnf(p23792,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p23791,p23775]) ).
cnf(p23793,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p23792]) ).
cnf(p23796,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p23793]) ).
cnf(p23798,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p23796]) ).
cnf(p23799,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p23798,c33]) ).
cnf(p23800,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p23799]) ).
cnf(p23802,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p23800]) ).
cnf(f3,axiom,
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(suc(A_4)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_61) ).
fof(f3_nnf,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(suc(A_4)))) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(suc(A_4)))) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p23803,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p23802,c3]) ).
cnf(f30,axiom,
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(suc(B_20)))
| ~ qtd2(f(suc(B_20)),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_30) ).
fof(f30_nnf,plain,
! [B_20] :
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(suc(B_20)))
| ~ qtd2(f(suc(B_20)),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [B_20] :
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(suc(B_20)))
| ~ qtd2(f(suc(B_20)),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p9186,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(s(s(qtd1)),f(suc(X0))) ),
inference(resolution,[status(thm)],[p9184,c30]) ).
cnf(p9220,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p9186,c0]) ).
cnf(p11248,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11224,p9220]) ).
cnf(p19443,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19439,p11248]) ).
cnf(p20536,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19443]) ).
cnf(p20538,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p20536]) ).
cnf(p20539,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p20538,p9186]) ).
cnf(p20541,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p20539]) ).
cnf(p20544,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p20541]) ).
cnf(p20545,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(resolution,[status(thm)],[p20544,c30]) ).
cnf(p20561,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p20545]) ).
cnf(p20563,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0))) ),
inference(factoring,[status(thm)],[p20561]) ).
cnf(p11391,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(suc(suc(X0)))))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11236,p9186]) ).
cnf(p19239,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19183,p11391]) ).
cnf(p20069,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19239]) ).
cnf(p20577,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p20563,p20069]) ).
cnf(p20606,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20577]) ).
cnf(p20608,plain,
( ~ qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20606]) ).
cnf(p11291,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11231,p9186]) ).
cnf(p20575,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p20563,p11291]) ).
cnf(p20593,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20575]) ).
cnf(p20595,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20593]) ).
cnf(p20610,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p20608,p20595]) ).
cnf(p20613,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20610]) ).
cnf(p20614,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20613]) ).
cnf(p20616,plain,
( qtd2(f(suc(X0)),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20614]) ).
cnf(p20617,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p20616,c30]) ).
cnf(p20619,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20617]) ).
cnf(p20621,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(factoring,[status(thm)],[p20619]) ).
cnf(p23862,plain,
( qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p23803,p20621]) ).
cnf(p23866,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p23862]) ).
cnf(f12,axiom,
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(B_20))
| ~ qtd2(f(B_20),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_184) ).
fof(f12_nnf,plain,
! [B_20] :
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(B_20))
| ~ qtd2(f(B_20),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [B_20] :
( qtd2(f(B_20),s(qtd1))
| qtd0(s(qtd1),f(B_20))
| ~ qtd2(f(B_20),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p9185,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(s(s(qtd1)),f(X0)) ),
inference(resolution,[status(thm)],[p9184,c12]) ).
cnf(p11390,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(suc(X0))))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11236,p9185]) ).
cnf(p19231,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19183,p11390]) ).
cnf(p19733,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19231]) ).
cnf(p3979,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd0(s(s(qtd1)),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p3978,c12]) ).
cnf(p4002,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p3979,c0]) ).
cnf(p4189,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4002]) ).
cnf(p4190,plain,
( ~ qtd0(s(s(qtd1)),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p4189]) ).
cnf(p11245,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11224,p4190]) ).
cnf(p11321,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p11245,c12]) ).
cnf(p11397,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p11321]) ).
cnf(p11399,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p11397]) ).
cnf(p19442,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19439,p11399]) ).
cnf(p19511,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(s(qtd1)),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19442]) ).
cnf(p19514,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19511,p9185]) ).
cnf(p19519,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19514]) ).
cnf(p19521,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19519]) ).
cnf(p19522,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(resolution,[status(thm)],[p19521,c12]) ).
cnf(p19549,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p19522]) ).
cnf(p19551,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p19549]) ).
cnf(p19736,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19733,p19551]) ).
cnf(p19740,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19736]) ).
cnf(p19742,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19740]) ).
cnf(p11290,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p11231,p9185]) ).
cnf(p19565,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p19551,p11290]) ).
cnf(p19704,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p19565]) ).
cnf(p19706,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(s(qtd1)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p19704]) ).
cnf(p19707,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p19706,c12]) ).
cnf(p19720,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p19707]) ).
cnf(p19722,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p19720]) ).
cnf(p19745,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(resolution,[status(thm)],[p19742,p19722]) ).
cnf(p19746,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19745]) ).
cnf(p19748,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(s(qtd1))) ),
inference(factoring,[status(thm)],[p19746]) ).
cnf(p19749,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p19748,c12]) ).
cnf(p19752,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p19749]) ).
cnf(p19754,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(s(qtd1),f(X0)) ),
inference(factoring,[status(thm)],[p19752]) ).
cnf(f40,axiom,
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(suc(suc(B_23))))
| ~ qtd2(f(suc(suc(B_23))),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11) ).
fof(f40_nnf,plain,
! [B_23] :
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(suc(suc(B_23))))
| ~ qtd2(f(suc(suc(B_23))),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [B_23] :
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(suc(suc(B_23))))
| ~ qtd2(f(suc(suc(B_23))),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p19757,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd0(s(qtd1),f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p19754,c40]) ).
cnf(f43,axiom,
( iLEQ(suc(A_4),suc(A_4))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(A_4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_204) ).
fof(f43_nnf,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(A_4)) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [A_4] :
( iLEQ(suc(A_4),suc(A_4))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(A_4)) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,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)],[f43_sk]) ).
cnf(p19773,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(resolution,[status(thm)],[p19757,c43]) ).
cnf(p20630,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p20621,p19773]) ).
cnf(p23875,plain,
( iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p23866,p20630]) ).
cnf(p24804,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p23875]) ).
cnf(p24805,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p24804]) ).
cnf(p24806,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p24805,p19757]) ).
cnf(p24807,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p24806]) ).
cnf(p24809,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| iLEQ(suc(suc(suc(X0))),suc(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p24807]) ).
cnf(f20,axiom,
( ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(f(B_21),f(suc(B_21)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(suc(A_4))))
| ~ qtd0(s(qtd1),f(B_21))
| ~ qtd0(s(qtd1),f(suc(suc(B_21))))
| ~ qtd0(s(qtd1),f(suc(B_21)))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ iLEQ(suc(A_4),suc(B_21)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_175) ).
fof(f20_nnf,plain,
! [A_4,B_21] :
( ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(f(B_21),f(suc(B_21)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(suc(A_4))))
| ~ qtd0(s(qtd1),f(B_21))
| ~ qtd0(s(qtd1),f(suc(suc(B_21))))
| ~ qtd0(s(qtd1),f(suc(B_21)))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ iLEQ(suc(A_4),suc(B_21)) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [A_4,B_21] :
( ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(f(B_21),f(suc(B_21)))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(suc(suc(A_4))))
| ~ qtd0(s(qtd1),f(B_21))
| ~ qtd0(s(qtd1),f(suc(suc(B_21))))
| ~ qtd0(s(qtd1),f(suc(B_21)))
| ~ qtd0(f(A_4),f(suc(A_4)))
| ~ iLEQ(suc(A_4),suc(B_21)) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(suc(X1))))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p128,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c20]) ).
cnf(p788,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p128]) ).
cnf(p790,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p788]) ).
cnf(p792,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p790]) ).
cnf(p24819,plain,
( ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(suc(suc(X0))))))
| ~ qtd0(s(qtd1),f(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)],[p24809,p792]) ).
cnf(f31,axiom,
( qtd0(f(B_21),f(suc(B_21)))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(B_21))
| ~ qtd0(s(qtd1),f(suc(B_21)))
| ~ iLEQ(suc(A_4),suc(B_21)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_87) ).
fof(f31_nnf,plain,
! [A_4,B_21] :
( qtd0(f(B_21),f(suc(B_21)))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(B_21))
| ~ qtd0(s(qtd1),f(suc(B_21)))
| ~ iLEQ(suc(A_4),suc(B_21)) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A_4,B_21] :
( qtd0(f(B_21),f(suc(B_21)))
| qtd0(f(A_4),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(A_4))
| ~ qtd0(s(qtd1),f(suc(A_4)))
| ~ qtd0(s(qtd1),f(B_21))
| ~ qtd0(s(qtd1),f(suc(B_21)))
| ~ iLEQ(suc(A_4),suc(B_21)) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X1))
| ~ qtd0(s(qtd1),f(suc(X1)))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p253,plain,
( qtd0(f(X0),f(suc(X0)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c31]) ).
cnf(p271,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p253]) ).
cnf(p272,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p271]) ).
cnf(p24815,plain,
( qtd0(f(suc(suc(X0))),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(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)],[p24809,p272]) ).
cnf(p24823,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| qtd0(f(suc(suc(X0))),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)],[p24815,p20621]) ).
cnf(p24824,plain,
( qtd0(f(suc(suc(X0))),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)],[p24823]) ).
cnf(p24825,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(resolution,[status(thm)],[p24824,p19757]) ).
cnf(p24827,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)],[p24825]) ).
cnf(p24829,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)],[p24827]) ).
cnf(p24846,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1))
| ~ qtd0(s(qtd1),f(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(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(resolution,[status(thm)],[p24819,p24829]) ).
cnf(p25400,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(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(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p24846]) ).
cnf(p25749,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(s(qtd1),f(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(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p25400]) ).
cnf(p25751,plain,
( ~ qtd0(s(qtd1),f(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(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p25749]) ).
cnf(p25752,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ 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)],[p25751,p20621]) ).
cnf(p25753,plain,
( ~ 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(factoring,[status(thm)],[p25752]) ).
cnf(p25754,plain,
( qtd2(f(suc(suc(X0))),s(qtd1))
| ~ 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)],[p25753,p23802]) ).
cnf(p25755,plain,
( ~ 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)],[p25754]) ).
cnf(p25756,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(resolution,[status(thm)],[p25755,p19757]) ).
cnf(p25757,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)],[p25756]) ).
cnf(p25759,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0))))
| qtd2(f(suc(suc(X0))),s(qtd1)) ),
inference(factoring,[status(thm)],[p25757]) ).
cnf(p25760,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)],[p25759,c40]) ).
cnf(p25761,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p25760]) ).
cnf(p25763,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(suc(X0)))) ),
inference(factoring,[status(thm)],[p25761]) ).
cnf(f35,axiom,
( iLEQ(suc(A_5),suc(A_5))
| ~ qtd0(qtd1,f(A_5))
| ~ qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(suc(A_5)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_44) ).
fof(f35_nnf,plain,
! [A_5] :
( iLEQ(suc(A_5),suc(A_5))
| ~ qtd0(qtd1,f(A_5))
| ~ qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(suc(A_5)))) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [A_5] :
( iLEQ(suc(A_5),suc(A_5))
| ~ qtd0(qtd1,f(A_5))
| ~ qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(suc(A_5)))) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0)))) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p25765,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p25763,c35]) ).
cnf(f28,axiom,
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(suc(B_23)))
| ~ qtd2(f(suc(B_23)),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_168) ).
fof(f28_nnf,plain,
! [B_23] :
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(suc(B_23)))
| ~ qtd2(f(suc(B_23)),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [B_23] :
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(suc(B_23)))
| ~ qtd2(f(suc(B_23)),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd2(f(suc(X0)),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p19756,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(s(qtd1),f(suc(X0))) ),
inference(resolution,[status(thm)],[p19754,c28]) ).
cnf(p19766,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p19756,c43]) ).
cnf(p20626,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p20621,p19766]) ).
cnf(p23874,plain,
( iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p23866,p20626]) ).
cnf(p24475,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p23874]) ).
cnf(p24476,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24475]) ).
cnf(p24477,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p24476,p19756]) ).
cnf(p24481,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24477]) ).
cnf(p24483,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| iLEQ(suc(suc(X0)),suc(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24481]) ).
cnf(p24492,plain,
( ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(suc(suc(X0)))))
| ~ qtd0(s(qtd1),f(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)],[p24483,p792]) ).
cnf(p24488,plain,
( qtd0(f(suc(X0)),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(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)],[p24483,p272]) ).
cnf(p24496,plain,
( qtd2(f(suc(X0)),s(qtd1))
| qtd0(f(suc(X0)),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)],[p24488,p20621]) ).
cnf(p24498,plain,
( qtd0(f(suc(X0)),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)],[p24496]) ).
cnf(p24499,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p24498,p19756]) ).
cnf(p24502,plain,
( qtd2(f(X0),qtd1)
| qtd0(f(suc(X0)),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24499]) ).
cnf(p24504,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)],[p24502]) ).
cnf(p24717,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1))
| ~ qtd0(s(qtd1),f(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(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(resolution,[status(thm)],[p24492,p24504]) ).
cnf(p24872,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| ~ qtd0(s(qtd1),f(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(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24717]) ).
cnf(p24875,plain,
( qtd2(f(X0),qtd1)
| ~ qtd0(s(qtd1),f(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(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24872]) ).
cnf(p24877,plain,
( ~ qtd0(s(qtd1),f(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(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24875]) ).
cnf(p24879,plain,
( qtd2(f(suc(X0)),s(qtd1))
| ~ 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)],[p24877,p20621]) ).
cnf(p24880,plain,
( ~ 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(factoring,[status(thm)],[p24879]) ).
cnf(p24881,plain,
( qtd2(f(suc(X0)),s(qtd1))
| ~ 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)],[p24880,p23802]) ).
cnf(p24882,plain,
( ~ 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)],[p24881]) ).
cnf(p24885,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(resolution,[status(thm)],[p24882,p19756]) ).
cnf(p24887,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24885]) ).
cnf(p24889,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(suc(X0)),s(qtd1)) ),
inference(factoring,[status(thm)],[p24887]) ).
cnf(p24890,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(resolution,[status(thm)],[p24889,c28]) ).
cnf(p24895,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p24890]) ).
cnf(p24897,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(suc(X0))) ),
inference(factoring,[status(thm)],[p24895]) ).
cnf(p25822,plain,
( qtd2(f(X0),qtd1)
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(resolution,[status(thm)],[p25765,p24897]) ).
cnf(p25824,plain,
( iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1) ),
inference(factoring,[status(thm)],[p25822]) ).
cnf(f46,axiom,
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(B_23))
| ~ qtd2(f(B_23),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_173) ).
fof(f46_nnf,plain,
! [B_23] :
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(B_23))
| ~ qtd2(f(B_23),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
! [B_23] :
( qtd2(f(B_23),qtd1)
| qtd0(qtd1,f(B_23))
| ~ qtd2(f(B_23),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p19755,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd0(s(qtd1),f(X0)) ),
inference(resolution,[status(thm)],[p19754,c46]) ).
cnf(p19759,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p19755,c43]) ).
cnf(p20625,plain,
( iLEQ(suc(X0),suc(X0))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p20621,p19759]) ).
cnf(p23873,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p23866,p20625]) ).
cnf(p24079,plain,
( iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p23873]) ).
cnf(p24082,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p24079]) ).
cnf(p24083,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(resolution,[status(thm)],[p24082,p19755]) ).
cnf(p24087,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p24083]) ).
cnf(p24089,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0))
| qtd2(f(X0),s(qtd1)) ),
inference(factoring,[status(thm)],[p24087]) ).
cnf(p24091,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)],[p24089,c46]) ).
cnf(p24106,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p24091]) ).
cnf(p24108,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p24106]) ).
cnf(p24117,plain,
( ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| ~ qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24108,p792]) ).
cnf(p24113,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24108,p272]) ).
cnf(p24124,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24113,p20621]) ).
cnf(p24126,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24124,p19755]) ).
cnf(p24130,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24126]) ).
cnf(p24133,plain,
( qtd2(f(X0),s(qtd1))
| qtd0(f(X0),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24130]) ).
cnf(p24153,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24117,p24133]) ).
cnf(p24382,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24153]) ).
cnf(p24384,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| ~ qtd0(s(qtd1),f(suc(X0)))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24382]) ).
cnf(p24385,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24384,p20621]) ).
cnf(p24388,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(s(qtd1),f(X0))
| ~ qtd0(s(qtd1),f(suc(suc(X0))))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24385]) ).
cnf(p24393,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),s(qtd1))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24388,p23802]) ).
cnf(p24394,plain,
( qtd2(f(X0),s(qtd1))
| ~ qtd0(s(qtd1),f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24393]) ).
cnf(p24395,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24394,p19755]) ).
cnf(p24403,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24395]) ).
cnf(p24405,plain,
( qtd2(f(X0),s(qtd1))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24403]) ).
cnf(p24406,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0))
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(resolution,[status(thm)],[p24405,c46]) ).
cnf(p24418,plain,
( qtd2(f(X0),qtd1)
| qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24406]) ).
cnf(p24420,plain,
( qtd2(f(X0),qtd1)
| qtd0(qtd1,f(X0)) ),
inference(factoring,[status(thm)],[p24418]) ).
cnf(f19,axiom,
~ qtd2(f(z),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_96) ).
fof(f19_nnf,plain,
~ qtd2(f(z),qtd1),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
~ qtd2(f(z),qtd1),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
~ qtd2(f(z),qtd1),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p24421,plain,
qtd0(qtd1,f(z)),
inference(resolution,[status(thm)],[p24420,c19]) ).
cnf(f38,axiom,
( iLEQ(suc(A_5),suc(A_5))
| qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19) ).
fof(f38_nnf,plain,
! [A_5] :
( iLEQ(suc(A_5),suc(A_5))
| qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5)) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [A_5] :
( iLEQ(suc(A_5),suc(A_5))
| qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5)) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,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)],[f38_sk]) ).
cnf(p24422,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z))) ),
inference(resolution,[status(thm)],[p24421,c38]) ).
cnf(p24927,plain,
( iLEQ(suc(z),suc(z))
| qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p24897,p24422]) ).
cnf(p25828,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25824,p24927]) ).
cnf(p25832,plain,
( qtd2(f(z),qtd1)
| iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p25828]) ).
cnf(p25833,plain,
( iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p25832]) ).
cnf(p25834,plain,
( iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25833,p24421]) ).
cnf(f4,axiom,
( qtd0(f(B_24),f(suc(B_24)))
| qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(B_24))
| ~ qtd0(qtd1,f(suc(B_24)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5))
| ~ iLEQ(suc(A_5),suc(B_24)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_169) ).
fof(f4_nnf,plain,
! [A_5,B_24] :
( qtd0(f(B_24),f(suc(B_24)))
| qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(B_24))
| ~ qtd0(qtd1,f(suc(B_24)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5))
| ~ iLEQ(suc(A_5),suc(B_24)) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A_5,B_24] :
( qtd0(f(B_24),f(suc(B_24)))
| qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(B_24))
| ~ qtd0(qtd1,f(suc(B_24)))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5))
| ~ iLEQ(suc(A_5),suc(B_24)) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( qtd0(f(X1),f(suc(X1)))
| qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X1))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X1)) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p52,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[c4]) ).
cnf(p78,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p52]) ).
cnf(p79,plain,
( qtd0(f(X0),f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0)) ),
inference(factoring,[status(thm)],[p78]) ).
cnf(p25836,plain,
( qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z)))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25834,p79]) ).
cnf(p25845,plain,
( qtd0(f(z),f(suc(z)))
| ~ qtd0(qtd1,f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25836,p24421]) ).
cnf(p25846,plain,
( qtd2(f(z),qtd1)
| qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25845,p24897]) ).
cnf(p25847,plain,
( qtd0(f(z),f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p25846]) ).
cnf(f32,axiom,
( ~ qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(B_24))
| ~ qtd0(qtd1,f(suc(B_24)))
| ~ qtd0(qtd1,f(suc(suc(A_5))))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5))
| ~ iLEQ(suc(A_5),suc(B_24))
| ~ qtd0(qtd1,f(suc(suc(B_24))))
| ~ qtd0(f(B_24),f(suc(B_24))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_105) ).
fof(f32_nnf,plain,
! [B_24,A_5] :
( ~ qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(B_24))
| ~ qtd0(qtd1,f(suc(B_24)))
| ~ qtd0(qtd1,f(suc(suc(A_5))))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5))
| ~ iLEQ(suc(A_5),suc(B_24))
| ~ qtd0(qtd1,f(suc(suc(B_24))))
| ~ qtd0(f(B_24),f(suc(B_24))) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [B_24,A_5] :
( ~ qtd0(f(A_5),f(suc(A_5)))
| ~ qtd0(qtd1,f(B_24))
| ~ qtd0(qtd1,f(suc(B_24)))
| ~ qtd0(qtd1,f(suc(suc(A_5))))
| ~ qtd0(qtd1,f(suc(A_5)))
| ~ qtd0(qtd1,f(A_5))
| ~ iLEQ(suc(A_5),suc(B_24))
| ~ qtd0(qtd1,f(suc(suc(B_24))))
| ~ qtd0(f(B_24),f(suc(B_24))) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( ~ qtd0(f(X1),f(suc(X1)))
| ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X1))))
| ~ qtd0(qtd1,f(suc(X1)))
| ~ qtd0(qtd1,f(X1))
| ~ iLEQ(suc(X1),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p281,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[c32]) ).
cnf(p562,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p281]) ).
cnf(p566,plain,
( ~ qtd0(qtd1,f(X0))
| ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p562]) ).
cnf(p571,plain,
( ~ qtd0(qtd1,f(suc(X0)))
| ~ qtd0(qtd1,f(X0))
| ~ iLEQ(suc(X0),suc(X0))
| ~ qtd0(qtd1,f(suc(suc(X0))))
| ~ qtd0(f(X0),f(suc(X0))) ),
inference(factoring,[status(thm)],[p566]) ).
cnf(p25852,plain,
( ~ qtd0(qtd1,f(suc(z)))
| ~ qtd0(qtd1,f(z))
| ~ iLEQ(suc(z),suc(z))
| ~ qtd0(qtd1,f(suc(suc(z))))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25847,p571]) ).
cnf(p25872,plain,
( qtd2(f(z),qtd1)
| ~ qtd0(qtd1,f(suc(z)))
| ~ qtd0(qtd1,f(z))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25852,p25763]) ).
cnf(p25873,plain,
( ~ qtd0(qtd1,f(suc(z)))
| ~ qtd0(qtd1,f(z))
| ~ iLEQ(suc(z),suc(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p25872]) ).
cnf(p25875,plain,
( qtd2(f(z),qtd1)
| ~ qtd0(qtd1,f(suc(z)))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25873,p25834]) ).
cnf(p25876,plain,
( ~ qtd0(qtd1,f(suc(z)))
| ~ qtd0(qtd1,f(z))
| qtd2(f(z),qtd1) ),
inference(factoring,[status(thm)],[p25875]) ).
cnf(p25877,plain,
( ~ qtd0(qtd1,f(suc(z)))
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25876,p24421]) ).
cnf(p25878,plain,
( qtd2(f(z),qtd1)
| qtd2(f(z),qtd1) ),
inference(resolution,[status(thm)],[p25877,p24897]) ).
cnf(p25880,plain,
qtd2(f(z),qtd1),
inference(factoring,[status(thm)],[p25878]) ).
cnf(p25881,plain,
$false,
inference(resolution,[status(thm)],[p25880,c19]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO685-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n013.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Fri Sep 25 03:23:21 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 65.37/42.56 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 65.37/42.56 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------