%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV006-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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.15s 5.44s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 47
% Syntax : Number of formulae : 207 ( 70 unt; 0 def)
% Number of atoms : 413 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 434 ( 228 ~; 206 |; 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 : 130 ( 1 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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_outch2_in1or1,axiom,
! [VAR_0] :
( connection(out(c,h2(VAR_0)),in(n1,or1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_outch2_in1or1) ).
cnf(c_14,plain,
( connection(out(c,h2(A)),in(n1,or1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_outch2_in1or1]) ).
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_0_0x,axiom,
! [VAR_0] :
( value(in(n1,VAR_0),n0)
| ~ value(out(n1,VAR_0),n0)
| ~ type(VAR_0,or)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',or_0_0x) ).
cnf(c_34,plain,
( value(in(n1,A),n0)
| ~ value(out(n1,A),n0)
| ~ type(A,or)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[or_0_0x]) ).
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_0_1_bw,axiom,
! [VAR_0] :
( value(in(n1,VAR_0),n1)
| ~ value(out(n1,VAR_0),n0)
| ~ type(VAR_0,not)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',not_0_1_bw) ).
cnf(c_38,plain,
( value(in(n1,A),n1)
| ~ value(out(n1,A),n0)
| ~ type(A,not)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[not_0_1_bw]) ).
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),n1),
file('theBenchmark.p',in1_1) ).
cnf(c_48,plain,
value(in(n1,f),n1),
inference(clausify,[status(thm)],[in1_1]) ).
fof(in2_0,axiom,
value(in(n2,f),n0),
file('theBenchmark.p',in2_0) ).
cnf(c_49,plain,
value(in(n2,f),n0),
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_or1_not1h2,axiom,
( ~ mode(not1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('theBenchmark.p',diagnosis_or1_not1h2) ).
cnf(c_53,plain,
( ~ mode(not1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
inference(clausify,[status(thm)],[diagnosis_or1_not1h2]) ).
fof(diagnosis_and2,axiom,
~ mode(and2(h2(f)),abnormal),
file('theBenchmark.p',diagnosis_and2) ).
cnf(c_54,plain,
~ mode(and2(h2(f)),abnormal),
inference(clausify,[status(thm)],[diagnosis_and2]) ).
fof(diagnosis_or1_and1h2,axiom,
( ~ mode(and1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('theBenchmark.p',diagnosis_or1_and1h2) ).
cnf(c_55,plain,
( ~ mode(and1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
inference(clausify,[status(thm)],[diagnosis_or1_and1h2]) ).
fof(diagnosis_or1h1,axiom,
~ mode(or1(h1(f)),abnormal),
file('theBenchmark.p',diagnosis_or1h1) ).
cnf(c_56,plain,
~ mode(or1(h1(f)),abnormal),
inference(clausify,[status(thm)],[diagnosis_or1h1]) ).
fof(diagnosis_not1h1,axiom,
~ mode(not1(h1(f)),abnormal),
file('theBenchmark.p',diagnosis_not1h1) ).
cnf(c_57,plain,
~ mode(not1(h1(f)),abnormal),
inference(clausify,[status(thm)],[diagnosis_not1h1]) ).
fof(diagnosis_and2h1,axiom,
~ mode(and2(h1(f)),abnormal),
file('theBenchmark.p',diagnosis_and2h1) ).
cnf(c_58,plain,
~ mode(and2(h1(f)),abnormal),
inference(clausify,[status(thm)],[diagnosis_and2h1]) ).
fof(diagnosis_and1h1,axiom,
~ mode(and1(h1(f)),abnormal),
file('theBenchmark.p',diagnosis_and1h1) ).
cnf(c_59,plain,
~ mode(and1(h1(f)),abnormal),
inference(clausify,[status(thm)],[diagnosis_and1h1]) ).
cnf(c_62,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_64,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_66,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_69,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_71,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_72,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_74,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_76,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_78,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_82,plain,
( value(out(c,h2(A)),B)
| ~ value(in(n1,or1(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_14,c_2]) ).
cnf(c_84,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_86,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_88,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_91,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_93,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_94,plain,
type(or1(f),or),
inference(resolve,[status(thm)],[c_47,c_46]) ).
cnf(c_95,plain,
type(h2(f),halfadder),
inference(resolve,[status(thm)],[c_47,c_45]) ).
cnf(c_96,plain,
type(h1(f),halfadder),
inference(resolve,[status(thm)],[c_47,c_44]) ).
cnf(c_98,plain,
~ value(in(n1,f),n0),
inference(resolve,[status(thm)],[c_23,c_48]) ).
cnf(c_99,plain,
~ value(in(n2,f),n1),
inference(resolve,[status(thm)],[c_49,c_23]) ).
cnf(c_100,plain,
~ value(in(c,f),n0),
inference(resolve,[status(thm)],[c_23,c_50]) ).
cnf(c_103,plain,
( value(out(s,h1(f)),A)
| ~ value(in(n2,h2(f)),A) ),
inference(resolve,[status(thm)],[c_78,c_47]) ).
cnf(c_107,plain,
( value(out(c,h2(f)),A)
| ~ value(in(n1,or1(f)),A) ),
inference(resolve,[status(thm)],[c_82,c_47]) ).
cnf(c_116,plain,
( value(out(s,h2(f)),A)
| ~ value(out(s,f),A) ),
inference(resolve,[status(thm)],[c_91,c_47]) ).
cnf(c_118,plain,
( value(out(n1,or1(f)),A)
| ~ value(out(c,f),A) ),
inference(resolve,[status(thm)],[c_93,c_47]) ).
cnf(c_119,plain,
( mode(or1(f),abnormal)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_94,c_25]) ).
cnf(c_333,plain,
( value(in(n1,f),A)
| ~ value(in(n1,h2(f)),A) ),
inference(resolve,[status(thm)],[c_84,c_47]) ).
cnf(c_120,plain,
~ value(in(n1,h2(f)),n0),
inference(resolve,[status(thm)],[c_333,c_98]) ).
cnf(c_334,plain,
( value(in(n2,f),A)
| ~ value(in(n1,h1(f)),A) ),
inference(resolve,[status(thm)],[c_86,c_47]) ).
cnf(c_121,plain,
~ value(in(n1,h1(f)),n1),
inference(resolve,[status(thm)],[c_334,c_99]) ).
cnf(c_335,plain,
( value(in(c,f),A)
| ~ value(in(n2,h1(f)),A) ),
inference(resolve,[status(thm)],[c_88,c_47]) ).
cnf(c_122,plain,
~ value(in(n2,h1(f)),n0),
inference(resolve,[status(thm)],[c_335,c_100]) ).
cnf(c_132,plain,
( value(out(n1,and1(h2(f))),A)
| ~ value(out(s,h2(f)),A) ),
inference(resolve,[status(thm)],[c_95,c_69]) ).
cnf(c_143,plain,
type(not1(h2(f)),not),
inference(resolve,[status(thm)],[c_95,c_42]) ).
cnf(c_144,plain,
type(and2(h2(f)),and),
inference(resolve,[status(thm)],[c_95,c_41]) ).
cnf(c_145,plain,
type(and1(h2(f)),and),
inference(resolve,[status(thm)],[c_95,c_40]) ).
cnf(c_165,plain,
type(or1(h1(f)),or),
inference(resolve,[status(thm)],[c_96,c_43]) ).
cnf(c_166,plain,
type(not1(h1(f)),not),
inference(resolve,[status(thm)],[c_96,c_42]) ).
cnf(c_167,plain,
type(and2(h1(f)),and),
inference(resolve,[status(thm)],[c_96,c_41]) ).
cnf(c_168,plain,
type(and1(h1(f)),and),
inference(resolve,[status(thm)],[c_96,c_40]) ).
cnf(c_171,plain,
( mode(not1(h2(f)),abnormal)
| mode(not1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_143,c_25]) ).
cnf(c_336,plain,
( value(in(n1,h2(f)),A)
| ~ value(in(n1,and2(h2(f))),A) ),
inference(resolve,[status(thm)],[c_64,c_95]) ).
cnf(c_173,plain,
~ value(in(n1,and2(h2(f))),n0),
inference(resolve,[status(thm)],[c_336,c_120]) ).
cnf(c_337,plain,
( value(in(n1,h1(f)),A)
| ~ value(in(n1,and2(h1(f))),A) ),
inference(resolve,[status(thm)],[c_64,c_96]) ).
cnf(c_175,plain,
~ value(in(n1,and2(h1(f))),n1),
inference(resolve,[status(thm)],[c_337,c_121]) ).
cnf(c_338,plain,
( value(in(n2,h1(f)),A)
| ~ value(in(n2,or1(h1(f))),A) ),
inference(resolve,[status(thm)],[c_62,c_96]) ).
cnf(c_178,plain,
~ value(in(n2,or1(h1(f))),n0),
inference(resolve,[status(thm)],[c_338,c_122]) ).
cnf(c_339,plain,
( mode(and2(h2(f)),abnormal)
| mode(and2(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_144,c_25]) ).
cnf(c_179,plain,
mode(and2(h2(f)),ok),
inference(resolve,[status(thm)],[c_54,c_339]) ).
cnf(c_180,plain,
( mode(and1(h2(f)),abnormal)
| mode(and1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_145,c_25]) ).
cnf(c_340,plain,
( mode(or1(h1(f)),abnormal)
| mode(or1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_165,c_25]) ).
cnf(c_181,plain,
mode(or1(h1(f)),ok),
inference(resolve,[status(thm)],[c_56,c_340]) ).
cnf(c_341,plain,
( mode(not1(h1(f)),abnormal)
| mode(not1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_166,c_25]) ).
cnf(c_182,plain,
mode(not1(h1(f)),ok),
inference(resolve,[status(thm)],[c_57,c_341]) ).
cnf(c_342,plain,
( mode(and2(h1(f)),abnormal)
| mode(and2(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_167,c_25]) ).
cnf(c_184,plain,
mode(and2(h1(f)),ok),
inference(resolve,[status(thm)],[c_58,c_342]) ).
cnf(c_343,plain,
( mode(and1(h1(f)),abnormal)
| mode(and1(h1(f)),ok) ),
inference(resolve,[status(thm)],[c_168,c_25]) ).
cnf(c_185,plain,
mode(and1(h1(f)),ok),
inference(resolve,[status(thm)],[c_59,c_343]) ).
cnf(c_344,plain,
( value(in(n2,and2(h2(f))),n0)
| value(in(n1,and2(h2(f))),n0)
| ~ value(out(n1,and2(h2(f))),n0)
| ~ type(and2(h2(f)),and) ),
inference(resolve,[status(thm)],[c_179,c_28]) ).
cnf(c_345,plain,
( value(in(n2,and2(h2(f))),n0)
| value(in(n1,and2(h2(f))),n0)
| ~ value(out(n1,and2(h2(f))),n0) ),
inference(resolve,[status(thm)],[c_144,c_344]) ).
cnf(c_195,plain,
( value(in(n2,and2(h2(f))),n0)
| ~ value(out(n1,and2(h2(f))),n0) ),
inference(resolve,[status(thm)],[c_173,c_345]) ).
cnf(c_346,plain,
( value(in(n2,or1(h1(f))),n0)
| ~ value(out(n1,or1(h1(f))),n0)
| ~ type(or1(h1(f)),or) ),
inference(resolve,[status(thm)],[c_181,c_35]) ).
cnf(c_347,plain,
( value(in(n2,or1(h1(f))),n0)
| ~ value(out(n1,or1(h1(f))),n0) ),
inference(resolve,[status(thm)],[c_165,c_346]) ).
cnf(c_201,plain,
~ value(out(n1,or1(h1(f))),n0),
inference(resolve,[status(thm)],[c_178,c_347]) ).
cnf(c_348,plain,
( value(in(n1,not1(h1(f))),n1)
| ~ value(out(n1,not1(h1(f))),n0)
| ~ type(not1(h1(f)),not) ),
inference(resolve,[status(thm)],[c_182,c_38]) ).
cnf(c_207,plain,
( value(in(n1,not1(h1(f))),n1)
| ~ value(out(n1,not1(h1(f))),n0) ),
inference(resolve,[status(thm)],[c_166,c_348]) ).
cnf(c_349,plain,
( value(in(n1,and2(h1(f))),n1)
| ~ value(out(n1,and2(h1(f))),n1)
| ~ type(and2(h1(f)),and) ),
inference(resolve,[status(thm)],[c_184,c_29]) ).
cnf(c_350,plain,
( value(in(n1,and2(h1(f))),n1)
| ~ value(out(n1,and2(h1(f))),n1) ),
inference(resolve,[status(thm)],[c_167,c_349]) ).
cnf(c_227,plain,
~ value(out(n1,and2(h1(f))),n1),
inference(resolve,[status(thm)],[c_175,c_350]) ).
cnf(c_351,plain,
( value(in(n2,and1(h1(f))),n0)
| value(in(n1,and1(h1(f))),n0)
| ~ value(out(n1,and1(h1(f))),n0)
| ~ type(and1(h1(f)),and) ),
inference(resolve,[status(thm)],[c_185,c_28]) ).
cnf(c_243,plain,
( value(in(n2,and1(h1(f))),n0)
| value(in(n1,and1(h1(f))),n0)
| ~ value(out(n1,and1(h1(f))),n0) ),
inference(resolve,[status(thm)],[c_168,c_351]) ).
cnf(c_352,plain,
( value(out(n1,or1(h1(f))),A)
| ~ value(in(n1,and1(h1(f))),A) ),
inference(resolve,[status(thm)],[c_72,c_96]) ).
cnf(c_246,plain,
~ value(in(n1,and1(h1(f))),n0),
inference(resolve,[status(thm)],[c_352,c_201]) ).
cnf(c_247,plain,
( value(in(n2,and1(h1(f))),n0)
| ~ value(out(n1,and1(h1(f))),n0) ),
inference(resolve,[status(thm)],[c_246,c_243]) ).
cnf(c_353,plain,
( value(out(n1,and2(h1(f))),A)
| ~ value(in(n1,not1(h1(f))),A) ),
inference(resolve,[status(thm)],[c_74,c_96]) ).
cnf(c_250,plain,
~ value(in(n1,not1(h1(f))),n1),
inference(resolve,[status(thm)],[c_353,c_227]) ).
cnf(c_254,plain,
~ value(out(n1,not1(h1(f))),n0),
inference(resolve,[status(thm)],[c_250,c_207]) ).
cnf(c_258,plain,
( ~ mode(or1(f),abnormal)
| mode(not1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_171,c_53]) ).
cnf(c_354,plain,
( value(out(n1,not1(h1(f))),A)
| ~ value(in(n2,and1(h1(f))),A) ),
inference(resolve,[status(thm)],[c_76,c_96]) ).
cnf(c_259,plain,
~ value(in(n2,and1(h1(f))),n0),
inference(resolve,[status(thm)],[c_354,c_254]) ).
cnf(c_260,plain,
~ value(out(n1,and1(h1(f))),n0),
inference(resolve,[status(thm)],[c_259,c_247]) ).
cnf(c_263,plain,
( mode(or1(f),ok)
| mode(not1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_258,c_119]) ).
cnf(c_355,plain,
( value(in(n1,not1(h2(f))),n0)
| ~ value(out(n1,not1(h2(f))),n1)
| ~ type(not1(h2(f)),not)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_263,c_39]) ).
cnf(c_264,plain,
( value(in(n1,not1(h2(f))),n0)
| ~ value(out(n1,not1(h2(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_143,c_355]) ).
cnf(c_278,plain,
( ~ mode(or1(f),abnormal)
| mode(and1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_180,c_55]) ).
cnf(c_279,plain,
( mode(or1(f),ok)
| mode(and1(h2(f)),ok) ),
inference(resolve,[status(thm)],[c_278,c_119]) ).
cnf(c_356,plain,
( value(out(n1,and1(h1(f))),A)
| ~ value(out(s,h1(f)),A) ),
inference(resolve,[status(thm)],[c_69,c_96]) ).
cnf(c_280,plain,
~ value(out(s,h1(f)),n0),
inference(resolve,[status(thm)],[c_356,c_260]) ).
cnf(c_281,plain,
~ value(in(n2,h2(f)),n0),
inference(resolve,[status(thm)],[c_103,c_280]) ).
cnf(c_357,plain,
( value(in(n2,h2(f)),A)
| ~ value(in(n2,and2(h2(f))),A) ),
inference(resolve,[status(thm)],[c_66,c_95]) ).
cnf(c_282,plain,
~ value(in(n2,and2(h2(f))),n0),
inference(resolve,[status(thm)],[c_357,c_281]) ).
cnf(c_284,plain,
~ value(out(n1,and2(h2(f))),n0),
inference(resolve,[status(thm)],[c_282,c_195]) ).
cnf(c_358,plain,
( value(in(n2,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_279,c_30]) ).
cnf(c_293,plain,
( value(in(n2,and1(h2(f))),n1)
| ~ value(out(n1,and1(h2(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_145,c_358]) ).
cnf(c_359,plain,
( value(out(n1,and2(h2(f))),A)
| ~ value(in(n1,not1(h2(f))),A) ),
inference(resolve,[status(thm)],[c_74,c_95]) ).
cnf(c_298,plain,
~ value(in(n1,not1(h2(f))),n0),
inference(resolve,[status(thm)],[c_359,c_284]) ).
cnf(c_360,plain,
( value(out(n1,and2(h2(f))),A)
| ~ value(out(c,h2(f)),A) ),
inference(resolve,[status(thm)],[c_71,c_95]) ).
cnf(c_299,plain,
~ value(out(c,h2(f)),n0),
inference(resolve,[status(thm)],[c_360,c_284]) ).
cnf(c_302,plain,
( ~ value(out(n1,not1(h2(f))),n1)
| mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_298,c_264]) ).
cnf(c_303,plain,
~ value(in(n1,or1(f)),n0),
inference(resolve,[status(thm)],[c_107,c_299]) ).
cnf(c_306,plain,
value(out(s,h2(f)),n1),
inference(resolve,[status(thm)],[c_116,c_51]) ).
cnf(c_307,plain,
value(out(n1,or1(f)),n0),
inference(resolve,[status(thm)],[c_118,c_52]) ).
cnf(c_361,plain,
( value(in(n1,or1(f)),n0)
| ~ value(out(n1,or1(f)),n0)
| ~ mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_34,c_94]) ).
cnf(c_362,plain,
( value(in(n1,or1(f)),n0)
| ~ mode(or1(f),ok) ),
inference(resolve,[status(thm)],[c_361,c_307]) ).
cnf(c_308,plain,
~ mode(or1(f),ok),
inference(resolve,[status(thm)],[c_362,c_303]) ).
cnf(c_309,plain,
~ value(out(n1,not1(h2(f))),n1),
inference(resolve,[status(thm)],[c_308,c_302]) ).
cnf(c_315,plain,
( value(in(n2,and1(h2(f))),n1)
| ~ value(out(n1,and1(h2(f))),n1) ),
inference(resolve,[status(thm)],[c_308,c_293]) ).
cnf(c_363,plain,
( value(out(n1,not1(h2(f))),A)
| ~ value(in(n2,and1(h2(f))),A) ),
inference(resolve,[status(thm)],[c_76,c_95]) ).
cnf(c_329,plain,
~ value(in(n2,and1(h2(f))),n1),
inference(resolve,[status(thm)],[c_363,c_309]) ).
cnf(c_330,plain,
~ value(out(n1,and1(h2(f))),n1),
inference(resolve,[status(thm)],[c_329,c_315]) ).
cnf(c_364,plain,
value(out(n1,and1(h2(f))),n1),
inference(resolve,[status(thm)],[c_132,c_306]) ).
cnf(c_332,plain,
$false,
inference(resolve,[status(thm)],[c_330,c_364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV006-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.39 % Computer : n001.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Fri Sep 25 16:05:47 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.39 % Process 3771518 was started by sandbox on n001,
% 0.10/5.39 % Fri Sep 25 16:05:47 2026
% 0.10/5.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/5.40
% 0.15/5.40 % From the command line: assign(max_seconds, 300).
% 0.15/5.44
% 0.15/5.44 % SZS status Unsatisfiable for theBenchmark
% 0.15/5.44
% 0.15/5.44 % Proof 1 at 0.02 (+ 0.00) seconds.
% 0.15/5.44 % Length of proof is 128.
% 0.15/5.44 % Level of proof is 20.
% 0.15/5.44 % Maximum clause weight is 21.000.
% 0.15/5.44 % Given clauses 170.
% 0.15/5.44
% 0.15/5.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------