%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYO630-1 : TPTP v9.3.1. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:48:33 PM UTC 2026
% Result : Unsatisfiable 4.92s 1.19s
% Output : Proof 4.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 16
% Syntax : Number of formulae : 248 ( 19 unt; 0 def)
% Number of atoms : 1231 ( 0 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 1146 ( 163 ~; 983 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 8 ( 3 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-1 aty)
% Number of variables : 302 ( 3 sgn 42 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f15,axiom,
( qtd2(f(B_0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(B_0))
| ~ iLEQ(A_1,B_0)
| ~ qtd2(f(A_1),s(s(s(s(s(qtd1)))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7_16) ).
fof(f15_nnf,plain,
! [A_1,B_0] :
( qtd2(f(B_0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(B_0))
| ~ iLEQ(A_1,B_0)
| ~ qtd2(f(A_1),s(s(s(s(s(qtd1)))))) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A_1,B_0] :
( qtd2(f(B_0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(B_0))
| ~ iLEQ(A_1,B_0)
| ~ qtd2(f(A_1),s(s(s(s(s(qtd1)))))) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( qtd2(f(X1),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(X1))
| ~ iLEQ(X0,X1)
| ~ qtd2(f(X0),s(s(s(s(s(qtd1)))))) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(f0,axiom,
( qtd2(f(A),s(s(s(s(s(qtd1))))))
| qtd0(s(s(s(s(s(qtd1))))),f(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8_01) ).
fof(f0_nnf,plain,
! [A] :
( qtd2(f(A),s(s(s(s(s(qtd1))))))
| qtd0(s(s(s(s(s(qtd1))))),f(A)) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A] :
( qtd2(f(A),s(s(s(s(s(qtd1))))))
| qtd0(s(s(s(s(s(qtd1))))),f(A)) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( qtd2(f(X0),s(s(s(s(s(qtd1))))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p32,plain,
( qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd2(f(X1),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(X1))
| ~ iLEQ(X0,X1) ),
inference(resolution,[status(thm)],[c15,c0]) ).
cnf(f1,axiom,
iLEQ(A_2,g(A_2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13_02) ).
fof(f1_nnf,plain,
! [A_2] : iLEQ(A_2,g(A_2)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A_2] : iLEQ(A_2,g(A_2)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
iLEQ(X0,g(X0)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p34,plain,
( qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p32,c1]) ).
cnf(f16,axiom,
( qtd2(f(B_2),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_2))
| ~ iLEQ(A_4,B_2)
| ~ qtd2(f(A_4),s(s(s(s(qtd1))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_26_17) ).
fof(f16_nnf,plain,
! [A_4,B_2] :
( qtd2(f(B_2),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_2))
| ~ iLEQ(A_4,B_2)
| ~ qtd2(f(A_4),s(s(s(s(qtd1))))) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A_4,B_2] :
( qtd2(f(B_2),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(B_2))
| ~ iLEQ(A_4,B_2)
| ~ qtd2(f(A_4),s(s(s(s(qtd1))))) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( qtd2(f(X1),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(X0,X1)
| ~ qtd2(f(X0),s(s(s(s(qtd1))))) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p36,plain,
( qtd2(f(X1),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(g(X0),X1)
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p34,c16]) ).
cnf(p39,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p36,c1]) ).
cnf(f14,axiom,
( qtd2(f(B_4),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_4))
| ~ iLEQ(A_7,B_4)
| ~ qtd2(f(A_7),s(s(s(qtd1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16_15) ).
fof(f14_nnf,plain,
! [A_7,B_4] :
( qtd2(f(B_4),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_4))
| ~ iLEQ(A_7,B_4)
| ~ qtd2(f(A_7),s(s(s(qtd1)))) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [A_7,B_4] :
( qtd2(f(B_4),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(B_4))
| ~ iLEQ(A_7,B_4)
| ~ qtd2(f(A_7),s(s(s(qtd1)))) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(X0,X1)
| ~ qtd2(f(X0),s(s(s(qtd1)))) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p42,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p39,c14]) ).
cnf(p54,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p42,c1]) ).
cnf(f31,axiom,
( qtd2(f(B_6),s(qtd1))
| qtd0(s(qtd1),f(B_6))
| ~ iLEQ(A_10,B_6)
| ~ qtd2(f(A_10),s(s(qtd1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17_32) ).
fof(f31_nnf,plain,
! [A_10,B_6] :
( qtd2(f(B_6),s(qtd1))
| qtd0(s(qtd1),f(B_6))
| ~ iLEQ(A_10,B_6)
| ~ qtd2(f(A_10),s(s(qtd1))) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A_10,B_6] :
( qtd2(f(B_6),s(qtd1))
| qtd0(s(qtd1),f(B_6))
| ~ iLEQ(A_10,B_6)
| ~ qtd2(f(A_10),s(s(qtd1))) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(X0,X1)
| ~ qtd2(f(X0),s(s(qtd1))) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p78,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p54,c31]) ).
cnf(p89,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p78,c1]) ).
cnf(f5,axiom,
( qtd2(f(B_8),qtd1)
| qtd0(qtd1,f(B_8))
| ~ iLEQ(A_13,B_8)
| ~ qtd2(f(A_13),s(qtd1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1_06) ).
fof(f5_nnf,plain,
! [A_13,B_8] :
( qtd2(f(B_8),qtd1)
| qtd0(qtd1,f(B_8))
| ~ iLEQ(A_13,B_8)
| ~ qtd2(f(A_13),s(qtd1)) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A_13,B_8] :
( qtd2(f(B_8),qtd1)
| qtd0(qtd1,f(B_8))
| ~ iLEQ(A_13,B_8)
| ~ qtd2(f(A_13),s(qtd1)) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(X0,X1)
| ~ qtd2(f(X0),s(qtd1)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p134,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p89,c5]) ).
cnf(f3,axiom,
iLEQ(A_14,A_14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18_04) ).
fof(f3_nnf,plain,
! [A_14] : iLEQ(A_14,A_14),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A_14] : iLEQ(A_14,A_14),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
iLEQ(X0,X0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p148,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p134,c3]) ).
cnf(f9,axiom,
( qtd0(f(A_2),f(g(A_2)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(A_2)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(A_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3_10) ).
fof(f9_nnf,plain,
! [A_2] :
( qtd0(f(A_2),f(g(A_2)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(A_2)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(A_2)) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A_2] :
( qtd0(f(A_2),f(g(A_2)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(A_2)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(A_2)) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(X0)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p161,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(X0)))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p148,c9]) ).
cnf(p33,plain,
( qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd2(f(X0),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(resolution,[status(thm)],[p32,c3]) ).
cnf(p220,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0)))
| qtd0(f(X0),f(g(X0)))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p161,p33]) ).
cnf(p258,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(f(X0),f(g(X0)))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p220]) ).
cnf(f4,axiom,
~ qtd0(f(A_8),f(g(A_8))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_31_05) ).
fof(f4_nnf,plain,
! [A_8] : ~ qtd0(f(A_8),f(g(A_8))),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A_8] : ~ qtd0(f(A_8),f(g(A_8))),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
~ qtd0(f(X0),f(g(X0))),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p346,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p258,c4]) ).
cnf(p353,plain,
( qtd2(f(X1),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(g(X0),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p346,c16]) ).
cnf(p416,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| ~ iLEQ(g(X0),g(g(X0)))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p353]) ).
cnf(p448,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p416,c1]) ).
cnf(p449,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p448,c14]) ).
cnf(p461,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| ~ iLEQ(g(g(X0)),g(g(g(X0))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p449]) ).
cnf(p464,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p461,c1]) ).
cnf(p465,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p464,c31]) ).
cnf(p467,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p465,c1]) ).
cnf(p468,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p467]) ).
cnf(p470,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p468,c5]) ).
cnf(p473,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p470,c3]) ).
cnf(p474,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p473]) ).
cnf(p476,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p474]) ).
cnf(f29,axiom,
( qtd0(f(A_5),f(g(A_5)))
| ~ qtd0(s(s(s(s(qtd1)))),f(g(A_5)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12_30) ).
fof(f29_nnf,plain,
! [A_5] :
( qtd0(f(A_5),f(g(A_5)))
| ~ qtd0(s(s(s(s(qtd1)))),f(g(A_5)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_5)) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [A_5] :
( qtd0(f(A_5),f(g(A_5)))
| ~ qtd0(s(s(s(s(qtd1)))),f(g(A_5)))
| ~ qtd0(s(s(s(s(qtd1)))),f(A_5)) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(g(X0)))
| ~ qtd0(s(s(s(s(qtd1)))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p478,plain,
( qtd0(f(g(X0)),f(g(g(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(g(g(X0))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p476,c29]) ).
cnf(p38,plain,
( qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p36,c3]) ).
cnf(p40,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(X0)))
| qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p38,c9]) ).
cnf(p45,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0)))
| qtd0(f(X0),f(g(X0)))
| qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p40,p33]) ).
cnf(p58,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(f(X0),f(g(X0)))
| qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p45]) ).
cnf(p59,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p58,c4]) ).
cnf(p60,plain,
( qtd2(f(X1),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(g(X0),X1)
| qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p59,c16]) ).
cnf(p61,plain,
( qtd2(f(g(X0)),s(s(s(qtd1))))
| ~ iLEQ(g(X0),g(X0))
| qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p60]) ).
cnf(p65,plain,
( ~ iLEQ(g(X0),g(X0))
| qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p61]) ).
cnf(p67,plain,
( qtd2(f(g(X0)),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(X0)))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p65,c3]) ).
cnf(p480,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(f(g(X0)),f(g(g(X0))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p478,p67]) ).
cnf(p481,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(f(g(X0)),f(g(g(X0))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p480]) ).
cnf(p482,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p481,c4]) ).
cnf(p484,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p482,c14]) ).
cnf(p485,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| ~ iLEQ(g(g(X0)),g(g(g(X0))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p484]) ).
cnf(p487,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p485,c1]) ).
cnf(p488,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p487,c31]) ).
cnf(p491,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p488,c1]) ).
cnf(p492,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p491]) ).
cnf(p493,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p492,c5]) ).
cnf(p496,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p493,c3]) ).
cnf(p498,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p496]) ).
cnf(p500,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p498]) ).
cnf(f10,axiom,
( qtd0(f(A_8),f(g(A_8)))
| ~ qtd0(s(s(s(qtd1))),f(g(A_8)))
| ~ qtd0(s(s(s(qtd1))),f(A_8)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_21_11) ).
fof(f10_nnf,plain,
! [A_8] :
( qtd0(f(A_8),f(g(A_8)))
| ~ qtd0(s(s(s(qtd1))),f(g(A_8)))
| ~ qtd0(s(s(s(qtd1))),f(A_8)) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A_8] :
( qtd0(f(A_8),f(g(A_8)))
| ~ qtd0(s(s(s(qtd1))),f(g(A_8)))
| ~ qtd0(s(s(s(qtd1))),f(A_8)) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(s(qtd1))),f(g(X0)))
| ~ qtd0(s(s(s(qtd1))),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p501,plain,
( qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(g(g(g(X0)))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p500,c10]) ).
cnf(p53,plain,
( qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p42,c3]) ).
cnf(p55,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(X0)))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p53,c9]) ).
cnf(p79,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0)))
| qtd0(f(X0),f(g(X0)))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p55,p33]) ).
cnf(p90,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(f(X0),f(g(X0)))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p79]) ).
cnf(p91,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p90,c4]) ).
cnf(p92,plain,
( qtd2(f(X1),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(g(X0),X1)
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p91,c16]) ).
cnf(p96,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| ~ iLEQ(g(X0),g(g(X0)))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p92]) ).
cnf(p99,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p96,c1]) ).
cnf(p100,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p99,c14]) ).
cnf(p101,plain,
( qtd2(f(g(g(X0))),s(s(qtd1)))
| ~ iLEQ(g(g(X0)),g(g(X0)))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p100]) ).
cnf(p105,plain,
( ~ iLEQ(g(g(X0)),g(g(X0)))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p101]) ).
cnf(p107,plain,
( qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p105,c3]) ).
cnf(p108,plain,
( qtd0(f(g(X0)),f(g(g(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(g(g(X0))))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p107,c29]) ).
cnf(p110,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(f(g(X0)),f(g(g(X0))))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p108,p67]) ).
cnf(p112,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(f(g(X0)),f(g(g(X0))))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p110]) ).
cnf(p113,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p112,c4]) ).
cnf(p114,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p113,c14]) ).
cnf(p115,plain,
( qtd2(f(g(g(X0))),s(s(qtd1)))
| ~ iLEQ(g(g(X0)),g(g(X0)))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p114]) ).
cnf(p119,plain,
( ~ iLEQ(g(g(X0)),g(g(X0)))
| qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p115]) ).
cnf(p122,plain,
( qtd2(f(g(g(X0))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(X0))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p119,c3]) ).
cnf(p503,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p501,p122]) ).
cnf(p530,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p503]) ).
cnf(p535,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p530,c4]) ).
cnf(p536,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p535,c31]) ).
cnf(p538,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p536,c1]) ).
cnf(p539,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p538]) ).
cnf(p541,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p539,c5]) ).
cnf(p544,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p541,c3]) ).
cnf(p545,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p544]) ).
cnf(p547,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p545]) ).
cnf(f11,axiom,
( qtd0(f(A_11),f(g(A_11)))
| ~ qtd0(s(s(qtd1)),f(g(A_11)))
| ~ qtd0(s(s(qtd1)),f(A_11)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_27_12) ).
fof(f11_nnf,plain,
! [A_11] :
( qtd0(f(A_11),f(g(A_11)))
| ~ qtd0(s(s(qtd1)),f(g(A_11)))
| ~ qtd0(s(s(qtd1)),f(A_11)) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A_11] :
( qtd0(f(A_11),f(g(A_11)))
| ~ qtd0(s(s(qtd1)),f(g(A_11)))
| ~ qtd0(s(s(qtd1)),f(A_11)) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(qtd1)),f(g(X0)))
| ~ qtd0(s(s(qtd1)),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p549,plain,
( qtd0(f(g(g(g(X0)))),f(g(g(g(g(X0))))))
| ~ qtd0(s(s(qtd1)),f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p547,c11]) ).
cnf(p88,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p78,c3]) ).
cnf(p93,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(X0)))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p88,c9]) ).
cnf(p140,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0)))
| qtd0(f(X0),f(g(X0)))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p93,p33]) ).
cnf(p164,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(f(X0),f(g(X0)))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p140]) ).
cnf(p165,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p164,c4]) ).
cnf(p166,plain,
( qtd2(f(X1),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(g(X0),X1)
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p165,c16]) ).
cnf(p167,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| ~ iLEQ(g(X0),g(g(X0)))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p166]) ).
cnf(p169,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p167,c1]) ).
cnf(p171,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p169,c14]) ).
cnf(p172,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| ~ iLEQ(g(g(X0)),g(g(g(X0))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p171]) ).
cnf(p174,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p172,c1]) ).
cnf(p175,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p174,c31]) ).
cnf(p179,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p175,c3]) ).
cnf(p181,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p179]) ).
cnf(p183,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p181]) ).
cnf(p184,plain,
( qtd0(f(g(X0)),f(g(g(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(g(g(X0))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p183,c29]) ).
cnf(p187,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(f(g(X0)),f(g(g(X0))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p184,p67]) ).
cnf(p189,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(f(g(X0)),f(g(g(X0))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p187]) ).
cnf(p190,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p189,c4]) ).
cnf(p191,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p190,c14]) ).
cnf(p194,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| ~ iLEQ(g(g(X0)),g(g(g(X0))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p191]) ).
cnf(p196,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p194,c1]) ).
cnf(p197,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p196,c31]) ).
cnf(p200,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p197,c3]) ).
cnf(p203,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p200]) ).
cnf(p205,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p203]) ).
cnf(p206,plain,
( qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(g(g(g(X0)))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p205,c10]) ).
cnf(p210,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p206,p122]) ).
cnf(p213,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p210]) ).
cnf(p214,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p213,c4]) ).
cnf(p215,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p214,c31]) ).
cnf(p218,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p215,c3]) ).
cnf(p222,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p218]) ).
cnf(p224,plain,
( qtd2(f(g(g(g(X0)))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(X0)))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p222]) ).
cnf(p551,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(f(g(g(g(X0)))),f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p549,p224]) ).
cnf(p552,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(f(g(g(g(X0)))),f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(factoring,[status(thm)],[p551]) ).
cnf(p553,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p552,c4]) ).
cnf(p554,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p553,c5]) ).
cnf(p557,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p554,c3]) ).
cnf(p558,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(factoring,[status(thm)],[p557]) ).
cnf(p560,plain,
( qtd2(f(g(g(g(g(X0))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(X0))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(factoring,[status(thm)],[p558]) ).
cnf(p149,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p134,c1]) ).
cnf(f6,axiom,
~ qtd2(f(A_15),qtd1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6_07) ).
fof(f6_nnf,plain,
! [A_15] : ~ qtd2(f(A_15),qtd1),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A_15] : ~ qtd2(f(A_15),qtd1),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
~ qtd2(f(X0),qtd1),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p212,plain,
( qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(s(qtd1))))),f(X0))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p149,c6]) ).
cnf(p238,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(s(s(s(s(qtd1))))),f(g(X0)))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p212,c9]) ).
cnf(p242,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0)))
| qtd0(f(X0),f(g(X0)))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p238,p33]) ).
cnf(p316,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(f(X0),f(g(X0)))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p242]) ).
cnf(p318,plain,
( qtd2(f(g(X0)),s(s(s(s(qtd1)))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p316,c4]) ).
cnf(p319,plain,
( qtd2(f(X1),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(X1))
| ~ iLEQ(g(X0),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p318,c16]) ).
cnf(p320,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| ~ iLEQ(g(X0),g(g(X0)))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p319]) ).
cnf(p323,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p320,c1]) ).
cnf(p324,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p323,c14]) ).
cnf(p325,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| ~ iLEQ(g(g(X0)),g(g(g(X0))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p324]) ).
cnf(p327,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p325,c1]) ).
cnf(p329,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p327,c31]) ).
cnf(p331,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p329,c1]) ).
cnf(p332,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p331]) ).
cnf(p333,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p332,c5]) ).
cnf(p339,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p333,c1]) ).
cnf(p344,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(factoring,[status(thm)],[p339]) ).
cnf(p345,plain,
( qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(s(s(s(s(qtd1)))),f(g(X0))) ),
inference(resolution,[status(thm)],[p344,c6]) ).
cnf(p347,plain,
( qtd0(f(g(X0)),f(g(g(X0))))
| ~ qtd0(s(s(s(s(qtd1)))),f(g(g(X0))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p345,c29]) ).
cnf(p350,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(s(s(s(qtd1))),f(g(g(X0))))
| qtd0(f(g(X0)),f(g(g(X0))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p347,p67]) ).
cnf(p354,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(f(g(X0)),f(g(g(X0))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p350]) ).
cnf(p357,plain,
( qtd2(f(g(g(X0))),s(s(s(qtd1))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p354,c4]) ).
cnf(p358,plain,
( qtd2(f(X1),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(X1))
| ~ iLEQ(g(g(X0)),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p357,c14]) ).
cnf(p359,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| ~ iLEQ(g(g(X0)),g(g(g(X0))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p358]) ).
cnf(p361,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p359,c1]) ).
cnf(p363,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p361,c31]) ).
cnf(p365,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p363,c1]) ).
cnf(p366,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p365]) ).
cnf(p367,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p366,c5]) ).
cnf(p372,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p367,c1]) ).
cnf(p375,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(factoring,[status(thm)],[p372]) ).
cnf(p376,plain,
( qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(s(s(s(qtd1))),f(g(g(X0)))) ),
inference(resolution,[status(thm)],[p375,c6]) ).
cnf(p378,plain,
( qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| ~ qtd0(s(s(s(qtd1))),f(g(g(g(X0)))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p376,c10]) ).
cnf(p381,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(s(s(qtd1)),f(g(g(g(X0)))))
| qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p378,p122]) ).
cnf(p383,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(f(g(g(X0))),f(g(g(g(X0)))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p381]) ).
cnf(p384,plain,
( qtd2(f(g(g(g(X0)))),s(s(qtd1)))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p383,c4]) ).
cnf(p386,plain,
( qtd2(f(X1),s(qtd1))
| qtd0(s(qtd1),f(X1))
| ~ iLEQ(g(g(g(X0))),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p384,c31]) ).
cnf(p388,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p386,c1]) ).
cnf(p389,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p388]) ).
cnf(p390,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p389,c5]) ).
cnf(p394,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p390,c1]) ).
cnf(p397,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(factoring,[status(thm)],[p394]) ).
cnf(p398,plain,
( qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(s(s(qtd1)),f(g(g(g(X0))))) ),
inference(resolution,[status(thm)],[p397,c6]) ).
cnf(p399,plain,
( qtd0(f(g(g(g(X0)))),f(g(g(g(g(X0))))))
| ~ qtd0(s(s(qtd1)),f(g(g(g(g(X0))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p398,c11]) ).
cnf(p401,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(s(qtd1),f(g(g(g(g(X0))))))
| qtd0(f(g(g(g(X0)))),f(g(g(g(g(X0))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p399,p224]) ).
cnf(p410,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(f(g(g(g(X0)))),f(g(g(g(g(X0))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(factoring,[status(thm)],[p401]) ).
cnf(p411,plain,
( qtd2(f(g(g(g(g(X0))))),s(qtd1))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p410,c4]) ).
cnf(p412,plain,
( qtd2(f(X1),qtd1)
| qtd0(qtd1,f(X1))
| ~ iLEQ(g(g(g(g(X0)))),X1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p411,c5]) ).
cnf(p415,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p412,c1]) ).
cnf(p424,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(factoring,[status(thm)],[p415]) ).
cnf(p425,plain,
( qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd0(s(qtd1),f(g(g(g(g(X0)))))) ),
inference(resolution,[status(thm)],[p424,c6]) ).
cnf(f12,axiom,
( qtd0(f(A_14),f(g(A_14)))
| ~ qtd0(s(qtd1),f(g(A_14)))
| ~ qtd0(s(qtd1),f(A_14)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_30_13) ).
fof(f12_nnf,plain,
! [A_14] :
( qtd0(f(A_14),f(g(A_14)))
| ~ qtd0(s(qtd1),f(g(A_14)))
| ~ qtd0(s(qtd1),f(A_14)) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A_14] :
( qtd0(f(A_14),f(g(A_14)))
| ~ qtd0(s(qtd1),f(g(A_14)))
| ~ qtd0(s(qtd1),f(A_14)) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(s(qtd1),f(g(X0)))
| ~ qtd0(s(qtd1),f(X0)) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p426,plain,
( qtd0(f(g(g(g(g(X0))))),f(g(g(g(g(g(X0)))))))
| ~ qtd0(s(qtd1),f(g(g(g(g(g(X0)))))))
| qtd0(qtd1,f(g(g(g(g(g(X0))))))) ),
inference(resolution,[status(thm)],[p425,c12]) ).
cnf(p562,plain,
( qtd0(f(g(g(g(g(X0))))),f(g(g(g(g(g(X0)))))))
| qtd0(qtd1,f(g(g(g(g(g(X0)))))))
| qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0))))))) ),
inference(resolution,[status(thm)],[p560,p426]) ).
cnf(p568,plain,
( qtd0(f(g(g(g(g(X0))))),f(g(g(g(g(g(X0)))))))
| qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0))))))) ),
inference(factoring,[status(thm)],[p562]) ).
cnf(p570,plain,
( qtd2(f(g(g(g(g(g(X0)))))),qtd1)
| qtd0(qtd1,f(g(g(g(g(g(X0))))))) ),
inference(resolution,[status(thm)],[p568,c4]) ).
cnf(p571,plain,
qtd0(qtd1,f(g(g(g(g(g(X0))))))),
inference(resolution,[status(thm)],[p570,c6]) ).
cnf(f23,axiom,
( qtd0(f(A_15),f(g(A_15)))
| ~ qtd0(qtd1,f(g(A_15)))
| ~ qtd0(qtd1,f(A_15)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_29_24) ).
fof(f23_nnf,plain,
! [A_15] :
( qtd0(f(A_15),f(g(A_15)))
| ~ qtd0(qtd1,f(g(A_15)))
| ~ qtd0(qtd1,f(A_15)) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A_15] :
( qtd0(f(A_15),f(g(A_15)))
| ~ qtd0(qtd1,f(g(A_15)))
| ~ qtd0(qtd1,f(A_15)) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( qtd0(f(X0),f(g(X0)))
| ~ qtd0(qtd1,f(g(X0)))
| ~ qtd0(qtd1,f(X0)) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p572,plain,
( qtd0(f(g(g(g(g(g(X0)))))),f(g(g(g(g(g(g(X0))))))))
| ~ qtd0(qtd1,f(g(g(g(g(g(g(X0)))))))) ),
inference(resolution,[status(thm)],[p571,c23]) ).
cnf(p573,plain,
qtd0(f(g(g(g(g(g(X0)))))),f(g(g(g(g(g(g(X0)))))))),
inference(resolution,[status(thm)],[p572,p571]) ).
cnf(p574,plain,
$false,
inference(resolution,[status(thm)],[p573,c4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO630-1 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n001.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 25 03:23:23 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.92/1.19 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.92/1.19 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------