%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : HWV008-2.001 : TPTP v9.0.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n029.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 Jul 24 06:38:35 PM UTC 2025
% Result : Unsatisfiable 6.04s 1.12s
% Output : CNFRefutation 6.04s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named diagnosis_or1f1)
% Comments :
%------------------------------------------------------------------------------
cnf(63,plain,
~ abnormal(or1(f1(a))),
inference(cnf,[status(esa)],[diagnosis_or1f1]) ).
cnf(l0,plain,
~ abnormal(or1(f1(a))),
inference(instantiation,[status(thm)],[63]) ).
cnf(20,plain,
( ~ logic_or(X0)
| or_ok(X0)
| abnormal(X0) ),
inference(cnf,[status(esa)],[or_ok_or_abnormal]) ).
cnf(l1,plain,
( ~ logic_or(or1(f1(a)))
| or_ok(or1(f1(a)))
| abnormal(or1(f1(a))) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(42,plain,
( ~ fulladder(X0)
| logic_or(or1(X0)) ),
inference(cnf,[status(esa)],[fulladder_or1]) ).
cnf(l2,plain,
( ~ fulladder(f1(a))
| logic_or(or1(f1(a))) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(51,plain,
( ~ nbit_adder1(X0)
| fulladder(f1(X0)) ),
inference(cnf,[status(esa)],[nbit_adder_fulladder1]) ).
cnf(l4,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(16,plain,
( ~ one(out1(X0))
| ~ or_ok(X0)
| one(in1(X0))
| one(in2(X0)) ),
inference(cnf,[status(esa)],[or_1_11]) ).
cnf(l3,plain,
( ~ one(out1(or1(f1(a))))
| ~ or_ok(or1(f1(a)))
| one(in1(or1(f1(a))))
| one(in2(or1(f1(a)))) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(57,plain,
nbit_adder1(a),
inference(cnf,[status(esa)],[a_isa_1bit_adder]) ).
cnf(l7,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(1,plain,
( ~ connection(X0,X1)
| ~ one(X0)
| one(X1) ),
inference(cnf,[status(esa)],[value_propagation_one1]) ).
cnf(l8,plain,
( ~ connection(outc(f1(a)),out1(or1(f1(a))))
| ~ one(outc(f1(a)))
| one(out1(or1(f1(a)))) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9,plain,
( ~ connection(outc(a),outc(f1(a)))
| ~ one(outc(a))
| one(outc(f1(a))) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(3,plain,
( ~ connection(X0,X1)
| ~ one(X1)
| one(X0) ),
inference(cnf,[status(esa)],[value_propagation_one2]) ).
cnf(l799,plain,
( ~ connection(outc(h1(f1(a))),in2(or1(f1(a))))
| ~ one(in2(or1(f1(a))))
| one(outc(h1(f1(a)))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(44,plain,
( ~ fulladder(X0)
| connection(outc(h1(X0)),in2(or1(X0))) ),
inference(cnf,[status(esa)],[fulladder_connection_outch1_in2or1]) ).
cnf(l833,plain,
( ~ fulladder(f1(a))
| connection(outc(h1(f1(a))),in2(or1(f1(a)))) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(50,plain,
( ~ fulladder(X0)
| connection(outc(X0),out1(or1(X0))) ),
inference(cnf,[status(esa)],[fulladder_connection_outc_out1or1]) ).
cnf(l13,plain,
( ~ fulladder(f1(a))
| connection(outc(f1(a)),out1(or1(f1(a)))) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l812,plain,
( ~ connection(outc(h1(f1(a))),out1(and2(h1(f1(a)))))
| ~ one(outc(h1(f1(a))))
| one(out1(and2(h1(f1(a))))) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(62,plain,
one(outc(a)),
inference(cnf,[status(esa)],[outc_0]) ).
cnf(l12,plain,
one(outc(a)),
inference(instantiation,[status(thm)],[62]) ).
cnf(l834,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(9,plain,
( ~ and_ok(X0)
| ~ one(out1(X0))
| one(in1(X0)) ),
inference(cnf,[status(esa)],[and_1_1x]) ).
cnf(l821,plain,
( ~ and_ok(and2(h1(f1(a))))
| ~ one(out1(and2(h1(f1(a)))))
| one(in1(and2(h1(f1(a))))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l15,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(12,plain,
( ~ logic_and(X0)
| and_ok(X0)
| abnormal(X0) ),
inference(cnf,[status(esa)],[and_ok_or_abnormal]) ).
cnf(l1001,plain,
( ~ logic_and(and2(h1(f1(a))))
| and_ok(and2(h1(f1(a))))
| abnormal(and2(h1(f1(a)))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l32,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(53,plain,
( ~ nbit_adder1(X0)
| connection(outc(X0),outc(f1(X0))) ),
inference(cnf,[status(esa)],[nbit_adder_connection_outc_outcf1]) ).
cnf(l11,plain,
( ~ nbit_adder1(a)
| connection(outc(a),outc(f1(a))) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(64,plain,
~ abnormal(and2(h1(f1(a)))),
inference(cnf,[status(esa)],[diagnosis_and2h1f1]) ).
cnf(l1002,plain,
~ abnormal(and2(h1(f1(a)))),
inference(instantiation,[status(thm)],[64]) ).
cnf(l5,plain,
( ~ connection(outc(h2(f1(a))),in1(or1(f1(a))))
| ~ one(in1(or1(f1(a))))
| one(outc(h2(f1(a)))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l10,plain,
( ~ connection(outc(h2(f1(a))),out1(and2(h2(f1(a)))))
| ~ one(outc(h2(f1(a))))
| one(out1(and2(h2(f1(a))))) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(36,plain,
( ~ halfadder(X0)
| connection(outc(X0),out1(and2(X0))) ),
inference(cnf,[status(esa)],[halfadder_connection_outc_out1and2]) ).
cnf(l814,plain,
( ~ halfadder(h1(f1(a)))
| connection(outc(h1(f1(a))),out1(and2(h1(f1(a))))) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l835,plain,
( ~ connection(in1(h1(f1(a))),in1(and2(h1(f1(a)))))
| ~ one(in1(and2(h1(f1(a)))))
| one(in1(h1(f1(a)))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1008,plain,
( ~ connection(in2(f1(a)),in1(h1(f1(a))))
| ~ one(in1(h1(f1(a))))
| one(in2(f1(a))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(33,plain,
( ~ halfadder(X0)
| connection(in1(X0),in1(and2(X0))) ),
inference(cnf,[status(esa)],[halfadder_connection_in1_in1and2]) ).
cnf(l1012,plain,
( ~ halfadder(h1(f1(a)))
| connection(in1(h1(f1(a))),in1(and2(h1(f1(a))))) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(40,plain,
( ~ fulladder(X0)
| halfadder(h1(X0)) ),
inference(cnf,[status(esa)],[fulladder_halfadder1]) ).
cnf(l1016,plain,
( ~ fulladder(f1(a))
| halfadder(h1(f1(a))) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l815,plain,
( ~ fulladder(f1(a))
| halfadder(h1(f1(a))) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l845,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(28,plain,
( ~ halfadder(X0)
| logic_and(and2(X0)) ),
inference(cnf,[status(esa)],[halfadder_and2]) ).
cnf(l1003,plain,
( ~ halfadder(h1(f1(a)))
| logic_and(and2(h1(f1(a)))) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1017,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(47,plain,
( ~ fulladder(X0)
| connection(in2(X0),in1(h1(X0))) ),
inference(cnf,[status(esa)],[fulladder_connection_in2_in1h1]) ).
cnf(l1009,plain,
( ~ fulladder(f1(a))
| connection(in2(f1(a)),in1(h1(f1(a)))) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(45,plain,
( ~ fulladder(X0)
| connection(outc(h2(X0)),in1(or1(X0))) ),
inference(cnf,[status(esa)],[fulladder_connection_outch2_in1or1]) ).
cnf(l6,plain,
( ~ fulladder(f1(a))
| connection(outc(h2(f1(a))),in1(or1(f1(a)))) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l14,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1013,plain,
( ~ fulladder(f1(a))
| halfadder(h1(f1(a))) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l17,plain,
( ~ halfadder(h2(f1(a)))
| connection(outc(h2(f1(a))),out1(and2(h2(f1(a))))) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(41,plain,
( ~ fulladder(X0)
| halfadder(h2(X0)) ),
inference(cnf,[status(esa)],[fulladder_halfadder2]) ).
cnf(l21,plain,
( ~ fulladder(f1(a))
| halfadder(h2(f1(a))) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l875,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l889,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l22,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1011,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l164,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1077,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1014,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1010,plain,
( ~ connection(inb1(a),in2(f1(a)))
| ~ one(in2(f1(a)))
| one(inb1(a)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l19,plain,
( ~ and_ok(and2(h2(f1(a))))
| ~ one(out1(and2(h2(f1(a)))))
| one(in1(and2(h2(f1(a))))) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1025,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1032,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l163,plain,
( ~ logic_and(and2(h2(f1(a))))
| and_ok(and2(h2(f1(a))))
| abnormal(and2(h2(f1(a)))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(4,plain,
( ~ zero(X0)
| ~ one(X0) ),
inference(cnf,[status(esa)],[unique_value]) ).
cnf(l1073,plain,
( ~ zero(inb1(a))
| ~ one(inb1(a)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l23,plain,
( ~ connection(in1(h2(f1(a))),in1(and2(h2(f1(a)))))
| ~ one(in1(and2(h2(f1(a)))))
| one(in1(h2(f1(a)))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l33,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(55,plain,
( ~ nbit_adder1(X0)
| connection(inb1(X0),in2(f1(X0))) ),
inference(cnf,[status(esa)],[nbit_adder_connection_inb1_in2f1]) ).
cnf(l1070,plain,
( ~ nbit_adder1(a)
| connection(inb1(a),in2(f1(a))) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l350,plain,
( ~ halfadder(h2(f1(a)))
| logic_and(and2(h2(f1(a)))) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l353,plain,
( ~ fulladder(f1(a))
| halfadder(h2(f1(a))) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l203,plain,
( ~ halfadder(h2(f1(a)))
| connection(in1(h2(f1(a))),in1(and2(h2(f1(a))))) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l175,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1072,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(59,plain,
zero(inb1(a)),
inference(cnf,[status(esa)],[inb1_0]) ).
cnf(l1080,plain,
zero(inb1(a)),
inference(instantiation,[status(thm)],[59]) ).
cnf(l640,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l710,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l207,plain,
( ~ fulladder(f1(a))
| halfadder(h2(f1(a))) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l393,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l669,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l204,plain,
( ~ connection(in1(f1(a)),in1(h2(f1(a))))
| ~ one(in1(h2(f1(a))))
| one(in1(f1(a))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(46,plain,
( ~ fulladder(X0)
| connection(in1(X0),in1(h2(X0))) ),
inference(cnf,[status(esa)],[fulladder_connection_in1_in1h2]) ).
cnf(l205,plain,
( ~ fulladder(f1(a))
| connection(in1(f1(a)),in1(h2(f1(a)))) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l206,plain,
( ~ nbit_adder1(a)
| fulladder(f1(a)) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l210,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(65,plain,
~ abnormal(and2(h2(f1(a)))),
inference(cnf,[status(esa)],[diagnosis_and2h2f1]) ).
cnf(l445,plain,
~ abnormal(and2(h2(f1(a)))),
inference(instantiation,[status(thm)],[65]) ).
cnf(l656,plain,
( ~ connection(ina1(a),in1(f1(a)))
| ~ one(in1(f1(a)))
| one(ina1(a)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(54,plain,
( ~ nbit_adder1(X0)
| connection(ina1(X0),in1(f1(X0))) ),
inference(cnf,[status(esa)],[nbit_adder_connection_ina1_in1f1]) ).
cnf(l667,plain,
( ~ nbit_adder1(a)
| connection(ina1(a),in1(f1(a))) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l668,plain,
nbit_adder1(a),
inference(instantiation,[status(thm)],[57]) ).
cnf(l753,plain,
( ~ zero(ina1(a))
| ~ one(ina1(a)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(58,plain,
zero(ina1(a)),
inference(cnf,[status(esa)],[ina1_0]) ).
cnf(l762,plain,
zero(ina1(a)),
inference(instantiation,[status(thm)],[58]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l4,l3,l7,l8,l9,l799,l833,l13,l812,l12,l834,l821,l15,l1001,l32,l11,l1002,l5,l10,l814,l835,l1008,l1012,l1016,l815,l845,l1003,l1017,l1009,l6,l14,l1013,l17,l21,l875,l889,l22,l1011,l164,l1077,l1014,l1010,l19,l1025,l1032,l163,l1073,l23,l33,l1070,l350,l353,l203,l175,l1072,l1080,l640,l710,l207,l393,l669,l204,l205,l206,l210,l445,l656,l667,l668,l753,l762]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : HWV008-2.001 : TPTP v9.0.0. Bugfixed v2.7.0.
% 0.11/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 17:45:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.33 % launching worker at depth: 3
% 0.12/0.33 % launching worker at depth: 5
% 0.12/0.33 % launching worker at depth: 2
% 0.12/0.33 % launching worker at depth: 6
% 0.12/0.33 % launching worker at depth: 4
% 0.12/0.33 % launching worker at depth: 1
% 0.12/0.33 % launching worker at depth: 7
% 0.12/0.33 % launching worker at depth: 8
% 0.12/0.33 % launching worker at depth: 9
% 0.12/0.33 % launching worker at depth: 10
% 0.12/0.33 % launching worker at depth: 11
% 0.12/0.34 % launching worker at depth: 12
% 0.12/0.41 % launching worker at depth: 13
% 0.19/0.49 % launching worker at depth: 14
% 2.40/0.63 % launching worker at depth: 15
% 6.04/1.11 % launching worker at depth: 16
% 6.04/1.12 % SZS status Theorem for theBenchmark
% 6.04/1.12 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------