%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HWV003-3 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n007.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 : Fri Sep 25 01:39:54 PM UTC 2026
% Result : Unsatisfiable 1.00s 1.20s
% Output : CNFRefutation 1.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 56
% Syntax : Number of formulae : 113 ( 1 unt; 0 def)
% Number of atoms : 279 ( 0 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 296 ( 130 ~; 166 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 22 usr; 23 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( a
| a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1A) ).
fof(f2,negated_conjecture,
( b
| a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1B) ).
fof(f3,negated_conjecture,
( ~ b
| ~ a
| ~ a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1C) ).
fof(f4,negated_conjecture,
( a
| a12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2A) ).
fof(f5,negated_conjecture,
( a11
| a12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2B) ).
fof(f6,negated_conjecture,
( ~ a11
| ~ a
| ~ a12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2C) ).
fof(f7,negated_conjecture,
( b
| a13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3A) ).
fof(f8,negated_conjecture,
( a11
| a13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3B) ).
fof(f9,negated_conjecture,
( ~ a11
| ~ b
| ~ a13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3C) ).
fof(f10,negated_conjecture,
( a12
| a14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4A) ).
fof(f11,negated_conjecture,
( a13
| a14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4B) ).
fof(f12,negated_conjecture,
( ~ a13
| ~ a12
| ~ a14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4C) ).
fof(f13,negated_conjecture,
( a14
| a15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5A) ).
fof(f14,negated_conjecture,
( cI
| a15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5B) ).
fof(f15,negated_conjecture,
( ~ cI
| ~ a14
| ~ a15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5C) ).
fof(f16,negated_conjecture,
( a14
| a16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6A) ).
fof(f17,negated_conjecture,
( a15
| a16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6B) ).
fof(f18,negated_conjecture,
( ~ a15
| ~ a14
| ~ a16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6C) ).
fof(f19,negated_conjecture,
( a15
| a17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7A) ).
fof(f20,negated_conjecture,
( cI
| a17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7B) ).
fof(f21,negated_conjecture,
( ~ cI
| ~ a15
| ~ a17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7C) ).
fof(f22,negated_conjecture,
( a16
| s1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8A) ).
fof(f23,negated_conjecture,
( a17
| s1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8B) ).
fof(f24,negated_conjecture,
( ~ a17
| ~ a16
| ~ s1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8C) ).
fof(f25,negated_conjecture,
( a15
| c1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9A) ).
fof(f26,negated_conjecture,
( a11
| c1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9B) ).
fof(f27,negated_conjecture,
( ~ a11
| ~ a15
| ~ c1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9C) ).
fof(f28,negated_conjecture,
( ~ b
| a
| a21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10A) ).
fof(f29,negated_conjecture,
( b
| ~ a
| a21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10B) ).
fof(f30,negated_conjecture,
( b
| a
| ~ a21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10C) ).
fof(f31,negated_conjecture,
( ~ b
| ~ a
| ~ a21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10D) ).
fof(f32,negated_conjecture,
( cI
| ~ a22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11A) ).
fof(f33,negated_conjecture,
( a23
| ~ a22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11B) ).
fof(f34,negated_conjecture,
( ~ a23
| ~ cI
| a22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11C) ).
fof(f35,negated_conjecture,
( ~ a
| a23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12A) ).
fof(f36,negated_conjecture,
( ~ b
| a23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12B) ).
fof(f37,negated_conjecture,
( b
| a
| ~ a23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12C) ).
fof(f38,negated_conjecture,
( cI
| a24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13A) ).
fof(f40,negated_conjecture,
( a
| ~ a25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14A) ).
fof(f41,negated_conjecture,
( b
| ~ a25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14B) ).
fof(f42,negated_conjecture,
( ~ b
| ~ a
| a25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14C) ).
fof(f44,negated_conjecture,
( a25
| ~ a26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15B) ).
fof(f45,negated_conjecture,
( ~ a25
| ~ a24
| a26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15C) ).
fof(f46,negated_conjecture,
( ~ a21
| cI
| s2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16A) ).
fof(f47,negated_conjecture,
( a21
| ~ cI
| s2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16B) ).
fof(f48,negated_conjecture,
( a21
| cI
| ~ s2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16C) ).
fof(f49,negated_conjecture,
( ~ a21
| ~ cI
| ~ s2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16D) ).
fof(f50,negated_conjecture,
( ~ a22
| c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17A) ).
fof(f51,negated_conjecture,
( ~ a26
| c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17B) ).
fof(f52,negated_conjecture,
( a26
| a22
| ~ c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17C) ).
fof(f54,negated_conjecture,
( s2
| ~ s1
| conjline18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18B) ).
fof(f55,negated_conjecture,
( s2
| s1
| ~ conjline18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18C) ).
fof(f56,negated_conjecture,
( ~ s2
| ~ s1
| ~ conjline18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18D) ).
fof(f59,negated_conjecture,
( c2
| c1
| ~ conjline19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19C) ).
fof(f60,negated_conjecture,
( ~ c2
| ~ c1
| ~ conjline19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19D) ).
fof(f61,negated_conjecture,
( conjline19
| conjline18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
tcf(c_110,negated_conjecture,
( a
| a11 ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_111,negated_conjecture,
( b
| a11 ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_112,negated_conjecture,
( ~ b
| ~ a
| ~ a11 ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_113,negated_conjecture,
( a12
| a ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_114,negated_conjecture,
( a12
| a11 ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_115,negated_conjecture,
( ~ a12
| ~ a
| ~ a11 ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_116,negated_conjecture,
( a13
| b ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_117,negated_conjecture,
( a13
| a11 ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_118,negated_conjecture,
( ~ a13
| ~ b
| ~ a11 ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_119,negated_conjecture,
( a14
| a12 ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_120,negated_conjecture,
( a14
| a13 ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_121,negated_conjecture,
( ~ a14
| ~ a13
| ~ a12 ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_122,negated_conjecture,
( a15
| a14 ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_123,negated_conjecture,
( cI
| a15 ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_124,negated_conjecture,
( ~ cI
| ~ a15
| ~ a14 ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_125,negated_conjecture,
( a16
| a14 ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_126,negated_conjecture,
( a16
| a15 ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_127,negated_conjecture,
( ~ a16
| ~ a15
| ~ a14 ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_128,negated_conjecture,
( a17
| a15 ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_129,negated_conjecture,
( a17
| cI ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_130,negated_conjecture,
( ~ a17
| ~ cI
| ~ a15 ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_131,negated_conjecture,
( s1
| a16 ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_132,negated_conjecture,
( s1
| a17 ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_133,negated_conjecture,
( ~ s1
| ~ a17
| ~ a16 ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_134,negated_conjecture,
( c1
| a15 ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_135,negated_conjecture,
( c1
| a11 ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_136,negated_conjecture,
( ~ c1
| ~ a15
| ~ a11 ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_137,negated_conjecture,
( a21
| a
| ~ b ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_138,negated_conjecture,
( a21
| b
| ~ a ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_139,negated_conjecture,
( b
| a
| ~ a21 ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_140,negated_conjecture,
( ~ a21
| ~ b
| ~ a ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_141,negated_conjecture,
( cI
| ~ a22 ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_142,negated_conjecture,
( a23
| ~ a22 ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_143,negated_conjecture,
( a22
| ~ a23
| ~ cI ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_144,negated_conjecture,
( a23
| ~ a ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_145,negated_conjecture,
( a23
| ~ b ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_146,negated_conjecture,
( b
| a
| ~ a23 ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_147,negated_conjecture,
( a24
| cI ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_149,negated_conjecture,
( a
| ~ a25 ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_150,negated_conjecture,
( b
| ~ a25 ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_151,negated_conjecture,
( a25
| ~ b
| ~ a ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_153,negated_conjecture,
( a25
| ~ a26 ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_154,negated_conjecture,
( a26
| ~ a25
| ~ a24 ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_155,negated_conjecture,
( s2
| cI
| ~ a21 ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_156,negated_conjecture,
( s2
| a21
| ~ cI ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_157,negated_conjecture,
( a21
| cI
| ~ s2 ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_158,negated_conjecture,
( ~ s2
| ~ a21
| ~ cI ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_159,negated_conjecture,
( c2
| ~ a22 ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_160,negated_conjecture,
( c2
| ~ a26 ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_161,negated_conjecture,
( a26
| a22
| ~ c2 ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_163,negated_conjecture,
( conjline18
| s2
| ~ s1 ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_164,negated_conjecture,
( s2
| s1
| ~ conjline18 ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_165,negated_conjecture,
( ~ conjline18
| ~ s2
| ~ s1 ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_168,negated_conjecture,
( c2
| c1
| ~ conjline19 ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_169,negated_conjecture,
( ~ conjline19
| ~ c2
| ~ c1 ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_170,negated_conjecture,
( conjline19
| conjline18 ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_171,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_112,c_115,c_118,c_121,c_124,c_127,c_130,c_133,c_136,c_140,c_158,c_165,c_169,c_143,c_151,c_154,c_137,c_138,c_139,c_146,c_155,c_156,c_157,c_161,c_163,c_164,c_168,c_141,c_142,c_144,c_145,c_149,c_150,c_153,c_159,c_160,c_110,c_111,c_113,c_114,c_116,c_117,c_119,c_120,c_122,c_123,c_125,c_126,c_128,c_129,c_131,c_132,c_134,c_135,c_147,c_170]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV003-3 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n007.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 16:18:07 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.45 % Proving...
% 1.00/1.20 % SZS status Started for theBenchmark.p
% 1.00/1.20 % SZS status Unsatisfiable for theBenchmark.p
% 1.00/1.20
% 1.00/1.20 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.00/1.20
% 1.00/1.20 % ------ iProver source info
% 1.00/1.20
% 1.00/1.20 % git: date: 2026-07-19 20:42:38 +0200
% 1.00/1.20 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.00/1.20 % git: non_committed_changes: false
% 1.00/1.20
% 1.00/1.20 % ------ Parsing...% successful
% 1.00/1.20
% 1.00/1.20
% 1.00/1.20 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 1.00/1.20 %
% 1.00/1.20
% 1.00/1.20 % ------ Preprocessing...%
% 1.00/1.20
% 1.00/1.20 % SZS status Unsatisfiable for theBenchmark.p
% 1.00/1.20
% 1.00/1.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.00/1.20
% 1.00/1.20
%------------------------------------------------------------------------------