%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN100-1.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:37:03 AM UTC 2026
% Result : Unsatisfiable 0.15s 10.48s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 21
% Syntax : Number of formulae : 92 ( 15 unt; 0 def)
% Number of atoms : 274 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 371 ( 189 ~; 182 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 54 ( 0 sgn 18 !; 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_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_7,axiom,
! [VAR_0] :
( ~ q_5(VAR_0)
| ~ p_4(VAR_0)
| q_3(VAR_0) ),
file('theBenchmark.p',m_s3_type12_7) ).
cnf(c_15,plain,
( ~ q_5(A)
| ~ p_4(A)
| q_3(A) ),
inference(clausify,[status(thm)],[m_s3_type12_7]) ).
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]) ).
fof(m_s3_type11_4,axiom,
! [VAR_0] :
( ~ q_3(VAR_0)
| ~ q_2(VAR_0)
| p_1(VAR_0) ),
file('theBenchmark.p',m_s3_type11_4) ).
cnf(c_19,plain,
( ~ q_3(A)
| ~ q_2(A)
| p_1(A) ),
inference(clausify,[status(thm)],[m_s3_type11_4]) ).
fof(m_s3_type11_11,axiom,
! [VAR_0] :
( ~ p_7(VAR_0)
| ~ p_6(VAR_0)
| p_5(VAR_0) ),
file('theBenchmark.p',m_s3_type11_11) ).
cnf(c_20,plain,
( ~ p_7(A)
| ~ p_6(A)
| p_5(A) ),
inference(clausify,[status(thm)],[m_s3_type11_11]) ).
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_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_33,plain,
( ~ p_7(A)
| ~ q_6(A)
| q_5(A) ),
inference(clausify,[status(thm)],[m_s3_type12_12]) ).
cnf(c_38,plain,
( ~ q_5(A)
| ~ q_4(A)
| ~ q_4(A)
| q_2(A) ),
inference(resolve,[status(thm)],[c_13,c_11]) ).
fof(m_s3_type12_11,axiom,
! [VAR_0] :
( ~ q_7(VAR_0)
| ~ p_6(VAR_0)
| q_5(VAR_0) ),
file('theBenchmark.p',m_s3_type12_11) ).
cnf(c_39,plain,
( ~ q_7(A)
| ~ p_6(A)
| q_5(A) ),
inference(clausify,[status(thm)],[m_s3_type12_11]) ).
fof(m_s3_type12_10,axiom,
! [VAR_0] :
( ~ p_6(VAR_0)
| ~ q_5(VAR_0)
| q_4(VAR_0) ),
file('theBenchmark.p',m_s3_type12_10) ).
cnf(c_40,plain,
( ~ p_6(A)
| ~ q_5(A)
| q_4(A) ),
inference(clausify,[status(thm)],[m_s3_type12_10]) ).
fof(m_s3_type11_10,axiom,
! [VAR_0] :
( ~ q_6(VAR_0)
| ~ q_5(VAR_0)
| p_4(VAR_0) ),
file('theBenchmark.p',m_s3_type11_10) ).
cnf(c_41,plain,
( ~ q_6(A)
| ~ q_5(A)
| p_4(A) ),
inference(clausify,[status(thm)],[m_s3_type11_10]) ).
cnf(c_45,plain,
( ~ q_5(A)
| ~ p_4(A)
| ~ q_2(A)
| p_1(A) ),
inference(resolve,[status(thm)],[c_19,c_15]) ).
fof(m_s3_type11_15,axiom,
! [VAR_0] :
( ~ p_9(VAR_0)
| ~ p_8(VAR_0)
| p_7(VAR_0) ),
file('theBenchmark.p',m_s3_type11_15) ).
cnf(c_46,plain,
( ~ p_9(A)
| ~ p_8(A)
| p_7(A) ),
inference(clausify,[status(thm)],[m_s3_type11_15]) ).
cnf(c_52,plain,
( ~ q_4(A)
| ~ q_4(A)
| q_2(A)
| ~ p_7(A)
| ~ q_6(A) ),
inference(resolve,[status(thm)],[c_33,c_38]) ).
cnf(c_54,plain,
( ~ p_7(A)
| ~ q_6(A)
| ~ q_6(A)
| p_4(A) ),
inference(resolve,[status(thm)],[c_41,c_33]) ).
cnf(c_57,plain,
( ~ p_7(A)
| ~ q_6(A)
| ~ p_4(A)
| ~ q_2(A)
| p_1(A) ),
inference(resolve,[status(thm)],[c_45,c_33]) ).
cnf(c_63,plain,
( ~ q_4(A)
| ~ q_4(A)
| p_2(A)
| ~ p_7(A)
| ~ p_6(A) ),
inference(resolve,[status(thm)],[c_20,c_24]) ).
fof(m_s3_type12_16,axiom,
! [VAR_0] :
( ~ p_9(VAR_0)
| ~ q_8(VAR_0)
| q_7(VAR_0) ),
file('theBenchmark.p',m_s3_type12_16) ).
cnf(c_70,plain,
( ~ p_9(A)
| ~ q_8(A)
| q_7(A) ),
inference(clausify,[status(thm)],[m_s3_type12_16]) ).
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_82,plain,
( ~ p_8(A)
| ~ q_7(A)
| q_6(A) ),
inference(clausify,[status(thm)],[m_s3_type12_14]) ).
fof(m_s3_type11_14,axiom,
! [VAR_0] :
( ~ q_8(VAR_0)
| ~ q_7(VAR_0)
| p_6(VAR_0) ),
file('theBenchmark.p',m_s3_type11_14) ).
cnf(c_83,plain,
( ~ q_8(A)
| ~ q_7(A)
| p_6(A) ),
inference(clausify,[status(thm)],[m_s3_type11_14]) ).
cnf(c_89,plain,
( ~ q_7(A)
| ~ p_6(A)
| ~ p_6(A)
| q_4(A) ),
inference(resolve,[status(thm)],[c_40,c_39]) ).
cnf(c_105,plain,
( ~ p_9(A)
| ~ q_8(A)
| ~ p_8(A)
| q_6(A) ),
inference(resolve,[status(thm)],[c_82,c_70]) ).
cnf(c_106,plain,
( ~ p_9(A)
| ~ q_8(A)
| ~ q_8(A)
| p_6(A) ),
inference(resolve,[status(thm)],[c_83,c_70]) ).
cnf(c_112,plain,
( ~ p_9(A)
| ~ q_8(A)
| ~ p_6(A)
| ~ p_6(A)
| q_4(A) ),
inference(resolve,[status(thm)],[c_89,c_70]) ).
fof(m_t3_2,axiom,
p_9(a),
file('theBenchmark.p',m_t3_2) ).
cnf(c_116,plain,
p_9(a),
inference(clausify,[status(thm)],[m_t3_2]) ).
cnf(c_122,plain,
( ~ q_4(A)
| ~ q_4(A)
| q_2(A)
| ~ q_6(A)
| ~ p_9(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_46,c_52]) ).
cnf(c_124,plain,
( ~ q_6(A)
| ~ q_6(A)
| p_4(A)
| ~ p_9(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_46,c_54]) ).
cnf(c_127,plain,
( ~ q_6(A)
| ~ p_4(A)
| ~ q_2(A)
| p_1(A)
| ~ p_9(A)
| ~ p_8(A) ),
inference(resolve,[status(thm)],[c_46,c_57]) ).
cnf(c_132,plain,
( ~ p_9(A)
| ~ p_8(A)
| ~ q_4(A)
| ~ q_4(A)
| p_2(A)
| ~ p_6(A) ),
inference(resolve,[status(thm)],[c_63,c_46]) ).
cnf(c_539,plain,
( ~ p_2(A)
| ~ p_1(A)
| ~ q_2(A)
| ~ p_1(A) ),
inference(resolve,[status(thm)],[c_7,c_5]) ).
cnf(c_540,plain,
( ~ p_2(A)
| ~ q_2(A)
| ~ p_1(A) ),
inference(copy,[status(thm)],[c_539]) ).
fof(m_t3_1,axiom,
p_8(a),
file('theBenchmark.p',m_t3_1) ).
cnf(c_545,plain,
p_8(a),
inference(clausify,[status(thm)],[m_t3_1]) ).
fof(m_t3_3,axiom,
q_8(a),
file('theBenchmark.p',m_t3_3) ).
cnf(c_546,plain,
q_8(a),
inference(clausify,[status(thm)],[m_t3_3]) ).
cnf(c_582,plain,
( ~ q_8(a)
| ~ p_8(a)
| q_6(a) ),
inference(resolve,[status(thm)],[c_116,c_105]) ).
cnf(c_744,plain,
( ~ q_8(a)
| q_6(a) ),
inference(resolve,[status(thm)],[c_545,c_582]) ).
cnf(c_583,plain,
q_6(a),
inference(resolve,[status(thm)],[c_546,c_744]) ).
cnf(c_584,plain,
( ~ q_8(a)
| ~ q_8(a)
| p_6(a) ),
inference(resolve,[status(thm)],[c_116,c_106]) ).
cnf(c_745,plain,
( ~ q_8(a)
| p_6(a) ),
inference(copy,[status(thm)],[c_584]) ).
cnf(c_585,plain,
p_6(a),
inference(resolve,[status(thm)],[c_546,c_745]) ).
cnf(c_592,plain,
( ~ q_8(a)
| ~ p_6(a)
| ~ p_6(a)
| q_4(a) ),
inference(resolve,[status(thm)],[c_116,c_112]) ).
cnf(c_746,plain,
( ~ q_8(a)
| ~ p_6(a)
| q_4(a) ),
inference(copy,[status(thm)],[c_592]) ).
cnf(c_747,plain,
( ~ q_8(a)
| q_4(a) ),
inference(resolve,[status(thm)],[c_585,c_746]) ).
cnf(c_593,plain,
q_4(a),
inference(resolve,[status(thm)],[c_546,c_747]) ).
cnf(c_604,plain,
( ~ q_4(a)
| ~ q_4(a)
| q_2(a)
| ~ q_6(a)
| ~ p_8(a) ),
inference(resolve,[status(thm)],[c_122,c_116]) ).
cnf(c_748,plain,
( ~ q_4(a)
| q_2(a)
| ~ q_6(a)
| ~ p_8(a) ),
inference(copy,[status(thm)],[c_604]) ).
cnf(c_749,plain,
( ~ q_4(a)
| q_2(a)
| ~ q_6(a) ),
inference(resolve,[status(thm)],[c_545,c_748]) ).
cnf(c_750,plain,
( ~ q_4(a)
| q_2(a) ),
inference(resolve,[status(thm)],[c_583,c_749]) ).
cnf(c_605,plain,
q_2(a),
inference(resolve,[status(thm)],[c_593,c_750]) ).
cnf(c_609,plain,
( ~ q_6(a)
| ~ q_6(a)
| p_4(a)
| ~ p_8(a) ),
inference(resolve,[status(thm)],[c_124,c_116]) ).
cnf(c_751,plain,
( ~ q_6(a)
| p_4(a)
| ~ p_8(a) ),
inference(copy,[status(thm)],[c_609]) ).
cnf(c_752,plain,
( ~ q_6(a)
| p_4(a) ),
inference(resolve,[status(thm)],[c_545,c_751]) ).
cnf(c_610,plain,
p_4(a),
inference(resolve,[status(thm)],[c_583,c_752]) ).
cnf(c_618,plain,
( ~ q_6(a)
| ~ p_4(a)
| ~ q_2(a)
| p_1(a)
| ~ p_8(a) ),
inference(resolve,[status(thm)],[c_127,c_116]) ).
cnf(c_753,plain,
( ~ q_6(a)
| ~ p_4(a)
| ~ q_2(a)
| p_1(a) ),
inference(resolve,[status(thm)],[c_545,c_618]) ).
cnf(c_754,plain,
( ~ q_6(a)
| ~ p_4(a)
| p_1(a) ),
inference(resolve,[status(thm)],[c_605,c_753]) ).
cnf(c_755,plain,
( ~ q_6(a)
| p_1(a) ),
inference(resolve,[status(thm)],[c_610,c_754]) ).
cnf(c_619,plain,
p_1(a),
inference(resolve,[status(thm)],[c_583,c_755]) ).
cnf(c_626,plain,
( ~ p_8(a)
| ~ q_4(a)
| ~ q_4(a)
| p_2(a)
| ~ p_6(a) ),
inference(resolve,[status(thm)],[c_132,c_116]) ).
cnf(c_756,plain,
( ~ p_8(a)
| ~ q_4(a)
| p_2(a)
| ~ p_6(a) ),
inference(copy,[status(thm)],[c_626]) ).
cnf(c_757,plain,
( ~ p_8(a)
| ~ q_4(a)
| p_2(a) ),
inference(resolve,[status(thm)],[c_585,c_756]) ).
cnf(c_758,plain,
( ~ p_8(a)
| p_2(a) ),
inference(resolve,[status(thm)],[c_593,c_757]) ).
cnf(c_627,plain,
p_2(a),
inference(resolve,[status(thm)],[c_545,c_758]) ).
cnf(c_759,plain,
( ~ p_2(a)
| ~ q_2(a) ),
inference(resolve,[status(thm)],[c_619,c_540]) ).
cnf(c_760,plain,
~ p_2(a),
inference(resolve,[status(thm)],[c_605,c_759]) ).
cnf(c_743,plain,
$false,
inference(resolve,[status(thm)],[c_627,c_760]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN100-1.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.39 % Computer : n002.cluster.edu
% 0.10/10.39 % Model : x86_64 x86_64
% 0.10/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.39 % Memory : 8046.5625MB
% 0.10/10.39 % OS : Linux 6.8.0-71-generic
% 0.10/10.39 % CPULimit : 300
% 0.10/10.39 % WCLimit : 300
% 0.10/10.39 % DateTime : Sat Sep 26 17:14:31 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.10/10.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/10.39 % Process 2283904 was started by sandbox2 on n002,
% 0.10/10.39 % Sat Sep 26 17:14:31 2026
% 0.10/10.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/10.40
% 0.15/10.40 % From the command line: assign(max_seconds, 300).
% 0.15/10.48
% 0.15/10.48 % SZS status Unsatisfiable for theBenchmark
% 0.15/10.48
% 0.15/10.48 % Proof 1 at 0.07 (+ 0.01) seconds.
% 0.15/10.48 % Length of proof is 54.
% 0.15/10.48 % Level of proof is 7.
% 0.15/10.48 % Maximum clause weight is 6.000.
% 0.15/10.48 % Given clauses 84.
% 0.15/10.48
% 0.15/10.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------