%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN036+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:17 AM UTC 2026
% Result : Theorem 0.19s 15.81s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(pel34,conjecture,
( ( ? [X] :
! [Y] :
( big_p(X)
<=> big_p(Y) )
<=> ( ? [U] : big_q(U)
<=> ! [W] : big_q(W) ) )
<=> ( ? [X1] :
! [Y1] :
( big_q(X1)
<=> big_q(Y1) )
<=> ( ? [U1] : big_p(U1)
<=> ! [W1] : big_p(W1) ) ) ),
file('theBenchmark.p',pel34) ).
fof(pel34_neg,negated_conjecture,
~ ( ( ? [X] :
! [Y] :
( big_p(X)
<=> big_p(Y) )
<=> ( ? [U] : big_q(U)
<=> ! [W] : big_q(W) ) )
<=> ( ? [X1] :
! [Y1] :
( big_q(X1)
<=> big_q(Y1) )
<=> ( ? [U1] : big_p(U1)
<=> ! [W1] : big_p(W1) ) ) ),
inference(assume_negation,[status(cth)],[pel34]) ).
fof(nnf_1,plain,
( ( ( ( ( ( ? [W1] : ~ big_p(W1)
| ! [U1] : ~ big_p(U1) )
& ( ! [X40] : big_p(X40)
| ? [X39] : big_p(X39) ) )
| ! [X1] :
? [Y1] :
( ( ~ big_q(Y1)
| ~ big_q(X1) )
& ( big_q(Y1)
| big_q(X1) ) ) )
& ( ( ( ? [X38] : ~ big_p(X38)
| ? [X37] : big_p(X37) )
& ( ! [X36] : big_p(X36)
| ! [X35] : ~ big_p(X35) ) )
| ? [X33] :
! [X34] :
( ( ~ big_q(X34)
| big_q(X33) )
& ( big_q(X34)
| ~ big_q(X33) ) ) ) )
| ( ( ( ( ? [W] : ~ big_q(W)
| ! [U] : ~ big_q(U) )
& ( ! [X32] : big_q(X32)
| ? [X31] : big_q(X31) ) )
| ! [X] :
? [Y] :
( ( ~ big_p(Y)
| ~ big_p(X) )
& ( big_p(Y)
| big_p(X) ) ) )
& ( ( ( ? [X30] : ~ big_q(X30)
| ? [X29] : big_q(X29) )
& ( ! [X28] : big_q(X28)
| ! [X27] : ~ big_q(X27) ) )
| ? [X25] :
! [X26] :
( ( ~ big_p(X26)
| big_p(X25) )
& ( big_p(X26)
| ~ big_p(X25) ) ) ) ) )
& ( ( ( ( ( ? [X24] : ~ big_p(X24)
| ! [X23] : ~ big_p(X23) )
& ( ! [X22] : big_p(X22)
| ? [X21] : big_p(X21) ) )
| ? [X19] :
! [X20] :
( ( ~ big_q(X20)
| big_q(X19) )
& ( big_q(X20)
| ~ big_q(X19) ) ) )
& ( ( ( ? [X18] : ~ big_p(X18)
| ? [X17] : big_p(X17) )
& ( ! [X16] : big_p(X16)
| ! [X15] : ~ big_p(X15) ) )
| ! [X13] :
? [X14] :
( ( ~ big_q(X14)
| ~ big_q(X13) )
& ( big_q(X14)
| big_q(X13) ) ) ) )
| ( ( ( ( ? [X12] : ~ big_q(X12)
| ! [X11] : ~ big_q(X11) )
& ( ! [X10] : big_q(X10)
| ? [X9] : big_q(X9) ) )
| ? [X7] :
! [X8] :
( ( ~ big_p(X8)
| big_p(X7) )
& ( big_p(X8)
| ~ big_p(X7) ) ) )
& ( ( ( ? [X6] : ~ big_q(X6)
| ? [X5] : big_q(X5) )
& ( ! [X4] : big_q(X4)
| ! [X3] : ~ big_q(X3) ) )
| ! [X0] :
? [X2] :
( ( ~ big_p(X2)
| ~ big_p(X0) )
& ( big_p(X2)
| big_p(X0) ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[pel34_neg]) ).
fof(sk_pel34_neg_sk,plain,
( ( ( ( ( ( ~ big_p(sK15)
| ! [U1] : ~ big_p(U1) )
& ( ! [X40] : big_p(X40)
| big_p(sK13) ) )
| ! [X1] :
( ( ~ big_q(sK12(X1))
| ~ big_q(X1) )
& ( big_q(sK12(X1))
| big_q(X1) ) ) )
& ( ( ( ~ big_p(sK23)
| big_p(sK22) )
& ( ! [X36] : big_p(X36)
| ! [X35] : ~ big_p(X35) ) )
| ! [X34] :
( ( ~ big_q(X34)
| big_q(sK9) )
& ( big_q(X34)
| ~ big_q(sK9) ) ) ) )
| ( ( ( ( ~ big_q(sK14)
| ! [U] : ~ big_q(U) )
& ( ! [X32] : big_q(X32)
| big_q(sK11) ) )
| ! [X] :
( ( ~ big_p(sK10(X))
| ~ big_p(X) )
& ( big_p(sK10(X))
| big_p(X) ) ) )
& ( ( ( ~ big_q(sK21)
| big_q(sK20) )
& ( ! [X28] : big_q(X28)
| ! [X27] : ~ big_q(X27) ) )
| ! [X26] :
( ( ~ big_p(X26)
| big_p(sK8) )
& ( big_p(X26)
| ~ big_p(sK8) ) ) ) ) )
& ( ( ( ( ( ~ big_p(sK3)
| ! [X23] : ~ big_p(X23) )
& ( ! [X22] : big_p(X22)
| big_p(sK2) ) )
| ! [X20] :
( ( ~ big_q(X20)
| big_q(sK1) )
& ( big_q(X20)
| ~ big_q(sK1) ) ) )
& ( ( ( ~ big_p(sK19)
| big_p(sK18) )
& ( ! [X16] : big_p(X16)
| ! [X15] : ~ big_p(X15) ) )
| ! [X13] :
( ( ~ big_q(sK6(X13))
| ~ big_q(X13) )
& ( big_q(sK6(X13))
| big_q(X13) ) ) ) )
| ( ( ( ( ~ big_q(sK7)
| ! [X11] : ~ big_q(X11) )
& ( ! [X10] : big_q(X10)
| big_q(sK5) ) )
| ! [X8] :
( ( ~ big_p(X8)
| big_p(sK4) )
& ( big_p(X8)
| ~ big_p(sK4) ) ) )
& ( ( ( ~ big_q(sK17)
| big_q(sK16) )
& ( ! [X4] : big_q(X4)
| ! [X3] : ~ big_q(X3) ) )
| ! [X0] :
( ( ~ big_p(sK0(X0))
| ~ big_p(X0) )
& ( big_p(sK0(X0))
| big_p(X0) ) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK16,sK17,sK4,sK5,sK7,sK6,sK18,sK19,sK1,sK2,sK3,sK8,sK20,sK21,sK10,sK11,sK14,sK9,sK22,sK23,sK12,sK13,sK15]),skolemize(X2,sK0(X0)),skolemize(X5,sK16),skolemize(X6,sK17),skolemize(X7,sK4),skolemize(X9,sK5),skolemize(X12,sK7),skolemize(X14,sK6(X13)),skolemize(X17,sK18),skolemize(X18,sK19),skolemize(X19,sK1),skolemize(X21,sK2),skolemize(X24,sK3),skolemize(X25,sK8),skolemize(X29,sK20),skolemize(X30,sK21),skolemize(Y,sK10(X)),skolemize(X31,sK11),skolemize(W,sK14),skolemize(X33,sK9),skolemize(X37,sK22),skolemize(X38,sK23),skolemize(Y1,sK12(X1)),skolemize(X39,sK13),skolemize(W1,sK15)],[nnf_1]) ).
fof(sk_pel34_neg,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK15)
| ~ big_p(VAR_3)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK13)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK15)
| ~ big_p(VAR_3)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK13)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK23)
| big_p(sK22)
| ~ big_q(VAR_2)
| big_q(sK9)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK9)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK23)
| big_p(sK22)
| big_q(VAR_2)
| ~ big_q(sK9)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK9)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK15)
| ~ big_p(VAR_3)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK13)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK15)
| ~ big_p(VAR_3)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK13)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK23)
| big_p(sK22)
| ~ big_q(VAR_2)
| big_q(sK9)
| big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK9)
| big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK23)
| big_p(sK22)
| big_q(VAR_2)
| ~ big_q(sK9)
| big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK9)
| big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK10(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK15)
| ~ big_p(VAR_3)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK13)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK15)
| ~ big_p(VAR_3)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK13)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK23)
| big_p(sK22)
| ~ big_q(VAR_2)
| big_q(sK9)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK9)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK23)
| big_p(sK22)
| big_q(VAR_2)
| ~ big_q(sK9)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK9)
| ~ big_q(sK14)
| ~ big_q(VAR_1)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK15)
| ~ big_p(VAR_3)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK11)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK13)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK11)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK15)
| ~ big_p(VAR_3)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK11)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK13)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK11)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK23)
| big_p(sK22)
| ~ big_q(VAR_2)
| big_q(sK9)
| big_q(VAR_1)
| big_q(sK11)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK9)
| big_q(VAR_1)
| big_q(sK11)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK23)
| big_p(sK22)
| big_q(VAR_2)
| ~ big_q(sK9)
| big_q(VAR_1)
| big_q(sK11)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK9)
| big_q(VAR_1)
| big_q(sK11)
| big_p(sK10(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK15)
| ~ big_p(VAR_2)
| ~ big_q(sK12(VAR_1))
| ~ big_q(VAR_1)
| ~ big_q(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_p(VAR_2)
| big_p(sK13)
| ~ big_q(sK12(VAR_1))
| ~ big_q(VAR_1)
| ~ big_q(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK15)
| ~ big_p(VAR_2)
| big_q(sK12(VAR_1))
| big_q(VAR_1)
| ~ big_q(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_p(VAR_2)
| big_p(sK13)
| big_q(sK12(VAR_1))
| big_q(VAR_1)
| ~ big_q(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1] :
( ~ big_p(sK23)
| big_p(sK22)
| ~ big_q(VAR_1)
| big_q(sK9)
| ~ big_q(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| ~ big_p(VAR_2)
| ~ big_q(VAR_1)
| big_q(sK9)
| ~ big_q(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1] :
( ~ big_p(sK23)
| big_p(sK22)
| big_q(VAR_1)
| ~ big_q(sK9)
| ~ big_q(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| ~ big_q(sK9)
| ~ big_q(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_p(sK15)
| ~ big_p(VAR_4)
| ~ big_q(sK12(VAR_3))
| ~ big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| big_p(sK13)
| ~ big_q(sK12(VAR_3))
| ~ big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_p(sK15)
| ~ big_p(VAR_4)
| big_q(sK12(VAR_3))
| big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| big_p(sK13)
| big_q(sK12(VAR_3))
| big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK23)
| big_p(sK22)
| ~ big_q(VAR_3)
| big_q(sK9)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_p(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| big_q(sK9)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK23)
| big_p(sK22)
| big_q(VAR_3)
| ~ big_q(sK9)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_p(VAR_5)
| ~ big_p(VAR_4)
| big_q(VAR_3)
| ~ big_q(sK9)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK15)
| ~ big_p(VAR_2)
| ~ big_q(sK12(VAR_1))
| ~ big_q(VAR_1)
| ~ big_q(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_p(VAR_2)
| big_p(sK13)
| ~ big_q(sK12(VAR_1))
| ~ big_q(VAR_1)
| ~ big_q(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK15)
| ~ big_p(VAR_2)
| big_q(sK12(VAR_1))
| big_q(VAR_1)
| ~ big_q(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_p(VAR_2)
| big_p(sK13)
| big_q(sK12(VAR_1))
| big_q(VAR_1)
| ~ big_q(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1] :
( ~ big_p(sK23)
| big_p(sK22)
| ~ big_q(VAR_1)
| big_q(sK9)
| ~ big_q(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| ~ big_p(VAR_2)
| ~ big_q(VAR_1)
| big_q(sK9)
| ~ big_q(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1] :
( ~ big_p(sK23)
| big_p(sK22)
| big_q(VAR_1)
| ~ big_q(sK9)
| ~ big_q(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| ~ big_q(sK9)
| ~ big_q(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_p(sK15)
| ~ big_p(VAR_4)
| ~ big_q(sK12(VAR_3))
| ~ big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| big_p(sK13)
| ~ big_q(sK12(VAR_3))
| ~ big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_p(sK15)
| ~ big_p(VAR_4)
| big_q(sK12(VAR_3))
| big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| big_p(sK13)
| big_q(sK12(VAR_3))
| big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK23)
| big_p(sK22)
| ~ big_q(VAR_3)
| big_q(sK9)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_p(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| big_q(sK9)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK23)
| big_p(sK22)
| big_q(VAR_3)
| ~ big_q(sK9)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_p(VAR_5)
| ~ big_p(VAR_4)
| big_q(VAR_3)
| ~ big_q(sK9)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK3)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK1)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK2)
| ~ big_q(VAR_2)
| big_q(sK1)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK3)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK1)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK2)
| big_q(VAR_2)
| ~ big_q(sK1)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK19)
| big_p(sK18)
| ~ big_q(sK6(VAR_2))
| ~ big_q(VAR_2)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(sK6(VAR_2))
| ~ big_q(VAR_2)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK19)
| big_p(sK18)
| big_q(sK6(VAR_2))
| big_q(VAR_2)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| big_q(sK6(VAR_2))
| big_q(VAR_2)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK3)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK1)
| big_q(VAR_1)
| big_q(sK5)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK2)
| ~ big_q(VAR_2)
| big_q(sK1)
| big_q(VAR_1)
| big_q(sK5)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK3)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK1)
| big_q(VAR_1)
| big_q(sK5)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK2)
| big_q(VAR_2)
| ~ big_q(sK1)
| big_q(VAR_1)
| big_q(sK5)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK19)
| big_p(sK18)
| ~ big_q(sK6(VAR_2))
| ~ big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK5)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(sK6(VAR_2))
| ~ big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK5)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK19)
| big_p(sK18)
| big_q(sK6(VAR_2))
| big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK5)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| big_q(sK6(VAR_2))
| big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK5)
| ~ big_p(VAR_0)
| big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK3)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK1)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK2)
| ~ big_q(VAR_2)
| big_q(sK1)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK3)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK1)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK2)
| big_q(VAR_2)
| ~ big_q(sK1)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK19)
| big_p(sK18)
| ~ big_q(sK6(VAR_2))
| ~ big_q(VAR_2)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(sK6(VAR_2))
| ~ big_q(VAR_2)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK19)
| big_p(sK18)
| big_q(sK6(VAR_2))
| big_q(VAR_2)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| big_q(sK6(VAR_2))
| big_q(VAR_2)
| ~ big_q(sK7)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK3)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK1)
| big_q(VAR_1)
| big_q(sK5)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK2)
| ~ big_q(VAR_2)
| big_q(sK1)
| big_q(VAR_1)
| big_q(sK5)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK3)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK1)
| big_q(VAR_1)
| big_q(sK5)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| big_p(sK2)
| big_q(VAR_2)
| ~ big_q(sK1)
| big_q(VAR_1)
| big_q(sK5)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK19)
| big_p(sK18)
| ~ big_q(sK6(VAR_2))
| ~ big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK5)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(sK6(VAR_2))
| ~ big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK5)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK19)
| big_p(sK18)
| big_q(sK6(VAR_2))
| big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK5)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| ~ big_p(VAR_3)
| big_q(sK6(VAR_2))
| big_q(VAR_2)
| big_q(VAR_1)
| big_q(sK5)
| big_p(VAR_0)
| ~ big_p(sK4) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK3)
| ~ big_p(VAR_2)
| ~ big_q(VAR_1)
| big_q(sK1)
| ~ big_q(sK17)
| big_q(sK16)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_p(VAR_2)
| big_p(sK2)
| ~ big_q(VAR_1)
| big_q(sK1)
| ~ big_q(sK17)
| big_q(sK16)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK3)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| ~ big_q(sK1)
| ~ big_q(sK17)
| big_q(sK16)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_p(VAR_2)
| big_p(sK2)
| big_q(VAR_1)
| ~ big_q(sK1)
| ~ big_q(sK17)
| big_q(sK16)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ big_p(sK19)
| big_p(sK18)
| ~ big_q(sK6(VAR_1))
| ~ big_q(VAR_1)
| ~ big_q(sK17)
| big_q(sK16)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| ~ big_p(VAR_2)
| ~ big_q(sK6(VAR_1))
| ~ big_q(VAR_1)
| ~ big_q(sK17)
| big_q(sK16)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ big_p(sK19)
| big_p(sK18)
| big_q(sK6(VAR_1))
| big_q(VAR_1)
| ~ big_q(sK17)
| big_q(sK16)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| ~ big_p(VAR_2)
| big_q(sK6(VAR_1))
| big_q(VAR_1)
| ~ big_q(sK17)
| big_q(sK16)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_p(sK3)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| big_q(sK1)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| big_p(sK2)
| ~ big_q(VAR_3)
| big_q(sK1)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_p(sK3)
| ~ big_p(VAR_4)
| big_q(VAR_3)
| ~ big_q(sK1)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| big_p(sK2)
| big_q(VAR_3)
| ~ big_q(sK1)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK19)
| big_p(sK18)
| ~ big_q(sK6(VAR_3))
| ~ big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_p(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(sK6(VAR_3))
| ~ big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK19)
| big_p(sK18)
| big_q(sK6(VAR_3))
| big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_p(VAR_5)
| ~ big_p(VAR_4)
| big_q(sK6(VAR_3))
| big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK3)
| ~ big_p(VAR_2)
| ~ big_q(VAR_1)
| big_q(sK1)
| ~ big_q(sK17)
| big_q(sK16)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_p(VAR_2)
| big_p(sK2)
| ~ big_q(VAR_1)
| big_q(sK1)
| ~ big_q(sK17)
| big_q(sK16)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_p(sK3)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| ~ big_q(sK1)
| ~ big_q(sK17)
| big_q(sK16)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_p(VAR_2)
| big_p(sK2)
| big_q(VAR_1)
| ~ big_q(sK1)
| ~ big_q(sK17)
| big_q(sK16)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ big_p(sK19)
| big_p(sK18)
| ~ big_q(sK6(VAR_1))
| ~ big_q(VAR_1)
| ~ big_q(sK17)
| big_q(sK16)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| ~ big_p(VAR_2)
| ~ big_q(sK6(VAR_1))
| ~ big_q(VAR_1)
| ~ big_q(sK17)
| big_q(sK16)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ big_p(sK19)
| big_p(sK18)
| big_q(sK6(VAR_1))
| big_q(VAR_1)
| ~ big_q(sK17)
| big_q(sK16)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_p(VAR_3)
| ~ big_p(VAR_2)
| big_q(sK6(VAR_1))
| big_q(VAR_1)
| ~ big_q(sK17)
| big_q(sK16)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_p(sK3)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| big_q(sK1)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| big_p(sK2)
| ~ big_q(VAR_3)
| big_q(sK1)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_p(sK3)
| ~ big_p(VAR_4)
| big_q(VAR_3)
| ~ big_q(sK1)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_p(VAR_4)
| big_p(sK2)
| big_q(VAR_3)
| ~ big_q(sK1)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK19)
| big_p(sK18)
| ~ big_q(sK6(VAR_3))
| ~ big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_p(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(sK6(VAR_3))
| ~ big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_p(sK19)
| big_p(sK18)
| big_q(sK6(VAR_3))
| big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_p(VAR_5)
| ~ big_p(VAR_4)
| big_q(sK6(VAR_3))
| big_q(VAR_3)
| big_q(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_pel34_neg_sk]) ).
cnf(c_4,negated_conjecture,
( big_p(E)
| big_p(sK2)
| big_q(D)
| ~ big_q(sK1)
| big_q(C)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_6,negated_conjecture,
( big_p(E)
| big_p(sK2)
| ~ big_q(D)
| big_q(sK1)
| big_q(C)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_11,negated_conjecture,
( ~ big_p(sK3)
| ~ big_p(E)
| big_q(D)
| ~ big_q(sK1)
| big_q(C)
| ~ big_q(B)
| ~ big_p(sK0(A))
| ~ big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_13,negated_conjecture,
( ~ big_p(sK3)
| ~ big_p(E)
| ~ big_q(D)
| big_q(sK1)
| big_q(C)
| ~ big_q(B)
| ~ big_p(sK0(A))
| ~ big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_14,negated_conjecture,
( big_p(E)
| ~ big_p(D)
| big_q(sK6(C))
| big_q(C)
| big_q(B)
| big_q(sK5)
| big_p(A)
| ~ big_p(sK4) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_21,negated_conjecture,
( big_p(E)
| ~ big_p(D)
| ~ big_q(sK6(C))
| ~ big_q(C)
| ~ big_q(sK7)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK4) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_26,negated_conjecture,
( big_p(E)
| ~ big_p(D)
| big_q(sK6(C))
| big_q(C)
| big_q(B)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_28,negated_conjecture,
( big_p(D)
| big_p(sK2)
| big_q(C)
| ~ big_q(sK1)
| big_q(B)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_30,negated_conjecture,
( big_p(D)
| big_p(sK2)
| ~ big_q(C)
| big_q(sK1)
| big_q(B)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_33,negated_conjecture,
( big_p(E)
| ~ big_p(D)
| ~ big_q(sK6(C))
| ~ big_q(C)
| ~ big_q(sK7)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK4) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_38,negated_conjecture,
( big_p(F)
| ~ big_p(E)
| big_q(D)
| ~ big_q(sK9)
| big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK8) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_39,negated_conjecture,
( big_p(F)
| ~ big_p(E)
| ~ big_q(D)
| big_q(sK9)
| big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK8) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_44,negated_conjecture,
( big_p(F)
| ~ big_p(E)
| big_q(D)
| ~ big_q(sK9)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_45,negated_conjecture,
( big_p(F)
| ~ big_p(E)
| ~ big_q(D)
| big_q(sK9)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_52,negated_conjecture,
( big_p(D)
| big_p(sK13)
| big_q(sK12(C))
| big_q(C)
| big_q(B)
| big_q(sK11)
| big_p(sK10(A))
| big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_60,negated_conjecture,
( big_p(D)
| big_p(sK13)
| ~ big_q(sK12(C))
| ~ big_q(C)
| ~ big_q(sK14)
| ~ big_q(B)
| big_p(sK10(A))
| big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_65,negated_conjecture,
( ~ big_p(sK15)
| ~ big_p(D)
| big_q(sK12(C))
| big_q(C)
| big_q(B)
| big_q(sK11)
| ~ big_p(sK10(A))
| ~ big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_73,negated_conjecture,
( ~ big_p(sK15)
| ~ big_p(D)
| ~ big_q(sK12(C))
| ~ big_q(C)
| ~ big_q(sK14)
| ~ big_q(B)
| ~ big_p(sK10(A))
| ~ big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_78,plain,
( big_p(D)
| big_q(C)
| ~ big_q(sK1)
| big_q(B)
| ~ big_q(A)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_4]) ).
cnf(c_85,plain,
( big_p(D)
| ~ big_q(C)
| big_q(sK1)
| big_q(B)
| ~ big_q(A)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_6]) ).
cnf(c_86,plain,
( big_p(sK2)
| ~ big_q(D)
| big_q(sK1)
| big_q(C)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_6]) ).
cnf(c_99,plain,
( ~ big_p(sK3)
| big_q(D)
| ~ big_q(sK1)
| big_q(C)
| ~ big_q(B)
| ~ big_p(sK0(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_11]) ).
cnf(c_105,plain,
( ~ big_p(sK3)
| ~ big_q(D)
| big_q(sK1)
| big_q(C)
| ~ big_q(B)
| ~ big_p(sK0(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_13]) ).
cnf(c_108,plain,
( big_p(D)
| big_q(sK6(C))
| big_q(C)
| big_q(B)
| big_q(sK5)
| big_p(A)
| ~ big_p(sK4) ),
inference(factor,[status(thm)],[c_14]) ).
cnf(c_125,plain,
( big_p(D)
| ~ big_q(sK6(C))
| ~ big_q(C)
| ~ big_q(sK7)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK4) ),
inference(factor,[status(thm)],[c_21]) ).
cnf(c_136,plain,
( ~ big_p(D)
| big_q(sK6(C))
| big_q(C)
| big_q(B)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_26]) ).
cnf(c_142,plain,
( big_p(sK2)
| big_q(C)
| ~ big_q(sK1)
| big_q(B)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_28]) ).
cnf(c_146,plain,
( big_p(sK2)
| ~ big_q(C)
| big_q(sK1)
| big_q(B)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_30]) ).
cnf(c_153,plain,
( ~ big_p(D)
| ~ big_q(sK6(C))
| ~ big_q(C)
| ~ big_q(sK7)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_33]) ).
cnf(c_164,plain,
( big_p(E)
| big_q(D)
| ~ big_q(sK9)
| big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_38]) ).
cnf(c_168,plain,
( big_p(E)
| ~ big_q(D)
| big_q(sK9)
| big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_39]) ).
cnf(c_180,plain,
( ~ big_p(E)
| big_q(D)
| ~ big_q(sK9)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_44]) ).
cnf(c_184,plain,
( ~ big_p(E)
| ~ big_q(D)
| big_q(sK9)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_45]) ).
cnf(c_201,plain,
( big_p(sK13)
| big_q(sK12(C))
| big_q(C)
| big_q(B)
| big_q(sK11)
| big_p(sK10(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_52]) ).
cnf(c_219,plain,
( big_p(C)
| ~ big_q(sK12(B))
| ~ big_q(B)
| ~ big_q(sK14)
| ~ big_q(A)
| big_p(sK10(sK13))
| big_p(sK13) ),
inference(factor,[status(thm)],[c_60]) ).
cnf(c_220,plain,
( big_p(sK13)
| ~ big_q(sK12(C))
| ~ big_q(C)
| ~ big_q(sK14)
| ~ big_q(B)
| big_p(sK10(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_60]) ).
cnf(c_230,plain,
( ~ big_p(sK15)
| big_q(sK12(C))
| big_q(C)
| big_q(B)
| big_q(sK11)
| ~ big_p(sK10(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_65]) ).
cnf(c_246,plain,
( ~ big_p(sK15)
| ~ big_q(sK12(C))
| ~ big_q(C)
| ~ big_q(sK14)
| ~ big_q(B)
| ~ big_p(sK10(A))
| ~ big_p(A) ),
inference(factor,[status(thm)],[c_73]) ).
cnf(c_250,plain,
( big_q(C)
| ~ big_q(sK1)
| big_q(B)
| ~ big_q(A)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_78]) ).
cnf(c_259,plain,
( ~ big_q(C)
| big_q(sK1)
| big_q(B)
| ~ big_q(A)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_85]) ).
cnf(c_262,plain,
( big_p(sK2)
| big_q(sK1)
| big_q(C)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_86]) ).
cnf(c_273,plain,
( big_q(C)
| ~ big_q(sK1)
| big_q(B)
| ~ big_q(A)
| ~ big_p(sK0(sK3))
| ~ big_p(sK3) ),
inference(factor,[status(thm)],[c_99]) ).
cnf(c_280,plain,
( ~ big_q(C)
| big_q(sK1)
| big_q(B)
| ~ big_q(A)
| ~ big_p(sK0(sK3))
| ~ big_p(sK3) ),
inference(factor,[status(thm)],[c_105]) ).
cnf(c_284,plain,
( big_q(sK6(C))
| big_q(C)
| big_q(B)
| big_q(sK5)
| big_p(A)
| ~ big_p(sK4) ),
inference(factor,[status(thm)],[c_108]) ).
cnf(c_302,plain,
( ~ big_q(sK6(C))
| ~ big_q(C)
| ~ big_q(sK7)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK4) ),
inference(factor,[status(thm)],[c_125]) ).
cnf(c_314,plain,
( big_q(sK6(C))
| big_q(C)
| big_q(B)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_136]) ).
cnf(c_321,plain,
( big_p(sK2)
| big_q(B)
| ~ big_q(sK1)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_142]) ).
cnf(c_326,plain,
( big_p(sK2)
| ~ big_q(B)
| big_q(sK1)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_146]) ).
cnf(c_332,plain,
( ~ big_q(sK6(C))
| ~ big_q(C)
| ~ big_q(sK7)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_153]) ).
cnf(c_344,plain,
( big_q(D)
| ~ big_q(sK9)
| big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_164]) ).
cnf(c_350,plain,
( ~ big_q(D)
| big_q(sK9)
| big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_168]) ).
cnf(c_362,plain,
( big_q(D)
| ~ big_q(sK9)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_180]) ).
cnf(c_368,plain,
( ~ big_q(D)
| big_q(sK9)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_184]) ).
cnf(c_385,plain,
( big_p(sK13)
| big_q(sK12(B))
| big_q(B)
| big_q(sK11)
| big_p(sK10(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_201]) ).
cnf(c_400,plain,
( ~ big_q(sK12(B))
| ~ big_q(B)
| ~ big_q(sK14)
| ~ big_q(A)
| big_p(sK10(sK13))
| big_p(sK13) ),
inference(factor,[status(thm)],[c_219]) ).
cnf(c_402,plain,
( big_p(sK13)
| ~ big_q(sK12(B))
| ~ big_q(B)
| ~ big_q(sK14)
| big_p(sK10(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_220]) ).
cnf(c_411,plain,
( big_q(sK12(B))
| big_q(B)
| big_q(A)
| big_q(sK11)
| ~ big_p(sK10(sK15))
| ~ big_p(sK15) ),
inference(factor,[status(thm)],[c_230]) ).
cnf(c_425,plain,
( ~ big_q(sK12(B))
| ~ big_q(B)
| ~ big_q(sK14)
| ~ big_q(A)
| ~ big_p(sK10(sK15))
| ~ big_p(sK15) ),
inference(factor,[status(thm)],[c_246]) ).
cnf(c_428,plain,
( big_q(B)
| big_q(A)
| ~ big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_250]) ).
cnf(c_433,plain,
( big_q(sK1)
| big_q(B)
| ~ big_q(A)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_259]) ).
cnf(c_436,plain,
( big_p(sK2)
| big_q(sK1)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_262]) ).
cnf(c_439,plain,
( big_q(B)
| big_q(A)
| ~ big_q(sK1)
| ~ big_p(sK0(sK3))
| ~ big_p(sK3) ),
inference(factor,[status(thm)],[c_273]) ).
cnf(c_443,plain,
( big_q(sK1)
| big_q(B)
| ~ big_q(A)
| ~ big_p(sK0(sK3))
| ~ big_p(sK3) ),
inference(factor,[status(thm)],[c_280]) ).
cnf(c_446,plain,
( big_q(sK6(B))
| big_q(B)
| big_q(sK5)
| big_p(A)
| ~ big_p(sK4) ),
inference(factor,[status(thm)],[c_284]) ).
cnf(c_455,plain,
( ~ big_q(sK6(B))
| ~ big_q(B)
| ~ big_q(sK7)
| big_p(A)
| ~ big_p(sK4) ),
inference(factor,[status(thm)],[c_302]) ).
cnf(c_462,plain,
( big_q(sK6(B))
| big_q(B)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_314]) ).
cnf(c_466,plain,
( big_p(sK2)
| ~ big_q(sK1)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_321]) ).
cnf(c_471,plain,
( ~ big_q(sK6(B))
| ~ big_q(B)
| ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_332]) ).
cnf(c_478,plain,
( big_q(C)
| big_q(B)
| ~ big_q(sK9)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_344]) ).
cnf(c_482,plain,
( big_q(sK9)
| big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_350]) ).
cnf(c_488,plain,
( big_q(C)
| big_q(B)
| ~ big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_362]) ).
cnf(c_492,plain,
( big_q(sK9)
| big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_368]) ).
cnf(c_506,plain,
( ~ big_q(sK12(A))
| ~ big_q(A)
| ~ big_q(sK14)
| big_p(sK10(sK13))
| big_p(sK13) ),
inference(factor,[status(thm)],[c_400]) ).
cnf(c_508,plain,
( big_p(sK13)
| ~ big_q(sK12(sK14))
| ~ big_q(sK14)
| big_p(sK10(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_402]) ).
cnf(c_512,plain,
( big_q(sK12(A))
| big_q(A)
| big_q(sK11)
| ~ big_p(sK10(sK15))
| ~ big_p(sK15) ),
inference(factor,[status(thm)],[c_411]) ).
cnf(c_518,plain,
( ~ big_q(sK12(A))
| ~ big_q(A)
| ~ big_q(sK14)
| ~ big_p(sK10(sK15))
| ~ big_p(sK15) ),
inference(factor,[status(thm)],[c_425]) ).
cnf(c_520,plain,
( big_q(A)
| ~ big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_428]) ).
cnf(c_521,plain,
( big_q(sK1)
| ~ big_q(A)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_433]) ).
cnf(c_522,plain,
( big_q(A)
| ~ big_q(sK1)
| ~ big_p(sK0(sK3))
| ~ big_p(sK3) ),
inference(factor,[status(thm)],[c_439]) ).
cnf(c_523,plain,
( big_q(sK1)
| ~ big_q(A)
| ~ big_p(sK0(sK3))
| ~ big_p(sK3) ),
inference(factor,[status(thm)],[c_443]) ).
cnf(c_524,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(A)
| ~ big_p(sK4) ),
inference(factor,[status(thm)],[c_446]) ).
cnf(c_526,plain,
( ~ big_q(sK6(sK7))
| ~ big_q(sK7)
| big_p(A)
| ~ big_p(sK4) ),
inference(factor,[status(thm)],[c_455]) ).
cnf(c_528,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_462]) ).
cnf(c_530,plain,
( ~ big_q(sK6(sK7))
| ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_471]) ).
cnf(c_532,plain,
( big_q(B)
| ~ big_q(sK9)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_478]) ).
cnf(c_533,plain,
( big_q(sK9)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_482]) ).
cnf(c_534,plain,
( big_q(B)
| ~ big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_488]) ).
cnf(c_535,plain,
( big_q(sK9)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_492]) ).
cnf(c_537,plain,
( ~ big_q(sK12(sK14))
| ~ big_q(sK14)
| big_p(sK10(sK13))
| big_p(sK13) ),
inference(factor,[status(thm)],[c_506]) ).
cnf(c_538,plain,
( big_q(sK12(sK11))
| big_q(sK11)
| ~ big_p(sK10(sK15))
| ~ big_p(sK15) ),
inference(factor,[status(thm)],[c_512]) ).
cnf(c_603,plain,
( big_p(sK13)
| big_q(C)
| big_q(sK11)
| big_p(sK10(B))
| big_p(B)
| big_p(sK2)
| big_q(sK1)
| big_p(sK0(A))
| big_p(A) ),
inference(resolve,[status(thm)],[c_436,c_385]) ).
cnf(c_604,plain,
( big_p(sK13)
| big_q(B)
| big_q(sK11)
| big_p(sK10(A))
| big_p(A)
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_603]) ).
cnf(c_612,plain,
( big_p(sK13)
| big_q(A)
| big_q(sK11)
| big_p(sK10(sK2))
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_604]) ).
cnf(c_614,plain,
( big_p(sK13)
| big_q(sK11)
| big_p(sK10(A))
| big_p(A)
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_604]) ).
cnf(c_627,plain,
( big_p(sK13)
| big_q(sK11)
| big_p(sK10(sK2))
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_612]) ).
cnf(c_629,plain,
( big_q(sK11)
| big_p(sK10(sK13))
| big_p(sK13)
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_614]) ).
cnf(c_1823,plain,
( big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK13)
| big_p(sK10(sK2))
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_627,c_521]) ).
cnf(c_1824,plain,
( big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK13)
| big_p(sK10(sK2))
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1823]) ).
cnf(c_1825,plain,
( big_q(sK1)
| big_p(sK13)
| big_p(sK10(sK2))
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1824]) ).
cnf(c_682,plain,
( big_p(sK13)
| big_p(sK10(sK2))
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1825]) ).
cnf(c_1826,plain,
( big_q(A)
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_682,c_520]) ).
cnf(c_1827,plain,
( big_q(A)
| big_p(sK0(sK2))
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1826]) ).
cnf(c_688,plain,
( big_q(A)
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1827]) ).
cnf(c_1828,plain,
( big_p(sK13)
| ~ big_q(sK14)
| big_p(sK10(A))
| big_p(A)
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_688,c_508]) ).
cnf(c_696,plain,
( ~ big_q(sK14)
| big_p(sK10(A))
| big_p(A)
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1828]) ).
cnf(c_1829,plain,
( ~ big_q(sK14)
| big_p(sK10(sK2))
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_696]) ).
cnf(c_699,plain,
( ~ big_q(sK14)
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1829]) ).
cnf(c_1830,plain,
( big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_699,c_688]) ).
cnf(c_1831,plain,
( big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1830]) ).
cnf(c_1832,plain,
( big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1831]) ).
cnf(c_1833,plain,
( big_p(sK13)
| big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1832]) ).
cnf(c_700,plain,
( big_p(sK13)
| big_p(sK10(sK2))
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1833]) ).
cnf(c_704,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_700,c_528]) ).
cnf(c_1834,plain,
( big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK10(sK13))
| big_p(sK13)
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_629,c_521]) ).
cnf(c_1835,plain,
( big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK10(sK13))
| big_p(sK13)
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1834]) ).
cnf(c_1836,plain,
( big_q(sK1)
| big_p(sK10(sK13))
| big_p(sK13)
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1835]) ).
cnf(c_717,plain,
( big_p(sK10(sK13))
| big_p(sK13)
| big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1836]) ).
cnf(c_1837,plain,
( big_q(A)
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_717,c_520]) ).
cnf(c_1838,plain,
( big_q(A)
| big_p(sK0(sK2))
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1837]) ).
cnf(c_723,plain,
( big_q(A)
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1838]) ).
cnf(c_1839,plain,
( ~ big_q(sK14)
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_723,c_537]) ).
cnf(c_1840,plain,
( ~ big_q(sK14)
| big_p(sK10(sK13))
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1839]) ).
cnf(c_725,plain,
( ~ big_q(sK14)
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1840]) ).
cnf(c_1841,plain,
( big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_725,c_723]) ).
cnf(c_1842,plain,
( big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1841]) ).
cnf(c_1843,plain,
( big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1842]) ).
cnf(c_1844,plain,
( big_p(sK10(sK13))
| big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1843]) ).
cnf(c_729,plain,
( big_p(sK10(sK13))
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1844]) ).
cnf(c_1845,plain,
( big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_704,c_521]) ).
cnf(c_1846,plain,
( big_q(sK1)
| big_p(sK0(sK2))
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1845]) ).
cnf(c_839,plain,
( big_q(sK1)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1846]) ).
cnf(c_1847,plain,
( big_q(A)
| big_p(sK0(sK2))
| big_p(sK2)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_839,c_520]) ).
cnf(c_1848,plain,
( big_q(A)
| big_p(sK0(sK2))
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1847]) ).
cnf(c_850,plain,
( big_q(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1848]) ).
cnf(c_852,plain,
( big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(factor,[status(thm)],[c_850]) ).
cnf(c_1849,plain,
( big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_852,c_521]) ).
cnf(c_1850,plain,
( big_q(sK1)
| big_p(sK0(sK2))
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1849]) ).
cnf(c_856,plain,
( big_q(sK1)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1850]) ).
cnf(c_1851,plain,
( big_q(A)
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_856,c_520]) ).
cnf(c_1852,plain,
( big_q(A)
| big_p(sK0(sK2))
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1851]) ).
cnf(c_868,plain,
( big_q(A)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1852]) ).
cnf(c_1853,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_868,c_530]) ).
cnf(c_870,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1853]) ).
cnf(c_1854,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_870,c_868]) ).
cnf(c_1855,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| ~ big_p(A)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1854]) ).
cnf(c_1856,plain,
( big_p(sK4)
| big_p(sK13)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1855]) ).
cnf(c_1857,plain,
( big_p(sK4)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1856]) ).
cnf(c_879,plain,
( ~ big_p(A)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1857]) ).
cnf(c_1858,plain,
( big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_879,c_729]) ).
cnf(c_1859,plain,
( big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1858]) ).
cnf(c_1860,plain,
( big_p(sK13)
| big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1859]) ).
cnf(c_881,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK0(sK2))
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1860]) ).
cnf(c_1861,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK4)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_881,c_528]) ).
cnf(c_894,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1861]) ).
cnf(c_1862,plain,
( big_p(sK2)
| big_q(sK1)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_894,c_326]) ).
cnf(c_1863,plain,
( big_p(sK2)
| big_q(sK1)
| big_q(sK5)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1862]) ).
cnf(c_1864,plain,
( big_p(sK2)
| big_q(sK1)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1863]) ).
cnf(c_932,plain,
( big_q(sK1)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1864]) ).
cnf(c_1865,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK2)
| big_q(sK1)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_932,c_881]) ).
cnf(c_1866,plain,
( big_p(sK4)
| big_p(sK13)
| big_q(sK1)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1865]) ).
cnf(c_1867,plain,
( big_p(sK4)
| big_q(sK1)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1866]) ).
cnf(c_940,plain,
( big_q(sK1)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1867]) ).
cnf(c_1868,plain,
( big_p(sK2)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_940,c_466]) ).
cnf(c_1869,plain,
( big_p(sK2)
| big_q(sK5)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1868]) ).
cnf(c_1870,plain,
( big_p(sK2)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1869]) ).
cnf(c_942,plain,
( ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1870]) ).
cnf(c_1871,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK2)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_942,c_881]) ).
cnf(c_1872,plain,
( big_p(sK4)
| big_p(sK13)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1871]) ).
cnf(c_1873,plain,
( big_p(sK4)
| big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1872]) ).
cnf(c_949,plain,
( big_q(sK5)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1873]) ).
cnf(c_950,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_949,c_535]) ).
cnf(c_951,plain,
( big_q(sK9)
| big_p(A)
| ~ big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_949,c_533]) ).
cnf(c_963,plain,
( big_q(sK9)
| ~ big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_951]) ).
cnf(c_1874,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK2)
| big_q(sK9)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_950,c_881]) ).
cnf(c_1875,plain,
( big_p(sK4)
| big_p(sK13)
| big_q(sK9)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1874]) ).
cnf(c_1876,plain,
( big_p(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1875]) ).
cnf(c_972,plain,
( big_q(sK9)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1876]) ).
cnf(c_1877,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_972,c_534]) ).
cnf(c_973,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1877]) ).
cnf(c_1878,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK2)
| big_q(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_973,c_881]) ).
cnf(c_1879,plain,
( big_p(sK4)
| big_p(sK13)
| big_q(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1878]) ).
cnf(c_1880,plain,
( big_p(sK4)
| big_q(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1879]) ).
cnf(c_974,plain,
( big_q(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1880]) ).
cnf(c_1881,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_974,c_530]) ).
cnf(c_977,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1881]) ).
cnf(c_1882,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_977,c_974]) ).
cnf(c_1883,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1882]) ).
cnf(c_1884,plain,
( big_p(sK8)
| big_p(sK4)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1883]) ).
cnf(c_1885,plain,
( big_p(sK8)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1884]) ).
cnf(c_988,plain,
( ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1885]) ).
cnf(c_1886,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK2)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_988,c_881]) ).
cnf(c_1887,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1886]) ).
cnf(c_1888,plain,
( big_p(sK4)
| big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1887]) ).
cnf(c_989,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1888]) ).
cnf(c_1889,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK4)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_989,c_528]) ).
cnf(c_990,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1889]) ).
cnf(c_1890,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_990,c_535]) ).
cnf(c_1010,plain,
( big_q(sK9)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1890]) ).
cnf(c_1891,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK2)
| big_q(sK9)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1010,c_989]) ).
cnf(c_1892,plain,
( big_p(sK8)
| big_p(sK4)
| big_q(sK9)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1891]) ).
cnf(c_1893,plain,
( big_p(sK8)
| big_q(sK9)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1892]) ).
cnf(c_1021,plain,
( big_q(sK9)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1893]) ).
cnf(c_1894,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1021,c_534]) ).
cnf(c_1022,plain,
( big_q(B)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1894]) ).
cnf(c_1023,plain,
( ~ big_p(A)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_1022]) ).
cnf(c_1895,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK2)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1023,c_989]) ).
cnf(c_1896,plain,
( big_p(sK8)
| big_p(sK4)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1895]) ).
cnf(c_1897,plain,
( big_p(sK8)
| big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1896]) ).
cnf(c_1024,plain,
( big_q(sK5)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1897]) ).
cnf(c_1898,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1024,c_535]) ).
cnf(c_1025,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1898]) ).
cnf(c_1899,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK2)
| big_q(sK9)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1025,c_989]) ).
cnf(c_1900,plain,
( big_p(sK8)
| big_p(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1899]) ).
cnf(c_1901,plain,
( big_p(sK8)
| big_q(sK9)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1900]) ).
cnf(c_1043,plain,
( big_q(sK9)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1901]) ).
cnf(c_1902,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1043,c_534]) ).
cnf(c_1044,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1902]) ).
cnf(c_1903,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK2)
| big_q(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1044,c_989]) ).
cnf(c_1904,plain,
( big_p(sK8)
| big_p(sK4)
| big_q(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1903]) ).
cnf(c_1905,plain,
( big_p(sK8)
| big_q(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1904]) ).
cnf(c_1045,plain,
( big_q(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1905]) ).
cnf(c_1906,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1045,c_530]) ).
cnf(c_1194,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1906]) ).
cnf(c_1907,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK2)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1194,c_1045]) ).
cnf(c_1908,plain,
( big_p(sK8)
| big_p(sK4)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1907]) ).
cnf(c_1909,plain,
( big_p(sK8)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1908]) ).
cnf(c_1200,plain,
( ~ big_p(A)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1909]) ).
cnf(c_1910,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK2)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1200,c_989]) ).
cnf(c_1911,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1910]) ).
cnf(c_1912,plain,
( big_p(sK8)
| big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1911]) ).
cnf(c_1201,plain,
( big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1912]) ).
cnf(c_1913,plain,
( big_q(sK9)
| big_p(sK4)
| big_p(sK13)
| big_p(sK2)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1201,c_963]) ).
cnf(c_1914,plain,
( big_q(sK9)
| big_p(sK4)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1913]) ).
cnf(c_1202,plain,
( big_q(sK9)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1914]) ).
cnf(c_1915,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK4)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1201,c_528]) ).
cnf(c_1203,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1915]) ).
cnf(c_1205,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK8)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1202,c_532]) ).
cnf(c_1210,plain,
( big_q(A)
| ~ big_p(sK8)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_1205]) ).
cnf(c_1916,plain,
( big_p(sK4)
| big_p(sK2)
| big_q(A)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1210,c_1201]) ).
cnf(c_1917,plain,
( big_p(sK4)
| big_q(A)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1916]) ).
cnf(c_1219,plain,
( big_q(A)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1917]) ).
cnf(c_1918,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1219,c_530]) ).
cnf(c_1222,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1918]) ).
cnf(c_1919,plain,
( big_p(sK13)
| big_p(sK4)
| big_p(sK2)
| ~ big_p(A)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1222,c_1219]) ).
cnf(c_1920,plain,
( big_p(sK13)
| big_p(sK4)
| ~ big_p(A)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1919]) ).
cnf(c_1921,plain,
( big_p(sK13)
| ~ big_p(A)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1920]) ).
cnf(c_1231,plain,
( ~ big_p(A)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1921]) ).
cnf(c_1922,plain,
( big_p(sK4)
| big_p(sK2)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1231,c_1201]) ).
cnf(c_1923,plain,
( big_p(sK4)
| big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1922]) ).
cnf(c_1232,plain,
( big_p(sK13)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1923]) ).
cnf(c_1924,plain,
( big_p(sK2)
| big_q(sK1)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1203,c_326]) ).
cnf(c_1925,plain,
( big_p(sK2)
| big_q(sK1)
| big_q(sK5)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1924]) ).
cnf(c_1926,plain,
( big_p(sK2)
| big_q(sK1)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1925]) ).
cnf(c_1242,plain,
( big_q(sK1)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1926]) ).
cnf(c_1927,plain,
( big_p(sK4)
| big_p(sK2)
| big_q(sK1)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1242,c_1232]) ).
cnf(c_1928,plain,
( big_p(sK4)
| big_q(sK1)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1927]) ).
cnf(c_1251,plain,
( big_q(sK1)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1928]) ).
cnf(c_1929,plain,
( big_p(sK2)
| big_q(sK5)
| ~ big_p(A)
| big_p(sK4)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1251,c_466]) ).
cnf(c_1930,plain,
( big_p(sK2)
| big_q(sK5)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1929]) ).
cnf(c_1931,plain,
( big_p(sK2)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1930]) ).
cnf(c_1254,plain,
( ~ big_p(A)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1931]) ).
cnf(c_1932,plain,
( big_p(sK4)
| big_p(sK2)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1254,c_1232]) ).
cnf(c_1933,plain,
( big_p(sK4)
| big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1932]) ).
cnf(c_1260,plain,
( big_q(sK5)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1933]) ).
cnf(c_1261,plain,
( big_q(sK9)
| big_p(A)
| ~ big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1260,c_533]) ).
cnf(c_1273,plain,
( big_q(sK9)
| ~ big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_1261]) ).
cnf(c_1934,plain,
( big_p(sK4)
| big_p(sK2)
| big_q(sK9)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1273,c_1201]) ).
cnf(c_1935,plain,
( big_p(sK4)
| big_q(sK9)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1934]) ).
cnf(c_1283,plain,
( big_q(sK9)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1935]) ).
cnf(c_1284,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1283,c_532]) ).
cnf(c_1289,plain,
( big_q(A)
| ~ big_p(sK8)
| big_p(sK4)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_1284]) ).
cnf(c_1936,plain,
( big_p(sK4)
| big_p(sK2)
| big_q(A)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1289,c_1201]) ).
cnf(c_1937,plain,
( big_p(sK4)
| big_q(A)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1936]) ).
cnf(c_1296,plain,
( big_q(A)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1937]) ).
cnf(c_1938,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1296,c_530]) ).
cnf(c_1298,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1938]) ).
cnf(c_1939,plain,
( big_p(sK4)
| big_p(sK2)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1298,c_1296]) ).
cnf(c_1940,plain,
( big_p(sK4)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1939]) ).
cnf(c_1303,plain,
( ~ big_p(A)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1940]) ).
cnf(c_1941,plain,
( big_p(sK4)
| big_p(sK2)
| big_p(sK4)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_1303,c_1232]) ).
cnf(c_1942,plain,
( big_p(sK4)
| big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1941]) ).
cnf(c_1304,plain,
( big_p(sK4)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_1942]) ).
cnf(c_1943,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK4)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1304,c_528]) ).
cnf(c_1325,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1943]) ).
cnf(c_1342,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1325,c_535]) ).
cnf(c_1343,plain,
( big_q(sK9)
| big_p(A)
| ~ big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1325,c_533]) ).
cnf(c_1352,plain,
( big_q(sK9)
| ~ big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_1343]) ).
cnf(c_1944,plain,
( big_p(sK4)
| big_q(sK9)
| big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1342,c_1304]) ).
cnf(c_1361,plain,
( big_q(sK9)
| big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1944]) ).
cnf(c_1945,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1361,c_534]) ).
cnf(c_1362,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1945]) ).
cnf(c_1363,plain,
( ~ big_p(A)
| big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_1362]) ).
cnf(c_1946,plain,
( big_p(sK4)
| big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1363,c_1304]) ).
cnf(c_1364,plain,
( big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1946]) ).
cnf(c_1947,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1364,c_535]) ).
cnf(c_1365,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1947]) ).
cnf(c_1948,plain,
( big_p(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1365,c_1304]) ).
cnf(c_1378,plain,
( big_q(sK9)
| big_p(sK8)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1948]) ).
cnf(c_1949,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1378,c_534]) ).
cnf(c_1379,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1949]) ).
cnf(c_1950,plain,
( big_p(sK4)
| big_q(A)
| big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1379,c_1304]) ).
cnf(c_1380,plain,
( big_q(A)
| big_p(sK8)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1950]) ).
cnf(c_1951,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1380,c_530]) ).
cnf(c_1383,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1951]) ).
cnf(c_1952,plain,
( big_p(sK8)
| big_p(sK4)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1383,c_1380]) ).
cnf(c_1953,plain,
( big_p(sK8)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1952]) ).
cnf(c_1392,plain,
( ~ big_p(A)
| big_p(sK8)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1953]) ).
cnf(c_1954,plain,
( big_p(sK4)
| big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1392,c_1304]) ).
cnf(c_1393,plain,
( big_p(sK8)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1954]) ).
cnf(c_1955,plain,
( big_q(sK9)
| big_q(sK5)
| big_p(sK4)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1393,c_1352]) ).
cnf(c_1394,plain,
( big_q(sK9)
| big_q(sK5)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1955]) ).
cnf(c_1410,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1394,c_532]) ).
cnf(c_1415,plain,
( big_q(A)
| ~ big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_1410]) ).
cnf(c_1423,plain,
( ~ big_p(sK8)
| big_q(sK5)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_1415]) ).
cnf(c_1956,plain,
( big_p(sK4)
| big_q(sK5)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1423,c_1393]) ).
cnf(c_1426,plain,
( big_q(sK5)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1956]) ).
cnf(c_1427,plain,
( big_q(sK9)
| big_p(A)
| ~ big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1426,c_533]) ).
cnf(c_1437,plain,
( big_q(sK9)
| ~ big_p(sK8)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_1427]) ).
cnf(c_1957,plain,
( big_p(sK4)
| big_q(sK9)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1437,c_1393]) ).
cnf(c_1444,plain,
( big_q(sK9)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1957]) ).
cnf(c_1445,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK8)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1444,c_532]) ).
cnf(c_1450,plain,
( big_q(A)
| ~ big_p(sK8)
| big_p(sK4) ),
inference(factor,[status(thm)],[c_1445]) ).
cnf(c_1958,plain,
( big_p(sK4)
| big_q(A)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1450,c_1393]) ).
cnf(c_1455,plain,
( big_q(A)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1958]) ).
cnf(c_1959,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1455,c_530]) ).
cnf(c_1458,plain,
( ~ big_q(sK7)
| ~ big_p(A)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1959]) ).
cnf(c_1960,plain,
( big_p(sK4)
| ~ big_p(A)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1458,c_1455]) ).
cnf(c_1465,plain,
( ~ big_p(A)
| big_p(sK4) ),
inference(copy,[status(thm)],[c_1960]) ).
cnf(c_1961,plain,
( big_p(sK4)
| big_p(sK4) ),
inference(resolve,[status(thm)],[c_1465,c_1393]) ).
cnf(c_1466,plain,
big_p(sK4),
inference(copy,[status(thm)],[c_1961]) ).
cnf(c_1473,plain,
( ~ big_q(sK6(sK7))
| ~ big_q(sK7)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1466,c_526]) ).
cnf(c_1475,plain,
( big_q(sK6(sK5))
| big_q(sK5)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1466,c_524]) ).
cnf(c_1665,plain,
( big_q(sK9)
| ~ big_p(B)
| big_p(sK8)
| big_q(sK5)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1475,c_535]) ).
cnf(c_1666,plain,
( big_q(sK9)
| big_p(B)
| ~ big_p(sK8)
| big_q(sK5)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1475,c_533]) ).
cnf(c_1677,plain,
( big_q(sK9)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_1665]) ).
cnf(c_1678,plain,
( big_q(sK9)
| ~ big_p(sK8)
| big_q(sK5)
| big_p(A) ),
inference(factor,[status(thm)],[c_1666]) ).
cnf(c_1719,plain,
( big_q(sK9)
| big_q(sK5)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1677,c_1466]) ).
cnf(c_1962,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK5)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1719,c_534]) ).
cnf(c_1720,plain,
( big_q(B)
| ~ big_p(A)
| big_q(sK5)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_1962]) ).
cnf(c_1721,plain,
( ~ big_p(A)
| big_q(sK5)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_1720]) ).
cnf(c_1722,plain,
( big_q(sK5)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1721,c_1466]) ).
cnf(c_1963,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1722,c_535]) ).
cnf(c_1723,plain,
( big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_1963]) ).
cnf(c_1734,plain,
( big_q(sK9)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1723,c_1466]) ).
cnf(c_1964,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1734,c_534]) ).
cnf(c_1735,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_1964]) ).
cnf(c_1736,plain,
( big_q(A)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1735,c_1466]) ).
cnf(c_1738,plain,
( ~ big_q(sK7)
| big_p(A)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1736,c_1473]) ).
cnf(c_1746,plain,
( ~ big_q(sK7)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_1738]) ).
cnf(c_1965,plain,
( big_p(sK8)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_1746,c_1736]) ).
cnf(c_1749,plain,
big_p(sK8),
inference(copy,[status(thm)],[c_1965]) ).
cnf(c_1757,plain,
( big_q(sK9)
| big_q(sK5)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1749,c_1678]) ).
cnf(c_1758,plain,
( big_q(sK9)
| ~ big_q(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1749,c_533]) ).
cnf(c_1759,plain,
( big_q(B)
| ~ big_q(sK9)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1749,c_532]) ).
cnf(c_1764,plain,
( big_q(sK5)
| big_p(C)
| big_q(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1759,c_1757]) ).
cnf(c_1766,plain,
( big_q(sK5)
| big_q(B)
| big_p(A) ),
inference(factor,[status(thm)],[c_1764]) ).
cnf(c_1769,plain,
( big_q(sK5)
| big_p(A) ),
inference(factor,[status(thm)],[c_1766]) ).
cnf(c_1782,plain,
( big_q(sK9)
| big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1769,c_1758]) ).
cnf(c_1788,plain,
( big_q(sK9)
| big_p(A) ),
inference(factor,[status(thm)],[c_1782]) ).
cnf(c_1793,plain,
( big_q(C)
| big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1788,c_1759]) ).
cnf(c_1794,plain,
( big_q(B)
| big_p(A) ),
inference(factor,[status(thm)],[c_1793]) ).
cnf(c_1796,plain,
( ~ big_q(sK7)
| big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1794,c_1473]) ).
cnf(c_1804,plain,
( ~ big_q(sK7)
| big_p(A) ),
inference(factor,[status(thm)],[c_1796]) ).
cnf(c_1809,plain,
( big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_1804,c_1794]) ).
cnf(c_1810,plain,
big_p(A),
inference(factor,[status(thm)],[c_1809]) ).
cnf(c_1966,plain,
( big_q(sK12(sK11))
| big_q(sK11)
| ~ big_p(sK10(sK15)) ),
inference(resolve,[status(thm)],[c_1810,c_538]) ).
cnf(c_1812,plain,
( big_q(sK12(sK11))
| big_q(sK11) ),
inference(resolve,[status(thm)],[c_1810,c_1966]) ).
cnf(c_1967,plain,
( big_q(sK1)
| ~ big_q(A)
| ~ big_p(sK0(sK3)) ),
inference(resolve,[status(thm)],[c_1810,c_523]) ).
cnf(c_1813,plain,
( big_q(sK1)
| ~ big_q(A) ),
inference(resolve,[status(thm)],[c_1810,c_1967]) ).
cnf(c_1968,plain,
( big_q(A)
| ~ big_q(sK1)
| ~ big_p(sK0(sK3)) ),
inference(resolve,[status(thm)],[c_1810,c_522]) ).
cnf(c_1814,plain,
( big_q(A)
| ~ big_q(sK1) ),
inference(resolve,[status(thm)],[c_1810,c_1968]) ).
cnf(c_1969,plain,
( ~ big_q(sK12(A))
| ~ big_q(A)
| ~ big_q(sK14)
| ~ big_p(sK10(sK15)) ),
inference(resolve,[status(thm)],[c_1810,c_518]) ).
cnf(c_1815,plain,
( ~ big_q(sK12(A))
| ~ big_q(A)
| ~ big_q(sK14) ),
inference(resolve,[status(thm)],[c_1810,c_1969]) ).
cnf(c_1819,plain,
( big_q(sK1)
| big_q(sK11) ),
inference(resolve,[status(thm)],[c_1812,c_1813]) ).
cnf(c_1970,plain,
( big_q(sK1)
| big_q(sK1) ),
inference(resolve,[status(thm)],[c_1819,c_1813]) ).
cnf(c_1820,plain,
big_q(sK1),
inference(copy,[status(thm)],[c_1970]) ).
cnf(c_1821,plain,
big_q(A),
inference(resolve,[status(thm)],[c_1820,c_1814]) ).
cnf(c_1971,plain,
( ~ big_q(sK12(A))
| ~ big_q(A) ),
inference(resolve,[status(thm)],[c_1821,c_1815]) ).
cnf(c_1972,plain,
~ big_q(sK12(A)),
inference(resolve,[status(thm)],[c_1821,c_1971]) ).
cnf(c_1822,plain,
$false,
inference(resolve,[status(thm)],[c_1821,c_1972]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN036+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/15.42 % Computer : n002.cluster.edu
% 0.14/15.42 % Model : x86_64 x86_64
% 0.14/15.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/15.42 % Memory : 8046.5625MB
% 0.14/15.42 % OS : Linux 6.8.0-71-generic
% 0.14/15.42 % CPULimit : 300
% 0.14/15.42 % WCLimit : 300
% 0.14/15.42 % DateTime : Sat Sep 26 17:07:52 UTC 2026
% 0.14/15.43 % CPUTime :
% 0.14/15.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/15.43 % Process 2267756 was started by sandbox on n002,
% 0.14/15.43 % Sat Sep 26 17:07:52 2026
% 0.14/15.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/15.52
% 0.19/15.52 % From the command line: assign(max_seconds, 300).
% 0.19/15.81
% 0.19/15.81 % SZS status Theorem for theBenchmark
% 0.19/15.81
% 0.19/15.81 % Proof 1 at 0.18 (+ 0.07) seconds.
% 0.19/15.81 % Length of proof is 231.
% 0.19/15.81 % Level of proof is 124.
% 0.19/15.81 % Maximum clause weight is 30.000.
% 0.19/15.81 % Given clauses 311.
% 0.19/15.81
% 0.19/15.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------