%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV008-2.002 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:34:17 AM UTC 2026
% Result : Unsatisfiable 0.11s 0.44s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 29
% Syntax : Number of formulae : 127 ( 31 unt; 0 def)
% Number of atoms : 277 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 304 ( 154 ~; 150 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 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 : 72 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(value_propagation_zero2,axiom,
! [VAR_0,VAR_1] :
( zero(VAR_0)
| ~ zero(VAR_1)
| ~ connection(VAR_0,VAR_1) ),
file('theBenchmark.p',value_propagation_zero2) ).
cnf(c_3,plain,
( zero(A)
| ~ zero(B)
| ~ connection(A,B) ),
inference(clausify,[status(thm)],[value_propagation_zero2]) ).
fof(value_propagation_zero1,axiom,
! [VAR_0,VAR_1] :
( zero(VAR_1)
| ~ zero(VAR_0)
| ~ connection(VAR_0,VAR_1) ),
file('theBenchmark.p',value_propagation_zero1) ).
cnf(c_5,plain,
( zero(B)
| ~ zero(A)
| ~ connection(A,B) ),
inference(clausify,[status(thm)],[value_propagation_zero1]) ).
fof(halfadder_connection_in1_in1and2,axiom,
! [VAR_0] :
( connection(in1(VAR_0),in1(and2(VAR_0)))
| ~ halfadder(VAR_0) ),
file('theBenchmark.p',halfadder_connection_in1_in1and2) ).
cnf(c_7,plain,
( connection(in1(A),in1(and2(A)))
| ~ halfadder(A) ),
inference(clausify,[status(thm)],[halfadder_connection_in1_in1and2]) ).
fof(halfadder_connection_outc_out1and2,axiom,
! [VAR_0] :
( connection(outc(VAR_0),out1(and2(VAR_0)))
| ~ halfadder(VAR_0) ),
file('theBenchmark.p',halfadder_connection_outc_out1and2) ).
cnf(c_10,plain,
( connection(outc(A),out1(and2(A)))
| ~ halfadder(A) ),
inference(clausify,[status(thm)],[halfadder_connection_outc_out1and2]) ).
fof(fulladder_connection_outch1_in2or1,axiom,
! [VAR_0] :
( connection(outc(h1(VAR_0)),in2(or1(VAR_0)))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_connection_outch1_in2or1) ).
cnf(c_15,plain,
( connection(outc(h1(A)),in2(or1(A)))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_connection_outch1_in2or1]) ).
fof(fulladder_connection_outch2_in1or1,axiom,
! [VAR_0] :
( connection(outc(h2(VAR_0)),in1(or1(VAR_0)))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_connection_outch2_in1or1) ).
cnf(c_16,plain,
( connection(outc(h2(A)),in1(or1(A)))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_connection_outch2_in1or1]) ).
fof(fulladder_connection_in1_in1h2,axiom,
! [VAR_0] :
( connection(in1(VAR_0),in1(h2(VAR_0)))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_connection_in1_in1h2) ).
cnf(c_17,plain,
( connection(in1(A),in1(h2(A)))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_connection_in1_in1h2]) ).
fof(fulladder_connection_in2_in1h1,axiom,
! [VAR_0] :
( connection(in2(VAR_0),in1(h1(VAR_0)))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_connection_in2_in1h1) ).
cnf(c_18,plain,
( connection(in2(A),in1(h1(A)))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_connection_in2_in1h1]) ).
fof(fulladder_connection_outc_out1or1,axiom,
! [VAR_0] :
( connection(outc(VAR_0),out1(or1(VAR_0)))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_connection_outc_out1or1) ).
cnf(c_21,plain,
( connection(outc(A),out1(or1(A)))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_connection_outc_out1or1]) ).
fof(nbit_adder_connection_outc_outcf1,axiom,
! [VAR_0] :
( connection(outc(VAR_0),outc(f2(VAR_0)))
| ~ nbit_adder2(VAR_0) ),
file('theBenchmark.p',nbit_adder_connection_outc_outcf1) ).
cnf(c_24,plain,
( connection(outc(A),outc(f2(A)))
| ~ nbit_adder2(A) ),
inference(clausify,[status(thm)],[nbit_adder_connection_outc_outcf1]) ).
fof(nbit_adder_connection_ina2_in1f2,axiom,
! [VAR_0] :
( connection(ina2(VAR_0),in1(f2(VAR_0)))
| ~ nbit_adder2(VAR_0) ),
file('theBenchmark.p',nbit_adder_connection_ina2_in1f2) ).
cnf(c_27,plain,
( connection(ina2(A),in1(f2(A)))
| ~ nbit_adder2(A) ),
inference(clausify,[status(thm)],[nbit_adder_connection_ina2_in1f2]) ).
fof(nbit_adder_connection_inb2_in2f2,axiom,
! [VAR_0] :
( connection(inb2(VAR_0),in2(f2(VAR_0)))
| ~ nbit_adder2(VAR_0) ),
file('theBenchmark.p',nbit_adder_connection_inb2_in2f2) ).
cnf(c_28,plain,
( connection(inb2(A),in2(f2(A)))
| ~ nbit_adder2(A) ),
inference(clausify,[status(thm)],[nbit_adder_connection_inb2_in2f2]) ).
fof(and_ok_or_abnormal,axiom,
! [VAR_0] :
( abnormal(VAR_0)
| and_ok(VAR_0)
| ~ logic_and(VAR_0) ),
file('theBenchmark.p',and_ok_or_abnormal) ).
cnf(c_32,plain,
( abnormal(A)
| and_ok(A)
| ~ logic_and(A) ),
inference(clausify,[status(thm)],[and_ok_or_abnormal]) ).
fof(and_0x_0,axiom,
! [VAR_0] :
( zero(out1(VAR_0))
| ~ zero(in1(VAR_0))
| ~ and_ok(VAR_0) ),
file('theBenchmark.p',and_0x_0) ).
cnf(c_38,plain,
( zero(out1(A))
| ~ zero(in1(A))
| ~ and_ok(A) ),
inference(clausify,[status(thm)],[and_0x_0]) ).
cnf(c_45,plain,
( abnormal(A)
| ~ logic_and(A)
| zero(out1(A))
| ~ zero(in1(A)) ),
inference(resolve,[status(thm)],[c_38,c_32]) ).
fof(or_ok_or_abnormal,axiom,
! [VAR_0] :
( abnormal(VAR_0)
| or_ok(VAR_0)
| ~ logic_or(VAR_0) ),
file('theBenchmark.p',or_ok_or_abnormal) ).
cnf(c_46,plain,
( abnormal(A)
| or_ok(A)
| ~ logic_or(A) ),
inference(clausify,[status(thm)],[or_ok_or_abnormal]) ).
fof(diagnosis_or1f2a,axiom,
~ abnormal(or1(f2(a))),
file('theBenchmark.p',diagnosis_or1f2a) ).
cnf(c_49,plain,
~ abnormal(or1(f2(a))),
inference(clausify,[status(thm)],[diagnosis_or1f2a]) ).
fof(diagnosis_and2h1f2a,axiom,
~ abnormal(and2(h1(f2(a)))),
file('theBenchmark.p',diagnosis_and2h1f2a) ).
cnf(c_50,plain,
~ abnormal(and2(h1(f2(a)))),
inference(clausify,[status(thm)],[diagnosis_and2h1f2a]) ).
fof(diagnosis_and2h2f2a,axiom,
~ abnormal(and2(h2(f2(a)))),
file('theBenchmark.p',diagnosis_and2h2f2a) ).
cnf(c_51,plain,
~ abnormal(and2(h2(f2(a)))),
inference(clausify,[status(thm)],[diagnosis_and2h2f2a]) ).
fof(halfadder_and2,axiom,
! [VAR_0] :
( logic_and(and2(VAR_0))
| ~ halfadder(VAR_0) ),
file('theBenchmark.p',halfadder_and2) ).
cnf(c_52,plain,
( logic_and(and2(A))
| ~ halfadder(A) ),
inference(clausify,[status(thm)],[halfadder_and2]) ).
cnf(c_76,plain,
( ~ logic_and(and2(h1(f2(a))))
| zero(out1(and2(h1(f2(a)))))
| ~ zero(in1(and2(h1(f2(a))))) ),
inference(resolve,[status(thm)],[c_50,c_45]) ).
cnf(c_82,plain,
( ~ logic_and(and2(h2(f2(a))))
| zero(out1(and2(h2(f2(a)))))
| ~ zero(in1(and2(h2(f2(a))))) ),
inference(resolve,[status(thm)],[c_51,c_45]) ).
fof(or_00_0,axiom,
! [VAR_0] :
( zero(out1(VAR_0))
| ~ zero(in2(VAR_0))
| ~ zero(in1(VAR_0))
| ~ or_ok(VAR_0) ),
file('theBenchmark.p',or_00_0) ).
cnf(c_88,plain,
( zero(out1(A))
| ~ zero(in2(A))
| ~ zero(in1(A))
| ~ or_ok(A) ),
inference(clausify,[status(thm)],[or_00_0]) ).
cnf(c_100,plain,
( or_ok(or1(f2(a)))
| ~ logic_or(or1(f2(a))) ),
inference(resolve,[status(thm)],[c_49,c_46]) ).
fof(fulladder_or1,axiom,
! [VAR_0] :
( logic_or(or1(VAR_0))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_or1) ).
cnf(c_103,plain,
( logic_or(or1(A))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_or1]) ).
cnf(c_122,plain,
( zero(out1(or1(f2(a))))
| ~ zero(in2(or1(f2(a))))
| ~ zero(in1(or1(f2(a))))
| ~ logic_or(or1(f2(a))) ),
inference(resolve,[status(thm)],[c_100,c_88]) ).
fof(fulladder_halfadder1,axiom,
! [VAR_0] :
( halfadder(h1(VAR_0))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_halfadder1) ).
cnf(c_226,plain,
( halfadder(h1(A))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_halfadder1]) ).
cnf(c_232,plain,
( zero(out1(and2(h1(f2(a)))))
| ~ zero(in1(and2(h1(f2(a)))))
| ~ halfadder(h1(f2(a))) ),
inference(resolve,[status(thm)],[c_52,c_76]) ).
cnf(c_238,plain,
( zero(out1(and2(h2(f2(a)))))
| ~ zero(in1(and2(h2(f2(a)))))
| ~ halfadder(h2(f2(a))) ),
inference(resolve,[status(thm)],[c_52,c_82]) ).
fof(fulladder_halfadder2,axiom,
! [VAR_0] :
( halfadder(h2(VAR_0))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_halfadder2) ).
cnf(c_245,plain,
( halfadder(h2(A))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_halfadder2]) ).
cnf(c_257,plain,
( zero(in1(and2(A)))
| ~ zero(in1(A))
| ~ halfadder(A) ),
inference(resolve,[status(thm)],[c_7,c_5]) ).
cnf(c_267,plain,
( zero(outc(A))
| ~ zero(out1(and2(A)))
| ~ halfadder(A) ),
inference(resolve,[status(thm)],[c_10,c_3]) ).
fof(nbit_adder_fulladder2,axiom,
! [VAR_0] :
( fulladder(f2(VAR_0))
| ~ nbit_adder2(VAR_0) ),
file('theBenchmark.p',nbit_adder_fulladder2) ).
cnf(c_282,plain,
( fulladder(f2(A))
| ~ nbit_adder2(A) ),
inference(clausify,[status(thm)],[nbit_adder_fulladder2]) ).
cnf(c_290,plain,
( zero(in2(or1(A)))
| ~ zero(outc(h1(A)))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_15,c_5]) ).
cnf(c_294,plain,
( zero(in1(or1(A)))
| ~ zero(outc(h2(A)))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_16,c_5]) ).
cnf(c_298,plain,
( zero(in1(h2(A)))
| ~ zero(in1(A))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_17,c_5]) ).
cnf(c_302,plain,
( zero(in1(h1(A)))
| ~ zero(in2(A))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_18,c_5]) ).
cnf(c_312,plain,
( zero(outc(A))
| ~ zero(out1(or1(A)))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_21,c_3]) ).
cnf(c_320,plain,
( zero(out1(and2(h1(f2(a)))))
| ~ zero(in1(and2(h1(f2(a)))))
| ~ fulladder(f2(a)) ),
inference(resolve,[status(thm)],[c_226,c_232]) ).
cnf(c_326,plain,
( zero(out1(and2(h2(f2(a)))))
| ~ zero(in1(and2(h2(f2(a)))))
| ~ fulladder(f2(a)) ),
inference(resolve,[status(thm)],[c_245,c_238]) ).
cnf(c_349,plain,
( ~ fulladder(A)
| zero(in1(and2(h2(A))))
| ~ zero(in1(h2(A))) ),
inference(resolve,[status(thm)],[c_257,c_245]) ).
cnf(c_350,plain,
( ~ fulladder(A)
| zero(in1(and2(h1(A))))
| ~ zero(in1(h1(A))) ),
inference(resolve,[status(thm)],[c_257,c_226]) ).
cnf(c_369,plain,
( ~ fulladder(A)
| zero(outc(h2(A)))
| ~ zero(out1(and2(h2(A)))) ),
inference(resolve,[status(thm)],[c_267,c_245]) ).
cnf(c_370,plain,
( ~ fulladder(A)
| zero(outc(h1(A)))
| ~ zero(out1(and2(h1(A)))) ),
inference(resolve,[status(thm)],[c_267,c_226]) ).
cnf(c_403,plain,
( zero(out1(or1(f2(a))))
| ~ zero(in2(or1(f2(a))))
| ~ zero(in1(or1(f2(a))))
| ~ fulladder(f2(a)) ),
inference(resolve,[status(thm)],[c_103,c_122]) ).
fof(a_isa_2bit_adder,axiom,
nbit_adder2(a),
file('theBenchmark.p',a_isa_2bit_adder) ).
cnf(c_406,plain,
nbit_adder2(a),
inference(clausify,[status(thm)],[a_isa_2bit_adder]) ).
cnf(c_414,plain,
( zero(in2(or1(f2(A))))
| ~ zero(outc(h1(f2(A))))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_290]) ).
cnf(c_418,plain,
( zero(in1(or1(f2(A))))
| ~ zero(outc(h2(f2(A))))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_294]) ).
cnf(c_422,plain,
( zero(in1(h2(f2(A))))
| ~ zero(in1(f2(A)))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_298]) ).
cnf(c_426,plain,
( zero(in1(h1(f2(A))))
| ~ zero(in2(f2(A)))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_302]) ).
cnf(c_436,plain,
( zero(outc(f2(A)))
| ~ zero(out1(or1(f2(A))))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_312]) ).
cnf(c_444,plain,
( zero(out1(and2(h1(f2(a)))))
| ~ zero(in1(and2(h1(f2(a)))))
| ~ nbit_adder2(a) ),
inference(resolve,[status(thm)],[c_282,c_320]) ).
cnf(c_450,plain,
( zero(out1(and2(h2(f2(a)))))
| ~ zero(in1(and2(h2(f2(a)))))
| ~ nbit_adder2(a) ),
inference(resolve,[status(thm)],[c_282,c_326]) ).
cnf(c_473,plain,
( zero(in1(and2(h2(f2(A)))))
| ~ zero(in1(h2(f2(A))))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_349]) ).
cnf(c_474,plain,
( zero(in1(and2(h1(f2(A)))))
| ~ zero(in1(h1(f2(A))))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_350]) ).
cnf(c_493,plain,
( zero(outc(h2(f2(A))))
| ~ zero(out1(and2(h2(f2(A)))))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_369]) ).
cnf(c_494,plain,
( zero(outc(h1(f2(A))))
| ~ zero(out1(and2(h1(f2(A)))))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_282,c_370]) ).
cnf(c_630,plain,
( ~ nbit_adder2(a)
| zero(out1(or1(f2(a))))
| ~ zero(in2(or1(f2(a))))
| ~ zero(in1(or1(f2(a)))) ),
inference(resolve,[status(thm)],[c_403,c_282]) ).
cnf(c_642,plain,
( zero(outc(A))
| ~ zero(outc(f2(A)))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_24,c_3]) ).
cnf(c_656,plain,
( zero(in1(f2(A)))
| ~ zero(ina2(A))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_27,c_5]) ).
cnf(c_660,plain,
( zero(in2(f2(A)))
| ~ zero(inb2(A))
| ~ nbit_adder2(A) ),
inference(resolve,[status(thm)],[c_28,c_5]) ).
cnf(c_677,plain,
( zero(in2(f2(a)))
| ~ zero(inb2(a)) ),
inference(resolve,[status(thm)],[c_660,c_406]) ).
cnf(c_681,plain,
( zero(in1(f2(a)))
| ~ zero(ina2(a)) ),
inference(resolve,[status(thm)],[c_656,c_406]) ).
cnf(c_695,plain,
( zero(outc(a))
| ~ zero(outc(f2(a))) ),
inference(resolve,[status(thm)],[c_642,c_406]) ).
cnf(c_707,plain,
( zero(out1(or1(f2(a))))
| ~ zero(in2(or1(f2(a))))
| ~ zero(in1(or1(f2(a)))) ),
inference(resolve,[status(thm)],[c_406,c_630]) ).
cnf(c_843,plain,
( zero(outc(h1(f2(a))))
| ~ zero(out1(and2(h1(f2(a))))) ),
inference(resolve,[status(thm)],[c_406,c_494]) ).
cnf(c_844,plain,
( zero(outc(h2(f2(a))))
| ~ zero(out1(and2(h2(f2(a))))) ),
inference(resolve,[status(thm)],[c_406,c_493]) ).
cnf(c_863,plain,
( zero(in1(and2(h1(f2(a)))))
| ~ zero(in1(h1(f2(a)))) ),
inference(resolve,[status(thm)],[c_406,c_474]) ).
cnf(c_864,plain,
( zero(in1(and2(h2(f2(a)))))
| ~ zero(in1(h2(f2(a)))) ),
inference(resolve,[status(thm)],[c_406,c_473]) ).
cnf(c_887,plain,
( zero(out1(and2(h2(f2(a)))))
| ~ zero(in1(and2(h2(f2(a))))) ),
inference(resolve,[status(thm)],[c_406,c_450]) ).
cnf(c_893,plain,
( zero(out1(and2(h1(f2(a)))))
| ~ zero(in1(and2(h1(f2(a))))) ),
inference(resolve,[status(thm)],[c_406,c_444]) ).
cnf(c_901,plain,
( zero(outc(f2(a)))
| ~ zero(out1(or1(f2(a)))) ),
inference(resolve,[status(thm)],[c_406,c_436]) ).
cnf(c_911,plain,
( zero(in1(h1(f2(a))))
| ~ zero(in2(f2(a))) ),
inference(resolve,[status(thm)],[c_406,c_426]) ).
cnf(c_915,plain,
( zero(in1(h2(f2(a))))
| ~ zero(in1(f2(a))) ),
inference(resolve,[status(thm)],[c_406,c_422]) ).
cnf(c_919,plain,
( zero(in1(or1(f2(a))))
| ~ zero(outc(h2(f2(a)))) ),
inference(resolve,[status(thm)],[c_406,c_418]) ).
cnf(c_923,plain,
( zero(in2(or1(f2(a))))
| ~ zero(outc(h1(f2(a)))) ),
inference(resolve,[status(thm)],[c_406,c_414]) ).
fof(outc_1,axiom,
one(outc(a)),
file('theBenchmark.p',outc_1) ).
cnf(c_931,plain,
one(outc(a)),
inference(clausify,[status(thm)],[outc_1]) ).
fof(inb2_0,axiom,
zero(inb2(a)),
file('theBenchmark.p',inb2_0) ).
cnf(c_935,plain,
zero(inb2(a)),
inference(clausify,[status(thm)],[inb2_0]) ).
fof(ina2_0,axiom,
zero(ina2(a)),
file('theBenchmark.p',ina2_0) ).
cnf(c_937,plain,
zero(ina2(a)),
inference(clausify,[status(thm)],[ina2_0]) ).
fof(unique_value,axiom,
! [VAR_0] :
( ~ one(VAR_0)
| ~ zero(VAR_0) ),
file('theBenchmark.p',unique_value) ).
cnf(c_939,plain,
( ~ one(A)
| ~ zero(A) ),
inference(clausify,[status(thm)],[unique_value]) ).
cnf(c_944,plain,
zero(in2(f2(a))),
inference(resolve,[status(thm)],[c_935,c_677]) ).
cnf(c_946,plain,
zero(in1(f2(a))),
inference(resolve,[status(thm)],[c_937,c_681]) ).
cnf(c_950,plain,
zero(in1(h1(f2(a)))),
inference(resolve,[status(thm)],[c_944,c_911]) ).
cnf(c_952,plain,
zero(in1(h2(f2(a)))),
inference(resolve,[status(thm)],[c_946,c_915]) ).
cnf(c_958,plain,
zero(in1(and2(h1(f2(a))))),
inference(resolve,[status(thm)],[c_950,c_863]) ).
cnf(c_962,plain,
zero(in1(and2(h2(f2(a))))),
inference(resolve,[status(thm)],[c_952,c_864]) ).
cnf(c_965,plain,
zero(out1(and2(h1(f2(a))))),
inference(resolve,[status(thm)],[c_958,c_893]) ).
cnf(c_966,plain,
zero(out1(and2(h2(f2(a))))),
inference(resolve,[status(thm)],[c_962,c_887]) ).
cnf(c_967,plain,
zero(outc(h1(f2(a)))),
inference(resolve,[status(thm)],[c_965,c_843]) ).
cnf(c_969,plain,
zero(outc(h2(f2(a)))),
inference(resolve,[status(thm)],[c_966,c_844]) ).
cnf(c_971,plain,
zero(in2(or1(f2(a)))),
inference(resolve,[status(thm)],[c_967,c_923]) ).
cnf(c_972,plain,
zero(in1(or1(f2(a)))),
inference(resolve,[status(thm)],[c_969,c_919]) ).
cnf(c_984,plain,
( zero(out1(or1(f2(a))))
| ~ zero(in2(or1(f2(a)))) ),
inference(resolve,[status(thm)],[c_972,c_707]) ).
cnf(c_973,plain,
zero(out1(or1(f2(a)))),
inference(resolve,[status(thm)],[c_971,c_984]) ).
cnf(c_974,plain,
zero(outc(f2(a))),
inference(resolve,[status(thm)],[c_973,c_901]) ).
cnf(c_975,plain,
zero(outc(a)),
inference(resolve,[status(thm)],[c_974,c_695]) ).
cnf(c_985,plain,
~ zero(outc(a)),
inference(resolve,[status(thm)],[c_939,c_931]) ).
cnf(c_983,plain,
$false,
inference(resolve,[status(thm)],[c_975,c_985]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV008-2.002 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n017.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 15:55:02 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 2700921 was started by sandbox2 on n017,
% 0.11/0.37 % Fri Sep 25 15:55:02 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 0.11/0.44
% 0.11/0.44 % SZS status Unsatisfiable for theBenchmark
% 0.11/0.44
% 0.11/0.44 % Proof 1 at 0.04 (+ 0.00) seconds.
% 0.11/0.44 % Length of proof is 96.
% 0.11/0.44 % Level of proof is 13.
% 0.11/0.44 % Maximum clause weight is 37.000.
% 0.11/0.44 % Given clauses 195.
% 0.11/0.44
% 0.11/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------