%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN090-1.008 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 : Thu Sep 24 09:09:28 AM UTC 2026
% Result : Unsatisfiable 0.07s 0.37s
% Output : Proof 0.07s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(s3_goal_1,negated_conjecture,
( ~ q_0
| ~ p_0 ),
file('theBenchmark.p',s3_goal_1) ).
cnf(s3_type11_1,axiom,
( ~ p_2
| ~ p_1
| p_0 ),
file('theBenchmark.p',s3_type11_1) ).
cnf(s3_type11_2,axiom,
( ~ q_2
| ~ q_1
| p_0 ),
file('theBenchmark.p',s3_type11_2) ).
cnf(s3_type11_3,axiom,
( ~ p_3
| ~ p_2
| p_1 ),
file('theBenchmark.p',s3_type11_3) ).
cnf(s3_type11_4,axiom,
( ~ q_3
| ~ q_2
| p_1 ),
file('theBenchmark.p',s3_type11_4) ).
cnf(s3_type11_5,axiom,
( ~ p_4
| ~ p_3
| p_2 ),
file('theBenchmark.p',s3_type11_5) ).
cnf(s3_type11_6,axiom,
( ~ q_4
| ~ q_3
| p_2 ),
file('theBenchmark.p',s3_type11_6) ).
cnf(s3_type11_7,axiom,
( ~ p_5
| ~ p_4
| p_3 ),
file('theBenchmark.p',s3_type11_7) ).
cnf(s3_type11_8,axiom,
( ~ q_5
| ~ q_4
| p_3 ),
file('theBenchmark.p',s3_type11_8) ).
cnf(s3_type11_9,axiom,
( ~ p_6
| ~ p_5
| p_4 ),
file('theBenchmark.p',s3_type11_9) ).
cnf(s3_type11_10,axiom,
( ~ q_6
| ~ q_5
| p_4 ),
file('theBenchmark.p',s3_type11_10) ).
cnf(s3_type11_11,axiom,
( ~ p_7
| ~ p_6
| p_5 ),
file('theBenchmark.p',s3_type11_11) ).
cnf(s3_type11_12,axiom,
( ~ q_7
| ~ q_6
| p_5 ),
file('theBenchmark.p',s3_type11_12) ).
cnf(s3_type11_13,axiom,
( ~ p_8
| ~ p_7
| p_6 ),
file('theBenchmark.p',s3_type11_13) ).
cnf(s3_type11_14,axiom,
( ~ q_8
| ~ q_7
| p_6 ),
file('theBenchmark.p',s3_type11_14) ).
cnf(s3_type11_15,axiom,
( ~ p_9
| ~ p_8
| p_7 ),
file('theBenchmark.p',s3_type11_15) ).
cnf(s3_type11_16,axiom,
( ~ q_9
| ~ q_8
| p_7 ),
file('theBenchmark.p',s3_type11_16) ).
cnf(s3_type11_17,axiom,
( ~ p_10
| ~ p_9
| p_8 ),
file('theBenchmark.p',s3_type11_17) ).
cnf(s3_type11_18,axiom,
( ~ q_10
| ~ q_9
| p_8 ),
file('theBenchmark.p',s3_type11_18) ).
cnf(s3_type11_19,axiom,
( ~ p_11
| ~ p_10
| p_9 ),
file('theBenchmark.p',s3_type11_19) ).
cnf(s3_type11_20,axiom,
( ~ q_11
| ~ q_10
| p_9 ),
file('theBenchmark.p',s3_type11_20) ).
cnf(s3_type11_21,axiom,
( ~ p_12
| ~ p_11
| p_10 ),
file('theBenchmark.p',s3_type11_21) ).
cnf(s3_type11_22,axiom,
( ~ q_12
| ~ q_11
| p_10 ),
file('theBenchmark.p',s3_type11_22) ).
cnf(s3_type11_23,axiom,
( ~ p_13
| ~ p_12
| p_11 ),
file('theBenchmark.p',s3_type11_23) ).
cnf(s3_type11_24,axiom,
( ~ q_13
| ~ q_12
| p_11 ),
file('theBenchmark.p',s3_type11_24) ).
cnf(s3_type11_25,axiom,
( ~ p_14
| ~ p_13
| p_12 ),
file('theBenchmark.p',s3_type11_25) ).
cnf(s3_type11_26,axiom,
( ~ q_14
| ~ q_13
| p_12 ),
file('theBenchmark.p',s3_type11_26) ).
cnf(s3_type11_27,axiom,
( ~ p_15
| ~ p_14
| p_13 ),
file('theBenchmark.p',s3_type11_27) ).
cnf(s3_type11_28,axiom,
( ~ q_15
| ~ q_14
| p_13 ),
file('theBenchmark.p',s3_type11_28) ).
cnf(s3_type12_1,axiom,
( ~ q_2
| ~ p_1
| q_0 ),
file('theBenchmark.p',s3_type12_1) ).
cnf(s3_type12_2,axiom,
( ~ p_2
| ~ q_1
| q_0 ),
file('theBenchmark.p',s3_type12_2) ).
cnf(s3_type12_3,axiom,
( ~ q_3
| ~ p_2
| q_1 ),
file('theBenchmark.p',s3_type12_3) ).
cnf(s3_type12_4,axiom,
( ~ p_3
| ~ q_2
| q_1 ),
file('theBenchmark.p',s3_type12_4) ).
cnf(s3_type12_5,axiom,
( ~ q_4
| ~ p_3
| q_2 ),
file('theBenchmark.p',s3_type12_5) ).
cnf(s3_type12_6,axiom,
( ~ p_4
| ~ q_3
| q_2 ),
file('theBenchmark.p',s3_type12_6) ).
cnf(s3_type12_7,axiom,
( ~ q_5
| ~ p_4
| q_3 ),
file('theBenchmark.p',s3_type12_7) ).
cnf(s3_type12_8,axiom,
( ~ p_5
| ~ q_4
| q_3 ),
file('theBenchmark.p',s3_type12_8) ).
cnf(s3_type12_9,axiom,
( ~ q_6
| ~ p_5
| q_4 ),
file('theBenchmark.p',s3_type12_9) ).
cnf(s3_type12_10,axiom,
( ~ p_6
| ~ q_5
| q_4 ),
file('theBenchmark.p',s3_type12_10) ).
cnf(s3_type12_11,axiom,
( ~ q_7
| ~ p_6
| q_5 ),
file('theBenchmark.p',s3_type12_11) ).
cnf(s3_type12_12,axiom,
( ~ p_7
| ~ q_6
| q_5 ),
file('theBenchmark.p',s3_type12_12) ).
cnf(s3_type12_13,axiom,
( ~ q_8
| ~ p_7
| q_6 ),
file('theBenchmark.p',s3_type12_13) ).
cnf(s3_type12_14,axiom,
( ~ p_8
| ~ q_7
| q_6 ),
file('theBenchmark.p',s3_type12_14) ).
cnf(s3_type12_15,axiom,
( ~ q_9
| ~ p_8
| q_7 ),
file('theBenchmark.p',s3_type12_15) ).
cnf(s3_type12_16,axiom,
( ~ p_9
| ~ q_8
| q_7 ),
file('theBenchmark.p',s3_type12_16) ).
cnf(s3_type12_17,axiom,
( ~ q_10
| ~ p_9
| q_8 ),
file('theBenchmark.p',s3_type12_17) ).
cnf(s3_type12_18,axiom,
( ~ p_10
| ~ q_9
| q_8 ),
file('theBenchmark.p',s3_type12_18) ).
cnf(s3_type12_19,axiom,
( ~ q_11
| ~ p_10
| q_9 ),
file('theBenchmark.p',s3_type12_19) ).
cnf(s3_type12_20,axiom,
( ~ p_11
| ~ q_10
| q_9 ),
file('theBenchmark.p',s3_type12_20) ).
cnf(s3_type12_21,axiom,
( ~ q_12
| ~ p_11
| q_10 ),
file('theBenchmark.p',s3_type12_21) ).
cnf(s3_type12_22,axiom,
( ~ p_12
| ~ q_11
| q_10 ),
file('theBenchmark.p',s3_type12_22) ).
cnf(s3_type12_23,axiom,
( ~ q_13
| ~ p_12
| q_11 ),
file('theBenchmark.p',s3_type12_23) ).
cnf(s3_type12_24,axiom,
( ~ p_13
| ~ q_12
| q_11 ),
file('theBenchmark.p',s3_type12_24) ).
cnf(s3_type12_25,axiom,
( ~ q_14
| ~ p_13
| q_12 ),
file('theBenchmark.p',s3_type12_25) ).
cnf(s3_type12_26,axiom,
( ~ p_14
| ~ q_13
| q_12 ),
file('theBenchmark.p',s3_type12_26) ).
cnf(s3_type12_27,axiom,
( ~ q_15
| ~ p_14
| q_13 ),
file('theBenchmark.p',s3_type12_27) ).
cnf(s3_type12_28,axiom,
( ~ p_15
| ~ q_14
| q_13 ),
file('theBenchmark.p',s3_type12_28) ).
cnf(s3_type2_1,axiom,
( ~ p_7
| p_15 ),
file('theBenchmark.p',s3_type2_1) ).
cnf(s3_type2_2,axiom,
( ~ p_8
| p_16 ),
file('theBenchmark.p',s3_type2_2) ).
cnf(s3_type2_3,axiom,
( ~ q_7
| q_15 ),
file('theBenchmark.p',s3_type2_3) ).
cnf(s3_type2_4,axiom,
( ~ q_8
| q_16 ),
file('theBenchmark.p',s3_type2_4) ).
cnf(t3_1,axiom,
p_14,
file('theBenchmark.p',t3_1) ).
cnf(t3_2,axiom,
p_15,
file('theBenchmark.p',t3_2) ).
cnf(t3_3,axiom,
q_14,
file('theBenchmark.p',t3_3) ).
cnf(t3_4,axiom,
q_15,
file('theBenchmark.p',t3_4) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN090-1.008 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.03 This is a CNF_UNS_PRP problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n004.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sun Sep 20 06:25:04 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.37 % SZS status Unsatisfiable for theBenchmark
% 0.07/0.37 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------