%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HWV008-1.002 : TPTP v8.1.2. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:55 EDT 2024
% Result : Unsatisfiable 1.34s 1.52s
% Output : Refutation 1.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 29
% Syntax : Number of clauses : 92 ( 46 unt; 10 nHn; 92 RR)
% Number of literals : 153 ( 0 equ; 55 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 5 ( 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 : 43 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(equal_value1,axiom,
~ equal_value(n0,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',equal_value1) ).
cnf(unique_value,axiom,
( ~ value(X11,X10)
| ~ value(X11,X9)
| equal_value(X10,X9) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',unique_value) ).
cnf(fulladder_halfadder1,axiom,
( ~ type(X23,fulladder)
| type(h1(X23),halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_halfadder1) ).
cnf(a_isa_2bit_adder,plain,
type(a,nbit_adder(n2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_isa_2bit_adder) ).
cnf(nbit_adder_fulladder2,axiom,
( ~ type(X62,nbit_adder(n2))
| type(f(n2,X62),fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nbit_adder_fulladder2) ).
cnf(c75,plain,
type(f(n2,a),fulladder),
inference(resolution,[status(thm)],[nbit_adder_fulladder2,a_isa_2bit_adder]) ).
cnf(c78,plain,
type(h1(f(n2,a)),halfadder),
inference(resolution,[status(thm)],[c75,fulladder_halfadder1]) ).
cnf(halfadder_connection_outc_out1and2,axiom,
( ~ type(X70,halfadder)
| connection(out(c,X70),out(n1,and2(X70))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outc_out1and2) ).
cnf(c122,plain,
connection(out(c,h1(f(n2,a))),out(n1,and2(h1(f(n2,a))))),
inference(resolution,[status(thm)],[halfadder_connection_outc_out1and2,c78]) ).
cnf(value_propagation1,axiom,
( ~ connection(X5,X4)
| ~ value(X5,X3)
| value(X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',value_propagation1) ).
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(c151,plain,
connection(out(c,h1(f(n2,a))),in(n2,or1(f(n2,a)))),
inference(resolution,[status(thm)],[fulladder_connection_outch1_in2or1,c75]) ).
cnf(value_propagation2,axiom,
( ~ connection(X8,X7)
| ~ value(X7,X6)
| value(X8,X6) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',value_propagation2) ).
cnf(diagnosis_or1f2a,negated_conjecture,
~ mode(or1(f(n2,a)),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_or1f2a) ).
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(fulladder_or1,axiom,
( ~ type(X25,fulladder)
| type(or1(X25),or) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_or1) ).
cnf(c80,plain,
type(or1(f(n2,a)),or),
inference(resolution,[status(thm)],[c75,fulladder_or1]) ).
cnf(c91,plain,
( mode(or1(f(n2,a)),ok)
| mode(or1(f(n2,a)),abnormal) ),
inference(resolution,[status(thm)],[c80,ok_or_abnormal]) ).
cnf(c242,plain,
mode(or1(f(n2,a)),ok),
inference(resolution,[status(thm)],[c91,diagnosis_or1f2a]) ).
cnf(or_1_11,axiom,
( ~ mode(X51,ok)
| ~ type(X51,or)
| ~ value(out(n1,X51),n1)
| value(in(n1,X51),n1)
| value(in(n2,X51),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_1_11) ).
cnf(outc_1,plain,
value(out(c,a),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outc_1) ).
cnf(c15,plain,
( ~ connection(out(c,a),X46)
| value(X46,n1) ),
inference(resolution,[status(thm)],[outc_1,value_propagation1]) ).
cnf(nbit_adder_connection_outc_outcf1,axiom,
( ~ type(X87,nbit_adder(n2))
| connection(out(c,X87),out(c,f(n2,X87))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nbit_adder_connection_outc_outcf1) ).
cnf(c176,plain,
connection(out(c,a),out(c,f(n2,a))),
inference(resolution,[status(thm)],[nbit_adder_connection_outc_outcf1,a_isa_2bit_adder]) ).
cnf(c180,plain,
value(out(c,f(n2,a)),n1),
inference(resolution,[status(thm)],[c176,c15]) ).
cnf(c183,plain,
( ~ connection(out(c,f(n2,a)),X94)
| value(X94,n1) ),
inference(resolution,[status(thm)],[c180,value_propagation1]) ).
cnf(fulladder_connection_outc_out1or1,axiom,
( ~ type(X76,fulladder)
| connection(out(c,X76),out(n1,or1(X76))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outc_out1or1) ).
cnf(c137,plain,
connection(out(c,f(n2,a)),out(n1,or1(f(n2,a)))),
inference(resolution,[status(thm)],[fulladder_connection_outc_out1or1,c75]) ).
cnf(c298,plain,
value(out(n1,or1(f(n2,a))),n1),
inference(resolution,[status(thm)],[c137,c183]) ).
cnf(c301,plain,
( ~ mode(or1(f(n2,a)),ok)
| ~ type(or1(f(n2,a)),or)
| value(in(n1,or1(f(n2,a))),n1)
| value(in(n2,or1(f(n2,a))),n1) ),
inference(resolution,[status(thm)],[c298,or_1_11]) ).
cnf(c408,plain,
( ~ mode(or1(f(n2,a)),ok)
| value(in(n1,or1(f(n2,a))),n1)
| value(in(n2,or1(f(n2,a))),n1) ),
inference(resolution,[status(thm)],[c301,c80]) ).
cnf(c409,plain,
( value(in(n1,or1(f(n2,a))),n1)
| value(in(n2,or1(f(n2,a))),n1) ),
inference(resolution,[status(thm)],[c408,c242]) ).
cnf(c413,plain,
( value(in(n2,or1(f(n2,a))),n1)
| ~ value(in(n1,or1(f(n2,a))),X165)
| equal_value(X165,n1) ),
inference(resolution,[status(thm)],[c409,unique_value]) ).
cnf(fulladder_connection_outch2_in1or1,axiom,
( ~ type(X81,fulladder)
| connection(out(c,h2(X81)),in(n1,or1(X81))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outch2_in1or1) ).
cnf(c153,plain,
connection(out(c,h2(f(n2,a))),in(n1,or1(f(n2,a)))),
inference(resolution,[status(thm)],[fulladder_connection_outch2_in1or1,c75]) ).
cnf(fulladder_halfadder2,axiom,
( ~ type(X24,fulladder)
| type(h2(X24),halfadder) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_halfadder2) ).
cnf(c79,plain,
type(h2(f(n2,a)),halfadder),
inference(resolution,[status(thm)],[c75,fulladder_halfadder2]) ).
cnf(c121,plain,
connection(out(c,h2(f(n2,a))),out(n1,and2(h2(f(n2,a))))),
inference(resolution,[status(thm)],[halfadder_connection_outc_out1and2,c79]) ).
cnf(diagnosis_and2h1f2a,negated_conjecture,
~ mode(and2(h2(f(n2,a))),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_and2h1f2a) ).
cnf(halfadder_and2,axiom,
( ~ type(X19,halfadder)
| type(and2(X19),and) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_and2) ).
cnf(c86,plain,
type(and2(h2(f(n2,a))),and),
inference(resolution,[status(thm)],[c79,halfadder_and2]) ).
cnf(c96,plain,
( mode(and2(h2(f(n2,a))),ok)
| mode(and2(h2(f(n2,a))),abnormal) ),
inference(resolution,[status(thm)],[c86,ok_or_abnormal]) ).
cnf(c312,plain,
mode(and2(h2(f(n2,a))),ok),
inference(resolution,[status(thm)],[c96,diagnosis_and2h1f2a]) ).
cnf(and_0x_0,axiom,
( ~ mode(X17,ok)
| ~ type(X17,and)
| ~ value(in(X16,X17),n0)
| value(out(n1,X17),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_0x_0) ).
cnf(ina2_0,plain,
value(in(a2,a),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ina2_0) ).
cnf(c1,plain,
( ~ connection(in(a2,a),X29)
| value(X29,n0) ),
inference(resolution,[status(thm)],[ina2_0,value_propagation1]) ).
cnf(nbit_adder_connection_ina2_in1f2,axiom,
( ~ type(X95,nbit_adder(n2))
| connection(in(a2,X95),in(n1,f(n2,X95))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nbit_adder_connection_ina2_in1f2) ).
cnf(c194,plain,
connection(in(a2,a),in(n1,f(n2,a))),
inference(resolution,[status(thm)],[nbit_adder_connection_ina2_in1f2,a_isa_2bit_adder]) ).
cnf(c207,plain,
value(in(n1,f(n2,a)),n0),
inference(resolution,[status(thm)],[c194,c1]) ).
cnf(c211,plain,
( ~ connection(in(n1,f(n2,a)),X107)
| value(X107,n0) ),
inference(resolution,[status(thm)],[c207,value_propagation1]) ).
cnf(fulladder_connection_in1_in1h2,axiom,
( ~ type(X71,fulladder)
| connection(in(n1,X71),in(n1,h2(X71))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_in1_in1h2) ).
cnf(c125,plain,
connection(in(n1,f(n2,a)),in(n1,h2(f(n2,a)))),
inference(resolution,[status(thm)],[fulladder_connection_in1_in1h2,c75]) ).
cnf(c254,plain,
value(in(n1,h2(f(n2,a))),n0),
inference(resolution,[status(thm)],[c125,c211]) ).
cnf(c258,plain,
( ~ connection(in(n1,h2(f(n2,a))),X119)
| value(X119,n0) ),
inference(resolution,[status(thm)],[c254,value_propagation1]) ).
cnf(halfadder_connection_in1_in1and2,axiom,
( ~ type(X67,halfadder)
| connection(in(n1,X67),in(n1,and2(X67))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1and2) ).
cnf(c109,plain,
connection(in(n1,h2(f(n2,a))),in(n1,and2(h2(f(n2,a))))),
inference(resolution,[status(thm)],[halfadder_connection_in1_in1and2,c79]) ).
cnf(c369,plain,
value(in(n1,and2(h2(f(n2,a)))),n0),
inference(resolution,[status(thm)],[c109,c258]) ).
cnf(c371,plain,
( ~ mode(and2(h2(f(n2,a))),ok)
| ~ type(and2(h2(f(n2,a))),and)
| value(out(n1,and2(h2(f(n2,a)))),n0) ),
inference(resolution,[status(thm)],[c369,and_0x_0]) ).
cnf(c489,plain,
( ~ mode(and2(h2(f(n2,a))),ok)
| value(out(n1,and2(h2(f(n2,a)))),n0) ),
inference(resolution,[status(thm)],[c371,c86]) ).
cnf(c490,plain,
value(out(n1,and2(h2(f(n2,a)))),n0),
inference(resolution,[status(thm)],[c489,c312]) ).
cnf(c493,plain,
( ~ connection(X174,out(n1,and2(h2(f(n2,a)))))
| value(X174,n0) ),
inference(resolution,[status(thm)],[c490,value_propagation2]) ).
cnf(c499,plain,
value(out(c,h2(f(n2,a))),n0),
inference(resolution,[status(thm)],[c493,c121]) ).
cnf(c502,plain,
( ~ connection(out(c,h2(f(n2,a))),X176)
| value(X176,n0) ),
inference(resolution,[status(thm)],[c499,value_propagation1]) ).
cnf(c504,plain,
value(in(n1,or1(f(n2,a))),n0),
inference(resolution,[status(thm)],[c502,c153]) ).
cnf(c510,plain,
( value(in(n2,or1(f(n2,a))),n1)
| equal_value(n0,n1) ),
inference(resolution,[status(thm)],[c504,c413]) ).
cnf(c539,plain,
value(in(n2,or1(f(n2,a))),n1),
inference(resolution,[status(thm)],[c510,equal_value1]) ).
cnf(c542,plain,
( ~ connection(X183,in(n2,or1(f(n2,a))))
| value(X183,n1) ),
inference(resolution,[status(thm)],[c539,value_propagation2]) ).
cnf(c548,plain,
value(out(c,h1(f(n2,a))),n1),
inference(resolution,[status(thm)],[c542,c151]) ).
cnf(c551,plain,
( ~ connection(out(c,h1(f(n2,a))),X187)
| value(X187,n1) ),
inference(resolution,[status(thm)],[c548,value_propagation1]) ).
cnf(c555,plain,
value(out(n1,and2(h1(f(n2,a)))),n1),
inference(resolution,[status(thm)],[c551,c122]) ).
cnf(c562,plain,
( ~ value(out(n1,and2(h1(f(n2,a)))),X194)
| equal_value(X194,n1) ),
inference(resolution,[status(thm)],[c555,unique_value]) ).
cnf(diagnosis_and2h2f2a,negated_conjecture,
~ mode(and2(h1(f(n2,a))),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_and2h2f2a) ).
cnf(c81,plain,
type(and2(h1(f(n2,a))),and),
inference(resolution,[status(thm)],[c78,halfadder_and2]) ).
cnf(c92,plain,
( mode(and2(h1(f(n2,a))),ok)
| mode(and2(h1(f(n2,a))),abnormal) ),
inference(resolution,[status(thm)],[c81,ok_or_abnormal]) ).
cnf(c297,plain,
mode(and2(h1(f(n2,a))),ok),
inference(resolution,[status(thm)],[c92,diagnosis_and2h2f2a]) ).
cnf(inb2_0,plain,
value(in(b2,a),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inb2_0) ).
cnf(c3,plain,
( ~ connection(in(b2,a),X31)
| value(X31,n0) ),
inference(resolution,[status(thm)],[inb2_0,value_propagation1]) ).
cnf(nbit_adder_connection_inb2_in2f2,axiom,
( ~ type(X97,nbit_adder(n2))
| connection(in(b2,X97),in(n2,f(n2,X97))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nbit_adder_connection_inb2_in2f2) ).
cnf(c203,plain,
connection(in(b2,a),in(n2,f(n2,a))),
inference(resolution,[status(thm)],[nbit_adder_connection_inb2_in2f2,a_isa_2bit_adder]) ).
cnf(c217,plain,
value(in(n2,f(n2,a)),n0),
inference(resolution,[status(thm)],[c203,c3]) ).
cnf(c221,plain,
( ~ connection(in(n2,f(n2,a)),X110)
| value(X110,n0) ),
inference(resolution,[status(thm)],[c217,value_propagation1]) ).
cnf(fulladder_connection_in2_in1h1,axiom,
( ~ type(X72,fulladder)
| connection(in(n2,X72),in(n1,h1(X72))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-2.ax',fulladder_connection_in2_in1h1) ).
cnf(c127,plain,
connection(in(n2,f(n2,a)),in(n1,h1(f(n2,a)))),
inference(resolution,[status(thm)],[fulladder_connection_in2_in1h1,c75]) ).
cnf(c275,plain,
value(in(n1,h1(f(n2,a))),n0),
inference(resolution,[status(thm)],[c127,c221]) ).
cnf(c279,plain,
( ~ connection(in(n1,h1(f(n2,a))),X125)
| value(X125,n0) ),
inference(resolution,[status(thm)],[c275,value_propagation1]) ).
cnf(c110,plain,
connection(in(n1,h1(f(n2,a))),in(n1,and2(h1(f(n2,a))))),
inference(resolution,[status(thm)],[halfadder_connection_in1_in1and2,c78]) ).
cnf(c377,plain,
value(in(n1,and2(h1(f(n2,a)))),n0),
inference(resolution,[status(thm)],[c110,c279]) ).
cnf(c379,plain,
( ~ mode(and2(h1(f(n2,a))),ok)
| ~ type(and2(h1(f(n2,a))),and)
| value(out(n1,and2(h1(f(n2,a)))),n0) ),
inference(resolution,[status(thm)],[c377,and_0x_0]) ).
cnf(c513,plain,
( ~ mode(and2(h1(f(n2,a))),ok)
| value(out(n1,and2(h1(f(n2,a)))),n0) ),
inference(resolution,[status(thm)],[c379,c81]) ).
cnf(c578,plain,
value(out(n1,and2(h1(f(n2,a)))),n0),
inference(resolution,[status(thm)],[c513,c297]) ).
cnf(c583,plain,
equal_value(n0,n1),
inference(resolution,[status(thm)],[c578,c562]) ).
cnf(c588,plain,
$false,
inference(resolution,[status(thm)],[c583,equal_value1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : HWV008-1.002 : TPTP v8.1.2. Bugfixed v2.2.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 07:15:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.34/1.52 % Version: 1.5
% 1.34/1.52 % SZS status Unsatisfiable
% 1.34/1.52 % SZS output start CNFRefutation
% See solution above
% 1.34/1.52
% 1.34/1.52 % Initial clauses : 68
% 1.34/1.52 % Processed clauses : 399
% 1.34/1.52 % Factors computed : 1
% 1.34/1.52 % Resolvents computed: 588
% 1.34/1.52 % Tautologies deleted: 26
% 1.34/1.52 % Forward subsumed : 166
% 1.34/1.52 % Backward subsumed : 31
% 1.34/1.52 % -------- CPU Time ---------
% 1.34/1.52 % User time : 1.149 s
% 1.34/1.52 % System time : 0.017 s
% 1.34/1.52 % Total time : 1.166 s
%------------------------------------------------------------------------------