%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV005-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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 : Sun Sep 27 07:34:16 AM UTC 2026
% Result : Unsatisfiable 0.15s 0.39s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 24
% Syntax : Number of formulae : 89 ( 34 unt; 0 def)
% Number of atoms : 177 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 185 ( 97 ~; 88 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 12 con; 0-2 aty)
% Number of variables : 65 ( 1 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(halfadder_connection_in1_in1or1,axiom,
! [VAR_0] :
( connection(in(n1,VAR_0),in(n1,or1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_in1_in1or1) ).
cnf(c_1,plain,
( connection(in(n1,A),in(n1,or1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_in1_in1or1]) ).
fof(value_propagation2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( value(VAR_0,VAR_2)
| ~ value(VAR_1,VAR_2)
| ~ connection(VAR_0,VAR_1) ),
file('theBenchmark.p',value_propagation2) ).
cnf(c_2,plain,
( value(A,C)
| ~ value(B,C)
| ~ connection(A,B) ),
inference(clausify,[status(thm)],[value_propagation2]) ).
fof(value_propagation1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( value(VAR_1,VAR_2)
| ~ value(VAR_0,VAR_2)
| ~ connection(VAR_0,VAR_1) ),
file('theBenchmark.p',value_propagation1) ).
cnf(c_3,plain,
( value(B,C)
| ~ value(A,C)
| ~ connection(A,B) ),
inference(clausify,[status(thm)],[value_propagation1]) ).
fof(halfadder_connection_outs_out1and1,axiom,
! [VAR_0] :
( connection(out(s,VAR_0),out(n1,and1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_outs_out1and1) ).
cnf(c_7,plain,
( connection(out(s,A),out(n1,and1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_outs_out1and1]) ).
fof(halfadder_connection_outc_out1and2,axiom,
! [VAR_0] :
( connection(out(c,VAR_0),out(n1,and2(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_outc_out1and2) ).
cnf(c_8,plain,
( connection(out(c,A),out(n1,and2(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_outc_out1and2]) ).
fof(halfadder_connection_out1or1_in1_and1,axiom,
! [VAR_0] :
( connection(out(n1,or1(VAR_0)),in(n1,and1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_out1or1_in1_and1) ).
cnf(c_9,plain,
( connection(out(n1,or1(A)),in(n1,and1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_out1or1_in1_and1]) ).
fof(halfadder_connection_out1and2_in1not1,axiom,
! [VAR_0] :
( connection(out(n1,and2(VAR_0)),in(n1,not1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_out1and2_in1not1) ).
cnf(c_10,plain,
( connection(out(n1,and2(A)),in(n1,not1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_out1and2_in1not1]) ).
fof(halfadder_connection_out1not1_in2and1,axiom,
! [VAR_0] :
( connection(out(n1,not1(VAR_0)),in(n2,and1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_out1not1_in2and1) ).
cnf(c_11,plain,
( connection(out(n1,not1(A)),in(n2,and1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_out1not1_in2and1]) ).
fof(unique_value,axiom,
! [VAR_0,VAR_1,VAR_2] :
( equal_value(VAR_1,VAR_2)
| ~ value(VAR_0,VAR_2)
| ~ value(VAR_0,VAR_1) ),
file('theBenchmark.p',unique_value) ).
cnf(c_12,plain,
( equal_value(B,C)
| ~ value(A,C)
| ~ value(A,B) ),
inference(clausify,[status(thm)],[unique_value]) ).
fof(equal_value1,axiom,
~ equal_value(n0,n1),
file('theBenchmark.p',equal_value1) ).
cnf(c_13,plain,
~ equal_value(n0,n1),
inference(clausify,[status(thm)],[equal_value1]) ).
cnf(c_15,plain,
( ~ value(A,n1)
| ~ value(A,n0) ),
inference(resolve,[status(thm)],[c_12,c_13]) ).
fof(ok_or_abnormal,axiom,
! [VAR_0,VAR_1] :
( mode(VAR_0,abnormal)
| mode(VAR_0,ok)
| ~ type(VAR_0,VAR_1) ),
file('theBenchmark.p',ok_or_abnormal) ).
cnf(c_17,plain,
( mode(A,abnormal)
| mode(A,ok)
| ~ type(A,B) ),
inference(clausify,[status(thm)],[ok_or_abnormal]) ).
fof(and_0_00,axiom,
! [VAR_0] :
( value(in(n2,VAR_0),n0)
| value(in(n1,VAR_0),n0)
| ~ value(out(n1,VAR_0),n0)
| ~ type(VAR_0,and)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',and_0_00) ).
cnf(c_20,plain,
( value(in(n2,A),n0)
| value(in(n1,A),n0)
| ~ value(out(n1,A),n0)
| ~ type(A,and)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[and_0_00]) ).
fof(or_0_0x,axiom,
! [VAR_0] :
( value(in(n1,VAR_0),n0)
| ~ value(out(n1,VAR_0),n0)
| ~ type(VAR_0,or)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',or_0_0x) ).
cnf(c_26,plain,
( value(in(n1,A),n0)
| ~ value(out(n1,A),n0)
| ~ type(A,or)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[or_0_0x]) ).
fof(not_0_1_bw,axiom,
! [VAR_0] :
( value(in(n1,VAR_0),n1)
| ~ value(out(n1,VAR_0),n0)
| ~ type(VAR_0,not)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',not_0_1_bw) ).
cnf(c_30,plain,
( value(in(n1,A),n1)
| ~ value(out(n1,A),n0)
| ~ type(A,not)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[not_0_1_bw]) ).
fof(halfadder_and1,axiom,
! [VAR_0] :
( type(and1(VAR_0),and)
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_and1) ).
cnf(c_32,plain,
( type(and1(A),and)
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_and1]) ).
fof(halfadder_not1,axiom,
! [VAR_0] :
( type(not1(VAR_0),not)
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_not1) ).
cnf(c_34,plain,
( type(not1(A),not)
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_not1]) ).
fof(halfadder_or1,axiom,
! [VAR_0] :
( type(or1(VAR_0),or)
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_or1) ).
cnf(c_35,plain,
( type(or1(A),or)
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_or1]) ).
fof(h_isa_halfadder,axiom,
type(h,halfadder),
file('theBenchmark.p',h_isa_halfadder) ).
cnf(c_36,plain,
type(h,halfadder),
inference(clausify,[status(thm)],[h_isa_halfadder]) ).
fof(in1_1,axiom,
value(in(n1,h),n1),
file('theBenchmark.p',in1_1) ).
cnf(c_37,plain,
value(in(n1,h),n1),
inference(clausify,[status(thm)],[in1_1]) ).
fof(outs_0,axiom,
value(out(s,h),n0),
file('theBenchmark.p',outs_0) ).
cnf(c_39,plain,
value(out(s,h),n0),
inference(clausify,[status(thm)],[outs_0]) ).
fof(outc_0,axiom,
value(out(c,h),n0),
file('theBenchmark.p',outc_0) ).
cnf(c_40,plain,
value(out(c,h),n0),
inference(clausify,[status(thm)],[outc_0]) ).
fof(diagnosis_and1,axiom,
~ mode(and1(h),abnormal),
file('theBenchmark.p',diagnosis_and1) ).
cnf(c_41,plain,
~ mode(and1(h),abnormal),
inference(clausify,[status(thm)],[diagnosis_and1]) ).
fof(diagnosis_not1,axiom,
~ mode(not1(h),abnormal),
file('theBenchmark.p',diagnosis_not1) ).
cnf(c_42,plain,
~ mode(not1(h),abnormal),
inference(clausify,[status(thm)],[diagnosis_not1]) ).
fof(diagnosis_or1,axiom,
~ mode(or1(h),abnormal),
file('theBenchmark.p',diagnosis_or1) ).
cnf(c_43,plain,
~ mode(or1(h),abnormal),
inference(clausify,[status(thm)],[diagnosis_or1]) ).
cnf(c_44,plain,
( value(in(n1,A),B)
| ~ value(in(n1,or1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_53,plain,
( value(out(n1,and1(A)),B)
| ~ value(out(s,A),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_7,c_3]) ).
cnf(c_54,plain,
( value(out(c,A),B)
| ~ value(out(n1,and2(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_8,c_2]) ).
cnf(c_56,plain,
( value(out(n1,or1(A)),B)
| ~ value(in(n1,and1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_9,c_2]) ).
cnf(c_58,plain,
( value(out(n1,and2(A)),B)
| ~ value(in(n1,not1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_10,c_2]) ).
cnf(c_60,plain,
( value(out(n1,not1(A)),B)
| ~ value(in(n2,and1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_11,c_2]) ).
cnf(c_62,plain,
type(or1(h),or),
inference(resolve,[status(thm)],[c_36,c_35]) ).
cnf(c_63,plain,
type(not1(h),not),
inference(resolve,[status(thm)],[c_36,c_34]) ).
cnf(c_65,plain,
type(and1(h),and),
inference(resolve,[status(thm)],[c_36,c_32]) ).
cnf(c_67,plain,
~ value(in(n1,h),n0),
inference(resolve,[status(thm)],[c_15,c_37]) ).
cnf(c_70,plain,
~ value(out(c,h),n1),
inference(resolve,[status(thm)],[c_40,c_15]) ).
cnf(c_80,plain,
( value(out(n1,and1(h)),A)
| ~ value(out(s,h),A) ),
inference(resolve,[status(thm)],[c_53,c_36]) ).
cnf(c_153,plain,
( mode(or1(h),abnormal)
| mode(or1(h),ok) ),
inference(resolve,[status(thm)],[c_62,c_17]) ).
cnf(c_89,plain,
mode(or1(h),ok),
inference(resolve,[status(thm)],[c_43,c_153]) ).
cnf(c_154,plain,
( mode(not1(h),abnormal)
| mode(not1(h),ok) ),
inference(resolve,[status(thm)],[c_63,c_17]) ).
cnf(c_90,plain,
mode(not1(h),ok),
inference(resolve,[status(thm)],[c_42,c_154]) ).
cnf(c_155,plain,
( value(in(n1,h),A)
| ~ value(in(n1,or1(h)),A) ),
inference(resolve,[status(thm)],[c_44,c_36]) ).
cnf(c_93,plain,
~ value(in(n1,or1(h)),n0),
inference(resolve,[status(thm)],[c_155,c_67]) ).
cnf(c_156,plain,
( value(out(c,h),A)
| ~ value(out(n1,and2(h)),A) ),
inference(resolve,[status(thm)],[c_54,c_36]) ).
cnf(c_97,plain,
~ value(out(n1,and2(h)),n1),
inference(resolve,[status(thm)],[c_156,c_70]) ).
cnf(c_157,plain,
( mode(and1(h),abnormal)
| mode(and1(h),ok) ),
inference(resolve,[status(thm)],[c_65,c_17]) ).
cnf(c_98,plain,
mode(and1(h),ok),
inference(resolve,[status(thm)],[c_41,c_157]) ).
cnf(c_158,plain,
( value(in(n1,or1(h)),n0)
| ~ value(out(n1,or1(h)),n0)
| ~ type(or1(h),or) ),
inference(resolve,[status(thm)],[c_89,c_26]) ).
cnf(c_159,plain,
( value(in(n1,or1(h)),n0)
| ~ value(out(n1,or1(h)),n0) ),
inference(resolve,[status(thm)],[c_62,c_158]) ).
cnf(c_103,plain,
~ value(out(n1,or1(h)),n0),
inference(resolve,[status(thm)],[c_93,c_159]) ).
cnf(c_160,plain,
( value(in(n1,not1(h)),n1)
| ~ value(out(n1,not1(h)),n0)
| ~ type(not1(h),not) ),
inference(resolve,[status(thm)],[c_90,c_30]) ).
cnf(c_110,plain,
( value(in(n1,not1(h)),n1)
| ~ value(out(n1,not1(h)),n0) ),
inference(resolve,[status(thm)],[c_63,c_160]) ).
cnf(c_161,plain,
( value(in(n2,and1(h)),n0)
| value(in(n1,and1(h)),n0)
| ~ value(out(n1,and1(h)),n0)
| ~ type(and1(h),and) ),
inference(resolve,[status(thm)],[c_98,c_20]) ).
cnf(c_130,plain,
( value(in(n2,and1(h)),n0)
| value(in(n1,and1(h)),n0)
| ~ value(out(n1,and1(h)),n0) ),
inference(resolve,[status(thm)],[c_65,c_161]) ).
cnf(c_162,plain,
( value(out(n1,and2(h)),A)
| ~ value(in(n1,not1(h)),A) ),
inference(resolve,[status(thm)],[c_58,c_36]) ).
cnf(c_138,plain,
~ value(in(n1,not1(h)),n1),
inference(resolve,[status(thm)],[c_162,c_97]) ).
cnf(c_141,plain,
~ value(out(n1,not1(h)),n0),
inference(resolve,[status(thm)],[c_138,c_110]) ).
cnf(c_163,plain,
( value(out(n1,or1(h)),A)
| ~ value(in(n1,and1(h)),A) ),
inference(resolve,[status(thm)],[c_56,c_36]) ).
cnf(c_144,plain,
~ value(in(n1,and1(h)),n0),
inference(resolve,[status(thm)],[c_163,c_103]) ).
cnf(c_146,plain,
( value(in(n2,and1(h)),n0)
| ~ value(out(n1,and1(h)),n0) ),
inference(resolve,[status(thm)],[c_144,c_130]) ).
cnf(c_148,plain,
value(out(n1,and1(h)),n0),
inference(resolve,[status(thm)],[c_80,c_39]) ).
cnf(c_150,plain,
value(in(n2,and1(h)),n0),
inference(resolve,[status(thm)],[c_148,c_146]) ).
cnf(c_164,plain,
( value(out(n1,not1(h)),A)
| ~ value(in(n2,and1(h)),A) ),
inference(resolve,[status(thm)],[c_60,c_36]) ).
cnf(c_165,plain,
~ value(in(n2,and1(h)),n0),
inference(resolve,[status(thm)],[c_164,c_141]) ).
cnf(c_152,plain,
$false,
inference(resolve,[status(thm)],[c_150,c_165]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV005-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 16:01:37 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2375859 was started by sandbox on n018,
% 0.09/0.37 % Fri Sep 25 16:01:37 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 0.15/0.39
% 0.15/0.39 % SZS status Unsatisfiable for theBenchmark
% 0.15/0.39
% 0.15/0.39 % Proof 1 at 0.00 (+ 0.00) seconds.
% 0.15/0.39 % Length of proof is 52.
% 0.15/0.39 % Level of proof is 8.
% 0.15/0.39 % Maximum clause weight is 33.000.
% 0.15/0.39 % Given clauses 86.
% 0.15/0.39
% 0.15/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------