%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN036+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:37 AM UTC 2026
% Result : Theorem 2.96s 0.80s
% Output : CNFRefutation 2.96s
% 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_p(W) ) )
<=> ( ? [X1] :
! [Y1] :
( big_q(X1)
<=> big_q(Y1) )
<=> ( ? [U1] : big_p(U1)
<=> ! [W1] : big_q(W1) ) ) ),
file('theBenchmark.p',pel34) ).
fof(pel34_neg,negated_conjecture,
~ ( ( ? [X] :
! [Y] :
( big_p(X)
<=> big_p(Y) )
<=> ( ? [U] : big_q(U)
<=> ! [W] : big_p(W) ) )
<=> ( ? [X1] :
! [Y1] :
( big_q(X1)
<=> big_q(Y1) )
<=> ( ? [U1] : big_p(U1)
<=> ! [W1] : big_q(W1) ) ) ),
inference(assume_negation,[status(cth)],[pel34]) ).
fof(nnf_1,plain,
( ( ( ( ( ( ? [W1] : ~ big_q(W1)
| ! [U1] : ~ big_p(U1) )
& ( ! [X40] : big_q(X40)
| ? [X39] : big_p(X39) ) )
| ! [X1] :
? [Y1] :
( ( ~ big_q(Y1)
| ~ big_q(X1) )
& ( big_q(Y1)
| big_q(X1) ) ) )
& ( ( ( ? [X38] : ~ big_q(X38)
| ? [X37] : big_p(X37) )
& ( ! [X36] : big_q(X36)
| ! [X35] : ~ big_p(X35) ) )
| ? [X33] :
! [X34] :
( ( ~ big_q(X34)
| big_q(X33) )
& ( big_q(X34)
| ~ big_q(X33) ) ) ) )
| ( ( ( ( ? [W] : ~ big_p(W)
| ! [U] : ~ big_q(U) )
& ( ! [X32] : big_p(X32)
| ? [X31] : big_q(X31) ) )
| ! [X] :
? [Y] :
( ( ~ big_p(Y)
| ~ big_p(X) )
& ( big_p(Y)
| big_p(X) ) ) )
& ( ( ( ? [X30] : ~ big_p(X30)
| ? [X29] : big_q(X29) )
& ( ! [X28] : big_p(X28)
| ! [X27] : ~ big_q(X27) ) )
| ? [X25] :
! [X26] :
( ( ~ big_p(X26)
| big_p(X25) )
& ( big_p(X26)
| ~ big_p(X25) ) ) ) ) )
& ( ( ( ( ( ? [X24] : ~ big_q(X24)
| ! [X23] : ~ big_p(X23) )
& ( ! [X22] : big_q(X22)
| ? [X21] : big_p(X21) ) )
| ? [X19] :
! [X20] :
( ( ~ big_q(X20)
| big_q(X19) )
& ( big_q(X20)
| ~ big_q(X19) ) ) )
& ( ( ( ? [X18] : ~ big_q(X18)
| ? [X17] : big_p(X17) )
& ( ! [X16] : big_q(X16)
| ! [X15] : ~ big_p(X15) ) )
| ! [X13] :
? [X14] :
( ( ~ big_q(X14)
| ~ big_q(X13) )
& ( big_q(X14)
| big_q(X13) ) ) ) )
| ( ( ( ( ? [X12] : ~ big_p(X12)
| ! [X11] : ~ big_q(X11) )
& ( ! [X10] : big_p(X10)
| ? [X9] : big_q(X9) ) )
| ? [X7] :
! [X8] :
( ( ~ big_p(X8)
| big_p(X7) )
& ( big_p(X8)
| ~ big_p(X7) ) ) )
& ( ( ( ? [X6] : ~ big_p(X6)
| ? [X5] : big_q(X5) )
& ( ! [X4] : big_p(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_q(sK13)
| ! [U1] : ~ big_p(U1) )
& ( ! [X40] : big_q(X40)
| big_p(sK16) ) )
| ! [X1] :
( ( ~ big_q(sK12(X1))
| ~ big_q(X1) )
& ( big_q(sK12(X1))
| big_q(X1) ) ) )
& ( ( ( ~ big_q(sK23)
| big_p(sK22) )
& ( ! [X36] : big_q(X36)
| ! [X35] : ~ big_p(X35) ) )
| ! [X34] :
( ( ~ big_q(X34)
| big_q(sK11) )
& ( big_q(X34)
| ~ big_q(sK11) ) ) ) )
| ( ( ( ( ~ big_p(sK17)
| ! [U] : ~ big_q(U) )
& ( ! [X32] : big_p(X32)
| big_q(sK15) ) )
| ! [X] :
( ( ~ big_p(sK14(X))
| ~ big_p(X) )
& ( big_p(sK14(X))
| big_p(X) ) ) )
& ( ( ( ~ big_p(sK21)
| big_q(sK20) )
& ( ! [X28] : big_p(X28)
| ! [X27] : ~ big_q(X27) ) )
| ! [X26] :
( ( ~ big_p(X26)
| big_p(sK10) )
& ( big_p(X26)
| ~ big_p(sK10) ) ) ) ) )
& ( ( ( ( ( ~ big_q(sK19)
| ! [X23] : ~ big_p(X23) )
& ( ! [X22] : big_q(X22)
| big_p(sK5) ) )
| ! [X20] :
( ( ~ big_q(X20)
| big_q(sK4) )
& ( big_q(X20)
| ~ big_q(sK4) ) ) )
& ( ( ( ~ big_q(sK3)
| big_p(sK2) )
& ( ! [X16] : big_q(X16)
| ! [X15] : ~ big_p(X15) ) )
| ! [X13] :
( ( ~ big_q(sK1(X13))
| ~ big_q(X13) )
& ( big_q(sK1(X13))
| big_q(X13) ) ) ) )
| ( ( ( ( ~ big_p(sK18)
| ! [X11] : ~ big_q(X11) )
& ( ! [X10] : big_p(X10)
| big_q(sK9) ) )
| ! [X8] :
( ( ~ big_p(X8)
| big_p(sK8) )
& ( big_p(X8)
| ~ big_p(sK8) ) ) )
& ( ( ( ~ big_p(sK7)
| big_q(sK6) )
& ( ! [X4] : big_p(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,sK6,sK7,sK8,sK9,sK18,sK1,sK2,sK3,sK4,sK5,sK19,sK10,sK20,sK21,sK14,sK15,sK17,sK11,sK22,sK23,sK12,sK16,sK13]),skolemize(X2,sK0(X0)),skolemize(X5,sK6),skolemize(X6,sK7),skolemize(X7,sK8),skolemize(X9,sK9),skolemize(X12,sK18),skolemize(X14,sK1(X13)),skolemize(X17,sK2),skolemize(X18,sK3),skolemize(X19,sK4),skolemize(X21,sK5),skolemize(X24,sK19),skolemize(X25,sK10),skolemize(X29,sK20),skolemize(X30,sK21),skolemize(Y,sK14(X)),skolemize(X31,sK15),skolemize(W,sK17),skolemize(X33,sK11),skolemize(X37,sK22),skolemize(X38,sK23),skolemize(Y1,sK12(X1)),skolemize(X39,sK16),skolemize(W1,sK13)],[nnf_1]) ).
fof(sk_pel34_neg,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK13)
| ~ big_p(VAR_3)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK16)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK13)
| ~ big_p(VAR_3)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK16)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK23)
| big_p(sK22)
| ~ big_q(VAR_2)
| big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK23)
| big_p(sK22)
| big_q(VAR_2)
| ~ big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK13)
| ~ big_p(VAR_3)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK15)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK16)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK15)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK13)
| ~ big_p(VAR_3)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK15)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK16)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK15)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK23)
| big_p(sK22)
| ~ big_q(VAR_2)
| big_q(sK11)
| big_p(VAR_1)
| big_q(sK15)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK11)
| big_p(VAR_1)
| big_q(sK15)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK23)
| big_p(sK22)
| big_q(VAR_2)
| ~ big_q(sK11)
| big_p(VAR_1)
| big_q(sK15)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK11)
| big_p(VAR_1)
| big_q(sK15)
| ~ big_p(sK14(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK13)
| ~ big_p(VAR_3)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK16)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK13)
| ~ big_p(VAR_3)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK16)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK23)
| big_p(sK22)
| ~ big_q(VAR_2)
| big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK23)
| big_p(sK22)
| big_q(VAR_2)
| ~ big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(VAR_1)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK13)
| ~ big_p(VAR_3)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK15)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK16)
| ~ big_q(sK12(VAR_2))
| ~ big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK15)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK13)
| ~ big_p(VAR_3)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK15)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK16)
| big_q(sK12(VAR_2))
| big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK15)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK23)
| big_p(sK22)
| ~ big_q(VAR_2)
| big_q(sK11)
| big_p(VAR_1)
| big_q(sK15)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK11)
| big_p(VAR_1)
| big_q(sK15)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK23)
| big_p(sK22)
| big_q(VAR_2)
| ~ big_q(sK11)
| big_p(VAR_1)
| big_q(sK15)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK11)
| big_p(VAR_1)
| big_q(sK15)
| big_p(sK14(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK13)
| ~ big_p(VAR_2)
| ~ big_q(sK12(VAR_1))
| ~ big_q(VAR_1)
| ~ big_p(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_q(VAR_2)
| big_p(sK16)
| ~ big_q(sK12(VAR_1))
| ~ big_q(VAR_1)
| ~ big_p(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK13)
| ~ big_p(VAR_2)
| big_q(sK12(VAR_1))
| big_q(VAR_1)
| ~ big_p(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_q(VAR_2)
| big_p(sK16)
| big_q(sK12(VAR_1))
| big_q(VAR_1)
| ~ big_p(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1] :
( ~ big_q(sK23)
| big_p(sK22)
| ~ big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| ~ big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1] :
( ~ big_q(sK23)
| big_p(sK22)
| big_q(VAR_1)
| ~ big_q(sK11)
| ~ big_p(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| ~ big_q(sK11)
| ~ big_p(sK21)
| big_q(sK20)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_q(sK13)
| ~ big_p(VAR_4)
| ~ big_q(sK12(VAR_3))
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| big_p(sK16)
| ~ big_q(sK12(VAR_3))
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_q(sK13)
| ~ big_p(VAR_4)
| big_q(sK12(VAR_3))
| big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| big_p(sK16)
| big_q(sK12(VAR_3))
| big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK23)
| big_p(sK22)
| ~ big_q(VAR_3)
| big_q(sK11)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_q(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| big_q(sK11)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK23)
| big_p(sK22)
| big_q(VAR_3)
| ~ big_q(sK11)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_q(VAR_5)
| ~ big_p(VAR_4)
| big_q(VAR_3)
| ~ big_q(sK11)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK13)
| ~ big_p(VAR_2)
| ~ big_q(sK12(VAR_1))
| ~ big_q(VAR_1)
| ~ big_p(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_q(VAR_2)
| big_p(sK16)
| ~ big_q(sK12(VAR_1))
| ~ big_q(VAR_1)
| ~ big_p(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK13)
| ~ big_p(VAR_2)
| big_q(sK12(VAR_1))
| big_q(VAR_1)
| ~ big_p(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_q(VAR_2)
| big_p(sK16)
| big_q(sK12(VAR_1))
| big_q(VAR_1)
| ~ big_p(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1] :
( ~ big_q(sK23)
| big_p(sK22)
| ~ big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| ~ big_q(VAR_1)
| big_q(sK11)
| ~ big_p(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1] :
( ~ big_q(sK23)
| big_p(sK22)
| big_q(VAR_1)
| ~ big_q(sK11)
| ~ big_p(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| ~ big_q(sK11)
| ~ big_p(sK21)
| big_q(sK20)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_q(sK13)
| ~ big_p(VAR_4)
| ~ big_q(sK12(VAR_3))
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| big_p(sK16)
| ~ big_q(sK12(VAR_3))
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_q(sK13)
| ~ big_p(VAR_4)
| big_q(sK12(VAR_3))
| big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| big_p(sK16)
| big_q(sK12(VAR_3))
| big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK23)
| big_p(sK22)
| ~ big_q(VAR_3)
| big_q(sK11)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_q(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| big_q(sK11)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK23)
| big_p(sK22)
| big_q(VAR_3)
| ~ big_q(sK11)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( big_q(VAR_5)
| ~ big_p(VAR_4)
| big_q(VAR_3)
| ~ big_q(sK11)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK10) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK19)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK4)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK5)
| ~ big_q(VAR_2)
| big_q(sK4)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK19)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK4)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK5)
| big_q(VAR_2)
| ~ big_q(sK4)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(VAR_2))
| ~ big_q(VAR_2)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(sK1(VAR_2))
| ~ big_q(VAR_2)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK3)
| big_p(sK2)
| big_q(sK1(VAR_2))
| big_q(VAR_2)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(sK1(VAR_2))
| big_q(VAR_2)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK19)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK4)
| big_p(VAR_1)
| big_q(sK9)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK5)
| ~ big_q(VAR_2)
| big_q(sK4)
| big_p(VAR_1)
| big_q(sK9)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK19)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK4)
| big_p(VAR_1)
| big_q(sK9)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK5)
| big_q(VAR_2)
| ~ big_q(sK4)
| big_p(VAR_1)
| big_q(sK9)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(VAR_2))
| ~ big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK9)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(sK1(VAR_2))
| ~ big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK9)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK3)
| big_p(sK2)
| big_q(sK1(VAR_2))
| big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK9)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(sK1(VAR_2))
| big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK9)
| ~ big_p(VAR_0)
| big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK19)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK4)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK5)
| ~ big_q(VAR_2)
| big_q(sK4)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK19)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK4)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK5)
| big_q(VAR_2)
| ~ big_q(sK4)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(VAR_2))
| ~ big_q(VAR_2)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(sK1(VAR_2))
| ~ big_q(VAR_2)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK3)
| big_p(sK2)
| big_q(sK1(VAR_2))
| big_q(VAR_2)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(sK1(VAR_2))
| big_q(VAR_2)
| ~ big_p(sK18)
| ~ big_q(VAR_1)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK19)
| ~ big_p(VAR_3)
| ~ big_q(VAR_2)
| big_q(sK4)
| big_p(VAR_1)
| big_q(sK9)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK5)
| ~ big_q(VAR_2)
| big_q(sK4)
| big_p(VAR_1)
| big_q(sK9)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK19)
| ~ big_p(VAR_3)
| big_q(VAR_2)
| ~ big_q(sK4)
| big_p(VAR_1)
| big_q(sK9)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| big_p(sK5)
| big_q(VAR_2)
| ~ big_q(sK4)
| big_p(VAR_1)
| big_q(sK9)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(VAR_2))
| ~ big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK9)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| ~ big_q(sK1(VAR_2))
| ~ big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK9)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK3)
| big_p(sK2)
| big_q(sK1(VAR_2))
| big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK9)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( big_q(VAR_4)
| ~ big_p(VAR_3)
| big_q(sK1(VAR_2))
| big_q(VAR_2)
| big_p(VAR_1)
| big_q(sK9)
| big_p(VAR_0)
| ~ big_p(sK8) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK19)
| ~ big_p(VAR_2)
| ~ big_q(VAR_1)
| big_q(sK4)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_q(VAR_2)
| big_p(sK5)
| ~ big_q(VAR_1)
| big_q(sK4)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK19)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| ~ big_q(sK4)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_q(VAR_2)
| big_p(sK5)
| big_q(VAR_1)
| ~ big_q(sK4)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(VAR_1))
| ~ big_q(VAR_1)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| ~ big_q(sK1(VAR_1))
| ~ big_q(VAR_1)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ big_q(sK3)
| big_p(sK2)
| big_q(sK1(VAR_1))
| big_q(VAR_1)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| big_q(sK1(VAR_1))
| big_q(VAR_1)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_q(sK19)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| big_q(sK4)
| big_p(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_q(VAR_4)
| big_p(sK5)
| ~ big_q(VAR_3)
| big_q(sK4)
| big_p(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_q(sK19)
| ~ big_p(VAR_4)
| big_q(VAR_3)
| ~ big_q(sK4)
| big_p(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_q(VAR_4)
| big_p(sK5)
| big_q(VAR_3)
| ~ big_q(sK4)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(VAR_3))
| ~ big_q(VAR_3)
| big_p(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_q(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(sK1(VAR_3))
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK3)
| big_p(sK2)
| big_q(sK1(VAR_3))
| big_q(VAR_3)
| big_p(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_q(VAR_5)
| ~ big_p(VAR_4)
| big_q(sK1(VAR_3))
| big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| ~ big_p(sK0(VAR_0))
| ~ big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK19)
| ~ big_p(VAR_2)
| ~ big_q(VAR_1)
| big_q(sK4)
| ~ big_p(sK7)
| big_q(sK6)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_q(VAR_2)
| big_p(sK5)
| ~ big_q(VAR_1)
| big_q(sK4)
| ~ big_p(sK7)
| big_q(sK6)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ big_q(sK19)
| ~ big_p(VAR_2)
| big_q(VAR_1)
| ~ big_q(sK4)
| ~ big_p(sK7)
| big_q(sK6)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( big_q(VAR_2)
| big_p(sK5)
| big_q(VAR_1)
| ~ big_q(sK4)
| ~ big_p(sK7)
| big_q(sK6)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(VAR_1))
| ~ big_q(VAR_1)
| ~ big_p(sK7)
| big_q(sK6)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| ~ big_q(sK1(VAR_1))
| ~ big_q(VAR_1)
| ~ big_p(sK7)
| big_q(sK6)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ big_q(sK3)
| big_p(sK2)
| big_q(sK1(VAR_1))
| big_q(VAR_1)
| ~ big_p(sK7)
| big_q(sK6)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( big_q(VAR_3)
| ~ big_p(VAR_2)
| big_q(sK1(VAR_1))
| big_q(VAR_1)
| ~ big_p(sK7)
| big_q(sK6)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ big_q(sK19)
| ~ big_p(VAR_4)
| ~ big_q(VAR_3)
| big_q(sK4)
| big_p(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_q(VAR_4)
| big_p(sK5)
| ~ big_q(VAR_3)
| big_q(sK4)
| big_p(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_q(sK19)
| ~ big_p(VAR_4)
| big_q(VAR_3)
| ~ big_q(sK4)
| big_p(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_q(VAR_4)
| big_p(sK5)
| big_q(VAR_3)
| ~ big_q(sK4)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(VAR_3))
| ~ big_q(VAR_3)
| big_p(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_q(VAR_5)
| ~ big_p(VAR_4)
| ~ big_q(sK1(VAR_3))
| ~ big_q(VAR_3)
| big_p(VAR_2)
| ~ big_q(VAR_1)
| big_p(sK0(VAR_0))
| big_p(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ big_q(sK3)
| big_p(sK2)
| big_q(sK1(VAR_3))
| big_q(VAR_3)
| big_p(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_q(VAR_5)
| ~ big_p(VAR_4)
| big_q(sK1(VAR_3))
| big_q(VAR_3)
| big_p(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_5,negated_conjecture,
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(D))
| ~ big_q(D)
| big_p(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_q(E)
| big_p(sK5)
| big_q(D)
| ~ big_q(sK4)
| big_p(C)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_8,negated_conjecture,
( big_q(E)
| big_p(sK5)
| ~ big_q(D)
| big_q(sK4)
| big_p(C)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_24,negated_conjecture,
( big_q(D)
| ~ big_p(C)
| big_q(sK1(B))
| big_q(B)
| ~ big_p(sK7)
| big_q(sK6)
| ~ big_p(sK0(A))
| ~ big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_30,negated_conjecture,
( big_q(E)
| ~ big_p(D)
| big_q(sK1(C))
| big_q(C)
| big_p(B)
| big_q(sK9)
| big_p(A)
| ~ big_p(sK8) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_46,negated_conjecture,
( big_q(E)
| ~ big_p(D)
| big_q(sK1(C))
| big_q(C)
| big_p(B)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_50,negated_conjecture,
( big_q(D)
| big_p(sK5)
| big_q(C)
| ~ big_q(sK4)
| big_p(B)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_52,negated_conjecture,
( big_q(D)
| big_p(sK5)
| ~ big_q(C)
| big_q(sK4)
| big_p(B)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_62,negated_conjecture,
( big_q(F)
| ~ big_p(E)
| big_q(D)
| ~ big_q(sK11)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_64,negated_conjecture,
( big_q(F)
| ~ big_p(E)
| ~ big_q(D)
| big_q(sK11)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_69,negated_conjecture,
( ~ big_q(sK13)
| ~ big_p(E)
| ~ big_q(sK12(D))
| ~ big_q(D)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_76,negated_conjecture,
( big_q(F)
| ~ big_p(E)
| big_q(D)
| ~ big_q(sK11)
| big_p(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_78,negated_conjecture,
( big_q(F)
| ~ big_p(E)
| ~ big_q(D)
| big_q(sK11)
| big_p(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_83,negated_conjecture,
( ~ big_q(sK13)
| ~ big_p(E)
| ~ big_q(sK12(D))
| ~ big_q(D)
| big_p(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_94,negated_conjecture,
( big_q(D)
| big_p(sK16)
| big_q(sK12(C))
| big_q(C)
| big_p(B)
| big_q(sK15)
| big_p(sK14(A))
| big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_114,negated_conjecture,
( big_q(E)
| ~ big_p(D)
| big_q(C)
| ~ big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(B)
| ~ big_p(sK14(A))
| ~ big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_116,negated_conjecture,
( big_q(E)
| ~ big_p(D)
| ~ big_q(C)
| big_q(sK11)
| ~ big_p(sK17)
| ~ big_q(B)
| ~ big_p(sK14(A))
| ~ big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_121,negated_conjecture,
( ~ big_q(sK13)
| ~ big_p(D)
| ~ big_q(sK12(C))
| ~ big_q(C)
| ~ big_p(sK17)
| ~ big_q(B)
| ~ big_p(sK14(A))
| ~ big_p(A) ),
inference(split_conjunct,[status(thm)],[sk_pel34_neg]) ).
cnf(c_128,plain,
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(C))
| ~ big_q(C)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_5]) ).
cnf(c_130,plain,
( big_q(D)
| big_p(sK5)
| big_q(C)
| ~ big_q(sK4)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_6]) ).
cnf(c_135,plain,
( big_q(D)
| big_p(sK5)
| ~ big_q(C)
| big_q(sK4)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_8]) ).
cnf(c_171,plain,
( big_q(C)
| ~ big_p(B)
| big_q(sK1(A))
| big_q(A)
| big_q(sK6)
| ~ big_p(sK0(sK7))
| ~ big_p(sK7) ),
inference(factor,[status(thm)],[c_24]) ).
cnf(c_188,plain,
( big_q(D)
| big_q(sK1(C))
| big_q(C)
| big_p(B)
| big_q(sK9)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_30]) ).
cnf(c_227,plain,
( big_q(D)
| ~ big_p(C)
| big_q(sK1(B))
| big_q(B)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_46]) ).
cnf(c_238,plain,
( big_q(C)
| big_p(sK5)
| big_q(B)
| ~ big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_50]) ).
cnf(c_243,plain,
( big_q(C)
| big_p(sK5)
| ~ big_q(B)
| big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_52]) ).
cnf(c_266,plain,
( big_q(E)
| big_q(D)
| ~ big_q(sK11)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_62]) ).
cnf(c_272,plain,
( big_q(E)
| ~ big_q(D)
| big_q(sK11)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_64]) ).
cnf(c_285,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(D))
| ~ big_q(D)
| big_p(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_69]) ).
cnf(c_301,plain,
( big_q(E)
| ~ big_p(D)
| big_q(C)
| ~ big_q(sK11)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_76]) ).
cnf(c_307,plain,
( big_q(E)
| ~ big_p(D)
| ~ big_q(C)
| big_q(sK11)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_78]) ).
cnf(c_320,plain,
( ~ big_q(sK13)
| ~ big_p(D)
| ~ big_q(sK12(C))
| ~ big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_83]) ).
cnf(c_344,plain,
( big_q(C)
| big_p(sK16)
| big_q(sK12(B))
| big_q(B)
| big_q(sK15)
| big_p(sK14(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_94]) ).
cnf(c_388,plain,
( big_q(D)
| ~ big_p(C)
| big_q(B)
| ~ big_q(sK11)
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_114]) ).
cnf(c_394,plain,
( big_q(D)
| ~ big_p(C)
| ~ big_q(B)
| big_q(sK11)
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_116]) ).
cnf(c_407,plain,
( ~ big_q(sK13)
| ~ big_p(C)
| ~ big_q(sK12(B))
| ~ big_q(B)
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_121]) ).
cnf(c_415,plain,
( ~ big_q(sK3)
| big_p(sK2)
| ~ big_q(sK1(B))
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_128]) ).
cnf(c_417,plain,
( big_q(C)
| big_q(B)
| ~ big_q(sK4)
| ~ big_q(A)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_130]) ).
cnf(c_418,plain,
( big_q(C)
| big_p(sK5)
| big_q(B)
| ~ big_q(sK4)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_130]) ).
cnf(c_422,plain,
( big_q(C)
| ~ big_q(B)
| big_q(sK4)
| ~ big_q(A)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_135]) ).
cnf(c_423,plain,
( big_q(C)
| big_p(sK5)
| big_q(sK4)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_135]) ).
cnf(c_448,plain,
( big_q(B)
| big_q(sK1(A))
| big_q(A)
| big_q(sK6)
| ~ big_p(sK0(sK7))
| ~ big_p(sK7) ),
inference(factor,[status(thm)],[c_171]) ).
cnf(c_464,plain,
( big_q(C)
| big_q(sK1(B))
| big_q(B)
| big_q(sK9)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_188]) ).
cnf(c_500,plain,
( big_q(C)
| big_q(sK1(B))
| big_q(B)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_227]) ).
cnf(c_510,plain,
( big_q(B)
| big_p(sK5)
| ~ big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_238]) ).
cnf(c_515,plain,
( big_p(sK5)
| ~ big_q(B)
| big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_243]) ).
cnf(c_537,plain,
( big_q(D)
| big_q(C)
| ~ big_q(sK11)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_266]) ).
cnf(c_544,plain,
( big_q(D)
| ~ big_q(C)
| big_q(sK11)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_272]) ).
cnf(c_559,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(C))
| ~ big_q(C)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_285]) ).
cnf(c_569,plain,
( big_q(D)
| big_q(C)
| ~ big_q(sK11)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_301]) ).
cnf(c_575,plain,
( big_q(D)
| ~ big_q(C)
| big_q(sK11)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_307]) ).
cnf(c_587,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(C))
| ~ big_q(C)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_320]) ).
cnf(c_609,plain,
( big_p(sK16)
| big_q(sK12(B))
| big_q(B)
| big_q(sK15)
| big_p(sK14(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_344]) ).
cnf(c_637,plain,
( big_q(C)
| big_q(B)
| ~ big_q(sK11)
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_388]) ).
cnf(c_644,plain,
( big_q(C)
| ~ big_q(B)
| big_q(sK11)
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_394]) ).
cnf(c_657,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(B))
| ~ big_q(B)
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_407]) ).
cnf(c_663,plain,
( big_p(sK2)
| ~ big_q(sK1(sK3))
| ~ big_q(sK3)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_415]) ).
cnf(c_664,plain,
( big_q(B)
| big_q(A)
| ~ big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_417]) ).
cnf(c_666,plain,
( big_p(sK5)
| big_q(B)
| ~ big_q(sK4)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_418]) ).
cnf(c_667,plain,
( big_q(B)
| big_q(sK4)
| ~ big_q(A)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_422]) ).
cnf(c_669,plain,
( big_p(sK5)
| big_q(sK4)
| ~ big_q(B)
| big_p(sK0(A))
| big_p(A) ),
inference(factor,[status(thm)],[c_423]) ).
cnf(c_677,plain,
( big_q(A)
| big_q(sK1(sK6))
| big_q(sK6)
| ~ big_p(sK0(sK7))
| ~ big_p(sK7) ),
inference(factor,[status(thm)],[c_448]) ).
cnf(c_684,plain,
( big_q(B)
| big_q(sK1(sK9))
| big_q(sK9)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_464]) ).
cnf(c_699,plain,
( big_q(B)
| big_q(sK1(sK9))
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_500]) ).
cnf(c_704,plain,
( big_p(sK5)
| ~ big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_510]) ).
cnf(c_715,plain,
( big_q(C)
| big_q(B)
| ~ big_q(sK11)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_537]) ).
cnf(c_719,plain,
( big_q(C)
| big_q(sK11)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_544]) ).
cnf(c_726,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(B))
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_559]) ).
cnf(c_730,plain,
( big_q(C)
| big_q(B)
| ~ big_q(sK11)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_569]) ).
cnf(c_734,plain,
( big_q(C)
| big_q(sK11)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_575]) ).
cnf(c_739,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(B))
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_587]) ).
cnf(c_756,plain,
( big_q(B)
| big_q(A)
| ~ big_q(sK11)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_637]) ).
cnf(c_760,plain,
( big_q(B)
| big_q(sK11)
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_644]) ).
cnf(c_766,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(A))
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_657]) ).
cnf(c_770,plain,
( big_q(A)
| ~ big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_664]) ).
cnf(c_771,plain,
( big_q(sK4)
| ~ big_q(A)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_667]) ).
cnf(c_772,plain,
( big_q(sK1(sK6))
| big_q(sK6)
| ~ big_p(sK0(sK7))
| ~ big_p(sK7) ),
inference(factor,[status(thm)],[c_677]) ).
cnf(c_773,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(A)
| ~ big_p(sK8) ),
inference(factor,[status(thm)],[c_684]) ).
cnf(c_775,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_699]) ).
cnf(c_777,plain,
( big_q(B)
| ~ big_q(sK11)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_715]) ).
cnf(c_778,plain,
( big_q(sK11)
| ~ big_q(B)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_719]) ).
cnf(c_779,plain,
( ~ big_q(sK12(sK13))
| ~ big_q(sK13)
| big_p(A)
| ~ big_p(sK10) ),
inference(factor,[status(thm)],[c_726]) ).
cnf(c_780,plain,
( big_q(B)
| ~ big_q(sK11)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_730]) ).
cnf(c_781,plain,
( big_q(sK11)
| ~ big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_734]) ).
cnf(c_782,plain,
( ~ big_q(sK12(sK13))
| ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_739]) ).
cnf(c_784,plain,
( big_q(A)
| ~ big_q(sK11)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_756]) ).
cnf(c_785,plain,
( big_q(sK11)
| ~ big_q(A)
| ~ big_p(sK14(sK17))
| ~ big_p(sK17) ),
inference(factor,[status(thm)],[c_760]) ).
cnf(c_854,plain,
( big_p(sK16)
| big_q(C)
| big_q(sK15)
| big_p(sK14(B))
| big_p(B)
| big_p(sK5)
| big_q(sK4)
| big_p(sK0(A))
| big_p(A) ),
inference(resolve,[status(thm)],[c_669,c_609]) ).
cnf(c_855,plain,
( big_p(sK16)
| big_q(B)
| big_q(sK15)
| big_p(sK14(A))
| big_p(A)
| big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_854]) ).
cnf(c_863,plain,
( big_p(sK16)
| big_q(A)
| big_q(sK15)
| big_p(sK14(sK5))
| big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_855]) ).
cnf(c_878,plain,
( big_p(sK16)
| big_q(sK15)
| big_p(sK14(sK5))
| big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_863]) ).
cnf(c_3394,plain,
( big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5)
| big_p(sK16)
| big_p(sK14(sK5))
| big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_878,c_771]) ).
cnf(c_3395,plain,
( big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK16)
| big_p(sK14(sK5))
| big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3394]) ).
cnf(c_3396,plain,
( big_q(sK4)
| big_p(sK16)
| big_p(sK14(sK5))
| big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3395]) ).
cnf(c_927,plain,
( big_p(sK16)
| big_p(sK14(sK5))
| big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3396]) ).
cnf(c_3397,plain,
( big_q(A)
| big_p(sK0(sK5))
| big_p(sK5)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_927,c_770]) ).
cnf(c_3398,plain,
( big_q(A)
| big_p(sK0(sK5))
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3397]) ).
cnf(c_932,plain,
( big_q(A)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3398]) ).
cnf(c_942,plain,
( big_p(sK2)
| ~ big_q(sK3)
| big_p(sK0(A))
| big_p(A)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_932,c_663]) ).
cnf(c_3399,plain,
( big_p(sK2)
| ~ big_q(sK3)
| big_p(sK0(sK5))
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_942]) ).
cnf(c_945,plain,
( big_p(sK2)
| ~ big_q(sK3)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3399]) ).
cnf(c_3400,plain,
( big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5)
| big_p(sK2)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_945,c_932]) ).
cnf(c_3401,plain,
( big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK2)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3400]) ).
cnf(c_3402,plain,
( big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK2)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3401]) ).
cnf(c_3403,plain,
( big_p(sK16)
| big_p(sK2)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3402]) ).
cnf(c_1082,plain,
( big_p(sK2)
| big_p(sK16)
| big_p(sK14(sK5))
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3403]) ).
cnf(c_1085,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_1082,c_775]) ).
cnf(c_3404,plain,
( big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_1085,c_771]) ).
cnf(c_3405,plain,
( big_q(sK4)
| big_p(sK0(sK5))
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3404]) ).
cnf(c_2141,plain,
( big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3405]) ).
cnf(c_3406,plain,
( big_q(A)
| big_p(sK0(sK5))
| big_p(sK5)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2141,c_770]) ).
cnf(c_3407,plain,
( big_q(A)
| big_p(sK0(sK5))
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3406]) ).
cnf(c_2162,plain,
( big_q(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3407]) ).
cnf(c_2164,plain,
( big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2162]) ).
cnf(c_3408,plain,
( big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK5)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2164,c_771]) ).
cnf(c_3409,plain,
( big_q(sK4)
| big_p(sK0(sK5))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3408]) ).
cnf(c_2185,plain,
( big_q(sK4)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3409]) ).
cnf(c_3410,plain,
( big_q(A)
| big_p(sK0(sK5))
| big_p(sK5)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2185,c_770]) ).
cnf(c_3411,plain,
( big_q(A)
| big_p(sK0(sK5))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3410]) ).
cnf(c_2199,plain,
( big_q(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3411]) ).
cnf(c_3412,plain,
( big_p(sK2)
| ~ big_q(sK3)
| big_p(sK0(A))
| big_p(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2199,c_663]) ).
cnf(c_2207,plain,
( ~ big_q(sK3)
| big_p(sK0(A))
| big_p(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3412]) ).
cnf(c_3413,plain,
( ~ big_q(sK3)
| big_p(sK0(sK5))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2207]) ).
cnf(c_2209,plain,
( ~ big_q(sK3)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3413]) ).
cnf(c_3414,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2209,c_2199]) ).
cnf(c_3415,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3414]) ).
cnf(c_3416,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3415]) ).
cnf(c_3417,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3416]) ).
cnf(c_3418,plain,
( big_p(sK8)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3417]) ).
cnf(c_2210,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK5))
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3418]) ).
cnf(c_3419,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2210,c_775]) ).
cnf(c_2216,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3419]) ).
cnf(c_3420,plain,
( big_p(sK5)
| big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2216,c_515]) ).
cnf(c_3421,plain,
( big_p(sK5)
| big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3420]) ).
cnf(c_3422,plain,
( big_p(sK5)
| big_q(sK4)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3421]) ).
cnf(c_2233,plain,
( big_q(sK4)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3422]) ).
cnf(c_3423,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5)
| big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2233,c_2210]) ).
cnf(c_3424,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3423]) ).
cnf(c_3425,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3424]) ).
cnf(c_3426,plain,
( big_p(sK8)
| big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3425]) ).
cnf(c_2247,plain,
( big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3426]) ).
cnf(c_3427,plain,
( big_p(sK5)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2247,c_704]) ).
cnf(c_3428,plain,
( big_p(sK5)
| big_q(sK9)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3427]) ).
cnf(c_3429,plain,
( big_p(sK5)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3428]) ).
cnf(c_2249,plain,
( ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3429]) ).
cnf(c_3430,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2249,c_2210]) ).
cnf(c_3431,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3430]) ).
cnf(c_3432,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3431]) ).
cnf(c_3433,plain,
( big_p(sK8)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3432]) ).
cnf(c_2264,plain,
( big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3433]) ).
cnf(c_2266,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2264,c_781]) ).
cnf(c_3434,plain,
( big_p(sK5)
| big_q(sK4)
| big_p(sK0(A))
| big_p(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2264,c_669]) ).
cnf(c_2274,plain,
( big_q(sK4)
| big_p(sK0(A))
| big_p(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3434]) ).
cnf(c_2286,plain,
( big_q(sK4)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2274]) ).
cnf(c_3435,plain,
( big_p(sK5)
| big_q(B)
| big_p(sK0(A))
| big_p(A)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2286,c_666]) ).
cnf(c_2308,plain,
( big_q(B)
| big_p(sK0(A))
| big_p(A)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3435]) ).
cnf(c_3436,plain,
( big_q(A)
| big_p(sK0(sK8))
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2308]) ).
cnf(c_2309,plain,
( big_q(A)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3436]) ).
cnf(c_3437,plain,
( big_p(sK2)
| ~ big_q(sK3)
| big_p(sK0(A))
| big_p(A)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2309,c_663]) ).
cnf(c_2339,plain,
( ~ big_q(sK3)
| big_p(sK0(A))
| big_p(A)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3437]) ).
cnf(c_3438,plain,
( ~ big_q(sK3)
| big_p(sK0(sK8))
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2339]) ).
cnf(c_2342,plain,
( ~ big_q(sK3)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3438]) ).
cnf(c_3439,plain,
( big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2342,c_2309]) ).
cnf(c_3440,plain,
( big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3439]) ).
cnf(c_3441,plain,
( big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3440]) ).
cnf(c_3442,plain,
( big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3441]) ).
cnf(c_3443,plain,
( big_p(sK0(sK8))
| big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3442]) ).
cnf(c_2352,plain,
( big_p(sK0(sK8))
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3443]) ).
cnf(c_3444,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2266,c_2352]) ).
cnf(c_3445,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3444]) ).
cnf(c_3446,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3445]) ).
cnf(c_3447,plain,
( big_p(sK8)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3446]) ).
cnf(c_2353,plain,
( big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3447]) ).
cnf(c_3448,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2353,c_780]) ).
cnf(c_2355,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3448]) ).
cnf(c_3449,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2355,c_2352]) ).
cnf(c_3450,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3449]) ).
cnf(c_3451,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3450]) ).
cnf(c_3452,plain,
( big_p(sK8)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3451]) ).
cnf(c_2356,plain,
( big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3452]) ).
cnf(c_3453,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2356,c_782]) ).
cnf(c_2358,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3453]) ).
cnf(c_3454,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2358,c_2356]) ).
cnf(c_3455,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3454]) ).
cnf(c_3456,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3455]) ).
cnf(c_3457,plain,
( big_p(sK10)
| big_p(sK8)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3456]) ).
cnf(c_3458,plain,
( big_p(sK10)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3457]) ).
cnf(c_2363,plain,
( ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3458]) ).
cnf(c_3459,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2363,c_2352]) ).
cnf(c_3460,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3459]) ).
cnf(c_3461,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3460]) ).
cnf(c_3462,plain,
( big_p(sK8)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3461]) ).
cnf(c_2364,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK16)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3462]) ).
cnf(c_3463,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2364,c_775]) ).
cnf(c_2365,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3463]) ).
cnf(c_3464,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2365,c_781]) ).
cnf(c_2368,plain,
( big_q(sK11)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3464]) ).
cnf(c_3465,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_q(sK11)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2368,c_2364]) ).
cnf(c_3466,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_q(sK11)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3465]) ).
cnf(c_3467,plain,
( big_p(sK10)
| big_p(sK8)
| big_q(sK11)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3466]) ).
cnf(c_3468,plain,
( big_p(sK10)
| big_q(sK11)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3467]) ).
cnf(c_2377,plain,
( big_q(sK11)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3468]) ).
cnf(c_3469,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2377,c_780]) ).
cnf(c_2379,plain,
( big_q(B)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3469]) ).
cnf(c_2381,plain,
( ~ big_p(A)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2379]) ).
cnf(c_3470,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2381,c_2364]) ).
cnf(c_3471,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3470]) ).
cnf(c_3472,plain,
( big_p(sK10)
| big_p(sK8)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3471]) ).
cnf(c_3473,plain,
( big_p(sK10)
| big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3472]) ).
cnf(c_2382,plain,
( big_q(sK9)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3473]) ).
cnf(c_3474,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2382,c_781]) ).
cnf(c_2384,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3474]) ).
cnf(c_3475,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2384,c_2364]) ).
cnf(c_3476,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3475]) ).
cnf(c_3477,plain,
( big_p(sK10)
| big_p(sK8)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3476]) ).
cnf(c_3478,plain,
( big_p(sK10)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3477]) ).
cnf(c_2400,plain,
( big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3478]) ).
cnf(c_3479,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2400,c_780]) ).
cnf(c_2402,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3479]) ).
cnf(c_3480,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2402,c_2364]) ).
cnf(c_3481,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3480]) ).
cnf(c_3482,plain,
( big_p(sK10)
| big_p(sK8)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3481]) ).
cnf(c_3483,plain,
( big_p(sK10)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3482]) ).
cnf(c_2403,plain,
( big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3483]) ).
cnf(c_3484,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2403,c_782]) ).
cnf(c_2405,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3484]) ).
cnf(c_3485,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2405,c_2403]) ).
cnf(c_3486,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3485]) ).
cnf(c_3487,plain,
( big_p(sK10)
| big_p(sK8)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3486]) ).
cnf(c_3488,plain,
( big_p(sK10)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3487]) ).
cnf(c_2413,plain,
( ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3488]) ).
cnf(c_3489,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2413,c_2364]) ).
cnf(c_3490,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3489]) ).
cnf(c_3491,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3490]) ).
cnf(c_3492,plain,
( big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3491]) ).
cnf(c_2414,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3492]) ).
cnf(c_3493,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2414,c_775]) ).
cnf(c_2417,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3493]) ).
cnf(c_3494,plain,
( big_p(sK5)
| big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2417,c_515]) ).
cnf(c_3495,plain,
( big_p(sK5)
| big_q(sK4)
| big_q(sK9)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3494]) ).
cnf(c_3496,plain,
( big_p(sK5)
| big_q(sK4)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3495]) ).
cnf(c_2457,plain,
( big_q(sK4)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3496]) ).
cnf(c_3497,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2457,c_2414]) ).
cnf(c_3498,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3497]) ).
cnf(c_3499,plain,
( big_p(sK8)
| big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3498]) ).
cnf(c_2481,plain,
( big_q(sK4)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3499]) ).
cnf(c_3500,plain,
( big_p(sK5)
| big_q(sK9)
| ~ big_p(A)
| big_p(sK8)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2481,c_704]) ).
cnf(c_3501,plain,
( big_p(sK5)
| big_q(sK9)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3500]) ).
cnf(c_3502,plain,
( big_p(sK5)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3501]) ).
cnf(c_2484,plain,
( ~ big_p(A)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3502]) ).
cnf(c_3503,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2484,c_2414]) ).
cnf(c_3504,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3503]) ).
cnf(c_3505,plain,
( big_p(sK8)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3504]) ).
cnf(c_2492,plain,
( big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3505]) ).
cnf(c_2494,plain,
( big_q(sK11)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2492,c_778]) ).
cnf(c_2506,plain,
( big_q(sK11)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2494]) ).
cnf(c_3506,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_q(sK11)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2506,c_2414]) ).
cnf(c_3507,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK11)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3506]) ).
cnf(c_3508,plain,
( big_p(sK8)
| big_q(sK11)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3507]) ).
cnf(c_2520,plain,
( big_q(sK11)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3508]) ).
cnf(c_2522,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2520,c_777]) ).
cnf(c_2527,plain,
( big_q(A)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2522]) ).
cnf(c_3509,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_q(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2527,c_2414]) ).
cnf(c_3510,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3509]) ).
cnf(c_3511,plain,
( big_p(sK8)
| big_q(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3510]) ).
cnf(c_2535,plain,
( big_q(A)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3511]) ).
cnf(c_2537,plain,
( ~ big_q(sK13)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2535,c_779]) ).
cnf(c_2544,plain,
( ~ big_q(sK13)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(factor,[status(thm)],[c_2537]) ).
cnf(c_3512,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2544,c_2535]) ).
cnf(c_3513,plain,
( big_p(sK8)
| big_p(sK2)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3512]) ).
cnf(c_3514,plain,
( big_p(sK8)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3513]) ).
cnf(c_2551,plain,
( ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3514]) ).
cnf(c_3515,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK5)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(resolve,[status(thm)],[c_2551,c_2414]) ).
cnf(c_3516,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3515]) ).
cnf(c_3517,plain,
( big_p(sK8)
| big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3516]) ).
cnf(c_2552,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK5) ),
inference(copy,[status(thm)],[c_3517]) ).
cnf(c_3518,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2552,c_775]) ).
cnf(c_2573,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3518]) ).
cnf(c_2610,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2573,c_781]) ).
cnf(c_2611,plain,
( big_q(sK11)
| big_p(A)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2573,c_778]) ).
cnf(c_2622,plain,
( big_q(sK11)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_2611]) ).
cnf(c_3519,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK11)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2610,c_2552]) ).
cnf(c_3520,plain,
( big_p(sK8)
| big_q(sK11)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3519]) ).
cnf(c_2638,plain,
( big_q(sK11)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3520]) ).
cnf(c_3521,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2638,c_780]) ).
cnf(c_2640,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3521]) ).
cnf(c_2642,plain,
( ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_2640]) ).
cnf(c_3522,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2642,c_2552]) ).
cnf(c_3523,plain,
( big_p(sK8)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3522]) ).
cnf(c_2643,plain,
( big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3523]) ).
cnf(c_3524,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2643,c_781]) ).
cnf(c_2645,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3524]) ).
cnf(c_3525,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2645,c_2552]) ).
cnf(c_3526,plain,
( big_p(sK8)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3525]) ).
cnf(c_2656,plain,
( big_q(sK11)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3526]) ).
cnf(c_3527,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2656,c_780]) ).
cnf(c_2658,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3527]) ).
cnf(c_3528,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2658,c_2552]) ).
cnf(c_3529,plain,
( big_p(sK8)
| big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3528]) ).
cnf(c_2659,plain,
( big_q(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3529]) ).
cnf(c_3530,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2659,c_782]) ).
cnf(c_2661,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3530]) ).
cnf(c_3531,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2661,c_2659]) ).
cnf(c_3532,plain,
( big_p(sK10)
| big_p(sK8)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3531]) ).
cnf(c_3533,plain,
( big_p(sK10)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3532]) ).
cnf(c_2668,plain,
( ~ big_p(A)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3533]) ).
cnf(c_3534,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2668,c_2552]) ).
cnf(c_3535,plain,
( big_p(sK8)
| big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3534]) ).
cnf(c_2669,plain,
( big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3535]) ).
cnf(c_3536,plain,
( big_q(sK11)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2669,c_2622]) ).
cnf(c_3537,plain,
( big_q(sK11)
| big_q(sK9)
| big_p(sK8)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3536]) ).
cnf(c_2670,plain,
( big_q(sK11)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3537]) ).
cnf(c_2672,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2670,c_777]) ).
cnf(c_2678,plain,
( big_q(A)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_2672]) ).
cnf(c_2687,plain,
( ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_2678]) ).
cnf(c_3538,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2687,c_2669]) ).
cnf(c_3539,plain,
( big_p(sK8)
| big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3538]) ).
cnf(c_2715,plain,
( big_q(sK9)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3539]) ).
cnf(c_2717,plain,
( big_q(sK11)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2715,c_778]) ).
cnf(c_2730,plain,
( big_q(sK11)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_2717]) ).
cnf(c_3540,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(sK11)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2730,c_2669]) ).
cnf(c_3541,plain,
( big_p(sK8)
| big_q(sK11)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3540]) ).
cnf(c_2741,plain,
( big_q(sK11)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3541]) ).
cnf(c_2743,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2741,c_777]) ).
cnf(c_2748,plain,
( big_q(A)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_2743]) ).
cnf(c_3542,plain,
( big_p(sK8)
| big_p(sK2)
| big_q(A)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2748,c_2669]) ).
cnf(c_3543,plain,
( big_p(sK8)
| big_q(A)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3542]) ).
cnf(c_2766,plain,
( big_q(A)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3543]) ).
cnf(c_2768,plain,
( ~ big_q(sK13)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2766,c_779]) ).
cnf(c_2775,plain,
( ~ big_q(sK13)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(factor,[status(thm)],[c_2768]) ).
cnf(c_3544,plain,
( big_p(sK8)
| big_p(sK2)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2775,c_2766]) ).
cnf(c_3545,plain,
( big_p(sK8)
| ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3544]) ).
cnf(c_2790,plain,
( ~ big_p(sK10)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3545]) ).
cnf(c_3546,plain,
( big_p(sK8)
| big_p(sK2)
| big_p(sK8)
| big_p(sK2) ),
inference(resolve,[status(thm)],[c_2790,c_2669]) ).
cnf(c_3547,plain,
( big_p(sK8)
| big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3546]) ).
cnf(c_2791,plain,
( big_p(sK8)
| big_p(sK2) ),
inference(copy,[status(thm)],[c_3547]) ).
cnf(c_3548,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2791,c_775]) ).
cnf(c_2820,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3548]) ).
cnf(c_2838,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2820,c_781]) ).
cnf(c_2839,plain,
( big_q(sK11)
| big_p(A)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2820,c_778]) ).
cnf(c_2855,plain,
( big_q(sK11)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_2839]) ).
cnf(c_3549,plain,
( big_p(sK8)
| big_q(sK11)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2838,c_2791]) ).
cnf(c_2878,plain,
( big_q(sK11)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3549]) ).
cnf(c_3550,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2878,c_780]) ).
cnf(c_2880,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3550]) ).
cnf(c_2882,plain,
( ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_2880]) ).
cnf(c_3551,plain,
( big_p(sK8)
| big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2882,c_2791]) ).
cnf(c_2893,plain,
( big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3551]) ).
cnf(c_3552,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2893,c_781]) ).
cnf(c_2895,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3552]) ).
cnf(c_3553,plain,
( big_p(sK8)
| big_q(sK11)
| big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2895,c_2791]) ).
cnf(c_2911,plain,
( big_q(sK11)
| big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3553]) ).
cnf(c_3554,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2911,c_780]) ).
cnf(c_2913,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3554]) ).
cnf(c_3555,plain,
( big_p(sK8)
| big_q(A)
| big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2913,c_2791]) ).
cnf(c_2943,plain,
( big_q(A)
| big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3555]) ).
cnf(c_3556,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2943,c_782]) ).
cnf(c_2945,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3556]) ).
cnf(c_3557,plain,
( big_p(sK10)
| big_p(sK8)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2945,c_2943]) ).
cnf(c_3558,plain,
( big_p(sK10)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3557]) ).
cnf(c_2946,plain,
( ~ big_p(A)
| big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3558]) ).
cnf(c_3559,plain,
( big_p(sK8)
| big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2946,c_2791]) ).
cnf(c_2947,plain,
( big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3559]) ).
cnf(c_3560,plain,
( big_q(sK11)
| big_q(sK9)
| big_p(sK8)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2947,c_2855]) ).
cnf(c_2966,plain,
( big_q(sK11)
| big_q(sK9)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3560]) ).
cnf(c_2976,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2966,c_777]) ).
cnf(c_2982,plain,
( big_q(A)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_2976]) ).
cnf(c_2989,plain,
( ~ big_p(sK10)
| big_q(sK9)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_2982]) ).
cnf(c_3561,plain,
( big_p(sK8)
| big_q(sK9)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2989,c_2947]) ).
cnf(c_2991,plain,
( big_q(sK9)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3561]) ).
cnf(c_2993,plain,
( big_q(sK11)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_2991,c_778]) ).
cnf(c_3010,plain,
( big_q(sK11)
| ~ big_p(sK10)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_2993]) ).
cnf(c_3562,plain,
( big_p(sK8)
| big_q(sK11)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_3010,c_2947]) ).
cnf(c_3036,plain,
( big_q(sK11)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3562]) ).
cnf(c_3038,plain,
( big_q(B)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_3036,c_777]) ).
cnf(c_3043,plain,
( big_q(A)
| ~ big_p(sK10)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_3038]) ).
cnf(c_3563,plain,
( big_p(sK8)
| big_q(A)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_3043,c_2947]) ).
cnf(c_3047,plain,
( big_q(A)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3563]) ).
cnf(c_3049,plain,
( ~ big_q(sK13)
| big_p(A)
| ~ big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_3047,c_779]) ).
cnf(c_3052,plain,
( ~ big_q(sK13)
| ~ big_p(sK10)
| big_p(sK8) ),
inference(factor,[status(thm)],[c_3049]) ).
cnf(c_3564,plain,
( big_p(sK8)
| ~ big_p(sK10)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_3052,c_3047]) ).
cnf(c_3074,plain,
( ~ big_p(sK10)
| big_p(sK8) ),
inference(copy,[status(thm)],[c_3564]) ).
cnf(c_3565,plain,
( big_p(sK8)
| big_p(sK8) ),
inference(resolve,[status(thm)],[c_3074,c_2947]) ).
cnf(c_3075,plain,
big_p(sK8),
inference(copy,[status(thm)],[c_3565]) ).
cnf(c_3097,plain,
( big_q(sK1(sK9))
| big_q(sK9)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3075,c_773]) ).
cnf(c_3144,plain,
( big_q(sK11)
| ~ big_p(B)
| big_p(sK10)
| big_q(sK9)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3097,c_781]) ).
cnf(c_3145,plain,
( big_q(sK11)
| big_p(B)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3097,c_778]) ).
cnf(c_3159,plain,
( big_q(sK11)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_3144]) ).
cnf(c_3160,plain,
( big_q(sK11)
| ~ big_p(sK10)
| big_q(sK9)
| big_p(A) ),
inference(factor,[status(thm)],[c_3145]) ).
cnf(c_3249,plain,
( big_q(sK11)
| big_q(sK9)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3159,c_3075]) ).
cnf(c_3566,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_q(sK9)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3249,c_780]) ).
cnf(c_3251,plain,
( big_q(B)
| ~ big_p(A)
| big_q(sK9)
| big_p(sK10) ),
inference(copy,[status(thm)],[c_3566]) ).
cnf(c_3253,plain,
( ~ big_p(A)
| big_q(sK9)
| big_p(sK10) ),
inference(factor,[status(thm)],[c_3251]) ).
cnf(c_3254,plain,
( big_q(sK9)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3253,c_3075]) ).
cnf(c_3567,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3254,c_781]) ).
cnf(c_3266,plain,
( big_q(sK11)
| ~ big_p(A)
| big_p(sK10) ),
inference(copy,[status(thm)],[c_3567]) ).
cnf(c_3274,plain,
( big_q(sK11)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3266,c_3075]) ).
cnf(c_3568,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3274,c_780]) ).
cnf(c_3276,plain,
( big_q(B)
| ~ big_p(A)
| big_p(sK10) ),
inference(copy,[status(thm)],[c_3568]) ).
cnf(c_3277,plain,
( big_q(A)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3276,c_3075]) ).
cnf(c_3569,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3277,c_782]) ).
cnf(c_3287,plain,
( ~ big_q(sK13)
| ~ big_p(A)
| big_p(sK10) ),
inference(copy,[status(thm)],[c_3569]) ).
cnf(c_3570,plain,
( big_p(sK10)
| ~ big_p(A)
| big_p(sK10) ),
inference(resolve,[status(thm)],[c_3287,c_3277]) ).
cnf(c_3292,plain,
( ~ big_p(A)
| big_p(sK10) ),
inference(copy,[status(thm)],[c_3570]) ).
cnf(c_3293,plain,
big_p(sK10),
inference(resolve,[status(thm)],[c_3292,c_3075]) ).
cnf(c_3301,plain,
( big_q(sK11)
| big_q(sK9)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3293,c_3160]) ).
cnf(c_3315,plain,
( ~ big_q(sK12(sK13))
| ~ big_q(sK13)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3293,c_779]) ).
cnf(c_3316,plain,
( big_q(sK11)
| ~ big_q(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3293,c_778]) ).
cnf(c_3317,plain,
( big_q(B)
| ~ big_q(sK11)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3293,c_777]) ).
cnf(c_3336,plain,
( big_q(sK9)
| big_p(C)
| big_q(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3317,c_3301]) ).
cnf(c_3338,plain,
( big_q(sK9)
| big_q(B)
| big_p(A) ),
inference(factor,[status(thm)],[c_3336]) ).
cnf(c_3341,plain,
( big_q(sK9)
| big_p(A) ),
inference(factor,[status(thm)],[c_3338]) ).
cnf(c_3348,plain,
( big_q(sK11)
| big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3341,c_3316]) ).
cnf(c_3353,plain,
( big_q(sK11)
| big_p(A) ),
inference(factor,[status(thm)],[c_3348]) ).
cnf(c_3356,plain,
( big_q(C)
| big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3353,c_3317]) ).
cnf(c_3359,plain,
( big_q(B)
| big_p(A) ),
inference(factor,[status(thm)],[c_3356]) ).
cnf(c_3374,plain,
( big_p(B)
| ~ big_q(sK13)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3315,c_3359]) ).
cnf(c_3375,plain,
( ~ big_q(sK13)
| big_p(A) ),
inference(factor,[status(thm)],[c_3374]) ).
cnf(c_3376,plain,
( big_p(B)
| big_p(A) ),
inference(resolve,[status(thm)],[c_3375,c_3359]) ).
cnf(c_3377,plain,
big_p(A),
inference(factor,[status(thm)],[c_3376]) ).
cnf(c_3571,plain,
( big_q(sK11)
| ~ big_q(A)
| ~ big_p(sK14(sK17)) ),
inference(resolve,[status(thm)],[c_3377,c_785]) ).
cnf(c_3379,plain,
( big_q(sK11)
| ~ big_q(A) ),
inference(resolve,[status(thm)],[c_3377,c_3571]) ).
cnf(c_3572,plain,
( big_q(A)
| ~ big_q(sK11)
| ~ big_p(sK14(sK17)) ),
inference(resolve,[status(thm)],[c_3377,c_784]) ).
cnf(c_3380,plain,
( big_q(A)
| ~ big_q(sK11) ),
inference(resolve,[status(thm)],[c_3377,c_3572]) ).
cnf(c_3573,plain,
( big_q(sK1(sK6))
| big_q(sK6)
| ~ big_p(sK0(sK7)) ),
inference(resolve,[status(thm)],[c_3377,c_772]) ).
cnf(c_3381,plain,
( big_q(sK1(sK6))
| big_q(sK6) ),
inference(resolve,[status(thm)],[c_3377,c_3573]) ).
cnf(c_3574,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(A))
| ~ big_q(A)
| ~ big_p(sK14(sK17)) ),
inference(resolve,[status(thm)],[c_3377,c_766]) ).
cnf(c_3382,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(A))
| ~ big_q(A) ),
inference(resolve,[status(thm)],[c_3377,c_3574]) ).
cnf(c_3388,plain,
( big_q(sK11)
| big_q(sK6) ),
inference(resolve,[status(thm)],[c_3381,c_3379]) ).
cnf(c_3389,plain,
( big_q(A)
| big_q(sK6) ),
inference(resolve,[status(thm)],[c_3388,c_3380]) ).
cnf(c_3390,plain,
big_q(sK6),
inference(factor,[status(thm)],[c_3389]) ).
cnf(c_3391,plain,
big_q(sK11),
inference(resolve,[status(thm)],[c_3390,c_3379]) ).
cnf(c_3392,plain,
big_q(A),
inference(resolve,[status(thm)],[c_3391,c_3380]) ).
cnf(c_3575,plain,
( ~ big_q(sK13)
| ~ big_q(sK12(A)) ),
inference(resolve,[status(thm)],[c_3392,c_3382]) ).
cnf(c_3576,plain,
~ big_q(sK13),
inference(resolve,[status(thm)],[c_3392,c_3575]) ).
cnf(c_3393,plain,
$false,
inference(resolve,[status(thm)],[c_3392,c_3576]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN036+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.30 % Computer : n012.cluster.edu
% 0.02/0.30 % Model : x86_64 x86_64
% 0.02/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.30 % Memory : 8046.5625MB
% 0.02/0.30 % OS : Linux 6.8.0-71-generic
% 0.02/0.30 % CPULimit : 300
% 0.02/0.30 % WCLimit : 300
% 0.02/0.30 % DateTime : Sat Sep 26 17:04:36 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.02/0.30 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.30 % Process 1101134 was started by sandbox2 on n012,
% 0.02/0.30 % Sat Sep 26 17:04:36 2026
% 0.02/0.30 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/0.32
% 0.02/0.32 % From the command line: assign(max_seconds, 300).
% 2.96/0.80
% 2.96/0.80 % given #500 (T,wt=7): 3230 big_p(c9) | big_p(f1(c9)) | big_q(A). [resolve(3201,c,770,c),merge(c),merge(d)].
% 2.96/0.80
% 2.96/0.80 % SZS status Theorem for theBenchmark
% 2.96/0.80
% 2.96/0.80 % Proof 1 at 0.33 (+ 0.11) seconds.
% 2.96/0.80 % Length of proof is 254.
% 2.96/0.80 % Level of proof is 157.
% 2.96/0.80 % Maximum clause weight is 20.000.
% 2.96/0.80 % Given clauses 541.
% 2.96/0.80
% 2.96/0.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------