%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : HWV003-3 : TPTP v9.3.1. Released v2.7.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 : n013.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 08:42:33 AM UTC 2026
% Result : Unsatisfiable 0.11s 0.38s
% Output : Proof 0.11s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_1A,negated_conjecture,
( a
| a11 ),
file('theBenchmark.p',clause_1A) ).
cnf(clause_1B,negated_conjecture,
( b
| a11 ),
file('theBenchmark.p',clause_1B) ).
cnf(clause_1C,negated_conjecture,
( ~ b
| ~ a
| ~ a11 ),
file('theBenchmark.p',clause_1C) ).
cnf(clause_2A,negated_conjecture,
( a
| a12 ),
file('theBenchmark.p',clause_2A) ).
cnf(clause_2B,negated_conjecture,
( a11
| a12 ),
file('theBenchmark.p',clause_2B) ).
cnf(clause_2C,negated_conjecture,
( ~ a11
| ~ a
| ~ a12 ),
file('theBenchmark.p',clause_2C) ).
cnf(clause_3A,negated_conjecture,
( b
| a13 ),
file('theBenchmark.p',clause_3A) ).
cnf(clause_3B,negated_conjecture,
( a11
| a13 ),
file('theBenchmark.p',clause_3B) ).
cnf(clause_3C,negated_conjecture,
( ~ a11
| ~ b
| ~ a13 ),
file('theBenchmark.p',clause_3C) ).
cnf(clause_4A,negated_conjecture,
( a12
| a14 ),
file('theBenchmark.p',clause_4A) ).
cnf(clause_4B,negated_conjecture,
( a13
| a14 ),
file('theBenchmark.p',clause_4B) ).
cnf(clause_4C,negated_conjecture,
( ~ a13
| ~ a12
| ~ a14 ),
file('theBenchmark.p',clause_4C) ).
cnf(clause_5A,negated_conjecture,
( a14
| a15 ),
file('theBenchmark.p',clause_5A) ).
cnf(clause_5B,negated_conjecture,
( cI
| a15 ),
file('theBenchmark.p',clause_5B) ).
cnf(clause_5C,negated_conjecture,
( ~ cI
| ~ a14
| ~ a15 ),
file('theBenchmark.p',clause_5C) ).
cnf(clause_6A,negated_conjecture,
( a14
| a16 ),
file('theBenchmark.p',clause_6A) ).
cnf(clause_6B,negated_conjecture,
( a15
| a16 ),
file('theBenchmark.p',clause_6B) ).
cnf(clause_6C,negated_conjecture,
( ~ a15
| ~ a14
| ~ a16 ),
file('theBenchmark.p',clause_6C) ).
cnf(clause_7A,negated_conjecture,
( a15
| a17 ),
file('theBenchmark.p',clause_7A) ).
cnf(clause_7B,negated_conjecture,
( cI
| a17 ),
file('theBenchmark.p',clause_7B) ).
cnf(clause_7C,negated_conjecture,
( ~ cI
| ~ a15
| ~ a17 ),
file('theBenchmark.p',clause_7C) ).
cnf(clause_8A,negated_conjecture,
( a16
| s1 ),
file('theBenchmark.p',clause_8A) ).
cnf(clause_8B,negated_conjecture,
( a17
| s1 ),
file('theBenchmark.p',clause_8B) ).
cnf(clause_8C,negated_conjecture,
( ~ a17
| ~ a16
| ~ s1 ),
file('theBenchmark.p',clause_8C) ).
cnf(clause_9A,negated_conjecture,
( a15
| c1 ),
file('theBenchmark.p',clause_9A) ).
cnf(clause_9B,negated_conjecture,
( a11
| c1 ),
file('theBenchmark.p',clause_9B) ).
cnf(clause_9C,negated_conjecture,
( ~ a11
| ~ a15
| ~ c1 ),
file('theBenchmark.p',clause_9C) ).
cnf(clause_10A,negated_conjecture,
( ~ b
| a
| a21 ),
file('theBenchmark.p',clause_10A) ).
cnf(clause_10B,negated_conjecture,
( b
| ~ a
| a21 ),
file('theBenchmark.p',clause_10B) ).
cnf(clause_10C,negated_conjecture,
( b
| a
| ~ a21 ),
file('theBenchmark.p',clause_10C) ).
cnf(clause_10D,negated_conjecture,
( ~ b
| ~ a
| ~ a21 ),
file('theBenchmark.p',clause_10D) ).
cnf(clause_11A,negated_conjecture,
( cI
| ~ a22 ),
file('theBenchmark.p',clause_11A) ).
cnf(clause_11B,negated_conjecture,
( a23
| ~ a22 ),
file('theBenchmark.p',clause_11B) ).
cnf(clause_11C,negated_conjecture,
( ~ a23
| ~ cI
| a22 ),
file('theBenchmark.p',clause_11C) ).
cnf(clause_12A,negated_conjecture,
( ~ a
| a23 ),
file('theBenchmark.p',clause_12A) ).
cnf(clause_12B,negated_conjecture,
( ~ b
| a23 ),
file('theBenchmark.p',clause_12B) ).
cnf(clause_12C,negated_conjecture,
( b
| a
| ~ a23 ),
file('theBenchmark.p',clause_12C) ).
cnf(clause_13A,negated_conjecture,
( cI
| a24 ),
file('theBenchmark.p',clause_13A) ).
cnf(clause_13B,negated_conjecture,
( ~ cI
| ~ a24 ),
file('theBenchmark.p',clause_13B) ).
cnf(clause_14A,negated_conjecture,
( a
| ~ a25 ),
file('theBenchmark.p',clause_14A) ).
cnf(clause_14B,negated_conjecture,
( b
| ~ a25 ),
file('theBenchmark.p',clause_14B) ).
cnf(clause_14C,negated_conjecture,
( ~ b
| ~ a
| a25 ),
file('theBenchmark.p',clause_14C) ).
cnf(clause_15A,negated_conjecture,
( a24
| ~ a26 ),
file('theBenchmark.p',clause_15A) ).
cnf(clause_15B,negated_conjecture,
( a25
| ~ a26 ),
file('theBenchmark.p',clause_15B) ).
cnf(clause_15C,negated_conjecture,
( ~ a25
| ~ a24
| a26 ),
file('theBenchmark.p',clause_15C) ).
cnf(clause_16A,negated_conjecture,
( ~ a21
| cI
| s2 ),
file('theBenchmark.p',clause_16A) ).
cnf(clause_16B,negated_conjecture,
( a21
| ~ cI
| s2 ),
file('theBenchmark.p',clause_16B) ).
cnf(clause_16C,negated_conjecture,
( a21
| cI
| ~ s2 ),
file('theBenchmark.p',clause_16C) ).
cnf(clause_16D,negated_conjecture,
( ~ a21
| ~ cI
| ~ s2 ),
file('theBenchmark.p',clause_16D) ).
cnf(clause_17A,negated_conjecture,
( ~ a22
| c2 ),
file('theBenchmark.p',clause_17A) ).
cnf(clause_17B,negated_conjecture,
( ~ a26
| c2 ),
file('theBenchmark.p',clause_17B) ).
cnf(clause_17C,negated_conjecture,
( a26
| a22
| ~ c2 ),
file('theBenchmark.p',clause_17C) ).
cnf(clause_18A,negated_conjecture,
( ~ s2
| s1
| conjline18 ),
file('theBenchmark.p',clause_18A) ).
cnf(clause_18B,negated_conjecture,
( s2
| ~ s1
| conjline18 ),
file('theBenchmark.p',clause_18B) ).
cnf(clause_18C,negated_conjecture,
( s2
| s1
| ~ conjline18 ),
file('theBenchmark.p',clause_18C) ).
cnf(clause_18D,negated_conjecture,
( ~ s2
| ~ s1
| ~ conjline18 ),
file('theBenchmark.p',clause_18D) ).
cnf(clause_19A,negated_conjecture,
( ~ c2
| c1
| conjline19 ),
file('theBenchmark.p',clause_19A) ).
cnf(clause_19B,negated_conjecture,
( c2
| ~ c1
| conjline19 ),
file('theBenchmark.p',clause_19B) ).
cnf(clause_19C,negated_conjecture,
( c2
| c1
| ~ conjline19 ),
file('theBenchmark.p',clause_19C) ).
cnf(clause_19D,negated_conjecture,
( ~ c2
| ~ c1
| ~ conjline19 ),
file('theBenchmark.p',clause_19D) ).
cnf(clause_20,negated_conjecture,
( conjline19
| conjline18 ),
file('theBenchmark.p',clause_20) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV003-3 : TPTP v9.3.1. Released v2.7.0.
% 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.35 % Computer : n013.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 19 10:42:50 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.11/0.38 % SZS status Unsatisfiable for theBenchmark
% 0.11/0.38 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------