%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN096-1.008 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:37:02 AM UTC 2026
% Result : Unsatisfiable 19.64s 3.21s
% Output : CNFRefutation 19.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 30
% Syntax : Number of formulae : 166 ( 19 unt; 0 def)
% Number of atoms : 624 ( 0 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 923 ( 465 ~; 458 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 96 ( 0 sgn 27 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m_s3_type11_1,axiom,
! [VAR_0] :
( ~ p_2(VAR_0)
| ~ p_1(VAR_0)
| p_0(VAR_0) ),
file('theBenchmark.p',m_s3_type11_1) ).
cnf(c_1,plain,
( ~ p_2(A)
| ~ p_1(A)
| p_0(A) ),
inference(clausify,[status(thm)],[m_s3_type11_1]) ).
fof(m_s3_goal_1,axiom,
! [VAR_0] :
( ~ q_0(VAR_0)
| ~ p_0(VAR_0) ),
file('theBenchmark.p',m_s3_goal_1) ).
cnf(c_2,plain,
( ~ q_0(A)
| ~ p_0(A) ),
inference(clausify,[status(thm)],[m_s3_goal_1]) ).
cnf(c_5,plain,
( ~ q_0(A)
| ~ p_2(A)
| ~ p_1(A) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
fof(m_s3_type12_1,axiom,
! [VAR_0] :
( ~ q_2(VAR_0)
| ~ p_1(VAR_0)
| q_0(VAR_0) ),
file('theBenchmark.p',m_s3_type12_1) ).
cnf(c_7,plain,
( ~ q_2(A)
| ~ p_1(A)
| q_0(A) ),
inference(clausify,[status(thm)],[m_s3_type12_1]) ).
fof(m_s3_type11_3,axiom,
! [VAR_0] :
( ~ p_3(VAR_0)
| ~ p_2(VAR_0)
| p_1(VAR_0) ),
file('theBenchmark.p',m_s3_type11_3) ).
cnf(c_10,plain,
( ~ p_3(A)
| ~ p_2(A)
| p_1(A) ),
inference(clausify,[status(thm)],[m_s3_type11_3]) ).
fof(m_s3_type11_8,axiom,
! [VAR_0] :
( ~ q_5(VAR_0)
| ~ q_4(VAR_0)
| p_3(VAR_0) ),
file('theBenchmark.p',m_s3_type11_8) ).
cnf(c_11,plain,
( ~ q_5(A)
| ~ q_4(A)
| p_3(A) ),
inference(clausify,[status(thm)],[m_s3_type11_8]) ).
fof(m_s3_type12_5,axiom,
! [VAR_0] :
( ~ q_4(VAR_0)
| ~ p_3(VAR_0)
| q_2(VAR_0) ),
file('theBenchmark.p',m_s3_type12_5) ).
cnf(c_13,plain,
( ~ q_4(A)
| ~ p_3(A)
| q_2(A) ),
inference(clausify,[status(thm)],[m_s3_type12_5]) ).
fof(m_s3_type12_8,axiom,
! [VAR_0] :
( ~ p_5(VAR_0)
| ~ q_4(VAR_0)
| q_3(VAR_0) ),
file('theBenchmark.p',m_s3_type12_8) ).
cnf(c_16,plain,
( ~ p_5(A)
| ~ q_4(A)
| q_3(A) ),
inference(clausify,[status(thm)],[m_s3_type12_8]) ).
fof(m_s3_type11_6,axiom,
! [VAR_0] :
( ~ q_4(VAR_0)
| ~ q_3(VAR_0)
| p_2(VAR_0) ),
file('theBenchmark.p',m_s3_type11_6) ).
cnf(c_18,plain,
( ~ q_4(A)
| ~ q_3(A)
| p_2(A) ),
inference(clausify,[status(thm)],[m_s3_type11_6]) ).
cnf(c_24,plain,
( ~ p_5(A)
| ~ q_4(A)
| ~ q_4(A)
| p_2(A) ),
inference(resolve,[status(thm)],[c_18,c_16]) ).
fof(m_s3_type11_12,axiom,
! [VAR_0] :
( ~ q_7(VAR_0)
| ~ q_6(VAR_0)
| p_5(VAR_0) ),
file('theBenchmark.p',m_s3_type11_12) ).
cnf(c_26,plain,
( ~ q_7(A)
| ~ q_6(A)
| p_5(A) ),
inference(clausify,[status(thm)],[m_s3_type11_12]) ).
fof(m_s3_type12_9,axiom,
! [VAR_0] :
( ~ q_6(VAR_0)
| ~ p_5(VAR_0)
| q_4(VAR_0) ),
file('theBenchmark.p',m_s3_type12_9) ).
cnf(c_27,plain,
( ~ q_6(A)
| ~ p_5(A)
| q_4(A) ),
inference(clausify,[status(thm)],[m_s3_type12_9]) ).
fof(m_s3_type12_12,axiom,
! [VAR_0] :
( ~ p_7(VAR_0)
| ~ q_6(VAR_0)
| q_5(VAR_0) ),
file('theBenchmark.p',m_s3_type12_12) ).
cnf(c_32,plain,
( ~ p_7(A)
| ~ q_6(A)
| q_5(A) ),
inference(clausify,[status(thm)],[m_s3_type12_12]) ).
cnf(c_34,plain,
( ~ p_2(A)
| p_1(A)
| ~ q_5(A)
| ~ q_4(A) ),
inference(resolve,[status(thm)],[c_11,c_10]) ).
cnf(c_36,plain,
( ~ q_5(A)
| ~ q_4(A)
| ~ q_4(A)
| q_2(A) ),
inference(resolve,[status(thm)],[c_13,c_11]) ).
cnf(c_47,plain,
( ~ p_2(A)
| p_1(A)
| ~ q_4(A)
| ~ p_7(A)
| ~ q_6(A) ),
inference(resolve,[status(thm)],[c_32,c_34]) ).
cnf(c_49,plain,
( ~ q_4(A)
| ~ q_4(A)
| q_2(A)
| ~ p_7(A)
| ~ q_6(A) ),
inference(resolve,[status(thm)],[c_32,c_36]) ).
fof(m_s3_type11_16,axiom,
! [VAR_0] :
( ~ q_9(VAR_0)
| ~ q_8(VAR_0)
| p_7(VAR_0) ),
file('theBenchmark.p',m_s3_type11_16) ).
cnf(c_55,plain,
( ~ q_9(A)
| ~ q_8(A)
| p_7(A) ),
inference(clausify,[status(thm)],[m_s3_type11_16]) ).
cnf(c_72,plain,
( ~ q_4(A)
| ~ q_4(A)
| p_2(A)
| ~ q_7(A)
| ~ q_6(A) ),
inference(resolve,[status(thm)],[c_26,c_24]) ).
cnf(c_74,plain,
( ~ q_7(A)
| ~ q_6(A)
| ~ q_6(A)
| q_4(A) ),
inference(resolve,[status(thm)],[c_27,c_26]) ).
fof(m_s3_type12_15,axiom,
! [VAR_0] :
( ~ q_9(VAR_0)
| ~ p_8(VAR_0)
| q_7(VAR_0) ),
file('theBenchmark.p',m_s3_type12_15) ).
cnf(c_78,plain,
( ~ q_9(A)
| ~ p_8(A)
| q_7(A) ),
inference(clausify,[status(thm)],[m_s3_type12_15]) ).
fof(m_s3_type12_14,axiom,
! [VAR_0] :
( ~ p_8(VAR_0)
| ~ q_7(VAR_0)
| q_6(VAR_0) ),
file('theBenchmark.p',m_s3_type12_14) ).
cnf(c_79,plain,
( ~ p_8(A)
| ~ q_7(A)
| q_6(A) ),
inference(clausify,[status(thm)],[m_s3_type12_14]) ).
fof(m_s3_type12_20,axiom,
! [VAR_0] :
( ~ p_11(VAR_0)
| ~ q_10(VAR_0)
| q_9(VAR_0) ),
file('theBenchmark.p',m_s3_type12_20) ).
cnf(c_134,plain,
( ~ p_11(A)
| ~ q_10(A)
| q_9(A) ),
inference(clausify,[status(thm)],[m_s3_type12_20]) ).
cnf(c_137,plain,
( ~ p_2(A)
| p_1(A)
| ~ q_4(A)
| ~ q_6(A)
| ~ q_9(A)
| ~ q_8(A) ),
inference(resolve,[status(thm)],[c_55,c_47]) ).
cnf(c_139,plain,
( ~ q_4(A)
| ~ q_4(A)
| q_2(A)
| ~ q_6(A)
| ~ q_9(A)
| ~ q_8(A) ),
inference(resolve,[status(thm)],[c_55,c_49]) ).
fof(m_s3_type12_19,axiom,
! [VAR_0] :
( ~ q_11(VAR_0)
| ~ p_10(VAR_0)
| q_9(VAR_0) ),
file('theBenchmark.p',m_s3_type12_19) ).
cnf(c_155,plain,
( ~ q_11(A)
| ~ p_10(A)
| q_9(A) ),
inference(clausify,[status(thm)],[m_s3_type12_19]) ).
fof(m_s3_type12_18,axiom,
! [VAR_0] :
( ~ p_10(VAR_0)
| ~ q_9(VAR_0)
| q_8(VAR_0) ),
file('theBenchmark.p',m_s3_type12_18) ).
cnf(c_156,plain,
( ~ p_10(A)
| ~ q_9(A)
| q_8(A) ),
inference(clausify,[status(thm)],[m_s3_type12_18]) ).
fof(m_s3_type11_18,axiom,
! [VAR_0] :
( ~ q_10(VAR_0)
| ~ q_9(VAR_0)
| p_8(VAR_0) ),
file('theBenchmark.p',m_s3_type11_18) ).
cnf(c_157,plain,
( ~ q_10(A)
| ~ q_9(A)
| p_8(A) ),
inference(clausify,[status(thm)],[m_s3_type11_18]) ).
cnf(c_162,plain,
( ~ q_4(A)
| ~ q_4(A)
| p_2(A)
| ~ q_6(A)
| ~ q_9(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_78,c_72]) ).
cnf(c_164,plain,
( ~ q_6(A)
| ~ q_6(A)
| q_4(A)
| ~ q_9(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_78,c_74]) ).
cnf(c_168,plain,
( ~ q_9(A)
| ~ p_8(A)
| ~ p_8(A)
| q_6(A) ),
inference(resolve,[status(thm)],[c_79,c_78]) ).
fof(m_s3_type11_23,axiom,
! [VAR_0] :
( ~ p_13(VAR_0)
| ~ p_12(VAR_0)
| p_11(VAR_0) ),
file('theBenchmark.p',m_s3_type11_23) ).
cnf(c_178,plain,
( ~ p_13(A)
| ~ p_12(A)
| p_11(A) ),
inference(clausify,[status(thm)],[m_s3_type11_23]) ).
fof(m_s3_type11_21,axiom,
! [VAR_0] :
( ~ p_12(VAR_0)
| ~ p_11(VAR_0)
| p_10(VAR_0) ),
file('theBenchmark.p',m_s3_type11_21) ).
cnf(c_179,plain,
( ~ p_12(A)
| ~ p_11(A)
| p_10(A) ),
inference(clausify,[status(thm)],[m_s3_type11_21]) ).
cnf(c_201,plain,
( ~ p_11(A)
| ~ q_10(A)
| ~ q_10(A)
| p_8(A) ),
inference(resolve,[status(thm)],[c_157,c_134]) ).
fof(m_s3_type12_24,axiom,
! [VAR_0] :
( ~ p_13(VAR_0)
| ~ q_12(VAR_0)
| q_11(VAR_0) ),
file('theBenchmark.p',m_s3_type12_24) ).
cnf(c_264,plain,
( ~ p_13(A)
| ~ q_12(A)
| q_11(A) ),
inference(clausify,[status(thm)],[m_s3_type12_24]) ).
fof(m_s3_type12_23,axiom,
! [VAR_0] :
( ~ q_13(VAR_0)
| ~ p_12(VAR_0)
| q_11(VAR_0) ),
file('theBenchmark.p',m_s3_type12_23) ).
cnf(c_306,plain,
( ~ q_13(A)
| ~ p_12(A)
| q_11(A) ),
inference(clausify,[status(thm)],[m_s3_type12_23]) ).
fof(m_s3_type12_22,axiom,
! [VAR_0] :
( ~ p_12(VAR_0)
| ~ q_11(VAR_0)
| q_10(VAR_0) ),
file('theBenchmark.p',m_s3_type12_22) ).
cnf(c_307,plain,
( ~ p_12(A)
| ~ q_11(A)
| q_10(A) ),
inference(clausify,[status(thm)],[m_s3_type12_22]) ).
cnf(c_311,plain,
( ~ p_2(A)
| p_1(A)
| ~ q_4(A)
| ~ q_6(A)
| ~ q_8(A)
| ~ q_11(A)
| ~ p_10(A) ),
inference(resolve,[status(thm)],[c_155,c_137]) ).
cnf(c_313,plain,
( ~ q_4(A)
| ~ q_4(A)
| q_2(A)
| ~ q_6(A)
| ~ q_8(A)
| ~ q_11(A)
| ~ p_10(A) ),
inference(resolve,[status(thm)],[c_155,c_139]) ).
cnf(c_329,plain,
( ~ q_11(A)
| ~ p_10(A)
| ~ p_10(A)
| q_8(A) ),
inference(resolve,[status(thm)],[c_156,c_155]) ).
cnf(c_335,plain,
( ~ q_11(A)
| ~ p_10(A)
| ~ q_4(A)
| ~ q_4(A)
| p_2(A)
| ~ q_6(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_162,c_155]) ).
cnf(c_337,plain,
( ~ q_11(A)
| ~ p_10(A)
| ~ q_6(A)
| ~ q_6(A)
| q_4(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_164,c_155]) ).
cnf(c_341,plain,
( ~ q_11(A)
| ~ p_10(A)
| ~ p_8(A)
| ~ p_8(A)
| q_6(A) ),
inference(resolve,[status(thm)],[c_168,c_155]) ).
fof(m_s3_type11_27,axiom,
! [VAR_0] :
( ~ p_15(VAR_0)
| ~ p_14(VAR_0)
| p_13(VAR_0) ),
file('theBenchmark.p',m_s3_type11_27) ).
cnf(c_350,plain,
( ~ p_15(A)
| ~ p_14(A)
| p_13(A) ),
inference(clausify,[status(thm)],[m_s3_type11_27]) ).
cnf(c_397,plain,
( ~ p_13(A)
| ~ q_12(A)
| ~ p_2(A)
| p_1(A)
| ~ q_4(A)
| ~ q_6(A)
| ~ q_8(A)
| ~ p_10(A) ),
inference(resolve,[status(thm)],[c_311,c_264]) ).
cnf(c_399,plain,
( ~ p_13(A)
| ~ q_12(A)
| ~ q_4(A)
| ~ q_4(A)
| q_2(A)
| ~ q_6(A)
| ~ q_8(A)
| ~ p_10(A) ),
inference(resolve,[status(thm)],[c_313,c_264]) ).
cnf(c_415,plain,
( ~ p_13(A)
| ~ q_12(A)
| ~ p_10(A)
| ~ p_10(A)
| q_8(A) ),
inference(resolve,[status(thm)],[c_329,c_264]) ).
cnf(c_420,plain,
( ~ p_13(A)
| ~ q_12(A)
| ~ p_10(A)
| ~ q_4(A)
| ~ q_4(A)
| p_2(A)
| ~ q_6(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_335,c_264]) ).
cnf(c_422,plain,
( ~ p_13(A)
| ~ q_12(A)
| ~ p_10(A)
| ~ q_6(A)
| ~ q_6(A)
| q_4(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_337,c_264]) ).
cnf(c_426,plain,
( ~ p_13(A)
| ~ q_12(A)
| ~ p_10(A)
| ~ p_8(A)
| ~ p_8(A)
| q_6(A) ),
inference(resolve,[status(thm)],[c_341,c_264]) ).
cnf(c_437,plain,
( ~ p_12(A)
| p_10(A)
| ~ p_13(A)
| ~ p_12(A) ),
inference(resolve,[status(thm)],[c_178,c_179]) ).
cnf(c_459,plain,
( ~ q_10(A)
| ~ q_10(A)
| p_8(A)
| ~ p_13(A)
| ~ p_12(A) ),
inference(resolve,[status(thm)],[c_178,c_201]) ).
fof(m_s3_type12_28,axiom,
! [VAR_0] :
( ~ p_15(VAR_0)
| ~ q_14(VAR_0)
| q_13(VAR_0) ),
file('theBenchmark.p',m_s3_type12_28) ).
cnf(c_520,plain,
( ~ p_15(A)
| ~ q_14(A)
| q_13(A) ),
inference(clausify,[status(thm)],[m_s3_type12_28]) ).
fof(m_s3_type12_26,axiom,
! [VAR_0] :
( ~ p_14(VAR_0)
| ~ q_13(VAR_0)
| q_12(VAR_0) ),
file('theBenchmark.p',m_s3_type12_26) ).
cnf(c_605,plain,
( ~ p_14(A)
| ~ q_13(A)
| q_12(A) ),
inference(clausify,[status(thm)],[m_s3_type12_26]) ).
fof(m_s3_type11_26,axiom,
! [VAR_0] :
( ~ q_14(VAR_0)
| ~ q_13(VAR_0)
| p_12(VAR_0) ),
file('theBenchmark.p',m_s3_type11_26) ).
cnf(c_606,plain,
( ~ q_14(A)
| ~ q_13(A)
| p_12(A) ),
inference(clausify,[status(thm)],[m_s3_type11_26]) ).
cnf(c_648,plain,
( ~ q_13(A)
| ~ p_12(A)
| ~ p_12(A)
| q_10(A) ),
inference(resolve,[status(thm)],[c_307,c_306]) ).
cnf(c_730,plain,
( ~ p_15(A)
| ~ q_14(A)
| ~ p_12(A)
| ~ p_12(A)
| q_10(A) ),
inference(resolve,[status(thm)],[c_648,c_520]) ).
cnf(c_772,plain,
( ~ p_15(A)
| ~ q_14(A)
| ~ q_14(A)
| p_12(A) ),
inference(resolve,[status(thm)],[c_606,c_520]) ).
cnf(c_773,plain,
( ~ p_15(A)
| ~ q_14(A)
| ~ p_14(A)
| q_12(A) ),
inference(resolve,[status(thm)],[c_605,c_520]) ).
fof(m_t3_2,axiom,
p_15(a),
file('theBenchmark.p',m_t3_2) ).
cnf(c_857,plain,
p_15(a),
inference(clausify,[status(thm)],[m_t3_2]) ).
cnf(c_903,plain,
( ~ q_12(A)
| ~ p_2(A)
| p_1(A)
| ~ q_4(A)
| ~ q_6(A)
| ~ q_8(A)
| ~ p_10(A)
| ~ p_15(A)
| ~ p_14(A) ),
inference(resolve,[status(thm)],[c_350,c_397]) ).
cnf(c_905,plain,
( ~ q_12(A)
| ~ q_4(A)
| ~ q_4(A)
| q_2(A)
| ~ q_6(A)
| ~ q_8(A)
| ~ p_10(A)
| ~ p_15(A)
| ~ p_14(A) ),
inference(resolve,[status(thm)],[c_350,c_399]) ).
cnf(c_920,plain,
( ~ q_12(A)
| ~ p_10(A)
| ~ p_10(A)
| q_8(A)
| ~ p_15(A)
| ~ p_14(A) ),
inference(resolve,[status(thm)],[c_350,c_415]) ).
cnf(c_925,plain,
( ~ q_12(A)
| ~ p_10(A)
| ~ q_4(A)
| ~ q_4(A)
| p_2(A)
| ~ q_6(A)
| ~ p_8(A)
| ~ p_15(A)
| ~ p_14(A) ),
inference(resolve,[status(thm)],[c_350,c_420]) ).
cnf(c_927,plain,
( ~ q_12(A)
| ~ p_10(A)
| ~ q_6(A)
| ~ q_6(A)
| q_4(A)
| ~ p_8(A)
| ~ p_15(A)
| ~ p_14(A) ),
inference(resolve,[status(thm)],[c_350,c_422]) ).
cnf(c_931,plain,
( ~ q_12(A)
| ~ p_10(A)
| ~ p_8(A)
| ~ p_8(A)
| q_6(A)
| ~ p_15(A)
| ~ p_14(A) ),
inference(resolve,[status(thm)],[c_350,c_426]) ).
cnf(c_943,plain,
( ~ p_15(A)
| ~ p_14(A)
| ~ p_12(A)
| p_10(A)
| ~ p_12(A) ),
inference(resolve,[status(thm)],[c_437,c_350]) ).
cnf(c_965,plain,
( ~ p_15(A)
| ~ p_14(A)
| ~ q_10(A)
| ~ q_10(A)
| p_8(A)
| ~ p_12(A) ),
inference(resolve,[status(thm)],[c_459,c_350]) ).
cnf(c_1696,plain,
( ~ q_12(a)
| ~ p_2(a)
| p_1(a)
| ~ q_4(a)
| ~ q_6(a)
| ~ q_8(a)
| ~ p_10(a)
| ~ p_14(a) ),
inference(resolve,[status(thm)],[c_903,c_857]) ).
cnf(c_1704,plain,
( ~ q_12(a)
| ~ q_4(a)
| ~ q_4(a)
| q_2(a)
| ~ q_6(a)
| ~ q_8(a)
| ~ p_10(a)
| ~ p_14(a) ),
inference(resolve,[status(thm)],[c_905,c_857]) ).
cnf(c_1705,plain,
( ~ q_12(a)
| ~ q_4(a)
| q_2(a)
| ~ q_6(a)
| ~ q_8(a)
| ~ p_10(a)
| ~ p_14(a) ),
inference(copy,[status(thm)],[c_1704]) ).
cnf(c_1769,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ p_10(a)
| q_8(a)
| ~ p_14(a) ),
inference(resolve,[status(thm)],[c_920,c_857]) ).
cnf(c_1770,plain,
( ~ q_12(a)
| ~ p_10(a)
| q_8(a)
| ~ p_14(a) ),
inference(copy,[status(thm)],[c_1769]) ).
cnf(c_1779,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_4(a)
| ~ q_4(a)
| p_2(a)
| ~ q_6(a)
| ~ p_8(a)
| ~ p_14(a) ),
inference(resolve,[status(thm)],[c_925,c_857]) ).
cnf(c_1780,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_4(a)
| p_2(a)
| ~ q_6(a)
| ~ p_8(a)
| ~ p_14(a) ),
inference(copy,[status(thm)],[c_1779]) ).
cnf(c_1784,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_6(a)
| ~ q_6(a)
| q_4(a)
| ~ p_8(a)
| ~ p_14(a) ),
inference(resolve,[status(thm)],[c_927,c_857]) ).
cnf(c_1785,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_6(a)
| q_4(a)
| ~ p_8(a)
| ~ p_14(a) ),
inference(copy,[status(thm)],[c_1784]) ).
cnf(c_1794,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ p_8(a)
| ~ p_8(a)
| q_6(a)
| ~ p_14(a) ),
inference(resolve,[status(thm)],[c_931,c_857]) ).
cnf(c_1795,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ p_8(a)
| q_6(a)
| ~ p_14(a) ),
inference(copy,[status(thm)],[c_1794]) ).
cnf(c_1931,plain,
( ~ p_14(a)
| ~ p_12(a)
| p_10(a)
| ~ p_12(a) ),
inference(resolve,[status(thm)],[c_943,c_857]) ).
cnf(c_1932,plain,
( ~ p_14(a)
| p_10(a)
| ~ p_12(a) ),
inference(copy,[status(thm)],[c_1931]) ).
cnf(c_2076,plain,
( ~ p_14(a)
| ~ q_10(a)
| ~ q_10(a)
| p_8(a)
| ~ p_12(a) ),
inference(resolve,[status(thm)],[c_965,c_857]) ).
cnf(c_2077,plain,
( ~ p_14(a)
| ~ q_10(a)
| p_8(a)
| ~ p_12(a) ),
inference(copy,[status(thm)],[c_2076]) ).
cnf(c_2373,plain,
( ~ q_14(a)
| ~ p_12(a)
| ~ p_12(a)
| q_10(a) ),
inference(resolve,[status(thm)],[c_857,c_730]) ).
cnf(c_2374,plain,
( ~ q_14(a)
| ~ p_12(a)
| q_10(a) ),
inference(copy,[status(thm)],[c_2373]) ).
cnf(c_2429,plain,
( ~ q_14(a)
| ~ q_14(a)
| p_12(a) ),
inference(resolve,[status(thm)],[c_857,c_772]) ).
cnf(c_2430,plain,
( ~ q_14(a)
| p_12(a) ),
inference(copy,[status(thm)],[c_2429]) ).
cnf(c_2431,plain,
( ~ q_14(a)
| ~ p_14(a)
| q_12(a) ),
inference(resolve,[status(thm)],[c_857,c_773]) ).
fof(m_t3_3,axiom,
q_14(a),
file('theBenchmark.p',m_t3_3) ).
cnf(c_2841,plain,
q_14(a),
inference(clausify,[status(thm)],[m_t3_3]) ).
fof(m_t3_1,axiom,
p_14(a),
file('theBenchmark.p',m_t3_1) ).
cnf(c_2842,plain,
p_14(a),
inference(clausify,[status(thm)],[m_t3_1]) ).
cnf(c_2849,plain,
( ~ p_2(A)
| ~ p_1(A)
| ~ q_2(A)
| ~ p_1(A) ),
inference(resolve,[status(thm)],[c_7,c_5]) ).
cnf(c_2850,plain,
( ~ p_2(A)
| ~ q_2(A)
| ~ p_1(A) ),
inference(copy,[status(thm)],[c_2849]) ).
cnf(c_4472,plain,
( ~ q_14(a)
| q_12(a) ),
inference(resolve,[status(thm)],[c_2842,c_2431]) ).
cnf(c_3908,plain,
q_12(a),
inference(resolve,[status(thm)],[c_2841,c_4472]) ).
cnf(c_3909,plain,
p_12(a),
inference(resolve,[status(thm)],[c_2841,c_2430]) ).
cnf(c_4473,plain,
( ~ q_14(a)
| q_10(a) ),
inference(resolve,[status(thm)],[c_3909,c_2374]) ).
cnf(c_3949,plain,
q_10(a),
inference(resolve,[status(thm)],[c_2841,c_4473]) ).
cnf(c_4474,plain,
( ~ p_14(a)
| ~ q_10(a)
| p_8(a) ),
inference(resolve,[status(thm)],[c_3909,c_2077]) ).
cnf(c_4475,plain,
( ~ p_14(a)
| p_8(a) ),
inference(resolve,[status(thm)],[c_3949,c_4474]) ).
cnf(c_4037,plain,
p_8(a),
inference(resolve,[status(thm)],[c_2842,c_4475]) ).
cnf(c_4476,plain,
( ~ p_14(a)
| p_10(a) ),
inference(resolve,[status(thm)],[c_3909,c_1932]) ).
cnf(c_4057,plain,
p_10(a),
inference(resolve,[status(thm)],[c_2842,c_4476]) ).
cnf(c_4477,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ p_8(a)
| q_6(a) ),
inference(resolve,[status(thm)],[c_2842,c_1795]) ).
cnf(c_4478,plain,
( ~ q_12(a)
| ~ p_10(a)
| q_6(a) ),
inference(resolve,[status(thm)],[c_4037,c_4477]) ).
cnf(c_4479,plain,
( ~ q_12(a)
| q_6(a) ),
inference(resolve,[status(thm)],[c_4057,c_4478]) ).
cnf(c_4066,plain,
q_6(a),
inference(resolve,[status(thm)],[c_3908,c_4479]) ).
cnf(c_4480,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_6(a)
| q_4(a)
| ~ p_8(a) ),
inference(resolve,[status(thm)],[c_2842,c_1785]) ).
cnf(c_4481,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_6(a)
| q_4(a) ),
inference(resolve,[status(thm)],[c_4037,c_4480]) ).
cnf(c_4482,plain,
( ~ q_12(a)
| ~ p_10(a)
| q_4(a) ),
inference(resolve,[status(thm)],[c_4066,c_4481]) ).
cnf(c_4483,plain,
( ~ q_12(a)
| q_4(a) ),
inference(resolve,[status(thm)],[c_4057,c_4482]) ).
cnf(c_4070,plain,
q_4(a),
inference(resolve,[status(thm)],[c_3908,c_4483]) ).
cnf(c_4484,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_4(a)
| p_2(a)
| ~ q_6(a)
| ~ p_8(a) ),
inference(resolve,[status(thm)],[c_2842,c_1780]) ).
cnf(c_4485,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_4(a)
| p_2(a)
| ~ q_6(a) ),
inference(resolve,[status(thm)],[c_4037,c_4484]) ).
cnf(c_4486,plain,
( ~ q_12(a)
| ~ p_10(a)
| ~ q_4(a)
| p_2(a) ),
inference(resolve,[status(thm)],[c_4066,c_4485]) ).
cnf(c_4487,plain,
( ~ q_12(a)
| ~ p_10(a)
| p_2(a) ),
inference(resolve,[status(thm)],[c_4070,c_4486]) ).
cnf(c_4488,plain,
( ~ q_12(a)
| p_2(a) ),
inference(resolve,[status(thm)],[c_4057,c_4487]) ).
cnf(c_4072,plain,
p_2(a),
inference(resolve,[status(thm)],[c_3908,c_4488]) ).
cnf(c_4489,plain,
( ~ q_12(a)
| ~ p_10(a)
| q_8(a) ),
inference(resolve,[status(thm)],[c_2842,c_1770]) ).
cnf(c_4490,plain,
( ~ q_12(a)
| q_8(a) ),
inference(resolve,[status(thm)],[c_4057,c_4489]) ).
cnf(c_4076,plain,
q_8(a),
inference(resolve,[status(thm)],[c_3908,c_4490]) ).
cnf(c_4491,plain,
( ~ q_12(a)
| ~ q_4(a)
| q_2(a)
| ~ q_6(a)
| ~ q_8(a)
| ~ p_10(a) ),
inference(resolve,[status(thm)],[c_2842,c_1705]) ).
cnf(c_4492,plain,
( ~ q_12(a)
| ~ q_4(a)
| q_2(a)
| ~ q_6(a)
| ~ q_8(a) ),
inference(resolve,[status(thm)],[c_4057,c_4491]) ).
cnf(c_4493,plain,
( ~ q_12(a)
| ~ q_4(a)
| q_2(a)
| ~ q_6(a) ),
inference(resolve,[status(thm)],[c_4076,c_4492]) ).
cnf(c_4494,plain,
( ~ q_12(a)
| ~ q_4(a)
| q_2(a) ),
inference(resolve,[status(thm)],[c_4066,c_4493]) ).
cnf(c_4495,plain,
( ~ q_12(a)
| q_2(a) ),
inference(resolve,[status(thm)],[c_4070,c_4494]) ).
cnf(c_4079,plain,
q_2(a),
inference(resolve,[status(thm)],[c_3908,c_4495]) ).
cnf(c_4496,plain,
( ~ q_12(a)
| ~ p_2(a)
| p_1(a)
| ~ q_4(a)
| ~ q_6(a)
| ~ q_8(a)
| ~ p_10(a) ),
inference(resolve,[status(thm)],[c_2842,c_1696]) ).
cnf(c_4497,plain,
( ~ q_12(a)
| ~ p_2(a)
| p_1(a)
| ~ q_4(a)
| ~ q_6(a)
| ~ q_8(a) ),
inference(resolve,[status(thm)],[c_4057,c_4496]) ).
cnf(c_4498,plain,
( ~ q_12(a)
| ~ p_2(a)
| p_1(a)
| ~ q_4(a)
| ~ q_6(a) ),
inference(resolve,[status(thm)],[c_4076,c_4497]) ).
cnf(c_4499,plain,
( ~ q_12(a)
| ~ p_2(a)
| p_1(a)
| ~ q_4(a) ),
inference(resolve,[status(thm)],[c_4066,c_4498]) ).
cnf(c_4500,plain,
( ~ q_12(a)
| ~ p_2(a)
| p_1(a) ),
inference(resolve,[status(thm)],[c_4070,c_4499]) ).
cnf(c_4501,plain,
( ~ q_12(a)
| p_1(a) ),
inference(resolve,[status(thm)],[c_4072,c_4500]) ).
cnf(c_4080,plain,
p_1(a),
inference(resolve,[status(thm)],[c_3908,c_4501]) ).
cnf(c_4502,plain,
( ~ q_2(a)
| ~ p_1(a) ),
inference(resolve,[status(thm)],[c_4072,c_2850]) ).
cnf(c_4503,plain,
~ q_2(a),
inference(resolve,[status(thm)],[c_4080,c_4502]) ).
cnf(c_4471,plain,
$false,
inference(resolve,[status(thm)],[c_4079,c_4503]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN096-1.008 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n026.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 26 17:13:40 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/0.36 % Process 1538490 was started by sandbox on n026,
% 0.14/0.36 % Sat Sep 26 17:13:40 2026
% 0.14/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.36
% 0.14/0.36 % From the command line: assign(max_seconds, 300).
% 19.64/3.21
% 19.64/3.21 % SZS status Unsatisfiable for theBenchmark
% 19.64/3.21
% 19.64/3.21 % Proof 1 at 2.79 (+ 0.04) seconds.
% 19.64/3.21 % Length of proof is 104.
% 19.64/3.21 % Level of proof is 11.
% 19.64/3.21 % Maximum clause weight is 21.000.
% 19.64/3.21 % Given clauses 434.
% 19.64/3.21
% 19.64/3.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------