%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN036-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Sun Sep 27 09:36:27 AM UTC 2026
% Result : Unsatisfiable 3.77s 0.98s
% Output : CNFRefutation 3.77s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(clause_4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(VAR_3)
| ~ big_q(f2(VAR_3))
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(f1(VAR_0))
| big_p(VAR_0) ),
file('theBenchmark.p',clause_4) ).
cnf(c_4,plain,
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(D)
| ~ big_q(f2(D))
| big_p(C)
| ~ big_q(B)
| big_p(f1(A))
| big_p(A) ),
inference(clausify,[status(thm)],[clause_4]) ).
fof(clause_5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| big_p(c9)
| big_q(c8)
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(f1(VAR_0))
| big_p(VAR_0) ),
file('theBenchmark.p',clause_5) ).
cnf(c_5,plain,
( big_q(E)
| big_p(c9)
| big_q(c8)
| ~ big_q(D)
| big_p(C)
| ~ big_q(B)
| big_p(f1(A))
| big_p(A) ),
inference(clausify,[status(thm)],[clause_5]) ).
fof(clause_7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| big_p(c9)
| ~ big_q(c8)
| big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(f1(VAR_0))
| big_p(VAR_0) ),
file('theBenchmark.p',clause_7) ).
cnf(c_7,plain,
( big_q(E)
| big_p(c9)
| ~ big_q(c8)
| big_q(D)
| big_p(C)
| ~ big_q(B)
| big_p(f1(A))
| big_p(A) ),
inference(clausify,[status(thm)],[clause_7]) ).
fof(clause_25,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| big_q(f2(VAR_1))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(VAR_0))
| ~ big_p(VAR_0) ),
file('theBenchmark.p',clause_25) ).
cnf(c_23,plain,
( big_q(D)
| ~ big_p(C)
| big_q(B)
| big_q(f2(B))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(A))
| ~ big_p(A) ),
inference(clausify,[status(thm)],[clause_25]) ).
fof(clause_33,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| big_q(f2(VAR_2))
| big_p(VAR_1)
| big_q(c4)
| big_p(VAR_0)
| ~ big_p(c3) ),
file('theBenchmark.p',clause_33) ).
cnf(c_29,plain,
( big_q(E)
| ~ big_p(D)
| big_q(C)
| big_q(f2(C))
| big_p(B)
| big_q(c4)
| big_p(A)
| ~ big_p(c3) ),
inference(clausify,[status(thm)],[clause_33]) ).
fof(clause_49,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| big_q(f2(VAR_2))
| big_p(VAR_1)
| big_q(c4)
| ~ big_p(VAR_0)
| big_p(c3) ),
file('theBenchmark.p',clause_49) ).
cnf(c_45,plain,
( big_q(E)
| ~ big_p(D)
| big_q(C)
| big_q(f2(C))
| big_p(B)
| big_q(c4)
| ~ big_p(A)
| big_p(c3) ),
inference(clausify,[status(thm)],[clause_49]) ).
fof(clause_65,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_q(VAR_5)
| ~ big_p(VAR_4)
| big_q(c16)
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(c11) ),
file('theBenchmark.p',clause_65) ).
cnf(c_61,plain,
( big_q(F)
| ~ big_p(E)
| big_q(c16)
| ~ big_q(D)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(clausify,[status(thm)],[clause_65]) ).
fof(clause_67,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_q(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(c16)
| big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(c11) ),
file('theBenchmark.p',clause_67) ).
cnf(c_63,plain,
( big_q(F)
| ~ big_p(E)
| ~ big_q(c16)
| big_q(D)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(clausify,[status(thm)],[clause_67]) ).
fof(clause_72,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_q(c20)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| ~ big_q(f4(VAR_3))
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(c11) ),
file('theBenchmark.p',clause_72) ).
cnf(c_68,plain,
( ~ big_q(c20)
| ~ big_p(E)
| ~ big_q(D)
| ~ big_q(f4(D))
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(clausify,[status(thm)],[clause_72]) ).
fof(clause_81,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_q(VAR_5)
| ~ big_p(VAR_4)
| big_q(c16)
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(c11) ),
file('theBenchmark.p',clause_81) ).
cnf(c_75,plain,
( big_q(F)
| ~ big_p(E)
| big_q(c16)
| ~ big_q(D)
| big_p(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(clausify,[status(thm)],[clause_81]) ).
fof(clause_83,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_q(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(c16)
| big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(c11) ),
file('theBenchmark.p',clause_83) ).
cnf(c_77,plain,
( big_q(F)
| ~ big_p(E)
| ~ big_q(c16)
| big_q(D)
| big_p(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(clausify,[status(thm)],[clause_83]) ).
fof(clause_88,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_q(c20)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| ~ big_q(f4(VAR_3))
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(c11) ),
file('theBenchmark.p',clause_88) ).
cnf(c_82,plain,
( ~ big_q(c20)
| ~ big_p(E)
| ~ big_q(D)
| ~ big_q(f4(D))
| big_p(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(clausify,[status(thm)],[clause_88]) ).
fof(clause_101,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(c19)
| big_q(VAR_2)
| big_q(f4(VAR_2))
| big_p(VAR_1)
| big_q(c14)
| big_p(f3(VAR_0))
| big_p(VAR_0) ),
file('theBenchmark.p',clause_101) ).
cnf(c_93,plain,
( big_q(D)
| big_p(c19)
| big_q(C)
| big_q(f4(C))
| big_p(B)
| big_q(c14)
| big_p(f3(A))
| big_p(A) ),
inference(clausify,[status(thm)],[clause_101]) ).
fof(clause_121,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(c16)
| ~ big_q(VAR_2)
| ~ big_p(c15)
| ~ big_q(VAR_1)
| ~ big_p(f3(VAR_0))
| ~ big_p(VAR_0) ),
file('theBenchmark.p',clause_121) ).
cnf(c_113,plain,
( big_q(E)
| ~ big_p(D)
| big_q(c16)
| ~ big_q(C)
| ~ big_p(c15)
| ~ big_q(B)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(clausify,[status(thm)],[clause_121]) ).
fof(clause_123,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(c16)
| big_q(VAR_2)
| ~ big_p(c15)
| ~ big_q(VAR_1)
| ~ big_p(f3(VAR_0))
| ~ big_p(VAR_0) ),
file('theBenchmark.p',clause_123) ).
cnf(c_115,plain,
( big_q(E)
| ~ big_p(D)
| ~ big_q(c16)
| big_q(C)
| ~ big_p(c15)
| ~ big_q(B)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(clausify,[status(thm)],[clause_123]) ).
fof(clause_128,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(c20)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| ~ big_q(f4(VAR_2))
| ~ big_p(c15)
| ~ big_q(VAR_1)
| ~ big_p(f3(VAR_0))
| ~ big_p(VAR_0) ),
file('theBenchmark.p',clause_128) ).
cnf(c_120,plain,
( ~ big_q(c20)
| ~ big_p(D)
| ~ big_q(C)
| ~ big_q(f4(C))
| ~ big_p(c15)
| ~ big_q(B)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(clausify,[status(thm)],[clause_128]) ).
cnf(c_127,plain,
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(C)
| ~ big_q(f2(C))
| ~ big_q(B)
| big_p(f1(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_4]) ).
cnf(c_129,plain,
( big_q(D)
| big_p(c9)
| big_q(c8)
| ~ big_q(C)
| ~ big_q(B)
| big_p(f1(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_5]) ).
cnf(c_134,plain,
( big_q(D)
| big_p(c9)
| ~ big_q(c8)
| big_q(C)
| ~ big_q(B)
| big_p(f1(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_7]) ).
cnf(c_171,plain,
( big_q(C)
| big_q(B)
| big_q(f2(B))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_23]) ).
cnf(c_187,plain,
( big_q(D)
| big_q(C)
| big_q(f2(C))
| big_p(B)
| big_q(c4)
| big_p(A)
| ~ big_p(c3) ),
inference(factor,[status(thm)],[c_29]) ).
cnf(c_226,plain,
( big_q(D)
| ~ big_p(C)
| big_q(B)
| big_q(f2(B))
| big_q(c4)
| ~ big_p(A)
| big_p(c3) ),
inference(factor,[status(thm)],[c_45]) ).
cnf(c_265,plain,
( big_q(E)
| big_q(c16)
| ~ big_q(D)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_61]) ).
cnf(c_271,plain,
( big_q(E)
| ~ big_q(c16)
| big_q(D)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_63]) ).
cnf(c_284,plain,
( ~ big_q(c20)
| ~ big_q(D)
| ~ big_q(f4(D))
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_68]) ).
cnf(c_300,plain,
( big_q(E)
| ~ big_p(D)
| big_q(c16)
| ~ big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_75]) ).
cnf(c_306,plain,
( big_q(E)
| ~ big_p(D)
| ~ big_q(c16)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_77]) ).
cnf(c_319,plain,
( ~ big_q(c20)
| ~ big_p(D)
| ~ big_q(C)
| ~ big_q(f4(C))
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_82]) ).
cnf(c_343,plain,
( big_q(C)
| big_p(c19)
| big_q(B)
| big_q(f4(B))
| big_q(c14)
| big_p(f3(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_93]) ).
cnf(c_388,plain,
( big_q(D)
| big_q(c16)
| ~ big_q(C)
| ~ big_p(c15)
| ~ big_q(B)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_113]) ).
cnf(c_394,plain,
( big_q(D)
| ~ big_q(c16)
| big_q(C)
| ~ big_p(c15)
| ~ big_q(B)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_115]) ).
cnf(c_407,plain,
( ~ big_q(c20)
| ~ big_q(C)
| ~ big_q(f4(C))
| ~ big_p(c15)
| ~ big_q(B)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_120]) ).
cnf(c_414,plain,
( ~ big_q(c7)
| big_p(c6)
| ~ big_q(B)
| ~ big_q(f2(B))
| big_p(f1(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_127]) ).
cnf(c_416,plain,
( big_q(C)
| big_q(c8)
| ~ big_q(B)
| ~ big_q(A)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_129]) ).
cnf(c_417,plain,
( big_q(C)
| big_p(c9)
| big_q(c8)
| ~ big_q(B)
| big_p(f1(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_129]) ).
cnf(c_422,plain,
( big_q(C)
| ~ big_q(c8)
| big_q(B)
| ~ big_q(A)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_134]) ).
cnf(c_451,plain,
( big_q(B)
| big_q(f2(B))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_171]) ).
cnf(c_463,plain,
( big_q(C)
| big_q(B)
| big_q(f2(B))
| big_q(c4)
| big_p(A)
| ~ big_p(c3) ),
inference(factor,[status(thm)],[c_187]) ).
cnf(c_499,plain,
( big_q(C)
| big_q(B)
| big_q(f2(B))
| big_q(c4)
| ~ big_p(A)
| big_p(c3) ),
inference(factor,[status(thm)],[c_226]) ).
cnf(c_536,plain,
( big_q(D)
| big_q(c16)
| ~ big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_265]) ).
cnf(c_544,plain,
( big_q(D)
| ~ big_q(c16)
| big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_271]) ).
cnf(c_558,plain,
( ~ big_q(c20)
| ~ big_q(C)
| ~ big_q(f4(C))
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_284]) ).
cnf(c_568,plain,
( big_q(D)
| big_q(c16)
| ~ big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_300]) ).
cnf(c_575,plain,
( big_q(D)
| ~ big_q(c16)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_306]) ).
cnf(c_586,plain,
( ~ big_q(c20)
| ~ big_q(C)
| ~ big_q(f4(C))
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_319]) ).
cnf(c_608,plain,
( big_p(c19)
| big_q(B)
| big_q(f4(B))
| big_q(c14)
| big_p(f3(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_343]) ).
cnf(c_639,plain,
( big_q(C)
| big_q(c16)
| ~ big_p(c15)
| ~ big_q(B)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_388]) ).
cnf(c_647,plain,
( big_q(C)
| big_q(B)
| ~ big_p(c15)
| ~ big_q(c16)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_394]) ).
cnf(c_658,plain,
( ~ big_q(c20)
| ~ big_q(B)
| ~ big_p(c15)
| ~ big_q(f4(B))
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_407]) ).
cnf(c_662,plain,
( big_p(c6)
| ~ big_q(c7)
| ~ big_q(f2(c7))
| big_p(f1(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_414]) ).
cnf(c_663,plain,
( big_q(B)
| big_q(c8)
| ~ big_q(A)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_416]) ).
cnf(c_665,plain,
( big_p(c9)
| big_q(c8)
| ~ big_q(B)
| big_p(f1(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_417]) ).
cnf(c_667,plain,
( big_q(B)
| big_q(A)
| ~ big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_422]) ).
cnf(c_683,plain,
( big_q(B)
| big_q(f2(c4))
| big_q(c4)
| big_p(A)
| ~ big_p(c3) ),
inference(factor,[status(thm)],[c_463]) ).
cnf(c_698,plain,
( big_q(B)
| big_q(f2(c4))
| big_q(c4)
| ~ big_p(A)
| big_p(c3) ),
inference(factor,[status(thm)],[c_499]) ).
cnf(c_714,plain,
( big_q(C)
| big_q(c16)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_536]) ).
cnf(c_718,plain,
( big_q(C)
| big_q(B)
| ~ big_q(c16)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_544]) ).
cnf(c_725,plain,
( ~ big_q(c20)
| ~ big_q(B)
| ~ big_q(f4(B))
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_558]) ).
cnf(c_729,plain,
( big_q(C)
| big_q(c16)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_568]) ).
cnf(c_733,plain,
( big_q(C)
| big_q(B)
| ~ big_q(c16)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_575]) ).
cnf(c_738,plain,
( ~ big_q(c20)
| ~ big_q(B)
| ~ big_q(f4(B))
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_586]) ).
cnf(c_758,plain,
( big_q(c16)
| ~ big_p(c15)
| ~ big_q(B)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_639]) ).
cnf(c_763,plain,
( big_q(B)
| ~ big_p(c15)
| ~ big_q(c16)
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_647]) ).
cnf(c_767,plain,
( ~ big_q(c20)
| ~ big_p(c15)
| ~ big_q(f4(c20))
| ~ big_p(f3(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_658]) ).
cnf(c_769,plain,
( big_q(c8)
| ~ big_q(A)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_663]) ).
cnf(c_770,plain,
( big_q(A)
| ~ big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_667]) ).
cnf(c_772,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(A)
| ~ big_p(c3) ),
inference(factor,[status(thm)],[c_683]) ).
cnf(c_774,plain,
( big_q(f2(c4))
| big_q(c4)
| ~ big_p(A)
| big_p(c3) ),
inference(factor,[status(thm)],[c_698]) ).
cnf(c_776,plain,
( big_q(c16)
| ~ big_q(B)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_714]) ).
cnf(c_777,plain,
( big_q(B)
| ~ big_q(c16)
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_718]) ).
cnf(c_778,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(A)
| ~ big_p(c11) ),
inference(factor,[status(thm)],[c_725]) ).
cnf(c_779,plain,
( big_q(c16)
| ~ big_q(B)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_729]) ).
cnf(c_780,plain,
( big_q(B)
| ~ big_q(c16)
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_733]) ).
cnf(c_781,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| ~ big_p(A)
| big_p(c11) ),
inference(factor,[status(thm)],[c_738]) ).
cnf(c_1053,plain,
( big_p(c19)
| big_q(C)
| big_q(c14)
| big_p(f3(B))
| big_p(B)
| big_p(c9)
| big_q(c8)
| big_p(f1(A))
| big_p(A) ),
inference(resolve,[status(thm)],[c_665,c_608]) ).
cnf(c_1054,plain,
( big_p(c19)
| big_q(B)
| big_q(c14)
| big_p(f3(A))
| big_p(A)
| big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_1053]) ).
cnf(c_1062,plain,
( big_p(c19)
| big_q(A)
| big_q(c14)
| big_p(f3(c9))
| big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_1054]) ).
cnf(c_1077,plain,
( big_p(c19)
| big_q(c14)
| big_p(f3(c9))
| big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_1062]) ).
cnf(c_4655,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_p(c19)
| big_p(f3(c9))
| big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_1077,c_769]) ).
cnf(c_4656,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c19)
| big_p(f3(c9))
| big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4655]) ).
cnf(c_4657,plain,
( big_q(c8)
| big_p(c19)
| big_p(f3(c9))
| big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4656]) ).
cnf(c_1150,plain,
( big_p(c19)
| big_p(f3(c9))
| big_q(c8)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4657]) ).
cnf(c_4658,plain,
( big_q(A)
| big_p(f1(c9))
| big_p(c9)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_1150,c_770]) ).
cnf(c_4659,plain,
( big_q(A)
| big_p(f1(c9))
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4658]) ).
cnf(c_1155,plain,
( big_q(A)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4659]) ).
cnf(c_1191,plain,
( big_p(c6)
| ~ big_q(c7)
| big_p(f1(A))
| big_p(A)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_1155,c_662]) ).
cnf(c_4660,plain,
( big_p(c6)
| ~ big_q(c7)
| big_p(f1(c9))
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_1191]) ).
cnf(c_1205,plain,
( big_p(c6)
| ~ big_q(c7)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4660]) ).
cnf(c_4661,plain,
( big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9)
| big_p(c6)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_1205,c_1155]) ).
cnf(c_4662,plain,
( big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c6)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4661]) ).
cnf(c_4663,plain,
( big_p(c19)
| big_p(f3(c9))
| big_p(c6)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4662]) ).
cnf(c_4664,plain,
( big_p(c19)
| big_p(c6)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4663]) ).
cnf(c_1487,plain,
( big_p(c6)
| big_p(c19)
| big_p(f3(c9))
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4664]) ).
cnf(c_1494,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_1487,c_774]) ).
cnf(c_4665,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_1494,c_769]) ).
cnf(c_4666,plain,
( big_q(c8)
| big_p(f1(c9))
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4665]) ).
cnf(c_2767,plain,
( big_q(c8)
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4666]) ).
cnf(c_4667,plain,
( big_q(c8)
| big_p(f1(c9))
| big_p(c9)
| big_q(c8)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2767,c_769]) ).
cnf(c_4668,plain,
( big_q(c8)
| big_p(f1(c9))
| big_q(c8)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4667]) ).
cnf(c_4669,plain,
( big_q(c8)
| big_q(c8)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4668]) ).
cnf(c_2804,plain,
( big_q(c8)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4669]) ).
cnf(c_4670,plain,
( big_q(A)
| big_p(f1(c9))
| big_p(c9)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2804,c_770]) ).
cnf(c_4671,plain,
( big_q(A)
| big_p(f1(c9))
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4670]) ).
cnf(c_2810,plain,
( big_q(A)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4671]) ).
cnf(c_4672,plain,
( big_p(c6)
| ~ big_q(c7)
| big_p(f1(A))
| big_p(A)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2810,c_662]) ).
cnf(c_2839,plain,
( ~ big_q(c7)
| big_p(f1(A))
| big_p(A)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4672]) ).
cnf(c_4673,plain,
( ~ big_q(c7)
| big_p(f1(c9))
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(factor,[status(thm)],[c_2839]) ).
cnf(c_2849,plain,
( ~ big_q(c7)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4673]) ).
cnf(c_4674,plain,
( big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2849,c_2810]) ).
cnf(c_4675,plain,
( big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4674]) ).
cnf(c_4676,plain,
( big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4675]) ).
cnf(c_4677,plain,
( big_p(c3)
| big_p(c6)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4676]) ).
cnf(c_4678,plain,
( big_p(c3)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4677]) ).
cnf(c_2851,plain,
( big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(f1(c9))
| big_p(c9) ),
inference(copy,[status(thm)],[c_4678]) ).
cnf(c_2876,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2851,c_780]) ).
cnf(c_2877,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2851,c_779]) ).
cnf(c_4679,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2851,c_774]) ).
cnf(c_2878,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4679]) ).
cnf(c_4680,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9)
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2878,c_2877]) ).
cnf(c_4681,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4680]) ).
cnf(c_4682,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4681]) ).
cnf(c_4683,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4682]) ).
cnf(c_2975,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4683]) ).
cnf(c_4684,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_2975,c_2877]) ).
cnf(c_4685,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4684]) ).
cnf(c_4686,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4685]) ).
cnf(c_4687,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4686]) ).
cnf(c_4688,plain,
( big_q(c16)
| big_p(c11)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4687]) ).
cnf(c_4689,plain,
( big_q(c16)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4688]) ).
cnf(c_3115,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4689]) ).
cnf(c_4690,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_3115,c_2876]) ).
cnf(c_4691,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4690]) ).
cnf(c_4692,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4691]) ).
cnf(c_4693,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4692]) ).
cnf(c_4694,plain,
( big_q(A)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4693]) ).
cnf(c_3116,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4694]) ).
cnf(c_4695,plain,
( ~ big_q(c20)
| ~ big_p(A)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_3116,c_781]) ).
cnf(c_3129,plain,
( ~ big_q(c20)
| ~ big_p(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4695]) ).
cnf(c_4696,plain,
( big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9)
| ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_3129,c_2851]) ).
cnf(c_4697,plain,
( big_p(c3)
| big_p(c6)
| big_p(c19)
| ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4696]) ).
cnf(c_4698,plain,
( big_p(c3)
| big_p(c6)
| ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4697]) ).
cnf(c_4699,plain,
( big_p(c3)
| ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4698]) ).
cnf(c_3153,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4699]) ).
cnf(c_4700,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(resolve,[status(thm)],[c_3153,c_3116]) ).
cnf(c_4701,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4700]) ).
cnf(c_4702,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4701]) ).
cnf(c_4703,plain,
( big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4702]) ).
cnf(c_4704,plain,
( big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4703]) ).
cnf(c_3155,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c9) ),
inference(copy,[status(thm)],[c_4704]) ).
cnf(c_4705,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3155,c_781]) ).
cnf(c_3180,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4705]) ).
cnf(c_4706,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3155,c_780]) ).
cnf(c_3181,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4706]) ).
cnf(c_4707,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3155,c_779]) ).
cnf(c_3182,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4707]) ).
cnf(c_4708,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3155,c_774]) ).
cnf(c_3183,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4708]) ).
cnf(c_4709,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3183,c_3182]) ).
cnf(c_4710,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4709]) ).
cnf(c_4711,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4710]) ).
cnf(c_4712,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4711]) ).
cnf(c_3474,plain,
( big_q(c16)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4712]) ).
cnf(c_4713,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3474,c_3182]) ).
cnf(c_4714,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4713]) ).
cnf(c_4715,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4714]) ).
cnf(c_4716,plain,
( big_q(c16)
| big_p(c11)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4715]) ).
cnf(c_4717,plain,
( big_q(c16)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4716]) ).
cnf(c_3502,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4717]) ).
cnf(c_4718,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3502,c_3181]) ).
cnf(c_4719,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4718]) ).
cnf(c_4720,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4719]) ).
cnf(c_4721,plain,
( big_q(A)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4720]) ).
cnf(c_3503,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4721]) ).
cnf(c_4722,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3503,c_3180]) ).
cnf(c_4723,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4722]) ).
cnf(c_4724,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4723]) ).
cnf(c_4725,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4724]) ).
cnf(c_3514,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4725]) ).
cnf(c_4726,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3514,c_3503]) ).
cnf(c_4727,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4726]) ).
cnf(c_4728,plain,
( big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4727]) ).
cnf(c_4729,plain,
( big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4728]) ).
cnf(c_3538,plain,
( big_p(c11)
| big_p(c3)
| big_p(c6)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4729]) ).
cnf(c_4730,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3538,c_781]) ).
cnf(c_3579,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4730]) ).
cnf(c_4731,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3538,c_780]) ).
cnf(c_3580,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4731]) ).
cnf(c_4732,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3538,c_779]) ).
cnf(c_3581,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4732]) ).
cnf(c_4733,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3538,c_774]) ).
cnf(c_3582,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4733]) ).
cnf(c_4734,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c19)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3582,c_3581]) ).
cnf(c_4735,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4734]) ).
cnf(c_4736,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4735]) ).
cnf(c_3756,plain,
( big_q(c16)
| big_q(c4)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4736]) ).
cnf(c_4737,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c19)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3756,c_3581]) ).
cnf(c_4738,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4737]) ).
cnf(c_4739,plain,
( big_q(c16)
| big_p(c11)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4738]) ).
cnf(c_4740,plain,
( big_q(c16)
| big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4739]) ).
cnf(c_3778,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4740]) ).
cnf(c_4741,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3778,c_3580]) ).
cnf(c_4742,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4741]) ).
cnf(c_4743,plain,
( big_q(A)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4742]) ).
cnf(c_3779,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4743]) ).
cnf(c_4744,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3779,c_3579]) ).
cnf(c_4745,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4744]) ).
cnf(c_4746,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4745]) ).
cnf(c_3783,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4746]) ).
cnf(c_4747,plain,
( big_p(c11)
| big_p(c3)
| big_p(c19)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(resolve,[status(thm)],[c_3783,c_3779]) ).
cnf(c_4748,plain,
( big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4747]) ).
cnf(c_4749,plain,
( big_p(c11)
| big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4748]) ).
cnf(c_3786,plain,
( big_p(c11)
| big_p(c3)
| big_p(c19) ),
inference(copy,[status(thm)],[c_4749]) ).
cnf(c_4750,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3786,c_781]) ).
cnf(c_3787,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4750]) ).
cnf(c_4751,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3786,c_780]) ).
cnf(c_3788,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4751]) ).
cnf(c_4752,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3786,c_779]) ).
cnf(c_3789,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4752]) ).
cnf(c_4753,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3786,c_774]) ).
cnf(c_3790,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4753]) ).
cnf(c_4754,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c4)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3790,c_3789]) ).
cnf(c_4755,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4754]) ).
cnf(c_3829,plain,
( big_q(c16)
| big_q(c4)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4755]) ).
cnf(c_4756,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3)
| big_q(c16)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3829,c_3789]) ).
cnf(c_4757,plain,
( big_q(c16)
| big_p(c11)
| big_q(c16)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4756]) ).
cnf(c_4758,plain,
( big_q(c16)
| big_q(c16)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4757]) ).
cnf(c_3838,plain,
( big_q(c16)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4758]) ).
cnf(c_4759,plain,
( big_q(A)
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3838,c_3788]) ).
cnf(c_4760,plain,
( big_q(A)
| big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4759]) ).
cnf(c_3839,plain,
( big_q(A)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4760]) ).
cnf(c_4761,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3839,c_3787]) ).
cnf(c_4762,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4761]) ).
cnf(c_3849,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4762]) ).
cnf(c_4763,plain,
( big_p(c11)
| big_p(c3)
| big_p(c11)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_3849,c_3839]) ).
cnf(c_4764,plain,
( big_p(c11)
| big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4763]) ).
cnf(c_3870,plain,
( big_p(c11)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4764]) ).
cnf(c_4765,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_3870,c_781]) ).
cnf(c_3933,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(c11) ),
inference(copy,[status(thm)],[c_4765]) ).
cnf(c_4766,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_3870,c_780]) ).
cnf(c_3934,plain,
( big_q(A)
| ~ big_q(c16)
| big_p(c11) ),
inference(copy,[status(thm)],[c_4766]) ).
cnf(c_4767,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_3870,c_779]) ).
cnf(c_3935,plain,
( big_q(c16)
| ~ big_q(A)
| big_p(c11) ),
inference(copy,[status(thm)],[c_4767]) ).
cnf(c_3937,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(A)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_3870,c_772]) ).
cnf(c_4013,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c11) ),
inference(factor,[status(thm)],[c_3937]) ).
cnf(c_4768,plain,
( big_q(c16)
| big_p(c11)
| big_q(c4)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_4013,c_3935]) ).
cnf(c_4063,plain,
( big_q(c16)
| big_q(c4)
| big_p(c11) ),
inference(copy,[status(thm)],[c_4768]) ).
cnf(c_4769,plain,
( big_q(c16)
| big_p(c11)
| big_q(c16)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_4063,c_3935]) ).
cnf(c_4770,plain,
( big_q(c16)
| big_q(c16)
| big_p(c11) ),
inference(copy,[status(thm)],[c_4769]) ).
cnf(c_4113,plain,
( big_q(c16)
| big_p(c11) ),
inference(copy,[status(thm)],[c_4770]) ).
cnf(c_4771,plain,
( big_q(A)
| big_p(c11)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_4113,c_3934]) ).
cnf(c_4115,plain,
( big_q(A)
| big_p(c11) ),
inference(copy,[status(thm)],[c_4771]) ).
cnf(c_4772,plain,
( ~ big_q(c20)
| big_p(c11)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_4115,c_3933]) ).
cnf(c_4126,plain,
( ~ big_q(c20)
| big_p(c11) ),
inference(copy,[status(thm)],[c_4772]) ).
cnf(c_4773,plain,
( big_p(c11)
| big_p(c11) ),
inference(resolve,[status(thm)],[c_4126,c_4115]) ).
cnf(c_4146,plain,
big_p(c11),
inference(copy,[status(thm)],[c_4773]) ).
cnf(c_4189,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20))
| big_p(A) ),
inference(resolve,[status(thm)],[c_4146,c_778]) ).
cnf(c_4190,plain,
( big_q(B)
| ~ big_q(c16)
| big_p(A) ),
inference(resolve,[status(thm)],[c_4146,c_777]) ).
cnf(c_4191,plain,
( big_q(c16)
| ~ big_q(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_4146,c_776]) ).
cnf(c_4282,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_4146,c_774]) ).
cnf(c_4405,plain,
( big_q(c16)
| big_p(A)
| big_q(c4)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_4282,c_4191]) ).
cnf(c_4418,plain,
( big_q(c16)
| big_q(c4)
| big_p(c3) ),
inference(factor,[status(thm)],[c_4405]) ).
cnf(c_4774,plain,
( big_q(c16)
| big_p(A)
| big_q(c16)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_4418,c_4191]) ).
cnf(c_4424,plain,
( big_p(A)
| big_q(c16)
| big_p(c3) ),
inference(copy,[status(thm)],[c_4774]) ).
cnf(c_4428,plain,
( big_q(c16)
| big_p(c3) ),
inference(factor,[status(thm)],[c_4424]) ).
cnf(c_4430,plain,
( big_q(B)
| big_p(A)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_4428,c_4190]) ).
cnf(c_4443,plain,
( big_q(A)
| big_p(c3) ),
inference(factor,[status(thm)],[c_4430]) ).
cnf(c_4451,plain,
( ~ big_q(c20)
| big_p(A)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_4443,c_4189]) ).
cnf(c_4471,plain,
( ~ big_q(c20)
| big_p(c3) ),
inference(factor,[status(thm)],[c_4451]) ).
cnf(c_4775,plain,
( big_p(c3)
| big_p(c3) ),
inference(resolve,[status(thm)],[c_4471,c_4443]) ).
cnf(c_4475,plain,
big_p(c3),
inference(copy,[status(thm)],[c_4775]) ).
cnf(c_4497,plain,
( big_q(f2(c4))
| big_q(c4)
| big_p(A) ),
inference(resolve,[status(thm)],[c_4475,c_772]) ).
cnf(c_4522,plain,
( ~ big_q(c20)
| ~ big_p(c15)
| ~ big_q(f4(c20))
| ~ big_p(f3(c3)) ),
inference(resolve,[status(thm)],[c_4475,c_767]) ).
cnf(c_4523,plain,
( big_q(A)
| ~ big_p(c15)
| ~ big_q(c16)
| ~ big_p(f3(c3)) ),
inference(resolve,[status(thm)],[c_4475,c_763]) ).
cnf(c_4524,plain,
( big_q(c16)
| ~ big_p(c15)
| ~ big_q(A)
| ~ big_p(f3(c3)) ),
inference(resolve,[status(thm)],[c_4475,c_758]) ).
cnf(c_4537,plain,
( big_q(A)
| big_q(f2(A))
| ~ big_p(c2)
| big_q(c1)
| ~ big_p(f1(c3)) ),
inference(resolve,[status(thm)],[c_4475,c_451]) ).
cnf(c_4545,plain,
( big_q(c16)
| big_p(B)
| big_q(c4)
| big_p(A) ),
inference(resolve,[status(thm)],[c_4497,c_4191]) ).
cnf(c_4557,plain,
( big_q(c16)
| big_q(c4)
| big_p(A) ),
inference(factor,[status(thm)],[c_4545]) ).
cnf(c_4776,plain,
( big_q(c16)
| big_p(B)
| big_q(c16)
| big_p(A) ),
inference(resolve,[status(thm)],[c_4557,c_4191]) ).
cnf(c_4576,plain,
( big_p(B)
| big_q(c16)
| big_p(A) ),
inference(copy,[status(thm)],[c_4776]) ).
cnf(c_4579,plain,
( big_q(c16)
| big_p(A) ),
inference(factor,[status(thm)],[c_4576]) ).
cnf(c_4582,plain,
( big_q(C)
| big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_4579,c_4190]) ).
cnf(c_4592,plain,
( big_q(B)
| big_p(A) ),
inference(factor,[status(thm)],[c_4582]) ).
cnf(c_4607,plain,
( ~ big_q(c20)
| big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_4592,c_4189]) ).
cnf(c_4624,plain,
( ~ big_q(c20)
| big_p(A) ),
inference(factor,[status(thm)],[c_4607]) ).
cnf(c_4634,plain,
( big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_4624,c_4592]) ).
cnf(c_4635,plain,
big_p(A),
inference(factor,[status(thm)],[c_4634]) ).
cnf(c_4777,plain,
( big_q(A)
| big_q(f2(A))
| ~ big_p(c2)
| big_q(c1) ),
inference(resolve,[status(thm)],[c_4635,c_4537]) ).
cnf(c_4636,plain,
( big_q(A)
| big_q(f2(A))
| big_q(c1) ),
inference(resolve,[status(thm)],[c_4635,c_4777]) ).
cnf(c_4778,plain,
( big_q(c16)
| ~ big_p(c15)
| ~ big_q(A) ),
inference(resolve,[status(thm)],[c_4635,c_4524]) ).
cnf(c_4643,plain,
( big_q(c16)
| ~ big_q(A) ),
inference(resolve,[status(thm)],[c_4635,c_4778]) ).
cnf(c_4779,plain,
( big_q(A)
| ~ big_p(c15)
| ~ big_q(c16) ),
inference(resolve,[status(thm)],[c_4635,c_4523]) ).
cnf(c_4644,plain,
( big_q(A)
| ~ big_q(c16) ),
inference(resolve,[status(thm)],[c_4635,c_4779]) ).
cnf(c_4780,plain,
( ~ big_q(c20)
| ~ big_p(c15)
| ~ big_q(f4(c20)) ),
inference(resolve,[status(thm)],[c_4635,c_4522]) ).
cnf(c_4645,plain,
( ~ big_q(c20)
| ~ big_q(f4(c20)) ),
inference(resolve,[status(thm)],[c_4635,c_4780]) ).
cnf(c_4646,plain,
( big_q(c16)
| big_q(A)
| big_q(c1) ),
inference(resolve,[status(thm)],[c_4636,c_4643]) ).
cnf(c_4647,plain,
( big_q(c16)
| big_q(c1) ),
inference(factor,[status(thm)],[c_4646]) ).
cnf(c_4781,plain,
( big_q(c16)
| big_q(c16) ),
inference(resolve,[status(thm)],[c_4647,c_4643]) ).
cnf(c_4652,plain,
big_q(c16),
inference(copy,[status(thm)],[c_4781]) ).
cnf(c_4653,plain,
big_q(A),
inference(resolve,[status(thm)],[c_4652,c_4644]) ).
cnf(c_4782,plain,
~ big_q(c20),
inference(resolve,[status(thm)],[c_4653,c_4645]) ).
cnf(c_4654,plain,
$false,
inference(resolve,[status(thm)],[c_4653,c_4782]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN036-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n015.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 26 17:08:14 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.38 % Process 349419 was started by sandbox on n015,
% 0.12/0.38 % Sat Sep 26 17:08:14 2026
% 0.12/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.39
% 0.12/0.39 % From the command line: assign(max_seconds, 300).
% 3.77/0.98
% 3.77/0.98 % SZS status Unsatisfiable for theBenchmark
% 3.77/0.98
% 3.77/0.98 % Proof 1 at 0.45 (+ 0.13) seconds.
% 3.77/0.98 % Length of proof is 173.
% 3.77/0.98 % Level of proof is 78.
% 3.77/0.98 % Maximum clause weight is 30.000.
% 3.77/0.98 % Given clauses 455.
% 3.77/0.98
% 3.77/0.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------