%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV007-1 : TPTP v9.3.1. Released v2.1.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:16 AM UTC 2026
% Result : Unsatisfiable 0.13s 0.45s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 45
% Syntax : Number of formulae : 192 ( 52 unt; 0 def)
% Number of atoms : 403 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 428 ( 217 ~; 211 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 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 : 129 ( 1 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(halfadder_connection_in1_in1or1,axiom,
! [VAR_0] :
( connection(in(n1,VAR_0),in(n1,or1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_in1_in1or1) ).
cnf(c_1,plain,
( connection(in(n1,A),in(n1,or1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_in1_in1or1]) ).
fof(value_propagation2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( value(VAR_0,VAR_2)
| ~ value(VAR_1,VAR_2)
| ~ connection(VAR_0,VAR_1) ),
file('theBenchmark.p',value_propagation2) ).
cnf(c_2,plain,
( value(A,C)
| ~ value(B,C)
| ~ connection(A,B) ),
inference(clausify,[status(thm)],[value_propagation2]) ).
fof(value_propagation1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( value(VAR_1,VAR_2)
| ~ value(VAR_0,VAR_2)
| ~ connection(VAR_0,VAR_1) ),
file('theBenchmark.p',value_propagation1) ).
cnf(c_3,plain,
( value(B,C)
| ~ value(A,C)
| ~ connection(A,B) ),
inference(clausify,[status(thm)],[value_propagation1]) ).
fof(halfadder_connection_in2_in2or1,axiom,
! [VAR_0] :
( connection(in(n2,VAR_0),in(n2,or1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_in2_in2or1) ).
cnf(c_4,plain,
( connection(in(n2,A),in(n2,or1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_in2_in2or1]) ).
fof(halfadder_connection_in1_in1and2,axiom,
! [VAR_0] :
( connection(in(n1,VAR_0),in(n1,and2(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_in1_in1and2) ).
cnf(c_5,plain,
( connection(in(n1,A),in(n1,and2(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_in1_in1and2]) ).
fof(halfadder_connection_in2_in2and2,axiom,
! [VAR_0] :
( connection(in(n2,VAR_0),in(n2,and2(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_in2_in2and2) ).
cnf(c_6,plain,
( connection(in(n2,A),in(n2,and2(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_in2_in2and2]) ).
fof(halfadder_connection_outs_out1and1,axiom,
! [VAR_0] :
( connection(out(s,VAR_0),out(n1,and1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_outs_out1and1) ).
cnf(c_7,plain,
( connection(out(s,A),out(n1,and1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_outs_out1and1]) ).
fof(halfadder_connection_outc_out1and2,axiom,
! [VAR_0] :
( connection(out(c,VAR_0),out(n1,and2(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_outc_out1and2) ).
cnf(c_8,plain,
( connection(out(c,A),out(n1,and2(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_outc_out1and2]) ).
fof(halfadder_connection_out1or1_in1_and1,axiom,
! [VAR_0] :
( connection(out(n1,or1(VAR_0)),in(n1,and1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_out1or1_in1_and1) ).
cnf(c_9,plain,
( connection(out(n1,or1(A)),in(n1,and1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_out1or1_in1_and1]) ).
fof(halfadder_connection_out1and2_in1not1,axiom,
! [VAR_0] :
( connection(out(n1,and2(VAR_0)),in(n1,not1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_out1and2_in1not1) ).
cnf(c_10,plain,
( connection(out(n1,and2(A)),in(n1,not1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_out1and2_in1not1]) ).
fof(halfadder_connection_out1not1_in2and1,axiom,
! [VAR_0] :
( connection(out(n1,not1(VAR_0)),in(n2,and1(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_out1not1_in2and1) ).
cnf(c_11,plain,
( connection(out(n1,not1(A)),in(n2,and1(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_out1not1_in2and1]) ).
fof(fulladder_connection_outsh1_in2h2,axiom,
! [VAR_0] :
( connection(out(s,h1(VAR_0)),in(n2,h2(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_outsh1_in2h2) ).
cnf(c_12,plain,
( connection(out(s,h1(A)),in(n2,h2(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_outsh1_in2h2]) ).
fof(fulladder_connection_outch1_in2or1,axiom,
! [VAR_0] :
( connection(out(c,h1(VAR_0)),in(n2,or1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_outch1_in2or1) ).
cnf(c_13,plain,
( connection(out(c,h1(A)),in(n2,or1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_outch1_in2or1]) ).
fof(fulladder_connection_in1_in1h2,axiom,
! [VAR_0] :
( connection(in(n1,VAR_0),in(n1,h2(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_in1_in1h2) ).
cnf(c_15,plain,
( connection(in(n1,A),in(n1,h2(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_in1_in1h2]) ).
fof(fulladder_connection_in2_in1h1,axiom,
! [VAR_0] :
( connection(in(n2,VAR_0),in(n1,h1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_in2_in1h1) ).
cnf(c_16,plain,
( connection(in(n2,A),in(n1,h1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_in2_in1h1]) ).
fof(fulladder_connection_inc_in2h1,axiom,
! [VAR_0] :
( connection(in(c,VAR_0),in(n2,h1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_inc_in2h1) ).
cnf(c_17,plain,
( connection(in(c,A),in(n2,h1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_inc_in2h1]) ).
fof(fulladder_connection_outs_outsh2,axiom,
! [VAR_0] :
( connection(out(s,VAR_0),out(s,h2(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_outs_outsh2) ).
cnf(c_18,plain,
( connection(out(s,A),out(s,h2(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_outs_outsh2]) ).
fof(fulladder_connection_outc_out1or1,axiom,
! [VAR_0] :
( connection(out(c,VAR_0),out(n1,or1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_outc_out1or1) ).
cnf(c_19,plain,
( connection(out(c,A),out(n1,or1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_outc_out1or1]) ).
fof(unique_value,axiom,
! [VAR_0,VAR_1,VAR_2] :
( equal_value(VAR_1,VAR_2)
| ~ value(VAR_0,VAR_2)
| ~ value(VAR_0,VAR_1) ),
file('theBenchmark.p',unique_value) ).
cnf(c_20,plain,
( equal_value(B,C)
| ~ value(A,C)
| ~ value(A,B) ),
inference(clausify,[status(thm)],[unique_value]) ).
fof(equal_value1,axiom,
~ equal_value(n0,n1),
file('theBenchmark.p',equal_value1) ).
cnf(c_21,plain,
~ equal_value(n0,n1),
inference(clausify,[status(thm)],[equal_value1]) ).
cnf(c_23,plain,
( ~ value(A,n1)
| ~ value(A,n0) ),
inference(resolve,[status(thm)],[c_20,c_21]) ).
fof(ok_or_abnormal,axiom,
! [VAR_0,VAR_1] :
( mode(VAR_0,abnormal)
| mode(VAR_0,ok)
| ~ type(VAR_0,VAR_1) ),
file('theBenchmark.p',ok_or_abnormal) ).
cnf(c_25,plain,
( mode(A,abnormal)
| mode(A,ok)
| ~ type(A,B) ),
inference(clausify,[status(thm)],[ok_or_abnormal]) ).
fof(and_0_00,axiom,
! [VAR_0] :
( value(in(n2,VAR_0),n0)
| value(in(n1,VAR_0),n0)
| ~ value(out(n1,VAR_0),n0)
| ~ type(VAR_0,and)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',and_0_00) ).
cnf(c_28,plain,
( value(in(n2,A),n0)
| value(in(n1,A),n0)
| ~ value(out(n1,A),n0)
| ~ type(A,and)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[and_0_00]) ).
fof(and_1_1x,axiom,
! [VAR_0] :
( value(in(n1,VAR_0),n1)
| ~ value(out(n1,VAR_0),n1)
| ~ type(VAR_0,and)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',and_1_1x) ).
cnf(c_29,plain,
( value(in(n1,A),n1)
| ~ value(out(n1,A),n1)
| ~ type(A,and)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[and_1_1x]) ).
fof(and_1_x1,axiom,
! [VAR_0] :
( value(in(n2,VAR_0),n1)
| ~ value(out(n1,VAR_0),n1)
| ~ type(VAR_0,and)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',and_1_x1) ).
cnf(c_30,plain,
( value(in(n2,A),n1)
| ~ value(out(n1,A),n1)
| ~ type(A,and)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[and_1_x1]) ).
fof(or_1_11,axiom,
! [VAR_0] :
( value(in(n2,VAR_0),n1)
| value(in(n1,VAR_0),n1)
| ~ value(out(n1,VAR_0),n1)
| ~ type(VAR_0,or)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',or_1_11) ).
cnf(c_33,plain,
( value(in(n2,A),n1)
| value(in(n1,A),n1)
| ~ value(out(n1,A),n1)
| ~ type(A,or)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[or_1_11]) ).
fof(or_0_01,axiom,
! [VAR_0] :
( value(in(n2,VAR_0),n0)
| ~ value(out(n1,VAR_0),n0)
| ~ type(VAR_0,or)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',or_0_01) ).
cnf(c_35,plain,
( value(in(n2,A),n0)
| ~ value(out(n1,A),n0)
| ~ type(A,or)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[or_0_01]) ).
fof(not_1_0_bw,axiom,
! [VAR_0] :
( value(in(n1,VAR_0),n0)
| ~ value(out(n1,VAR_0),n1)
| ~ type(VAR_0,not)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',not_1_0_bw) ).
cnf(c_39,plain,
( value(in(n1,A),n0)
| ~ value(out(n1,A),n1)
| ~ type(A,not)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[not_1_0_bw]) ).
fof(halfadder_and1,axiom,
! [VAR_0] :
( type(and1(VAR_0),and)
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_and1) ).
cnf(c_40,plain,
( type(and1(A),and)
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_and1]) ).
fof(halfadder_and2,axiom,
! [VAR_0] :
( type(and2(VAR_0),and)
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_and2) ).
cnf(c_41,plain,
( type(and2(A),and)
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_and2]) ).
fof(halfadder_not1,axiom,
! [VAR_0] :
( type(not1(VAR_0),not)
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_not1) ).
cnf(c_42,plain,
( type(not1(A),not)
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_not1]) ).
fof(halfadder_or1,axiom,
! [VAR_0] :
( type(or1(VAR_0),or)
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_or1) ).
cnf(c_43,plain,
( type(or1(A),or)
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_or1]) ).
fof(fulladder_halfadder1,axiom,
! [VAR_0] :
( type(h1(VAR_0),halfadder)
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_halfadder1) ).
cnf(c_44,plain,
( type(h1(A),halfadder)
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_halfadder1]) ).
fof(fulladder_halfadder2,axiom,
! [VAR_0] :
( type(h2(VAR_0),halfadder)
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_halfadder2) ).
cnf(c_45,plain,
( type(h2(A),halfadder)
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_halfadder2]) ).
fof(fulladder_or1,axiom,
! [VAR_0] :
( type(or1(VAR_0),or)
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_or1) ).
cnf(c_46,plain,
( type(or1(A),or)
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_or1]) ).
fof(f_isa_fulladder,axiom,
type(f,fulladder),
file('theBenchmark.p',f_isa_fulladder) ).
cnf(c_47,plain,
type(f,fulladder),
inference(clausify,[status(thm)],[f_isa_fulladder]) ).
fof(in1_1,axiom,
value(in(n1,f),n0),
file('theBenchmark.p',in1_1) ).
cnf(c_48,plain,
value(in(n1,f),n0),
inference(clausify,[status(thm)],[in1_1]) ).
fof(in2_0,axiom,
value(in(n2,f),n1),
file('theBenchmark.p',in2_0) ).
cnf(c_49,plain,
value(in(n2,f),n1),
inference(clausify,[status(thm)],[in2_0]) ).
fof(inc_1,axiom,
value(in(c,f),n1),
file('theBenchmark.p',inc_1) ).
cnf(c_50,plain,
value(in(c,f),n1),
inference(clausify,[status(thm)],[inc_1]) ).
fof(outs_1,axiom,
value(out(s,f),n1),
file('theBenchmark.p',outs_1) ).
cnf(c_51,plain,
value(out(s,f),n1),
inference(clausify,[status(thm)],[outs_1]) ).
fof(outc_0,axiom,
value(out(c,f),n0),
file('theBenchmark.p',outc_0) ).
cnf(c_52,plain,
value(out(c,f),n0),
inference(clausify,[status(thm)],[outc_0]) ).
fof(diagnosis_and2h1,axiom,
~ mode(and2(h1(f)),abnormal),
file('theBenchmark.p',diagnosis_and2h1) ).
cnf(c_53,plain,
~ mode(and2(h1(f)),abnormal),
inference(clausify,[status(thm)],[diagnosis_and2h1]) ).
fof(diagnosis_or1_and1h1,axiom,
( ~ mode(and1(h1(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('theBenchmark.p',diagnosis_or1_and1h1) ).
cnf(c_54,plain,
( ~ mode(and1(h1(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
inference(clausify,[status(thm)],[diagnosis_or1_and1h1]) ).
fof(diagnosis_or1_not1h1,axiom,
( ~ mode(not1(h1(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('theBenchmark.p',diagnosis_or1_not1h1) ).
cnf(c_55,plain,
( ~ mode(not1(h1(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
inference(clausify,[status(thm)],[diagnosis_or1_not1h1]) ).
fof(diagnosis_or1_and1h2,axiom,
( ~ mode(and1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('theBenchmark.p',diagnosis_or1_and1h2) ).
cnf(c_56,plain,
( ~ mode(and1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
inference(clausify,[status(thm)],[diagnosis_or1_and1h2]) ).
fof(diagnosis_or1_or1h2,axiom,
( ~ mode(or1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('theBenchmark.p',diagnosis_or1_or1h2) ).
cnf(c_57,plain,
( ~ mode(or1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
inference(clausify,[status(thm)],[diagnosis_or1_or1h2]) ).
cnf(c_58,plain,
( value(in(n1,A),B)
| ~ value(in(n1,or1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_60,plain,
( value(in(n2,A),B)
| ~ value(in(n2,or1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_62,plain,
( value(in(n1,A),B)
| ~ value(in(n1,and2(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_5,c_2]) ).
cnf(c_64,plain,
( value(in(n2,A),B)
| ~ value(in(n2,and2(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_6,c_2]) ).
cnf(c_67,plain,
( value(out(n1,and1(A)),B)
| ~ value(out(s,A),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_7,c_3]) ).
cnf(c_69,plain,
( value(out(n1,and2(A)),B)
| ~ value(out(c,A),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_8,c_3]) ).
cnf(c_70,plain,
( value(out(n1,or1(A)),B)
| ~ value(in(n1,and1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_9,c_2]) ).
cnf(c_72,plain,
( value(out(n1,and2(A)),B)
| ~ value(in(n1,not1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_10,c_2]) ).
cnf(c_74,plain,
( value(out(n1,not1(A)),B)
| ~ value(in(n2,and1(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_11,c_2]) ).
cnf(c_76,plain,
( value(out(s,h1(A)),B)
| ~ value(in(n2,h2(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_12,c_2]) ).
cnf(c_78,plain,
( value(out(c,h1(A)),B)
| ~ value(in(n2,or1(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_13,c_2]) ).
cnf(c_82,plain,
( value(in(n1,A),B)
| ~ value(in(n1,h2(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_15,c_2]) ).
cnf(c_84,plain,
( value(in(n2,A),B)
| ~ value(in(n1,h1(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_16,c_2]) ).
cnf(c_86,plain,
( value(in(c,A),B)
| ~ value(in(n2,h1(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_17,c_2]) ).
cnf(c_89,plain,
( value(out(s,h2(A)),B)
| ~ value(out(s,A),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_18,c_3]) ).
cnf(c_91,plain,
( value(out(n1,or1(A)),B)
| ~ value(out(c,A),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_19,c_3]) ).
cnf(c_92,plain,
type(or1(f),or),
inference(resolve,[status(thm)],[c_47,c_46]) ).
cnf(c_93,plain,
type(h2(f),halfadder),
inference(resolve,[status(thm)],[c_47,c_45]) ).
cnf(c_94,plain,
type(h1(f),halfadder),
inference(resolve,[status(thm)],[c_47,c_44]) ).
cnf(c_96,plain,
~ value(in(n1,f),n1),
inference(resolve,[status(thm)],[c_48,c_23]) ).
cnf(c_97,plain,
~ value(in(n2,f),n0),
inference(resolve,[status(thm)],[c_23,c_49]) ).
cnf(c_98,plain,
~ value(in(c,f),n0),
inference(resolve,[status(thm)],[c_23,c_50]) ).
cnf(c_101,plain,
( value(out(s,h1(f)),A)
| ~ value(in(n2,h2(f)),A) ),
inference(resolve,[status(thm)],[c_76,c_47]) ).
cnf(c_103,plain,
( value(out(c,h1(f)),A)
| ~ value(in(n2,or1(f)),A) ),
inference(resolve,[status(thm)],[c_78,c_47]) ).
cnf(c_114,plain,
( value(out(s,h2(f)),A)
| ~ value(out(s,f),A) ),
inference(resolve,[status(thm)],[c_89,c_47]) ).
cnf(c_116,plain,
( value(out(n1,or1(f)),A)
| ~ value(out(c,f),A) ),
inference(resolve,[status(thm)],[c_91,c_47]) ).
cnf(c_117,plain,
( mode(or1(f),abnormal)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_92,c_25]) ).
cnf(c_325,plain,
( value(in(n1,f),A)
| ~ value(in(n1,h2(f)),A) ),
inference(resolve,[status(thm)],[c_82,c_47]) ).
cnf(c_118,plain,
~ value(in(n1,h2(f)),n1),
inference(resolve,[status(thm)],[c_325,c_96]) ).
cnf(c_326,plain,
( value(in(n2,f),A)
| ~ value(in(n1,h1(f)),A) ),
inference(resolve,[status(thm)],[c_84,c_47]) ).
cnf(c_119,plain,
~ value(in(n1,h1(f)),n0),
inference(resolve,[status(thm)],[c_326,c_97]) ).
cnf(c_327,plain,
( value(in(c,f),A)
| ~ value(in(n2,h1(f)),A) ),
inference(resolve,[status(thm)],[c_86,c_47]) ).
cnf(c_120,plain,
~ value(in(n2,h1(f)),n0),
inference(resolve,[status(thm)],[c_327,c_98]) ).
cnf(c_130,plain,
( value(out(n1,and1(h2(f))),A)
| ~ value(out(s,h2(f)),A) ),
inference(resolve,[status(thm)],[c_93,c_67]) ).
cnf(c_140,plain,
type(or1(h2(f)),or),
inference(resolve,[status(thm)],[c_93,c_43]) ).
cnf(c_143,plain,
type(and1(h2(f)),and),
inference(resolve,[status(thm)],[c_93,c_40]) ).
cnf(c_164,plain,
type(not1(h1(f)),not),
inference(resolve,[status(thm)],[c_94,c_42]) ).
cnf(c_165,plain,
type(and2(h1(f)),and),
inference(resolve,[status(thm)],[c_94,c_41]) ).
cnf(c_166,plain,
type(and1(h1(f)),and),
inference(resolve,[status(thm)],[c_94,c_40]) ).
cnf(c_168,plain,
( mode(or1(h2(f)),abnormal)
| mode(or1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_140,c_25]) ).
cnf(c_328,plain,
( value(in(n1,h2(f)),A)
| ~ value(in(n1,or1(h2(f))),A) ),
inference(resolve,[status(thm)],[c_58,c_93]) ).
cnf(c_172,plain,
~ value(in(n1,or1(h2(f))),n1),
inference(resolve,[status(thm)],[c_328,c_118]) ).
cnf(c_329,plain,
( value(in(n1,h1(f)),A)
| ~ value(in(n1,and2(h1(f))),A) ),
inference(resolve,[status(thm)],[c_62,c_94]) ).
cnf(c_173,plain,
~ value(in(n1,and2(h1(f))),n0),
inference(resolve,[status(thm)],[c_329,c_119]) ).
cnf(c_330,plain,
( value(in(n2,h1(f)),A)
| ~ value(in(n2,and2(h1(f))),A) ),
inference(resolve,[status(thm)],[c_64,c_94]) ).
cnf(c_175,plain,
~ value(in(n2,and2(h1(f))),n0),
inference(resolve,[status(thm)],[c_330,c_120]) ).
cnf(c_178,plain,
( mode(and1(h2(f)),abnormal)
| mode(and1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_143,c_25]) ).
cnf(c_180,plain,
( mode(not1(h1(f)),abnormal)
| mode(not1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_164,c_25]) ).
cnf(c_331,plain,
( mode(and2(h1(f)),abnormal)
| mode(and2(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_165,c_25]) ).
cnf(c_182,plain,
mode(and2(h1(f)),ok),
inference(resolve,[status(thm)],[c_53,c_331]) ).
cnf(c_183,plain,
( mode(and1(h1(f)),abnormal)
| mode(and1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_166,c_25]) ).
cnf(c_332,plain,
( value(in(n2,and2(h1(f))),n0)
| value(in(n1,and2(h1(f))),n0)
| ~ value(out(n1,and2(h1(f))),n0)
| ~ type(and2(h1(f)),and) ),
inference(resolve,[status(thm)],[c_182,c_28]) ).
cnf(c_333,plain,
( value(in(n2,and2(h1(f))),n0)
| value(in(n1,and2(h1(f))),n0)
| ~ value(out(n1,and2(h1(f))),n0) ),
inference(resolve,[status(thm)],[c_165,c_332]) ).
cnf(c_334,plain,
( value(in(n2,and2(h1(f))),n0)
| ~ value(out(n1,and2(h1(f))),n0) ),
inference(resolve,[status(thm)],[c_173,c_333]) ).
cnf(c_192,plain,
~ value(out(n1,and2(h1(f))),n0),
inference(resolve,[status(thm)],[c_175,c_334]) ).
cnf(c_335,plain,
( value(out(n1,and2(h1(f))),A)
| ~ value(in(n1,not1(h1(f))),A) ),
inference(resolve,[status(thm)],[c_72,c_94]) ).
cnf(c_196,plain,
~ value(in(n1,not1(h1(f))),n0),
inference(resolve,[status(thm)],[c_335,c_192]) ).
cnf(c_336,plain,
( value(out(n1,and2(h1(f))),A)
| ~ value(out(c,h1(f)),A) ),
inference(resolve,[status(thm)],[c_69,c_94]) ).
cnf(c_197,plain,
~ value(out(c,h1(f)),n0),
inference(resolve,[status(thm)],[c_336,c_192]) ).
cnf(c_198,plain,
( ~ mode(or1(f),abnormal)
| mode(or1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_168,c_57]) ).
cnf(c_199,plain,
( mode(or1(f),ok)
| mode(or1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_198,c_117]) ).
cnf(c_200,plain,
~ value(in(n2,or1(f)),n0),
inference(resolve,[status(thm)],[c_103,c_197]) ).
cnf(c_337,plain,
( value(in(n2,or1(h2(f))),n1)
| value(in(n1,or1(h2(f))),n1)
| ~ value(out(n1,or1(h2(f))),n1)
| ~ type(or1(h2(f)),or)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_199,c_33]) ).
cnf(c_338,plain,
( value(in(n2,or1(h2(f))),n1)
| value(in(n1,or1(h2(f))),n1)
| ~ value(out(n1,or1(h2(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_140,c_337]) ).
cnf(c_206,plain,
( value(in(n2,or1(h2(f))),n1)
| ~ value(out(n1,or1(h2(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_172,c_338]) ).
cnf(c_211,plain,
( ~ mode(or1(f),abnormal)
| mode(and1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_178,c_56]) ).
cnf(c_212,plain,
( mode(or1(f),ok)
| mode(and1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_211,c_117]) ).
cnf(c_339,plain,
( value(in(n1,and1(h2(f))),n1)
| ~ value(out(n1,and1(h2(f))),n1)
| ~ type(and1(h2(f)),and)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_212,c_29]) ).
cnf(c_220,plain,
( value(in(n1,and1(h2(f))),n1)
| ~ value(out(n1,and1(h2(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_143,c_339]) ).
cnf(c_223,plain,
( ~ mode(or1(f),abnormal)
| mode(not1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_180,c_55]) ).
cnf(c_224,plain,
( mode(or1(f),ok)
| mode(not1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_223,c_117]) ).
cnf(c_340,plain,
( value(in(n1,not1(h1(f))),n0)
| ~ value(out(n1,not1(h1(f))),n1)
| ~ type(not1(h1(f)),not)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_224,c_39]) ).
cnf(c_341,plain,
( value(in(n1,not1(h1(f))),n0)
| ~ value(out(n1,not1(h1(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_164,c_340]) ).
cnf(c_225,plain,
( ~ value(out(n1,not1(h1(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_196,c_341]) ).
cnf(c_234,plain,
( ~ mode(or1(f),abnormal)
| mode(and1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_183,c_54]) ).
cnf(c_235,plain,
( mode(or1(f),ok)
| mode(and1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_234,c_117]) ).
cnf(c_342,plain,
( value(in(n2,and1(h1(f))),n1)
| ~ value(out(n1,and1(h1(f))),n1)
| ~ type(and1(h1(f)),and)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_235,c_30]) ).
cnf(c_245,plain,
( value(in(n2,and1(h1(f))),n1)
| ~ value(out(n1,and1(h1(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_166,c_342]) ).
cnf(c_253,plain,
value(out(s,h2(f)),n1),
inference(resolve,[status(thm)],[c_114,c_51]) ).
cnf(c_254,plain,
value(out(n1,or1(f)),n0),
inference(resolve,[status(thm)],[c_116,c_52]) ).
cnf(c_343,plain,
( value(in(n2,or1(f)),n0)
| ~ value(out(n1,or1(f)),n0)
| ~ mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_35,c_92]) ).
cnf(c_344,plain,
( value(in(n2,or1(f)),n0)
| ~ mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_343,c_254]) ).
cnf(c_255,plain,
~ mode(or1(f),ok),
inference(resolve,[status(thm)],[c_344,c_200]) ).
cnf(c_260,plain,
( value(in(n2,and1(h1(f))),n1)
| ~ value(out(n1,and1(h1(f))),n1) ),
inference(resolve,[status(thm)],[c_255,c_245]) ).
cnf(c_276,plain,
~ value(out(n1,not1(h1(f))),n1),
inference(resolve,[status(thm)],[c_255,c_225]) ).
cnf(c_280,plain,
( value(in(n1,and1(h2(f))),n1)
| ~ value(out(n1,and1(h2(f))),n1) ),
inference(resolve,[status(thm)],[c_255,c_220]) ).
cnf(c_290,plain,
( value(in(n2,or1(h2(f))),n1)
| ~ value(out(n1,or1(h2(f))),n1) ),
inference(resolve,[status(thm)],[c_255,c_206]) ).
cnf(c_345,plain,
( value(out(n1,not1(h1(f))),A)
| ~ value(in(n2,and1(h1(f))),A) ),
inference(resolve,[status(thm)],[c_74,c_94]) ).
cnf(c_304,plain,
~ value(in(n2,and1(h1(f))),n1),
inference(resolve,[status(thm)],[c_345,c_276]) ).
cnf(c_305,plain,
~ value(out(n1,and1(h1(f))),n1),
inference(resolve,[status(thm)],[c_304,c_260]) ).
cnf(c_312,plain,
value(out(n1,and1(h2(f))),n1),
inference(resolve,[status(thm)],[c_130,c_253]) ).
cnf(c_315,plain,
value(in(n1,and1(h2(f))),n1),
inference(resolve,[status(thm)],[c_312,c_280]) ).
cnf(c_346,plain,
( value(out(n1,and1(h1(f))),A)
| ~ value(out(s,h1(f)),A) ),
inference(resolve,[status(thm)],[c_67,c_94]) ).
cnf(c_317,plain,
~ value(out(s,h1(f)),n1),
inference(resolve,[status(thm)],[c_346,c_305]) ).
cnf(c_318,plain,
~ value(in(n2,h2(f)),n1),
inference(resolve,[status(thm)],[c_101,c_317]) ).
cnf(c_347,plain,
( value(in(n2,h2(f)),A)
| ~ value(in(n2,or1(h2(f))),A) ),
inference(resolve,[status(thm)],[c_60,c_93]) ).
cnf(c_320,plain,
~ value(in(n2,or1(h2(f))),n1),
inference(resolve,[status(thm)],[c_347,c_318]) ).
cnf(c_321,plain,
~ value(out(n1,or1(h2(f))),n1),
inference(resolve,[status(thm)],[c_320,c_290]) ).
cnf(c_348,plain,
( value(out(n1,or1(h2(f))),n1)
| ~ type(h2(f),halfadder) ),
inference(resolve,[status(thm)],[c_70,c_315]) ).
cnf(c_349,plain,
~ type(h2(f),halfadder),
inference(resolve,[status(thm)],[c_348,c_321]) ).
cnf(c_324,plain,
$false,
inference(resolve,[status(thm)],[c_93,c_349]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV007-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40 % Computer : n015.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Fri Sep 25 16:03:13 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.40 % Process 1780707 was started by sandbox2 on n015,
% 0.13/0.40 % Fri Sep 25 16:03:13 2026
% 0.13/0.40 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.41
% 0.13/0.41 % From the command line: assign(max_seconds, 300).
% 0.13/0.45
% 0.13/0.45 % SZS status Unsatisfiable for theBenchmark
% 0.13/0.45
% 0.13/0.45 % Proof 1 at 0.03 (+ 0.01) seconds.
% 0.13/0.45 % Length of proof is 122.
% 0.13/0.45 % Level of proof is 16.
% 0.13/0.45 % Maximum clause weight is 21.000.
% 0.13/0.45 % Given clauses 178.
% 0.13/0.45
% 0.13/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------