%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN100-1.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:29 AM UTC 2026
% Result : Unsatisfiable 0.14s 15.44s
% Output : Proof 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(m_s3_goal_1,negated_conjecture,
( ~ q_0(X)
| ~ p_0(X) ),
file('theBenchmark.p',m_s3_goal_1) ).
cnf(m_s3_type11_1,axiom,
( ~ p_2(X)
| ~ p_1(X)
| p_0(X) ),
file('theBenchmark.p',m_s3_type11_1) ).
cnf(m_s3_type11_2,axiom,
( ~ q_2(X)
| ~ q_1(X)
| p_0(X) ),
file('theBenchmark.p',m_s3_type11_2) ).
cnf(m_s3_type11_3,axiom,
( ~ p_3(X)
| ~ p_2(X)
| p_1(X) ),
file('theBenchmark.p',m_s3_type11_3) ).
cnf(m_s3_type11_4,axiom,
( ~ q_3(X)
| ~ q_2(X)
| p_1(X) ),
file('theBenchmark.p',m_s3_type11_4) ).
cnf(m_s3_type11_5,axiom,
( ~ p_4(X)
| ~ p_3(X)
| p_2(X) ),
file('theBenchmark.p',m_s3_type11_5) ).
cnf(m_s3_type11_6,axiom,
( ~ q_4(X)
| ~ q_3(X)
| p_2(X) ),
file('theBenchmark.p',m_s3_type11_6) ).
cnf(m_s3_type11_7,axiom,
( ~ p_5(X)
| ~ p_4(X)
| p_3(X) ),
file('theBenchmark.p',m_s3_type11_7) ).
cnf(m_s3_type11_8,axiom,
( ~ q_5(X)
| ~ q_4(X)
| p_3(X) ),
file('theBenchmark.p',m_s3_type11_8) ).
cnf(m_s3_type11_9,axiom,
( ~ p_6(X)
| ~ p_5(X)
| p_4(X) ),
file('theBenchmark.p',m_s3_type11_9) ).
cnf(m_s3_type11_10,axiom,
( ~ q_6(X)
| ~ q_5(X)
| p_4(X) ),
file('theBenchmark.p',m_s3_type11_10) ).
cnf(m_s3_type11_11,axiom,
( ~ p_7(X)
| ~ p_6(X)
| p_5(X) ),
file('theBenchmark.p',m_s3_type11_11) ).
cnf(m_s3_type11_12,axiom,
( ~ q_7(X)
| ~ q_6(X)
| p_5(X) ),
file('theBenchmark.p',m_s3_type11_12) ).
cnf(m_s3_type11_13,axiom,
( ~ p_8(X)
| ~ p_7(X)
| p_6(X) ),
file('theBenchmark.p',m_s3_type11_13) ).
cnf(m_s3_type11_14,axiom,
( ~ q_8(X)
| ~ q_7(X)
| p_6(X) ),
file('theBenchmark.p',m_s3_type11_14) ).
cnf(m_s3_type11_15,axiom,
( ~ p_9(X)
| ~ p_8(X)
| p_7(X) ),
file('theBenchmark.p',m_s3_type11_15) ).
cnf(m_s3_type11_16,axiom,
( ~ q_9(X)
| ~ q_8(X)
| p_7(X) ),
file('theBenchmark.p',m_s3_type11_16) ).
cnf(m_s3_type12_1,axiom,
( ~ q_2(X)
| ~ p_1(X)
| q_0(X) ),
file('theBenchmark.p',m_s3_type12_1) ).
cnf(m_s3_type12_2,axiom,
( ~ p_2(X)
| ~ q_1(X)
| q_0(X) ),
file('theBenchmark.p',m_s3_type12_2) ).
cnf(m_s3_type12_3,axiom,
( ~ q_3(X)
| ~ p_2(X)
| q_1(X) ),
file('theBenchmark.p',m_s3_type12_3) ).
cnf(m_s3_type12_4,axiom,
( ~ p_3(X)
| ~ q_2(X)
| q_1(X) ),
file('theBenchmark.p',m_s3_type12_4) ).
cnf(m_s3_type12_5,axiom,
( ~ q_4(X)
| ~ p_3(X)
| q_2(X) ),
file('theBenchmark.p',m_s3_type12_5) ).
cnf(m_s3_type12_6,axiom,
( ~ p_4(X)
| ~ q_3(X)
| q_2(X) ),
file('theBenchmark.p',m_s3_type12_6) ).
cnf(m_s3_type12_7,axiom,
( ~ q_5(X)
| ~ p_4(X)
| q_3(X) ),
file('theBenchmark.p',m_s3_type12_7) ).
cnf(m_s3_type12_8,axiom,
( ~ p_5(X)
| ~ q_4(X)
| q_3(X) ),
file('theBenchmark.p',m_s3_type12_8) ).
cnf(m_s3_type12_9,axiom,
( ~ q_6(X)
| ~ p_5(X)
| q_4(X) ),
file('theBenchmark.p',m_s3_type12_9) ).
cnf(m_s3_type12_10,axiom,
( ~ p_6(X)
| ~ q_5(X)
| q_4(X) ),
file('theBenchmark.p',m_s3_type12_10) ).
cnf(m_s3_type12_11,axiom,
( ~ q_7(X)
| ~ p_6(X)
| q_5(X) ),
file('theBenchmark.p',m_s3_type12_11) ).
cnf(m_s3_type12_12,axiom,
( ~ p_7(X)
| ~ q_6(X)
| q_5(X) ),
file('theBenchmark.p',m_s3_type12_12) ).
cnf(m_s3_type12_13,axiom,
( ~ q_8(X)
| ~ p_7(X)
| q_6(X) ),
file('theBenchmark.p',m_s3_type12_13) ).
cnf(m_s3_type12_14,axiom,
( ~ p_8(X)
| ~ q_7(X)
| q_6(X) ),
file('theBenchmark.p',m_s3_type12_14) ).
cnf(m_s3_type12_15,axiom,
( ~ q_9(X)
| ~ p_8(X)
| q_7(X) ),
file('theBenchmark.p',m_s3_type12_15) ).
cnf(m_s3_type12_16,axiom,
( ~ p_9(X)
| ~ q_8(X)
| q_7(X) ),
file('theBenchmark.p',m_s3_type12_16) ).
cnf(m_s3_type2_1,axiom,
( ~ p_4(X)
| p_9(X) ),
file('theBenchmark.p',m_s3_type2_1) ).
cnf(m_s3_type2_2,axiom,
( ~ p_5(X)
| p_10(X) ),
file('theBenchmark.p',m_s3_type2_2) ).
cnf(m_s3_type2_3,axiom,
( ~ q_4(X)
| q_9(X) ),
file('theBenchmark.p',m_s3_type2_3) ).
cnf(m_s3_type2_4,axiom,
( ~ q_5(X)
| q_10(X) ),
file('theBenchmark.p',m_s3_type2_4) ).
cnf(m_t3_1,axiom,
p_8(a),
file('theBenchmark.p',m_t3_1) ).
cnf(m_t3_2,axiom,
p_9(a),
file('theBenchmark.p',m_t3_2) ).
cnf(m_t3_3,axiom,
q_8(a),
file('theBenchmark.p',m_t3_3) ).
cnf(m_t3_4,axiom,
q_9(a),
file('theBenchmark.p',m_t3_4) ).
cnf(sym_m_s3_goal_1,axiom,
( sym_q_0(X)
| sym_p_0(X) ),
file('theBenchmark.p',sym_m_s3_goal_1) ).
cnf(sym_m_s3_type11_1,axiom,
( sym_p_2(X)
| sym_p_1(X)
| ~ sym_p_0(X) ),
file('theBenchmark.p',sym_m_s3_type11_1) ).
cnf(sym_m_s3_type11_2,axiom,
( sym_q_2(X)
| sym_q_1(X)
| ~ sym_p_0(X) ),
file('theBenchmark.p',sym_m_s3_type11_2) ).
cnf(sym_m_s3_type11_3,axiom,
( sym_p_3(X)
| sym_p_2(X)
| ~ sym_p_1(X) ),
file('theBenchmark.p',sym_m_s3_type11_3) ).
cnf(sym_m_s3_type11_4,axiom,
( sym_q_3(X)
| sym_q_2(X)
| ~ sym_p_1(X) ),
file('theBenchmark.p',sym_m_s3_type11_4) ).
cnf(sym_m_s3_type11_5,axiom,
( sym_p_4(X)
| sym_p_3(X)
| ~ sym_p_2(X) ),
file('theBenchmark.p',sym_m_s3_type11_5) ).
cnf(sym_m_s3_type11_6,axiom,
( sym_q_4(X)
| sym_q_3(X)
| ~ sym_p_2(X) ),
file('theBenchmark.p',sym_m_s3_type11_6) ).
cnf(sym_m_s3_type11_7,axiom,
( sym_p_5(X)
| sym_p_4(X)
| ~ sym_p_3(X) ),
file('theBenchmark.p',sym_m_s3_type11_7) ).
cnf(sym_m_s3_type11_8,axiom,
( sym_q_5(X)
| sym_q_4(X)
| ~ sym_p_3(X) ),
file('theBenchmark.p',sym_m_s3_type11_8) ).
cnf(sym_m_s3_type11_9,axiom,
( sym_p_6(X)
| sym_p_5(X)
| ~ sym_p_4(X) ),
file('theBenchmark.p',sym_m_s3_type11_9) ).
cnf(sym_m_s3_type11_10,axiom,
( sym_q_6(X)
| sym_q_5(X)
| ~ sym_p_4(X) ),
file('theBenchmark.p',sym_m_s3_type11_10) ).
cnf(sym_m_s3_type11_11,axiom,
( sym_p_7(X)
| sym_p_6(X)
| ~ sym_p_5(X) ),
file('theBenchmark.p',sym_m_s3_type11_11) ).
cnf(sym_m_s3_type11_12,axiom,
( sym_q_7(X)
| sym_q_6(X)
| ~ sym_p_5(X) ),
file('theBenchmark.p',sym_m_s3_type11_12) ).
cnf(sym_m_s3_type11_13,axiom,
( sym_p_8(X)
| sym_p_7(X)
| ~ sym_p_6(X) ),
file('theBenchmark.p',sym_m_s3_type11_13) ).
cnf(sym_m_s3_type11_14,axiom,
( sym_q_8(X)
| sym_q_7(X)
| ~ sym_p_6(X) ),
file('theBenchmark.p',sym_m_s3_type11_14) ).
cnf(sym_m_s3_type11_15,axiom,
( sym_p_9(X)
| sym_p_8(X)
| ~ sym_p_7(X) ),
file('theBenchmark.p',sym_m_s3_type11_15) ).
cnf(sym_m_s3_type11_16,axiom,
( sym_q_9(X)
| sym_q_8(X)
| ~ sym_p_7(X) ),
file('theBenchmark.p',sym_m_s3_type11_16) ).
cnf(sym_m_s3_type12_1,axiom,
( sym_q_2(X)
| sym_p_1(X)
| ~ sym_q_0(X) ),
file('theBenchmark.p',sym_m_s3_type12_1) ).
cnf(sym_m_s3_type12_2,axiom,
( sym_p_2(X)
| sym_q_1(X)
| ~ sym_q_0(X) ),
file('theBenchmark.p',sym_m_s3_type12_2) ).
cnf(sym_m_s3_type12_3,axiom,
( sym_q_3(X)
| sym_p_2(X)
| ~ sym_q_1(X) ),
file('theBenchmark.p',sym_m_s3_type12_3) ).
cnf(sym_m_s3_type12_4,axiom,
( sym_p_3(X)
| sym_q_2(X)
| ~ sym_q_1(X) ),
file('theBenchmark.p',sym_m_s3_type12_4) ).
cnf(sym_m_s3_type12_5,axiom,
( sym_q_4(X)
| sym_p_3(X)
| ~ sym_q_2(X) ),
file('theBenchmark.p',sym_m_s3_type12_5) ).
cnf(sym_m_s3_type12_6,axiom,
( sym_p_4(X)
| sym_q_3(X)
| ~ sym_q_2(X) ),
file('theBenchmark.p',sym_m_s3_type12_6) ).
cnf(sym_m_s3_type12_7,axiom,
( sym_q_5(X)
| sym_p_4(X)
| ~ sym_q_3(X) ),
file('theBenchmark.p',sym_m_s3_type12_7) ).
cnf(sym_m_s3_type12_8,axiom,
( sym_p_5(X)
| sym_q_4(X)
| ~ sym_q_3(X) ),
file('theBenchmark.p',sym_m_s3_type12_8) ).
cnf(sym_m_s3_type12_9,axiom,
( sym_q_6(X)
| sym_p_5(X)
| ~ sym_q_4(X) ),
file('theBenchmark.p',sym_m_s3_type12_9) ).
cnf(sym_m_s3_type12_10,axiom,
( sym_p_6(X)
| sym_q_5(X)
| ~ sym_q_4(X) ),
file('theBenchmark.p',sym_m_s3_type12_10) ).
cnf(sym_m_s3_type12_11,axiom,
( sym_q_7(X)
| sym_p_6(X)
| ~ sym_q_5(X) ),
file('theBenchmark.p',sym_m_s3_type12_11) ).
cnf(sym_m_s3_type12_12,axiom,
( sym_p_7(X)
| sym_q_6(X)
| ~ sym_q_5(X) ),
file('theBenchmark.p',sym_m_s3_type12_12) ).
cnf(sym_m_s3_type12_13,axiom,
( sym_q_8(X)
| sym_p_7(X)
| ~ sym_q_6(X) ),
file('theBenchmark.p',sym_m_s3_type12_13) ).
cnf(sym_m_s3_type12_14,axiom,
( sym_p_8(X)
| sym_q_7(X)
| ~ sym_q_6(X) ),
file('theBenchmark.p',sym_m_s3_type12_14) ).
cnf(sym_m_s3_type12_15,axiom,
( sym_q_9(X)
| sym_p_8(X)
| ~ sym_q_7(X) ),
file('theBenchmark.p',sym_m_s3_type12_15) ).
cnf(sym_m_s3_type12_16,axiom,
( sym_p_9(X)
| sym_q_8(X)
| ~ sym_q_7(X) ),
file('theBenchmark.p',sym_m_s3_type12_16) ).
cnf(sym_m_s3_type2_1,axiom,
( sym_p_4(X)
| ~ sym_p_9(X) ),
file('theBenchmark.p',sym_m_s3_type2_1) ).
cnf(sym_m_s3_type2_2,axiom,
( sym_p_5(X)
| ~ sym_p_10(X) ),
file('theBenchmark.p',sym_m_s3_type2_2) ).
cnf(sym_m_s3_type2_3,axiom,
( sym_q_4(X)
| ~ sym_q_9(X) ),
file('theBenchmark.p',sym_m_s3_type2_3) ).
cnf(sym_m_s3_type2_4,axiom,
( sym_q_5(X)
| ~ sym_q_10(X) ),
file('theBenchmark.p',sym_m_s3_type2_4) ).
cnf(sym_m_t3_1,axiom,
~ sym_p_8(a),
file('theBenchmark.p',sym_m_t3_1) ).
cnf(sym_m_t3_2,axiom,
~ sym_p_9(a),
file('theBenchmark.p',sym_m_t3_2) ).
cnf(sym_m_t3_3,axiom,
~ sym_q_8(a),
file('theBenchmark.p',sym_m_t3_3) ).
cnf(sym_m_t3_4,axiom,
~ sym_q_9(a),
file('theBenchmark.p',sym_m_t3_4) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN100-1.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.01 This is a CNF_UNS_EPR_NEQ_NHN problem
% 0.00/0.02 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.02/15.21 % CPULimit : 300
% 0.02/15.21 % WCLimit : 300
% 0.02/15.21 % DateTime : Sun Sep 20 06:24:39 UTC 2026
% 0.02/15.22 % CPUTime :
% 0.14/15.44 % SZS status Unsatisfiable for theBenchmark
% 0.14/15.44 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------