%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HWV005-1 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:28:52 PM UTC 2026
% Result : Unsatisfiable 1.27s 1.73s
% Output : CNFRefutation 1.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 25
% Syntax : Number of clauses : 77 ( 27 unt; 12 nHn; 77 RR)
% Number of literals : 157 ( 0 equ; 80 neg)
% Maximal clause size : 5 ( 2 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 : 59 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(value_propagation1,axiom,
( value(X2,X3)
| ~ connection(X1,X2)
| ~ value(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',value_propagation1) ).
cnf(outs_0,hypothesis,
value(out(s,h),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outs_0) ).
cnf(ok_or_abnormal,axiom,
( mode(X1,ok)
| mode(X1,abnormal)
| ~ type(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',ok_or_abnormal) ).
cnf(halfadder_and1,axiom,
( type(and1(X1),and)
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_and1) ).
cnf(halfadder_connection_outs_out1and1,axiom,
( connection(out(s,X1),out(n1,and1(X1)))
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outs_out1and1) ).
cnf(h_isa_halfadder,hypothesis,
type(h,halfadder),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_isa_halfadder) ).
cnf(diagnosis_and1,negated_conjecture,
~ mode(and1(h),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_and1) ).
cnf(in1_1,hypothesis,
value(in(n1,h),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',in1_1) ).
cnf(halfadder_or1,axiom,
( type(or1(X1),or)
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_or1) ).
cnf(and_0_00,axiom,
( value(in(n1,X1),n0)
| value(in(n2,X1),n0)
| ~ mode(X1,ok)
| ~ type(X1,and)
| ~ value(out(n1,X1),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_0_00) ).
cnf(halfadder_connection_in1_in1or1,axiom,
( connection(in(n1,X1),in(n1,or1(X1)))
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1or1) ).
cnf(diagnosis_or1,negated_conjecture,
~ mode(or1(h),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_or1) ).
cnf(outc_0,hypothesis,
value(out(c,h),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outc_0) ).
cnf(or_1x_1,axiom,
( value(out(n1,X1),n1)
| ~ mode(X1,ok)
| ~ type(X1,or)
| ~ value(in(X2,X1),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_1x_1) ).
cnf(value_propagation2,axiom,
( value(X1,X3)
| ~ connection(X1,X2)
| ~ value(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',value_propagation2) ).
cnf(halfadder_connection_outc_out1and2,axiom,
( connection(out(c,X1),out(n1,and2(X1)))
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outc_out1and2) ).
cnf(halfadder_connection_out1not1_in2and1,axiom,
( connection(out(n1,not1(X1)),in(n2,and1(X1)))
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1not1_in2and1) ).
cnf(halfadder_not1,axiom,
( type(not1(X1),not)
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_not1) ).
cnf(halfadder_connection_out1or1_in1_and1,axiom,
( connection(out(n1,or1(X1)),in(n1,and1(X1)))
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1or1_in1_and1) ).
cnf(unique_value,axiom,
( equal_value(X2,X3)
| ~ value(X1,X2)
| ~ value(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',unique_value) ).
cnf(diagnosis_not1,negated_conjecture,
~ mode(not1(h),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_not1) ).
cnf(halfadder_connection_out1and2_in1not1,axiom,
( connection(out(n1,and2(X1)),in(n1,not1(X1)))
| ~ type(X1,halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1and2_in1not1) ).
cnf(not_0_1_fw,axiom,
( value(out(n1,X1),n1)
| ~ mode(X1,ok)
| ~ type(X1,not)
| ~ value(in(n1,X1),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',not_0_1_fw) ).
cnf(equal_value2,axiom,
~ equal_value(n1,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',equal_value2) ).
cnf(equal_value1,axiom,
~ equal_value(n0,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',equal_value1) ).
cnf(c_0_25,axiom,
( value(X2,X3)
| ~ connection(X1,X2)
| ~ value(X1,X3) ),
value_propagation1 ).
cnf(c_0_26,hypothesis,
value(out(s,h),n0),
outs_0 ).
cnf(c_0_27,axiom,
( mode(X1,ok)
| mode(X1,abnormal)
| ~ type(X1,X2) ),
ok_or_abnormal ).
cnf(c_0_28,axiom,
( type(and1(X1),and)
| ~ type(X1,halfadder) ),
halfadder_and1 ).
cnf(c_0_29,hypothesis,
( value(X1,n0)
| ~ connection(out(s,h),X1) ),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_30,axiom,
( connection(out(s,X1),out(n1,and1(X1)))
| ~ type(X1,halfadder) ),
halfadder_connection_outs_out1and1 ).
cnf(c_0_31,hypothesis,
type(h,halfadder),
h_isa_halfadder ).
cnf(c_0_32,plain,
( mode(and1(X1),abnormal)
| mode(and1(X1),ok)
| ~ type(X1,halfadder) ),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_33,negated_conjecture,
~ mode(and1(h),abnormal),
diagnosis_and1 ).
cnf(c_0_34,hypothesis,
value(in(n1,h),n1),
in1_1 ).
cnf(c_0_35,axiom,
( type(or1(X1),or)
| ~ type(X1,halfadder) ),
halfadder_or1 ).
cnf(c_0_36,axiom,
( value(in(n1,X1),n0)
| value(in(n2,X1),n0)
| ~ mode(X1,ok)
| ~ type(X1,and)
| ~ value(out(n1,X1),n0) ),
and_0_00 ).
cnf(c_0_37,hypothesis,
value(out(n1,and1(h)),n0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31])]) ).
cnf(c_0_38,hypothesis,
mode(and1(h),ok),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_31]),c_0_33]) ).
cnf(c_0_39,hypothesis,
( value(X1,n1)
| ~ connection(in(n1,h),X1) ),
inference(spm,[status(thm)],[c_0_25,c_0_34]) ).
cnf(c_0_40,axiom,
( connection(in(n1,X1),in(n1,or1(X1)))
| ~ type(X1,halfadder) ),
halfadder_connection_in1_in1or1 ).
cnf(c_0_41,plain,
( mode(or1(X1),abnormal)
| mode(or1(X1),ok)
| ~ type(X1,halfadder) ),
inference(spm,[status(thm)],[c_0_27,c_0_35]) ).
cnf(c_0_42,negated_conjecture,
~ mode(or1(h),abnormal),
diagnosis_or1 ).
cnf(c_0_43,hypothesis,
( value(in(n2,and1(h)),n0)
| value(in(n1,and1(h)),n0)
| ~ type(and1(h),and) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_37]),c_0_38])]) ).
cnf(c_0_44,hypothesis,
value(out(c,h),n0),
outc_0 ).
cnf(c_0_45,axiom,
( value(out(n1,X1),n1)
| ~ mode(X1,ok)
| ~ type(X1,or)
| ~ value(in(X2,X1),n1) ),
or_1x_1 ).
cnf(c_0_46,hypothesis,
value(in(n1,or1(h)),n1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39,c_0_40]),c_0_31])]) ).
cnf(c_0_47,hypothesis,
mode(or1(h),ok),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41,c_0_31]),c_0_42]) ).
cnf(c_0_48,axiom,
( value(X1,X3)
| ~ connection(X1,X2)
| ~ value(X2,X3) ),
value_propagation2 ).
cnf(c_0_49,hypothesis,
( value(in(n1,and1(h)),n0)
| value(in(n2,and1(h)),n0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_28]),c_0_31])]) ).
cnf(c_0_50,hypothesis,
( value(X1,n0)
| ~ connection(out(c,h),X1) ),
inference(spm,[status(thm)],[c_0_25,c_0_44]) ).
cnf(c_0_51,axiom,
( connection(out(c,X1),out(n1,and2(X1)))
| ~ type(X1,halfadder) ),
halfadder_connection_outc_out1and2 ).
cnf(c_0_52,hypothesis,
( value(out(n1,or1(h)),n1)
| ~ type(or1(h),or) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_47])]) ).
cnf(c_0_53,hypothesis,
( value(in(n1,and1(h)),n0)
| value(X1,n0)
| ~ connection(X1,in(n2,and1(h))) ),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
cnf(c_0_54,axiom,
( connection(out(n1,not1(X1)),in(n2,and1(X1)))
| ~ type(X1,halfadder) ),
halfadder_connection_out1not1_in2and1 ).
cnf(c_0_55,axiom,
( type(not1(X1),not)
| ~ type(X1,halfadder) ),
halfadder_not1 ).
cnf(c_0_56,hypothesis,
value(out(n1,and2(h)),n0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_51]),c_0_31])]) ).
cnf(c_0_57,hypothesis,
( value(X1,n1)
| ~ type(or1(h),or)
| ~ connection(out(n1,or1(h)),X1) ),
inference(spm,[status(thm)],[c_0_25,c_0_52]) ).
cnf(c_0_58,axiom,
( connection(out(n1,or1(X1)),in(n1,and1(X1)))
| ~ type(X1,halfadder) ),
halfadder_connection_out1or1_in1_and1 ).
cnf(c_0_59,axiom,
( equal_value(X2,X3)
| ~ value(X1,X2)
| ~ value(X1,X3) ),
unique_value ).
cnf(c_0_60,hypothesis,
( value(out(n1,not1(h)),n0)
| value(in(n1,and1(h)),n0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_31])]) ).
cnf(c_0_61,plain,
( mode(not1(X1),abnormal)
| mode(not1(X1),ok)
| ~ type(X1,halfadder) ),
inference(spm,[status(thm)],[c_0_27,c_0_55]) ).
cnf(c_0_62,negated_conjecture,
~ mode(not1(h),abnormal),
diagnosis_not1 ).
cnf(c_0_63,hypothesis,
( value(X1,n0)
| ~ connection(out(n1,and2(h)),X1) ),
inference(spm,[status(thm)],[c_0_25,c_0_56]) ).
cnf(c_0_64,axiom,
( connection(out(n1,and2(X1)),in(n1,not1(X1)))
| ~ type(X1,halfadder) ),
halfadder_connection_out1and2_in1not1 ).
cnf(c_0_65,hypothesis,
( value(in(n1,and1(h)),n1)
| ~ type(or1(h),or) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_31])]) ).
cnf(c_0_66,hypothesis,
( equal_value(X1,n0)
| value(in(n1,and1(h)),n0)
| ~ value(out(n1,not1(h)),X1) ),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_67,axiom,
( value(out(n1,X1),n1)
| ~ mode(X1,ok)
| ~ type(X1,not)
| ~ value(in(n1,X1),n0) ),
not_0_1_fw ).
cnf(c_0_68,hypothesis,
mode(not1(h),ok),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_31]),c_0_62]) ).
cnf(c_0_69,hypothesis,
value(in(n1,not1(h)),n0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_64]),c_0_31])]) ).
cnf(c_0_70,axiom,
~ equal_value(n1,n0),
equal_value2 ).
cnf(c_0_71,hypothesis,
( equal_value(X1,n1)
| ~ type(or1(h),or)
| ~ value(in(n1,and1(h)),X1) ),
inference(spm,[status(thm)],[c_0_59,c_0_65]) ).
cnf(c_0_72,hypothesis,
( value(in(n1,and1(h)),n0)
| ~ type(not1(h),not) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_67]),c_0_68]),c_0_69])]),c_0_70]) ).
cnf(c_0_73,axiom,
~ equal_value(n0,n1),
equal_value1 ).
cnf(c_0_74,hypothesis,
( ~ type(or1(h),or)
| ~ type(not1(h),not) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_71,c_0_72]),c_0_73]) ).
cnf(c_0_75,hypothesis,
~ type(or1(h),or),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_55]),c_0_31])]) ).
cnf(c_0_76,hypothesis,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_35]),c_0_31])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV005-1 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n022.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 19:10:06 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 1.27/1.73 % Version : CSE_E---1.7
% 1.27/1.73 % Problem : theBenchmark.p
% 1.27/1.73 % SZS status Unsatisfiable for theBenchmark.p
% 1.27/1.73 % SZS output start CNFRefutation
% See solution above
% 1.27/1.73 % Total time : 1.373s
%------------------------------------------------------------------------------