%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HWV008-2.002 : TPTP v8.1.2. Bugfixed v2.7.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.06s 1.29s
% Output : Refutation 1.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 31
% Syntax : Number of clauses : 89 ( 43 unt; 10 nHn; 89 RR)
% Number of literals : 145 ( 0 equ; 51 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 1 con; 0-1 aty)
% Number of variables : 28 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(unique_value,axiom,
( ~ zero(X2)
| ~ one(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',unique_value) ).
cnf(value_propagation_one1,axiom,
( ~ connection(X9,X8)
| ~ one(X9)
| one(X8) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',value_propagation_one1) ).
cnf(fulladder_halfadder1,axiom,
( ~ fulladder(X16)
| halfadder(h1(X16)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_halfadder1) ).
cnf(a_isa_2bit_adder,plain,
nbit_adder2(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_isa_2bit_adder) ).
cnf(nbit_adder_fulladder2,axiom,
( ~ nbit_adder2(X22)
| fulladder(f2(X22)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nbit_adder_fulladder2) ).
cnf(c5,plain,
fulladder(f2(a)),
inference(resolution,[status(thm)],[nbit_adder_fulladder2,a_isa_2bit_adder]) ).
cnf(c6,plain,
halfadder(h1(f2(a))),
inference(resolution,[status(thm)],[c5,fulladder_halfadder1]) ).
cnf(halfadder_connection_outc_out1and2,axiom,
( ~ halfadder(X47)
| connection(outc(X47),out1(and2(X47))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_outc_out1and2) ).
cnf(c70,plain,
connection(outc(h1(f2(a))),out1(and2(h1(f2(a))))),
inference(resolution,[status(thm)],[halfadder_connection_outc_out1and2,c6]) ).
cnf(c404,plain,
( ~ one(outc(h1(f2(a))))
| one(out1(and2(h1(f2(a))))) ),
inference(resolution,[status(thm)],[c70,value_propagation_one1]) ).
cnf(value_propagation_one2,axiom,
( ~ connection(X19,X18)
| ~ one(X18)
| one(X19) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',value_propagation_one2) ).
cnf(fulladder_connection_outch1_in2or1,axiom,
( ~ fulladder(X65)
| connection(outc(h1(X65)),in2(or1(X65))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_outch1_in2or1) ).
cnf(c135,plain,
connection(outc(h1(f2(a))),in2(or1(f2(a)))),
inference(resolution,[status(thm)],[fulladder_connection_outch1_in2or1,c5]) ).
cnf(c255,plain,
( ~ one(in2(or1(f2(a))))
| one(outc(h1(f2(a)))) ),
inference(resolution,[status(thm)],[c135,value_propagation_one2]) ).
cnf(fulladder_connection_outch2_in1or1,axiom,
( ~ fulladder(X66)
| connection(outc(h2(X66)),in1(or1(X66))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_outch2_in1or1) ).
cnf(c142,plain,
connection(outc(h2(f2(a))),in1(or1(f2(a)))),
inference(resolution,[status(thm)],[fulladder_connection_outch2_in1or1,c5]) ).
cnf(c266,plain,
( ~ one(in1(or1(f2(a))))
| one(outc(h2(f2(a)))) ),
inference(resolution,[status(thm)],[c142,value_propagation_one2]) ).
cnf(diagnosis_or1f2a,negated_conjecture,
~ abnormal(or1(f2(a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1f2a) ).
cnf(fulladder_or1,axiom,
( ~ fulladder(X20)
| logic_or(or1(X20)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_or1) ).
cnf(c8,plain,
logic_or(or1(f2(a))),
inference(resolution,[status(thm)],[c5,fulladder_or1]) ).
cnf(or_ok_or_abnormal,axiom,
( ~ logic_or(X26)
| or_ok(X26)
| abnormal(X26) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',or_ok_or_abnormal) ).
cnf(c25,plain,
( or_ok(or1(f2(a)))
| abnormal(or1(f2(a))) ),
inference(resolution,[status(thm)],[or_ok_or_abnormal,c8]) ).
cnf(c153,plain,
or_ok(or1(f2(a))),
inference(resolution,[status(thm)],[c25,diagnosis_or1f2a]) ).
cnf(or_1_11,axiom,
( ~ or_ok(X38)
| ~ one(out1(X38))
| one(in1(X38))
| one(in2(X38)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',or_1_11) ).
cnf(outc_1,plain,
one(outc(a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outc_1) ).
cnf(nbit_adder_connection_outc_outcf1,axiom,
( ~ nbit_adder2(X57)
| connection(outc(X57),outc(f2(X57))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nbit_adder_connection_outc_outcf1) ).
cnf(c99,plain,
connection(outc(a),outc(f2(a))),
inference(resolution,[status(thm)],[nbit_adder_connection_outc_outcf1,a_isa_2bit_adder]) ).
cnf(c101,plain,
( ~ one(outc(a))
| one(outc(f2(a))) ),
inference(resolution,[status(thm)],[c99,value_propagation_one1]) ).
cnf(c150,plain,
one(outc(f2(a))),
inference(resolution,[status(thm)],[c101,outc_1]) ).
cnf(fulladder_connection_outc_out1or1,axiom,
( ~ fulladder(X53)
| connection(outc(X53),out1(or1(X53))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_outc_out1or1) ).
cnf(c83,plain,
connection(outc(f2(a)),out1(or1(f2(a)))),
inference(resolution,[status(thm)],[fulladder_connection_outc_out1or1,c5]) ).
cnf(c230,plain,
( ~ one(outc(f2(a)))
| one(out1(or1(f2(a)))) ),
inference(resolution,[status(thm)],[c83,value_propagation_one1]) ).
cnf(c317,plain,
one(out1(or1(f2(a)))),
inference(resolution,[status(thm)],[c230,c150]) ).
cnf(c322,plain,
( ~ or_ok(or1(f2(a)))
| one(in1(or1(f2(a))))
| one(in2(or1(f2(a)))) ),
inference(resolution,[status(thm)],[c317,or_1_11]) ).
cnf(c465,plain,
( one(in1(or1(f2(a))))
| one(in2(or1(f2(a)))) ),
inference(resolution,[status(thm)],[c322,c153]) ).
cnf(c466,plain,
( one(in2(or1(f2(a))))
| one(outc(h2(f2(a)))) ),
inference(resolution,[status(thm)],[c465,c266]) ).
cnf(c474,plain,
( one(outc(h2(f2(a))))
| one(outc(h1(f2(a)))) ),
inference(resolution,[status(thm)],[c466,c255]) ).
cnf(c486,plain,
( one(outc(h1(f2(a))))
| ~ zero(outc(h2(f2(a)))) ),
inference(resolution,[status(thm)],[c474,unique_value]) ).
cnf(value_propagation_zero2,axiom,
( ~ connection(X12,X11)
| ~ zero(X11)
| zero(X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',value_propagation_zero2) ).
cnf(fulladder_halfadder2,axiom,
( ~ fulladder(X17)
| halfadder(h2(X17)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_halfadder2) ).
cnf(c7,plain,
halfadder(h2(f2(a))),
inference(resolution,[status(thm)],[c5,fulladder_halfadder2]) ).
cnf(c68,plain,
connection(outc(h2(f2(a))),out1(and2(h2(f2(a))))),
inference(resolution,[status(thm)],[halfadder_connection_outc_out1and2,c7]) ).
cnf(c397,plain,
( ~ zero(out1(and2(h2(f2(a)))))
| zero(outc(h2(f2(a)))) ),
inference(resolution,[status(thm)],[c68,value_propagation_zero2]) ).
cnf(diagnosis_and2h2f2a,negated_conjecture,
~ abnormal(and2(h2(f2(a)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_and2h2f2a) ).
cnf(and_ok_or_abnormal,axiom,
( ~ logic_and(X25)
| and_ok(X25)
| abnormal(X25) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',and_ok_or_abnormal) ).
cnf(halfadder_and2,axiom,
( ~ halfadder(X13)
| logic_and(and2(X13)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_and2) ).
cnf(c21,plain,
logic_and(and2(h2(f2(a)))),
inference(resolution,[status(thm)],[c7,halfadder_and2]) ).
cnf(c40,plain,
( and_ok(and2(h2(f2(a))))
| abnormal(and2(h2(f2(a)))) ),
inference(resolution,[status(thm)],[c21,and_ok_or_abnormal]) ).
cnf(c281,plain,
and_ok(and2(h2(f2(a)))),
inference(resolution,[status(thm)],[c40,diagnosis_and2h2f2a]) ).
cnf(and_0x_0,axiom,
( ~ and_ok(X23)
| ~ zero(in1(X23))
| zero(out1(X23)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',and_0x_0) ).
cnf(ina2_0,plain,
zero(ina2(a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ina2_0) ).
cnf(value_propagation_zero1,axiom,
( ~ connection(X7,X6)
| ~ zero(X7)
| zero(X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-0.ax',value_propagation_zero1) ).
cnf(nbit_adder_connection_ina2_in1f2,axiom,
( ~ nbit_adder2(X61)
| connection(ina2(X61),in1(f2(X61))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nbit_adder_connection_ina2_in1f2) ).
cnf(c118,plain,
connection(ina2(a),in1(f2(a))),
inference(resolution,[status(thm)],[nbit_adder_connection_ina2_in1f2,a_isa_2bit_adder]) ).
cnf(c124,plain,
( ~ zero(ina2(a))
| zero(in1(f2(a))) ),
inference(resolution,[status(thm)],[c118,value_propagation_zero1]) ).
cnf(c171,plain,
zero(in1(f2(a))),
inference(resolution,[status(thm)],[c124,ina2_0]) ).
cnf(fulladder_connection_in1_in1h2,axiom,
( ~ fulladder(X48)
| connection(in1(X48),in1(h2(X48))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_in1_in1h2) ).
cnf(c71,plain,
connection(in1(f2(a)),in1(h2(f2(a)))),
inference(resolution,[status(thm)],[fulladder_connection_in1_in1h2,c5]) ).
cnf(c197,plain,
( ~ zero(in1(f2(a)))
| zero(in1(h2(f2(a)))) ),
inference(resolution,[status(thm)],[c71,value_propagation_zero1]) ).
cnf(c277,plain,
zero(in1(h2(f2(a)))),
inference(resolution,[status(thm)],[c197,c171]) ).
cnf(halfadder_connection_in1_in1and2,axiom,
( ~ halfadder(X44)
| connection(in1(X44),in1(and2(X44))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-1.ax',halfadder_connection_in1_in1and2) ).
cnf(c56,plain,
connection(in1(h2(f2(a))),in1(and2(h2(f2(a))))),
inference(resolution,[status(thm)],[halfadder_connection_in1_in1and2,c7]) ).
cnf(c350,plain,
( ~ zero(in1(h2(f2(a))))
| zero(in1(and2(h2(f2(a))))) ),
inference(resolution,[status(thm)],[c56,value_propagation_zero1]) ).
cnf(c499,plain,
zero(in1(and2(h2(f2(a))))),
inference(resolution,[status(thm)],[c350,c277]) ).
cnf(c500,plain,
( ~ and_ok(and2(h2(f2(a))))
| zero(out1(and2(h2(f2(a))))) ),
inference(resolution,[status(thm)],[c499,and_0x_0]) ).
cnf(c516,plain,
zero(out1(and2(h2(f2(a))))),
inference(resolution,[status(thm)],[c500,c281]) ).
cnf(c521,plain,
zero(outc(h2(f2(a)))),
inference(resolution,[status(thm)],[c516,c397]) ).
cnf(c522,plain,
one(outc(h1(f2(a)))),
inference(resolution,[status(thm)],[c521,c486]) ).
cnf(c527,plain,
one(out1(and2(h1(f2(a))))),
inference(resolution,[status(thm)],[c522,c404]) ).
cnf(c536,plain,
~ zero(out1(and2(h1(f2(a))))),
inference(resolution,[status(thm)],[c527,unique_value]) ).
cnf(diagnosis_and2h1f2a,negated_conjecture,
~ abnormal(and2(h1(f2(a)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_and2h1f2a) ).
cnf(c17,plain,
logic_and(and2(h1(f2(a)))),
inference(resolution,[status(thm)],[c6,halfadder_and2]) ).
cnf(c36,plain,
( and_ok(and2(h1(f2(a))))
| abnormal(and2(h1(f2(a)))) ),
inference(resolution,[status(thm)],[c17,and_ok_or_abnormal]) ).
cnf(c243,plain,
and_ok(and2(h1(f2(a)))),
inference(resolution,[status(thm)],[c36,diagnosis_and2h1f2a]) ).
cnf(inb2_0,plain,
zero(inb2(a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inb2_0) ).
cnf(nbit_adder_connection_inb2_in2f2,axiom,
( ~ nbit_adder2(X63)
| connection(inb2(X63),in2(f2(X63))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nbit_adder_connection_inb2_in2f2) ).
cnf(c125,plain,
connection(inb2(a),in2(f2(a))),
inference(resolution,[status(thm)],[nbit_adder_connection_inb2_in2f2,a_isa_2bit_adder]) ).
cnf(c129,plain,
( ~ zero(inb2(a))
| zero(in2(f2(a))) ),
inference(resolution,[status(thm)],[c125,value_propagation_zero1]) ).
cnf(c177,plain,
zero(in2(f2(a))),
inference(resolution,[status(thm)],[c129,inb2_0]) ).
cnf(fulladder_connection_in2_in1h1,axiom,
( ~ fulladder(X50)
| connection(in2(X50),in1(h1(X50))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV002-2.ax',fulladder_connection_in2_in1h1) ).
cnf(c77,plain,
connection(in2(f2(a)),in1(h1(f2(a)))),
inference(resolution,[status(thm)],[fulladder_connection_in2_in1h1,c5]) ).
cnf(c205,plain,
( ~ zero(in2(f2(a)))
| zero(in1(h1(f2(a)))) ),
inference(resolution,[status(thm)],[c77,value_propagation_zero1]) ).
cnf(c290,plain,
zero(in1(h1(f2(a)))),
inference(resolution,[status(thm)],[c205,c177]) ).
cnf(c58,plain,
connection(in1(h1(f2(a))),in1(and2(h1(f2(a))))),
inference(resolution,[status(thm)],[halfadder_connection_in1_in1and2,c6]) ).
cnf(c358,plain,
( ~ zero(in1(h1(f2(a))))
| zero(in1(and2(h1(f2(a))))) ),
inference(resolution,[status(thm)],[c58,value_propagation_zero1]) ).
cnf(c505,plain,
zero(in1(and2(h1(f2(a))))),
inference(resolution,[status(thm)],[c358,c290]) ).
cnf(c506,plain,
( ~ and_ok(and2(h1(f2(a))))
| zero(out1(and2(h1(f2(a))))) ),
inference(resolution,[status(thm)],[c505,and_0x_0]) ).
cnf(c539,plain,
zero(out1(and2(h1(f2(a))))),
inference(resolution,[status(thm)],[c506,c243]) ).
cnf(c544,plain,
$false,
inference(resolution,[status(thm)],[c539,c536]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.18 % Problem : HWV008-2.002 : TPTP v8.1.2. Bugfixed v2.7.0.
% 0.13/0.19 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.41 % Computer : n011.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8042.1875MB
% 0.14/0.41 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Thu May 9 07:19:53 EDT 2024
% 0.14/0.41 % CPUTime :
% 1.06/1.29 % Version: 1.5
% 1.06/1.29 % SZS status Unsatisfiable
% 1.06/1.29 % SZS output start CNFRefutation
% See solution above
% 1.06/1.29
% 1.06/1.29 % Initial clauses : 74
% 1.06/1.29 % Processed clauses : 472
% 1.06/1.29 % Factors computed : 0
% 1.06/1.29 % Resolvents computed: 545
% 1.06/1.29 % Tautologies deleted: 18
% 1.06/1.29 % Forward subsumed : 56
% 1.06/1.29 % Backward subsumed : 57
% 1.06/1.29 % -------- CPU Time ---------
% 1.06/1.29 % User time : 0.856 s
% 1.06/1.29 % System time : 0.021 s
% 1.06/1.29 % Total time : 0.877 s
%------------------------------------------------------------------------------