%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN102-1.007.007 : TPTP v9.3.1. Bugfixed v1.2.0.
% 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 : n018.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:30 AM UTC 2026
% Result : Unsatisfiable 0.03s 0.40s
% Output : Proof 0.03s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(n_s3_goal_1,negated_conjecture,
( ~ q_0(a,a,a,a,a,a,a)
| ~ p_0(a,a,a,a,a,a,a) ),
file('theBenchmark.p',n_s3_goal_1) ).
cnf(n_s3_type11_1,axiom,
( ~ p_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_1(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_0(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_1) ).
cnf(n_s3_type11_2,axiom,
( ~ q_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_1(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_0(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_2) ).
cnf(n_s3_type11_3,axiom,
( ~ p_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_1(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_3) ).
cnf(n_s3_type11_4,axiom,
( ~ q_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_1(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_4) ).
cnf(n_s3_type11_5,axiom,
( ~ p_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_5) ).
cnf(n_s3_type11_6,axiom,
( ~ q_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_6) ).
cnf(n_s3_type11_7,axiom,
( ~ p_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_7) ).
cnf(n_s3_type11_8,axiom,
( ~ q_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_8) ).
cnf(n_s3_type11_9,axiom,
( ~ p_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_9) ).
cnf(n_s3_type11_10,axiom,
( ~ q_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_10) ).
cnf(n_s3_type11_11,axiom,
( ~ p_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_11) ).
cnf(n_s3_type11_12,axiom,
( ~ q_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_12) ).
cnf(n_s3_type11_13,axiom,
( ~ p_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_13) ).
cnf(n_s3_type11_14,axiom,
( ~ q_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_14) ).
cnf(n_s3_type11_15,axiom,
( ~ p_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_15) ).
cnf(n_s3_type11_16,axiom,
( ~ q_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_16) ).
cnf(n_s3_type11_17,axiom,
( ~ p_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_17) ).
cnf(n_s3_type11_18,axiom,
( ~ q_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_18) ).
cnf(n_s3_type11_19,axiom,
( ~ p_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_19) ).
cnf(n_s3_type11_20,axiom,
( ~ q_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_20) ).
cnf(n_s3_type11_21,axiom,
( ~ p_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_21) ).
cnf(n_s3_type11_22,axiom,
( ~ q_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_22) ).
cnf(n_s3_type11_23,axiom,
( ~ p_13(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_23) ).
cnf(n_s3_type11_24,axiom,
( ~ q_13(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type11_24) ).
cnf(n_s3_type12_1,axiom,
( ~ q_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_1(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_0(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_1) ).
cnf(n_s3_type12_2,axiom,
( ~ p_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_1(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_0(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_2) ).
cnf(n_s3_type12_3,axiom,
( ~ q_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_1(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_3) ).
cnf(n_s3_type12_4,axiom,
( ~ p_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_1(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_4) ).
cnf(n_s3_type12_5,axiom,
( ~ q_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_5) ).
cnf(n_s3_type12_6,axiom,
( ~ p_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_2(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_6) ).
cnf(n_s3_type12_7,axiom,
( ~ q_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_7) ).
cnf(n_s3_type12_8,axiom,
( ~ p_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_3(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_8) ).
cnf(n_s3_type12_9,axiom,
( ~ q_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_9) ).
cnf(n_s3_type12_10,axiom,
( ~ p_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_4(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_10) ).
cnf(n_s3_type12_11,axiom,
( ~ q_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_11) ).
cnf(n_s3_type12_12,axiom,
( ~ p_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_5(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_12) ).
cnf(n_s3_type12_13,axiom,
( ~ q_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_13) ).
cnf(n_s3_type12_14,axiom,
( ~ p_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_14) ).
cnf(n_s3_type12_15,axiom,
( ~ q_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_15) ).
cnf(n_s3_type12_16,axiom,
( ~ p_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_16) ).
cnf(n_s3_type12_17,axiom,
( ~ q_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_17) ).
cnf(n_s3_type12_18,axiom,
( ~ p_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_8(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_18) ).
cnf(n_s3_type12_19,axiom,
( ~ q_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_19) ).
cnf(n_s3_type12_20,axiom,
( ~ p_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_9(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_20) ).
cnf(n_s3_type12_21,axiom,
( ~ q_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_21) ).
cnf(n_s3_type12_22,axiom,
( ~ p_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_10(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_22) ).
cnf(n_s3_type12_23,axiom,
( ~ q_13(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ p_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_23) ).
cnf(n_s3_type12_24,axiom,
( ~ p_13(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| ~ q_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_11(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type12_24) ).
cnf(n_s3_type2_1,axiom,
( ~ p_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_13(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type2_1) ).
cnf(n_s3_type2_2,axiom,
( ~ p_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| p_14(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type2_2) ).
cnf(n_s3_type2_3,axiom,
( ~ q_6(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_13(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type2_3) ).
cnf(n_s3_type2_4,axiom,
( ~ q_7(X_1,X_2,X_3,X_4,X_5,X_6,X_7)
| q_14(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_s3_type2_4) ).
cnf(n_t3_1,axiom,
( ~ nq_7(X_7)
| ~ nq_6(X_6)
| ~ nq_5(X_5)
| ~ nq_4(X_4)
| ~ nq_3(X_3)
| ~ nq_2(X_2)
| ~ nq_1(X_1)
| p_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_t3_1) ).
cnf(n_t3_2,axiom,
( ~ nq_7(X_7)
| ~ nq_6(X_6)
| ~ nq_5(X_5)
| ~ nq_4(X_4)
| ~ nq_3(X_3)
| ~ nq_2(X_2)
| ~ nq_1(X_1)
| p_13(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_t3_2) ).
cnf(n_t3_3,axiom,
( ~ nq_7(X_7)
| ~ nq_6(X_6)
| ~ nq_5(X_5)
| ~ nq_4(X_4)
| ~ nq_3(X_3)
| ~ nq_2(X_2)
| ~ nq_1(X_1)
| q_12(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_t3_3) ).
cnf(n_t3_4,axiom,
( ~ nq_7(X_7)
| ~ nq_6(X_6)
| ~ nq_5(X_5)
| ~ nq_4(X_4)
| ~ nq_3(X_3)
| ~ nq_2(X_2)
| ~ nq_1(X_1)
| q_13(X_1,X_2,X_3,X_4,X_5,X_6,X_7) ),
file('theBenchmark.p',n_t3_4) ).
cnf(n_1,axiom,
nq_1(a),
file('theBenchmark.p',n_1) ).
cnf(n_2,axiom,
nq_1(b),
file('theBenchmark.p',n_2) ).
cnf(n_3,axiom,
nq_2(a),
file('theBenchmark.p',n_3) ).
cnf(n_4,axiom,
nq_2(b),
file('theBenchmark.p',n_4) ).
cnf(n_5,axiom,
nq_3(a),
file('theBenchmark.p',n_5) ).
cnf(n_6,axiom,
nq_3(b),
file('theBenchmark.p',n_6) ).
cnf(n_7,axiom,
nq_4(a),
file('theBenchmark.p',n_7) ).
cnf(n_8,axiom,
nq_4(b),
file('theBenchmark.p',n_8) ).
cnf(n_9,axiom,
nq_5(a),
file('theBenchmark.p',n_9) ).
cnf(n_10,axiom,
nq_5(b),
file('theBenchmark.p',n_10) ).
cnf(n_11,axiom,
nq_6(a),
file('theBenchmark.p',n_11) ).
cnf(n_12,axiom,
nq_6(b),
file('theBenchmark.p',n_12) ).
cnf(n_13,axiom,
nq_7(a),
file('theBenchmark.p',n_13) ).
cnf(n_14,axiom,
nq_7(b),
file('theBenchmark.p',n_14) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN102-1.007.007 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.03 This is a CNF_UNS_EPR_NEQ_HRN 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.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.03/0.36 % CPULimit : 300
% 0.03/0.36 % WCLimit : 300
% 0.03/0.36 % DateTime : Sun Sep 20 06:26:42 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.40 % SZS status Unsatisfiable for theBenchmark
% 0.03/0.40 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------