%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV008-2.001 : 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 : n015.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.14s 0.39s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 31
% Syntax : Number of formulae : 133 ( 31 unt; 0 def)
% Number of atoms : 294 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 325 ( 164 ~; 161 |; 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 : 78 ( 0 sgn 26 !; 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_in2_in2and2,axiom,
! [VAR_0] :
( connection(in2(VAR_0),in2(and2(VAR_0)))
| ~ halfadder(VAR_0) ),
file('theBenchmark.p',halfadder_connection_in2_in2and2) ).
cnf(c_8,plain,
( connection(in2(A),in2(and2(A)))
| ~ halfadder(A) ),
inference(clausify,[status(thm)],[halfadder_connection_in2_in2and2]) ).
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_inc_in2h1,axiom,
! [VAR_0] :
( connection(inc(VAR_0),in2(h1(VAR_0)))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_connection_inc_in2h1) ).
cnf(c_19,plain,
( connection(inc(A),in2(h1(A)))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_connection_inc_in2h1]) ).
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(f1(VAR_0)))
| ~ nbit_adder1(VAR_0) ),
file('theBenchmark.p',nbit_adder_connection_outc_outcf1) ).
cnf(c_23,plain,
( connection(outc(A),outc(f1(A)))
| ~ nbit_adder1(A) ),
inference(clausify,[status(thm)],[nbit_adder_connection_outc_outcf1]) ).
fof(nbit_adder_connection_ina1_in1f1,axiom,
! [VAR_0] :
( connection(ina1(VAR_0),in1(f1(VAR_0)))
| ~ nbit_adder1(VAR_0) ),
file('theBenchmark.p',nbit_adder_connection_ina1_in1f1) ).
cnf(c_24,plain,
( connection(ina1(A),in1(f1(A)))
| ~ nbit_adder1(A) ),
inference(clausify,[status(thm)],[nbit_adder_connection_ina1_in1f1]) ).
fof(nbit_adder_connection_inc_incf1,axiom,
! [VAR_0] :
( connection(inc(VAR_0),inc(f1(VAR_0)))
| ~ nbit_adder1(VAR_0) ),
file('theBenchmark.p',nbit_adder_connection_inc_incf1) ).
cnf(c_26,plain,
( connection(inc(A),inc(f1(A)))
| ~ nbit_adder1(A) ),
inference(clausify,[status(thm)],[nbit_adder_connection_inc_incf1]) ).
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_28,plain,
( abnormal(A)
| and_ok(A)
| ~ logic_and(A) ),
inference(clausify,[status(thm)],[and_ok_or_abnormal]) ).
fof(and_x0_0,axiom,
! [VAR_0] :
( zero(out1(VAR_0))
| ~ zero(in2(VAR_0))
| ~ and_ok(VAR_0) ),
file('theBenchmark.p',and_x0_0) ).
cnf(c_33,plain,
( zero(out1(A))
| ~ zero(in2(A))
| ~ and_ok(A) ),
inference(clausify,[status(thm)],[and_x0_0]) ).
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_34,plain,
( zero(out1(A))
| ~ zero(in1(A))
| ~ and_ok(A) ),
inference(clausify,[status(thm)],[and_0x_0]) ).
cnf(c_40,plain,
( abnormal(A)
| ~ logic_and(A)
| zero(out1(A))
| ~ zero(in2(A)) ),
inference(resolve,[status(thm)],[c_33,c_28]) ).
cnf(c_41,plain,
( abnormal(A)
| ~ logic_and(A)
| zero(out1(A))
| ~ zero(in1(A)) ),
inference(resolve,[status(thm)],[c_34,c_28]) ).
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_42,plain,
( abnormal(A)
| or_ok(A)
| ~ logic_or(A) ),
inference(clausify,[status(thm)],[or_ok_or_abnormal]) ).
fof(diagnosis_or1f1,axiom,
~ abnormal(or1(f1(a))),
file('theBenchmark.p',diagnosis_or1f1) ).
cnf(c_45,plain,
~ abnormal(or1(f1(a))),
inference(clausify,[status(thm)],[diagnosis_or1f1]) ).
fof(diagnosis_and2h1f1,axiom,
~ abnormal(and2(h1(f1(a)))),
file('theBenchmark.p',diagnosis_and2h1f1) ).
cnf(c_46,plain,
~ abnormal(and2(h1(f1(a)))),
inference(clausify,[status(thm)],[diagnosis_and2h1f1]) ).
fof(diagnosis_and2h2f1,axiom,
~ abnormal(and2(h2(f1(a)))),
file('theBenchmark.p',diagnosis_and2h2f1) ).
cnf(c_47,plain,
~ abnormal(and2(h2(f1(a)))),
inference(clausify,[status(thm)],[diagnosis_and2h2f1]) ).
fof(halfadder_and2,axiom,
! [VAR_0] :
( logic_and(and2(VAR_0))
| ~ halfadder(VAR_0) ),
file('theBenchmark.p',halfadder_and2) ).
cnf(c_48,plain,
( logic_and(and2(A))
| ~ halfadder(A) ),
inference(clausify,[status(thm)],[halfadder_and2]) ).
cnf(c_71,plain,
( ~ logic_and(and2(h1(f1(a))))
| zero(out1(and2(h1(f1(a)))))
| ~ zero(in2(and2(h1(f1(a))))) ),
inference(resolve,[status(thm)],[c_46,c_40]) ).
cnf(c_78,plain,
( ~ logic_and(and2(h2(f1(a))))
| zero(out1(and2(h2(f1(a)))))
| ~ zero(in1(and2(h2(f1(a))))) ),
inference(resolve,[status(thm)],[c_47,c_41]) ).
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_84,plain,
( zero(out1(A))
| ~ zero(in2(A))
| ~ zero(in1(A))
| ~ or_ok(A) ),
inference(clausify,[status(thm)],[or_00_0]) ).
cnf(c_96,plain,
( or_ok(or1(f1(a)))
| ~ logic_or(or1(f1(a))) ),
inference(resolve,[status(thm)],[c_45,c_42]) ).
fof(fulladder_or1,axiom,
! [VAR_0] :
( logic_or(or1(VAR_0))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_or1) ).
cnf(c_99,plain,
( logic_or(or1(A))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_or1]) ).
cnf(c_118,plain,
( zero(out1(or1(f1(a))))
| ~ zero(in2(or1(f1(a))))
| ~ zero(in1(or1(f1(a))))
| ~ logic_or(or1(f1(a))) ),
inference(resolve,[status(thm)],[c_96,c_84]) ).
fof(fulladder_halfadder1,axiom,
! [VAR_0] :
( halfadder(h1(VAR_0))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_halfadder1) ).
cnf(c_222,plain,
( halfadder(h1(A))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_halfadder1]) ).
cnf(c_227,plain,
( zero(out1(and2(h1(f1(a)))))
| ~ zero(in2(and2(h1(f1(a)))))
| ~ halfadder(h1(f1(a))) ),
inference(resolve,[status(thm)],[c_48,c_71]) ).
cnf(c_234,plain,
( zero(out1(and2(h2(f1(a)))))
| ~ zero(in1(and2(h2(f1(a)))))
| ~ halfadder(h2(f1(a))) ),
inference(resolve,[status(thm)],[c_48,c_78]) ).
fof(fulladder_halfadder2,axiom,
! [VAR_0] :
( halfadder(h2(VAR_0))
| ~ fulladder(VAR_0) ),
file('theBenchmark.p',fulladder_halfadder2) ).
cnf(c_241,plain,
( halfadder(h2(A))
| ~ fulladder(A) ),
inference(clausify,[status(thm)],[fulladder_halfadder2]) ).
cnf(c_253,plain,
( zero(in1(and2(A)))
| ~ zero(in1(A))
| ~ halfadder(A) ),
inference(resolve,[status(thm)],[c_7,c_5]) ).
cnf(c_257,plain,
( zero(in2(and2(A)))
| ~ zero(in2(A))
| ~ halfadder(A) ),
inference(resolve,[status(thm)],[c_8,c_5]) ).
cnf(c_263,plain,
( zero(outc(A))
| ~ zero(out1(and2(A)))
| ~ halfadder(A) ),
inference(resolve,[status(thm)],[c_10,c_3]) ).
fof(nbit_adder_fulladder1,axiom,
! [VAR_0] :
( fulladder(f1(VAR_0))
| ~ nbit_adder1(VAR_0) ),
file('theBenchmark.p',nbit_adder_fulladder1) ).
cnf(c_278,plain,
( fulladder(f1(A))
| ~ nbit_adder1(A) ),
inference(clausify,[status(thm)],[nbit_adder_fulladder1]) ).
cnf(c_286,plain,
( zero(in2(or1(A)))
| ~ zero(outc(h1(A)))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_15,c_5]) ).
cnf(c_290,plain,
( zero(in1(or1(A)))
| ~ zero(outc(h2(A)))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_16,c_5]) ).
cnf(c_294,plain,
( zero(in1(h2(A)))
| ~ zero(in1(A))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_17,c_5]) ).
cnf(c_302,plain,
( zero(in2(h1(A)))
| ~ zero(inc(A))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_19,c_5]) ).
cnf(c_308,plain,
( zero(outc(A))
| ~ zero(out1(or1(A)))
| ~ fulladder(A) ),
inference(resolve,[status(thm)],[c_21,c_3]) ).
cnf(c_315,plain,
( zero(out1(and2(h1(f1(a)))))
| ~ zero(in2(and2(h1(f1(a)))))
| ~ fulladder(f1(a)) ),
inference(resolve,[status(thm)],[c_222,c_227]) ).
cnf(c_322,plain,
( zero(out1(and2(h2(f1(a)))))
| ~ zero(in1(and2(h2(f1(a)))))
| ~ fulladder(f1(a)) ),
inference(resolve,[status(thm)],[c_241,c_234]) ).
cnf(c_345,plain,
( ~ fulladder(A)
| zero(in1(and2(h2(A))))
| ~ zero(in1(h2(A))) ),
inference(resolve,[status(thm)],[c_253,c_241]) ).
cnf(c_354,plain,
( ~ fulladder(A)
| zero(in2(and2(h1(A))))
| ~ zero(in2(h1(A))) ),
inference(resolve,[status(thm)],[c_257,c_222]) ).
cnf(c_365,plain,
( ~ fulladder(A)
| zero(outc(h2(A)))
| ~ zero(out1(and2(h2(A)))) ),
inference(resolve,[status(thm)],[c_263,c_241]) ).
cnf(c_366,plain,
( ~ fulladder(A)
| zero(outc(h1(A)))
| ~ zero(out1(and2(h1(A)))) ),
inference(resolve,[status(thm)],[c_263,c_222]) ).
cnf(c_398,plain,
( zero(out1(or1(f1(a))))
| ~ zero(in2(or1(f1(a))))
| ~ zero(in1(or1(f1(a))))
| ~ fulladder(f1(a)) ),
inference(resolve,[status(thm)],[c_99,c_118]) ).
fof(a_isa_1bit_adder,axiom,
nbit_adder1(a),
file('theBenchmark.p',a_isa_1bit_adder) ).
cnf(c_401,plain,
nbit_adder1(a),
inference(clausify,[status(thm)],[a_isa_1bit_adder]) ).
cnf(c_409,plain,
( zero(in2(or1(f1(A))))
| ~ zero(outc(h1(f1(A))))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_286]) ).
cnf(c_413,plain,
( zero(in1(or1(f1(A))))
| ~ zero(outc(h2(f1(A))))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_290]) ).
cnf(c_417,plain,
( zero(in1(h2(f1(A))))
| ~ zero(in1(f1(A)))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_294]) ).
cnf(c_425,plain,
( zero(in2(h1(f1(A))))
| ~ zero(inc(f1(A)))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_302]) ).
cnf(c_431,plain,
( zero(outc(f1(A)))
| ~ zero(out1(or1(f1(A))))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_308]) ).
cnf(c_438,plain,
( zero(out1(and2(h1(f1(a)))))
| ~ zero(in2(and2(h1(f1(a)))))
| ~ nbit_adder1(a) ),
inference(resolve,[status(thm)],[c_278,c_315]) ).
cnf(c_445,plain,
( zero(out1(and2(h2(f1(a)))))
| ~ zero(in1(and2(h2(f1(a)))))
| ~ nbit_adder1(a) ),
inference(resolve,[status(thm)],[c_278,c_322]) ).
cnf(c_468,plain,
( zero(in1(and2(h2(f1(A)))))
| ~ zero(in1(h2(f1(A))))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_345]) ).
cnf(c_477,plain,
( zero(in2(and2(h1(f1(A)))))
| ~ zero(in2(h1(f1(A))))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_354]) ).
cnf(c_488,plain,
( zero(outc(h2(f1(A))))
| ~ zero(out1(and2(h2(f1(A)))))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_365]) ).
cnf(c_489,plain,
( zero(outc(h1(f1(A))))
| ~ zero(out1(and2(h1(f1(A)))))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_278,c_366]) ).
cnf(c_521,plain,
( ~ nbit_adder1(a)
| zero(out1(or1(f1(a))))
| ~ zero(in2(or1(f1(a))))
| ~ zero(in1(or1(f1(a)))) ),
inference(resolve,[status(thm)],[c_398,c_278]) ).
cnf(c_529,plain,
( zero(outc(A))
| ~ zero(outc(f1(A)))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_23,c_3]) ).
cnf(c_535,plain,
( zero(in1(f1(A)))
| ~ zero(ina1(A))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_24,c_5]) ).
cnf(c_543,plain,
( zero(inc(f1(A)))
| ~ zero(inc(A))
| ~ nbit_adder1(A) ),
inference(resolve,[status(thm)],[c_26,c_5]) ).
cnf(c_544,plain,
( zero(inc(f1(a)))
| ~ zero(inc(a)) ),
inference(resolve,[status(thm)],[c_543,c_401]) ).
cnf(c_552,plain,
( zero(in1(f1(a)))
| ~ zero(ina1(a)) ),
inference(resolve,[status(thm)],[c_535,c_401]) ).
cnf(c_558,plain,
( zero(outc(a))
| ~ zero(outc(f1(a))) ),
inference(resolve,[status(thm)],[c_529,c_401]) ).
cnf(c_566,plain,
( zero(out1(or1(f1(a))))
| ~ zero(in2(or1(f1(a))))
| ~ zero(in1(or1(f1(a)))) ),
inference(resolve,[status(thm)],[c_401,c_521]) ).
cnf(c_598,plain,
( zero(outc(h1(f1(a))))
| ~ zero(out1(and2(h1(f1(a))))) ),
inference(resolve,[status(thm)],[c_401,c_489]) ).
cnf(c_599,plain,
( zero(outc(h2(f1(a))))
| ~ zero(out1(and2(h2(f1(a))))) ),
inference(resolve,[status(thm)],[c_401,c_488]) ).
cnf(c_610,plain,
( zero(in2(and2(h1(f1(a)))))
| ~ zero(in2(h1(f1(a)))) ),
inference(resolve,[status(thm)],[c_401,c_477]) ).
cnf(c_619,plain,
( zero(in1(and2(h2(f1(a)))))
| ~ zero(in1(h2(f1(a)))) ),
inference(resolve,[status(thm)],[c_401,c_468]) ).
cnf(c_642,plain,
( zero(out1(and2(h2(f1(a)))))
| ~ zero(in1(and2(h2(f1(a))))) ),
inference(resolve,[status(thm)],[c_401,c_445]) ).
cnf(c_649,plain,
( zero(out1(and2(h1(f1(a)))))
| ~ zero(in2(and2(h1(f1(a))))) ),
inference(resolve,[status(thm)],[c_401,c_438]) ).
cnf(c_656,plain,
( zero(outc(f1(a)))
| ~ zero(out1(or1(f1(a)))) ),
inference(resolve,[status(thm)],[c_401,c_431]) ).
cnf(c_662,plain,
( zero(in2(h1(f1(a))))
| ~ zero(inc(f1(a))) ),
inference(resolve,[status(thm)],[c_401,c_425]) ).
cnf(c_670,plain,
( zero(in1(h2(f1(a))))
| ~ zero(in1(f1(a))) ),
inference(resolve,[status(thm)],[c_401,c_417]) ).
cnf(c_674,plain,
( zero(in1(or1(f1(a))))
| ~ zero(outc(h2(f1(a)))) ),
inference(resolve,[status(thm)],[c_401,c_413]) ).
cnf(c_678,plain,
( zero(in2(or1(f1(a))))
| ~ zero(outc(h1(f1(a)))) ),
inference(resolve,[status(thm)],[c_401,c_409]) ).
fof(outc_0,axiom,
one(outc(a)),
file('theBenchmark.p',outc_0) ).
cnf(c_686,plain,
one(outc(a)),
inference(clausify,[status(thm)],[outc_0]) ).
fof(inc_0,axiom,
zero(inc(a)),
file('theBenchmark.p',inc_0) ).
cnf(c_688,plain,
zero(inc(a)),
inference(clausify,[status(thm)],[inc_0]) ).
fof(ina1_0,axiom,
zero(ina1(a)),
file('theBenchmark.p',ina1_0) ).
cnf(c_690,plain,
zero(ina1(a)),
inference(clausify,[status(thm)],[ina1_0]) ).
fof(unique_value,axiom,
! [VAR_0] :
( ~ one(VAR_0)
| ~ zero(VAR_0) ),
file('theBenchmark.p',unique_value) ).
cnf(c_691,plain,
( ~ one(A)
| ~ zero(A) ),
inference(clausify,[status(thm)],[unique_value]) ).
cnf(c_694,plain,
zero(inc(f1(a))),
inference(resolve,[status(thm)],[c_688,c_544]) ).
cnf(c_696,plain,
zero(in1(f1(a))),
inference(resolve,[status(thm)],[c_690,c_552]) ).
cnf(c_699,plain,
zero(in2(h1(f1(a)))),
inference(resolve,[status(thm)],[c_694,c_662]) ).
cnf(c_701,plain,
zero(in1(h2(f1(a)))),
inference(resolve,[status(thm)],[c_696,c_670]) ).
cnf(c_705,plain,
zero(in2(and2(h1(f1(a))))),
inference(resolve,[status(thm)],[c_699,c_610]) ).
cnf(c_709,plain,
zero(in1(and2(h2(f1(a))))),
inference(resolve,[status(thm)],[c_701,c_619]) ).
cnf(c_710,plain,
zero(out1(and2(h1(f1(a))))),
inference(resolve,[status(thm)],[c_705,c_649]) ).
cnf(c_711,plain,
zero(out1(and2(h2(f1(a))))),
inference(resolve,[status(thm)],[c_709,c_642]) ).
cnf(c_712,plain,
zero(outc(h1(f1(a)))),
inference(resolve,[status(thm)],[c_710,c_598]) ).
cnf(c_714,plain,
zero(outc(h2(f1(a)))),
inference(resolve,[status(thm)],[c_711,c_599]) ).
cnf(c_716,plain,
zero(in2(or1(f1(a)))),
inference(resolve,[status(thm)],[c_712,c_678]) ).
cnf(c_717,plain,
zero(in1(or1(f1(a)))),
inference(resolve,[status(thm)],[c_714,c_674]) ).
cnf(c_722,plain,
( zero(out1(or1(f1(a))))
| ~ zero(in2(or1(f1(a)))) ),
inference(resolve,[status(thm)],[c_717,c_566]) ).
cnf(c_718,plain,
zero(out1(or1(f1(a)))),
inference(resolve,[status(thm)],[c_716,c_722]) ).
cnf(c_719,plain,
zero(outc(f1(a))),
inference(resolve,[status(thm)],[c_718,c_656]) ).
cnf(c_720,plain,
zero(outc(a)),
inference(resolve,[status(thm)],[c_719,c_558]) ).
cnf(c_723,plain,
~ zero(outc(a)),
inference(resolve,[status(thm)],[c_691,c_686]) ).
cnf(c_721,plain,
$false,
inference(resolve,[status(thm)],[c_720,c_723]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV008-2.001 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 16:02:57 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1780300 was started by sandbox2 on n015,
% 0.08/0.36 % Fri Sep 25 16:02:57 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/0.36
% 0.14/0.36 % From the command line: assign(max_seconds, 300).
% 0.14/0.39
% 0.14/0.39 % SZS status Unsatisfiable for theBenchmark
% 0.14/0.39
% 0.14/0.39 % Proof 1 at 0.02 (+ 0.00) seconds.
% 0.14/0.39 % Length of proof is 100.
% 0.14/0.39 % Level of proof is 13.
% 0.14/0.39 % Maximum clause weight is 37.000.
% 0.14/0.39 % Given clauses 86.
% 0.14/0.39
% 0.14/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------