%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HWV007-1 : TPTP v8.1.2. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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 : Thu May 9 17:24:54 EDT 2024
% Result : Unsatisfiable 1.68s 1.84s
% Output : Refutation 1.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 45
% Syntax : Number of clauses : 146 ( 60 unt; 18 nHn; 146 RR)
% Number of literals : 262 ( 0 equ; 104 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% Number of variables : 61 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(equal_value2,axiom,
~ equal_value(n1,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',equal_value2) ).
cnf(unique_value,axiom,
( ~ value(X9,X11)
| ~ value(X9,X10)
| equal_value(X11,X10) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',unique_value) ).
cnf(f_isa_fulladder,plain,
type(f,fulladder),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f_isa_fulladder) ).
cnf(fulladder_halfadder2,axiom,
( ~ type(X24,fulladder)
| type(h2(X24),halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_halfadder2) ).
cnf(c34,plain,
type(h2(f),halfadder),
inference(resolution,[status(thm)],[fulladder_halfadder2,f_isa_fulladder]) ).
cnf(halfadder_connection_in2_in2or1,axiom,
( ~ type(X51,halfadder)
| connection(in(n2,X51),in(n2,or1(X51))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in2_in2or1) ).
cnf(c59,plain,
connection(in(n2,h2(f)),in(n2,or1(h2(f)))),
inference(resolution,[status(thm)],[halfadder_connection_in2_in2or1,c34]) ).
cnf(value_propagation1,axiom,
( ~ connection(X4,X3)
| ~ value(X4,X5)
| value(X3,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',value_propagation1) ).
cnf(fulladder_connection_outsh1_in2h2,axiom,
( ~ type(X77,fulladder)
| connection(out(s,h1(X77)),in(n2,h2(X77))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outsh1_in2h2) ).
cnf(c112,plain,
connection(out(s,h1(f)),in(n2,h2(f))),
inference(resolution,[status(thm)],[fulladder_connection_outsh1_in2h2,f_isa_fulladder]) ).
cnf(fulladder_halfadder1,axiom,
( ~ type(X22,fulladder)
| type(h1(X22),halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_halfadder1) ).
cnf(c23,plain,
type(h1(f),halfadder),
inference(resolution,[status(thm)],[fulladder_halfadder1,f_isa_fulladder]) ).
cnf(halfadder_connection_outs_out1and1,axiom,
( ~ type(X55,halfadder)
| connection(out(s,X55),out(n1,and1(X55))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outs_out1and1) ).
cnf(c67,plain,
connection(out(s,h1(f)),out(n1,and1(h1(f)))),
inference(resolution,[status(thm)],[halfadder_connection_outs_out1and1,c23]) ).
cnf(value_propagation2,axiom,
( ~ connection(X7,X6)
| ~ value(X6,X8)
| value(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',value_propagation2) ).
cnf(diagnosis_or1_and1h1,negated_conjecture,
( ~ mode(or1(f),abnormal)
| ~ mode(and1(h1(f)),abnormal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_or1_and1h1) ).
cnf(ok_or_abnormal,axiom,
( ~ type(X15,X14)
| mode(X15,ok)
| mode(X15,abnormal) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',ok_or_abnormal) ).
cnf(halfadder_and1,axiom,
( ~ type(X16,halfadder)
| type(and1(X16),and) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_and1) ).
cnf(c28,plain,
type(and1(h1(f)),and),
inference(resolution,[status(thm)],[c23,halfadder_and1]) ).
cnf(c33,plain,
( mode(and1(h1(f)),ok)
| mode(and1(h1(f)),abnormal) ),
inference(resolution,[status(thm)],[c28,ok_or_abnormal]) ).
cnf(c135,plain,
( mode(and1(h1(f)),ok)
| ~ mode(or1(f),abnormal) ),
inference(resolution,[status(thm)],[c33,diagnosis_or1_and1h1]) ).
cnf(fulladder_connection_outch1_in2or1,axiom,
( ~ type(X80,fulladder)
| connection(out(c,h1(X80)),in(n2,or1(X80))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outch1_in2or1) ).
cnf(c115,plain,
connection(out(c,h1(f)),in(n2,or1(f))),
inference(resolution,[status(thm)],[fulladder_connection_outch1_in2or1,f_isa_fulladder]) ).
cnf(fulladder_or1,axiom,
( ~ type(X26,fulladder)
| type(or1(X26),or) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_or1) ).
cnf(c44,plain,
type(or1(f),or),
inference(resolution,[status(thm)],[fulladder_or1,f_isa_fulladder]) ).
cnf(c45,plain,
( mode(or1(f),ok)
| mode(or1(f),abnormal) ),
inference(resolution,[status(thm)],[c44,ok_or_abnormal]) ).
cnf(or_0_01,axiom,
( ~ mode(X49,ok)
| ~ type(X49,or)
| ~ value(out(n1,X49),n0)
| value(in(n2,X49),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_0_01) ).
cnf(outc_0,plain,
value(out(c,f),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outc_0) ).
cnf(c4,plain,
( ~ connection(out(c,f),X33)
| value(X33,n0) ),
inference(resolution,[status(thm)],[outc_0,value_propagation1]) ).
cnf(fulladder_connection_outc_out1or1,axiom,
( ~ type(X81,fulladder)
| connection(out(c,X81),out(n1,or1(X81))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outc_out1or1) ).
cnf(c116,plain,
connection(out(c,f),out(n1,or1(f))),
inference(resolution,[status(thm)],[fulladder_connection_outc_out1or1,f_isa_fulladder]) ).
cnf(c117,plain,
value(out(n1,or1(f)),n0),
inference(resolution,[status(thm)],[c116,c4]) ).
cnf(c123,plain,
( ~ mode(or1(f),ok)
| ~ type(or1(f),or)
| value(in(n2,or1(f)),n0) ),
inference(resolution,[status(thm)],[c117,or_0_01]) ).
cnf(c253,plain,
( ~ mode(or1(f),ok)
| value(in(n2,or1(f)),n0) ),
inference(resolution,[status(thm)],[c123,c44]) ).
cnf(c257,plain,
( value(in(n2,or1(f)),n0)
| mode(or1(f),abnormal) ),
inference(resolution,[status(thm)],[c253,c45]) ).
cnf(c260,plain,
( mode(or1(f),abnormal)
| ~ connection(X111,in(n2,or1(f)))
| value(X111,n0) ),
inference(resolution,[status(thm)],[c257,value_propagation2]) ).
cnf(c332,plain,
( mode(or1(f),abnormal)
| value(out(c,h1(f)),n0) ),
inference(resolution,[status(thm)],[c260,c115]) ).
cnf(c342,plain,
( mode(or1(f),abnormal)
| ~ value(out(c,h1(f)),X118)
| equal_value(X118,n0) ),
inference(resolution,[status(thm)],[c332,unique_value]) ).
cnf(halfadder_connection_outc_out1and2,axiom,
( ~ type(X56,halfadder)
| connection(out(c,X56),out(n1,and2(X56))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outc_out1and2) ).
cnf(c69,plain,
connection(out(c,h1(f)),out(n1,and2(h1(f)))),
inference(resolution,[status(thm)],[halfadder_connection_outc_out1and2,c23]) ).
cnf(diagnosis_and2h1,negated_conjecture,
~ mode(and2(h1(f)),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_and2h1) ).
cnf(halfadder_and2,axiom,
( ~ type(X17,halfadder)
| type(and2(X17),and) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_and2) ).
cnf(c25,plain,
type(and2(h1(f)),and),
inference(resolution,[status(thm)],[c23,halfadder_and2]) ).
cnf(c30,plain,
( mode(and2(h1(f)),ok)
| mode(and2(h1(f)),abnormal) ),
inference(resolution,[status(thm)],[c25,ok_or_abnormal]) ).
cnf(c130,plain,
mode(and2(h1(f)),ok),
inference(resolution,[status(thm)],[c30,diagnosis_and2h1]) ).
cnf(in2_0,plain,
value(in(n2,f),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',in2_0) ).
cnf(c1,plain,
( ~ connection(in(n2,f),X29)
| value(X29,n1) ),
inference(resolution,[status(thm)],[in2_0,value_propagation1]) ).
cnf(fulladder_connection_in2_in1h1,axiom,
( ~ type(X63,fulladder)
| connection(in(n2,X63),in(n1,h1(X63))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_in2_in1h1) ).
cnf(c80,plain,
connection(in(n2,f),in(n1,h1(f))),
inference(resolution,[status(thm)],[fulladder_connection_in2_in1h1,f_isa_fulladder]) ).
cnf(c81,plain,
value(in(n1,h1(f)),n1),
inference(resolution,[status(thm)],[c80,c1]) ).
cnf(c82,plain,
( ~ connection(in(n1,h1(f)),X65)
| value(X65,n1) ),
inference(resolution,[status(thm)],[c81,value_propagation1]) ).
cnf(halfadder_connection_in1_in1and2,axiom,
( ~ type(X52,halfadder)
| connection(in(n1,X52),in(n1,and2(X52))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1and2) ).
cnf(c62,plain,
connection(in(n1,h1(f)),in(n1,and2(h1(f)))),
inference(resolution,[status(thm)],[halfadder_connection_in1_in1and2,c23]) ).
cnf(c179,plain,
value(in(n1,and2(h1(f))),n1),
inference(resolution,[status(thm)],[c62,c82]) ).
cnf(and_11_1,axiom,
( ~ mode(X23,ok)
| ~ type(X23,and)
| ~ value(in(n1,X23),n1)
| ~ value(in(n2,X23),n1)
| value(out(n1,X23),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_11_1) ).
cnf(inc_1,plain,
value(in(c,f),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inc_1) ).
cnf(c2,plain,
( ~ connection(in(c,f),X30)
| value(X30,n1) ),
inference(resolution,[status(thm)],[inc_1,value_propagation1]) ).
cnf(fulladder_connection_inc_in2h1,axiom,
( ~ type(X69,fulladder)
| connection(in(c,X69),in(n2,h1(X69))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_inc_in2h1) ).
cnf(c92,plain,
connection(in(c,f),in(n2,h1(f))),
inference(resolution,[status(thm)],[fulladder_connection_inc_in2h1,f_isa_fulladder]) ).
cnf(c93,plain,
value(in(n2,h1(f)),n1),
inference(resolution,[status(thm)],[c92,c2]) ).
cnf(c94,plain,
( ~ connection(in(n2,h1(f)),X71)
| value(X71,n1) ),
inference(resolution,[status(thm)],[c93,value_propagation1]) ).
cnf(halfadder_connection_in2_in2and2,axiom,
( ~ type(X54,halfadder)
| connection(in(n2,X54),in(n2,and2(X54))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in2_in2and2) ).
cnf(c65,plain,
connection(in(n2,h1(f)),in(n2,and2(h1(f)))),
inference(resolution,[status(thm)],[halfadder_connection_in2_in2and2,c23]) ).
cnf(c191,plain,
value(in(n2,and2(h1(f))),n1),
inference(resolution,[status(thm)],[c65,c94]) ).
cnf(c197,plain,
( ~ mode(and2(h1(f)),ok)
| ~ type(and2(h1(f)),and)
| ~ value(in(n1,and2(h1(f))),n1)
| value(out(n1,and2(h1(f))),n1) ),
inference(resolution,[status(thm)],[c191,and_11_1]) ).
cnf(c390,plain,
( ~ mode(and2(h1(f)),ok)
| ~ type(and2(h1(f)),and)
| value(out(n1,and2(h1(f))),n1) ),
inference(resolution,[status(thm)],[c197,c179]) ).
cnf(c755,plain,
( ~ mode(and2(h1(f)),ok)
| value(out(n1,and2(h1(f))),n1) ),
inference(resolution,[status(thm)],[c390,c25]) ).
cnf(c782,plain,
value(out(n1,and2(h1(f))),n1),
inference(resolution,[status(thm)],[c755,c130]) ).
cnf(c788,plain,
( ~ connection(X173,out(n1,and2(h1(f))))
| value(X173,n1) ),
inference(resolution,[status(thm)],[c782,value_propagation2]) ).
cnf(c799,plain,
value(out(c,h1(f)),n1),
inference(resolution,[status(thm)],[c788,c69]) ).
cnf(c807,plain,
( mode(or1(f),abnormal)
| equal_value(n1,n0) ),
inference(resolution,[status(thm)],[c799,c342]) ).
cnf(c816,plain,
mode(or1(f),abnormal),
inference(resolution,[status(thm)],[c807,equal_value2]) ).
cnf(c820,plain,
mode(and1(h1(f)),ok),
inference(resolution,[status(thm)],[c816,c135]) ).
cnf(and_0x_0,axiom,
( ~ mode(X20,ok)
| ~ type(X20,and)
| ~ value(in(X19,X20),n0)
| value(out(n1,X20),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_0x_0) ).
cnf(halfadder_connection_out1not1_in2and1,axiom,
( ~ type(X74,halfadder)
| connection(out(n1,not1(X74)),in(n2,and1(X74))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1not1_in2and1) ).
cnf(c105,plain,
connection(out(n1,not1(h1(f))),in(n2,and1(h1(f)))),
inference(resolution,[status(thm)],[halfadder_connection_out1not1_in2and1,c23]) ).
cnf(diagnosis_or1_not1h1,negated_conjecture,
( ~ mode(or1(f),abnormal)
| ~ mode(not1(h1(f)),abnormal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_or1_not1h1) ).
cnf(halfadder_not1,axiom,
( ~ type(X18,halfadder)
| type(not1(X18),not) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_not1) ).
cnf(c27,plain,
type(not1(h1(f)),not),
inference(resolution,[status(thm)],[c23,halfadder_not1]) ).
cnf(c32,plain,
( mode(not1(h1(f)),ok)
| mode(not1(h1(f)),abnormal) ),
inference(resolution,[status(thm)],[c27,ok_or_abnormal]) ).
cnf(c132,plain,
( mode(not1(h1(f)),ok)
| ~ mode(or1(f),abnormal) ),
inference(resolution,[status(thm)],[c32,diagnosis_or1_not1h1]) ).
cnf(c821,plain,
mode(not1(h1(f)),ok),
inference(resolution,[status(thm)],[c816,c132]) ).
cnf(not_1_0_fw,axiom,
( ~ mode(X58,ok)
| ~ type(X58,not)
| ~ value(in(n1,X58),n1)
| value(out(n1,X58),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',not_1_0_fw) ).
cnf(halfadder_connection_out1and2_in1not1,axiom,
( ~ type(X70,halfadder)
| connection(out(n1,and2(X70)),in(n1,not1(X70))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1and2_in1not1) ).
cnf(c101,plain,
connection(out(n1,and2(h1(f))),in(n1,not1(h1(f)))),
inference(resolution,[status(thm)],[halfadder_connection_out1and2_in1not1,c23]) ).
cnf(c785,plain,
( ~ connection(out(n1,and2(h1(f))),X172)
| value(X172,n1) ),
inference(resolution,[status(thm)],[c782,value_propagation1]) ).
cnf(c792,plain,
value(in(n1,not1(h1(f))),n1),
inference(resolution,[status(thm)],[c785,c101]) ).
cnf(c798,plain,
( ~ mode(not1(h1(f)),ok)
| ~ type(not1(h1(f)),not)
| value(out(n1,not1(h1(f))),n0) ),
inference(resolution,[status(thm)],[c792,not_1_0_fw]) ).
cnf(c926,plain,
( ~ mode(not1(h1(f)),ok)
| value(out(n1,not1(h1(f))),n0) ),
inference(resolution,[status(thm)],[c798,c27]) ).
cnf(c927,plain,
value(out(n1,not1(h1(f))),n0),
inference(resolution,[status(thm)],[c926,c821]) ).
cnf(c928,plain,
( ~ connection(out(n1,not1(h1(f))),X281)
| value(X281,n0) ),
inference(resolution,[status(thm)],[c927,value_propagation1]) ).
cnf(c936,plain,
value(in(n2,and1(h1(f))),n0),
inference(resolution,[status(thm)],[c928,c105]) ).
cnf(c941,plain,
( ~ mode(and1(h1(f)),ok)
| ~ type(and1(h1(f)),and)
| value(out(n1,and1(h1(f))),n0) ),
inference(resolution,[status(thm)],[c936,and_0x_0]) ).
cnf(c997,plain,
( ~ mode(and1(h1(f)),ok)
| value(out(n1,and1(h1(f))),n0) ),
inference(resolution,[status(thm)],[c941,c28]) ).
cnf(c998,plain,
value(out(n1,and1(h1(f))),n0),
inference(resolution,[status(thm)],[c997,c820]) ).
cnf(c1002,plain,
( ~ connection(X300,out(n1,and1(h1(f))))
| value(X300,n0) ),
inference(resolution,[status(thm)],[c998,value_propagation2]) ).
cnf(c1007,plain,
value(out(s,h1(f)),n0),
inference(resolution,[status(thm)],[c1002,c67]) ).
cnf(c1008,plain,
( ~ connection(out(s,h1(f)),X301)
| value(X301,n0) ),
inference(resolution,[status(thm)],[c1007,value_propagation1]) ).
cnf(c1012,plain,
value(in(n2,h2(f)),n0),
inference(resolution,[status(thm)],[c1008,c112]) ).
cnf(c1014,plain,
( ~ connection(in(n2,h2(f)),X304)
| value(X304,n0) ),
inference(resolution,[status(thm)],[c1012,value_propagation1]) ).
cnf(c1021,plain,
value(in(n2,or1(h2(f))),n0),
inference(resolution,[status(thm)],[c1014,c59]) ).
cnf(c1028,plain,
( ~ value(in(n2,or1(h2(f))),X310)
| equal_value(X310,n0) ),
inference(resolution,[status(thm)],[c1021,unique_value]) ).
cnf(in1_1,plain,
value(in(n1,f),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',in1_1) ).
cnf(c0,plain,
( ~ connection(in(n1,f),X28)
| value(X28,n0) ),
inference(resolution,[status(thm)],[value_propagation1,in1_1]) ).
cnf(fulladder_connection_in1_in1h2,axiom,
( ~ type(X57,fulladder)
| connection(in(n1,X57),in(n1,h2(X57))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_in1_in1h2) ).
cnf(c70,plain,
connection(in(n1,f),in(n1,h2(f))),
inference(resolution,[status(thm)],[fulladder_connection_in1_in1h2,f_isa_fulladder]) ).
cnf(c71,plain,
value(in(n1,h2(f)),n0),
inference(resolution,[status(thm)],[c70,c0]) ).
cnf(c72,plain,
( ~ connection(in(n1,h2(f)),X59)
| value(X59,n0) ),
inference(resolution,[status(thm)],[c71,value_propagation1]) ).
cnf(halfadder_connection_in1_in1or1,axiom,
( ~ type(X50,halfadder)
| connection(in(n1,X50),in(n1,or1(X50))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1or1) ).
cnf(c57,plain,
connection(in(n1,h2(f)),in(n1,or1(h2(f)))),
inference(resolution,[status(thm)],[halfadder_connection_in1_in1or1,c34]) ).
cnf(c146,plain,
value(in(n1,or1(h2(f))),n0),
inference(resolution,[status(thm)],[c57,c72]) ).
cnf(c151,plain,
( ~ value(in(n1,or1(h2(f))),X88)
| equal_value(X88,n0) ),
inference(resolution,[status(thm)],[c146,unique_value]) ).
cnf(diagnosis_or1_or1h2,negated_conjecture,
( ~ mode(or1(f),abnormal)
| ~ mode(or1(h2(f)),abnormal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_or1_or1h2) ).
cnf(halfadder_or1,axiom,
( ~ type(X21,halfadder)
| type(or1(X21),or) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_or1) ).
cnf(c35,plain,
type(or1(h2(f)),or),
inference(resolution,[status(thm)],[c34,halfadder_or1]) ).
cnf(c40,plain,
( mode(or1(h2(f)),ok)
| mode(or1(h2(f)),abnormal) ),
inference(resolution,[status(thm)],[c35,ok_or_abnormal]) ).
cnf(c138,plain,
( mode(or1(h2(f)),ok)
| ~ mode(or1(f),abnormal) ),
inference(resolution,[status(thm)],[c40,diagnosis_or1_or1h2]) ).
cnf(c818,plain,
mode(or1(h2(f)),ok),
inference(resolution,[status(thm)],[c816,c138]) ).
cnf(or_1_11,axiom,
( ~ mode(X46,ok)
| ~ type(X46,or)
| ~ value(out(n1,X46),n1)
| value(in(n1,X46),n1)
| value(in(n2,X46),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_1_11) ).
cnf(halfadder_connection_out1or1_in1_and1,axiom,
( ~ type(X68,halfadder)
| connection(out(n1,or1(X68)),in(n1,and1(X68))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1or1_in1_and1) ).
cnf(c90,plain,
connection(out(n1,or1(h2(f))),in(n1,and1(h2(f)))),
inference(resolution,[status(thm)],[halfadder_connection_out1or1_in1_and1,c34]) ).
cnf(diagnosis_or1_and1h2,negated_conjecture,
( ~ mode(or1(f),abnormal)
| ~ mode(and1(h2(f)),abnormal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_or1_and1h2) ).
cnf(c39,plain,
type(and1(h2(f)),and),
inference(resolution,[status(thm)],[c34,halfadder_and1]) ).
cnf(c43,plain,
( mode(and1(h2(f)),ok)
| mode(and1(h2(f)),abnormal) ),
inference(resolution,[status(thm)],[c39,ok_or_abnormal]) ).
cnf(and_1_1x,axiom,
( ~ mode(X27,ok)
| ~ type(X27,and)
| ~ value(out(n1,X27),n1)
| value(in(n1,X27),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_1_1x) ).
cnf(outs_1,plain,
value(out(s,f),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outs_1) ).
cnf(c3,plain,
( ~ connection(out(s,f),X32)
| value(X32,n1) ),
inference(resolution,[status(thm)],[outs_1,value_propagation1]) ).
cnf(fulladder_connection_outs_outsh2,axiom,
( ~ type(X75,fulladder)
| connection(out(s,X75),out(s,h2(X75))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outs_outsh2) ).
cnf(c106,plain,
connection(out(s,f),out(s,h2(f))),
inference(resolution,[status(thm)],[fulladder_connection_outs_outsh2,f_isa_fulladder]) ).
cnf(c107,plain,
value(out(s,h2(f)),n1),
inference(resolution,[status(thm)],[c106,c3]) ).
cnf(c108,plain,
( ~ connection(out(s,h2(f)),X76)
| value(X76,n1) ),
inference(resolution,[status(thm)],[c107,value_propagation1]) ).
cnf(c66,plain,
connection(out(s,h2(f)),out(n1,and1(h2(f)))),
inference(resolution,[status(thm)],[halfadder_connection_outs_out1and1,c34]) ).
cnf(c192,plain,
value(out(n1,and1(h2(f))),n1),
inference(resolution,[status(thm)],[c66,c108]) ).
cnf(c203,plain,
( ~ mode(and1(h2(f)),ok)
| ~ type(and1(h2(f)),and)
| value(in(n1,and1(h2(f))),n1) ),
inference(resolution,[status(thm)],[c192,and_1_1x]) ).
cnf(c423,plain,
( ~ mode(and1(h2(f)),ok)
| value(in(n1,and1(h2(f))),n1) ),
inference(resolution,[status(thm)],[c203,c39]) ).
cnf(c532,plain,
( value(in(n1,and1(h2(f))),n1)
| mode(and1(h2(f)),abnormal) ),
inference(resolution,[status(thm)],[c423,c43]) ).
cnf(c575,plain,
( value(in(n1,and1(h2(f))),n1)
| ~ mode(or1(f),abnormal) ),
inference(resolution,[status(thm)],[c532,diagnosis_or1_and1h2]) ).
cnf(c819,plain,
value(in(n1,and1(h2(f))),n1),
inference(resolution,[status(thm)],[c816,c575]) ).
cnf(c840,plain,
( ~ connection(X193,in(n1,and1(h2(f))))
| value(X193,n1) ),
inference(resolution,[status(thm)],[c819,value_propagation2]) ).
cnf(c870,plain,
value(out(n1,or1(h2(f))),n1),
inference(resolution,[status(thm)],[c840,c90]) ).
cnf(c874,plain,
( ~ mode(or1(h2(f)),ok)
| ~ type(or1(h2(f)),or)
| value(in(n1,or1(h2(f))),n1)
| value(in(n2,or1(h2(f))),n1) ),
inference(resolution,[status(thm)],[c870,or_1_11]) ).
cnf(c1043,plain,
( ~ mode(or1(h2(f)),ok)
| value(in(n1,or1(h2(f))),n1)
| value(in(n2,or1(h2(f))),n1) ),
inference(resolution,[status(thm)],[c874,c35]) ).
cnf(c1044,plain,
( value(in(n1,or1(h2(f))),n1)
| value(in(n2,or1(h2(f))),n1) ),
inference(resolution,[status(thm)],[c1043,c818]) ).
cnf(c1046,plain,
( value(in(n2,or1(h2(f))),n1)
| equal_value(n1,n0) ),
inference(resolution,[status(thm)],[c1044,c151]) ).
cnf(c1063,plain,
equal_value(n1,n0),
inference(resolution,[status(thm)],[c1046,c1028]) ).
cnf(c1067,plain,
$false,
inference(resolution,[status(thm)],[c1063,equal_value2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : HWV007-1 : TPTP v8.1.2. Released v2.1.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n010.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 07:16:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.68/1.84 % Version: 1.5
% 1.68/1.84 % SZS status Unsatisfiable
% 1.68/1.84 % SZS output start CNFRefutation
% See solution above
% 1.68/1.85
% 1.68/1.85 % Initial clauses : 56
% 1.68/1.85 % Processed clauses : 488
% 1.68/1.85 % Factors computed : 1
% 1.68/1.85 % Resolvents computed: 1067
% 1.68/1.85 % Tautologies deleted: 14
% 1.68/1.85 % Forward subsumed : 596
% 1.68/1.85 % Backward subsumed : 170
% 1.68/1.85 % -------- CPU Time ---------
% 1.68/1.85 % User time : 1.480 s
% 1.68/1.85 % System time : 0.016 s
% 1.68/1.85 % Total time : 1.496 s
%------------------------------------------------------------------------------