%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV008-1.001 : 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 : n012.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.07s 0.34s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : HWV008-1.001 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Fri Sep 25 15:59:50 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/0.31 % Process 2493571 was started by sandbox on n012,
% 0.03/0.31 % Fri Sep 25 15:59:50 2026
% 0.03/0.31 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.03/0.31
% 0.03/0.31 % From the command line: assign(max_seconds, 300).
% 0.07/0.34
% 0.07/0.34 % SZS status Unsatisfiable for theBenchmark
% 0.07/0.34
% 0.07/0.34 % Proof 1 at 0.01 (+ 0.01) seconds.
% 0.07/0.34 % Length of proof is 72.
% 0.07/0.34 % Level of proof is 11.
% 0.07/0.34 % Maximum clause weight is 24.000.
% 0.07/0.34 % Given clauses 136.
% 0.07/0.34
% 0.07/0.34 % SZS output start CNFRefutation for theBenchmark
% 0.07/0.34 fof(value_propagation2, axiom, ! [VAR_0,VAR_1,VAR_2] : (~ (connection(VAR_0,VAR_1)) | ~ (value(VAR_1,VAR_2)) | value(VAR_0,VAR_2)), file('theBenchmark.p',value_propagation2)).
% 0.07/0.34 cnf(c_2, plain, ~connection(A,B) | ~value(B,C) | value(A,C), inference(clausify, [status(thm)], [value_propagation2])).
% 0.07/0.34 fof(value_propagation1, axiom, ! [VAR_0,VAR_1,VAR_2] : (~ (connection(VAR_0,VAR_1)) | ~ (value(VAR_0,VAR_2)) | value(VAR_1,VAR_2)), file('theBenchmark.p',value_propagation1)).
% 0.07/0.34 cnf(c_3, plain, ~connection(A,B) | ~value(A,C) | value(B,C), inference(clausify, [status(thm)], [value_propagation1])).
% 0.07/0.34 fof(halfadder_connection_in1_in1and2, axiom, ! [VAR_0] : (~ (type(VAR_0,halfadder)) | connection(in(n1,VAR_0),in(n1,and2(VAR_0)))), file('theBenchmark.p',halfadder_connection_in1_in1and2)).
% 0.07/0.34 cnf(c_5, plain, ~type(A,halfadder) | connection(in(n1,A),in(n1,and2(A))), inference(clausify, [status(thm)], [halfadder_connection_in1_in1and2])).
% 0.07/0.34 fof(halfadder_connection_in2_in2and2, axiom, ! [VAR_0] : (~ (type(VAR_0,halfadder)) | connection(in(n2,VAR_0),in(n2,and2(VAR_0)))), file('theBenchmark.p',halfadder_connection_in2_in2and2)).
% 0.07/0.34 cnf(c_6, plain, ~type(A,halfadder) | connection(in(n2,A),in(n2,and2(A))), inference(clausify, [status(thm)], [halfadder_connection_in2_in2and2])).
% 0.07/0.34 fof(halfadder_connection_outc_out1and2, axiom, ! [VAR_0] : (~ (type(VAR_0,halfadder)) | connection(out(c,VAR_0),out(n1,and2(VAR_0)))), file('theBenchmark.p',halfadder_connection_outc_out1and2)).
% 0.07/0.34 cnf(c_8, plain, ~type(A,halfadder) | connection(out(c,A),out(n1,and2(A))), inference(clausify, [status(thm)], [halfadder_connection_outc_out1and2])).
% 0.07/0.34 fof(fulladder_connection_outch1_in2or1, axiom, ! [VAR_0] : (~ (type(VAR_0,fulladder)) | connection(out(c,h1(VAR_0)),in(n2,or1(VAR_0)))), file('theBenchmark.p',fulladder_connection_outch1_in2or1)).
% 0.07/0.34 cnf(c_13, plain, ~type(A,fulladder) | connection(out(c,h1(A)),in(n2,or1(A))), inference(clausify, [status(thm)], [fulladder_connection_outch1_in2or1])).
% 0.07/0.34 fof(fulladder_connection_outch2_in1or1, axiom, ! [VAR_0] : (~ (type(VAR_0,fulladder)) | connection(out(c,h2(VAR_0)),in(n1,or1(VAR_0)))), file('theBenchmark.p',fulladder_connection_outch2_in1or1)).
% 0.07/0.34 cnf(c_14, plain, ~type(A,fulladder) | connection(out(c,h2(A)),in(n1,or1(A))), inference(clausify, [status(thm)], [fulladder_connection_outch2_in1or1])).
% 0.07/0.34 fof(fulladder_connection_in1_in1h2, axiom, ! [VAR_0] : (~ (type(VAR_0,fulladder)) | connection(in(n1,VAR_0),in(n1,h2(VAR_0)))), file('theBenchmark.p',fulladder_connection_in1_in1h2)).
% 0.07/0.34 cnf(c_15, plain, ~type(A,fulladder) | connection(in(n1,A),in(n1,h2(A))), inference(clausify, [status(thm)], [fulladder_connection_in1_in1h2])).
% 0.07/0.34 fof(fulladder_connection_inc_in2h1, axiom, ! [VAR_0] : (~ (type(VAR_0,fulladder)) | connection(in(c,VAR_0),in(n2,h1(VAR_0)))), file('theBenchmark.p',fulladder_connection_inc_in2h1)).
% 0.07/0.34 cnf(c_17, plain, ~type(A,fulladder) | connection(in(c,A),in(n2,h1(A))), inference(clausify, [status(thm)], [fulladder_connection_inc_in2h1])).
% 0.07/0.34 fof(fulladder_connection_outc_out1or1, axiom, ! [VAR_0] : (~ (type(VAR_0,fulladder)) | connection(out(c,VAR_0),out(n1,or1(VAR_0)))), file('theBenchmark.p',fulladder_connection_outc_out1or1)).
% 0.07/0.34 cnf(c_19, plain, ~type(A,fulladder) | connection(out(c,A),out(n1,or1(A))), inference(clausify, [status(thm)], [fulladder_connection_outc_out1or1])).
% 0.07/0.34 fof(nbit_adder_connection_outc_outcv1, axiom, ! [VAR_0] : (~ (type(VAR_0,nbit_adder(n1))) | connection(out(c,VAR_0),out(c,n1 v VAR_0))), file('theBenchmark.p',nbit_adder_connection_outc_outcv1)).
% 0.07/0.34 cnf(c_21, plain, ~type(A,nbit_adder(n1)) | connection(out(c,A),out(c,n1 v A)), inference(clausify, [status(thm)], [nbit_adder_connection_outc_outcv1])).
% 0.07/0.34 fof(nbit_adder_connection_ina1_in1v1, axiom, ! [VAR_0] : (~ (type(VAR_0,nbit_adder(n1))) | connection(in(a1,VAR_0),in(n1,n1 v VAR_0))), file('theBenchmark.p',nbit_adder_connection_ina1_in1v1)).
% 0.07/0.34 cnf(c_22, plain, ~type(A,nbit_adder(n1)) | connection(in(a1,A),in(n1,n1 v A)), inference(clausify, [status(thm)], [nbit_adder_connection_ina1_in1v1])).
% 0.07/0.34 fof(nbit_adder_connection_inc_incv1, axiom, ! [VAR_0] : (~ (type(VAR_0,nbit_adder(n1))) | connection(in(c,VAR_0),in(c,n1 v VAR_0))), file('theBenchmark.p',nbit_adder_connection_inc_incv1)).
% 0.07/0.34 cnf(c_24, plain, ~type(A,nbit_adder(n1)) | connection(in(c,A),in(c,n1 v A)), inference(clausify, [status(thm)], [nbit_adder_connection_inc_incv1])).
% 0.07/0.34 fof(unique_value, axiom, ! [VAR_0,VAR_1,VAR_2] : (~ (value(VAR_0,VAR_1)) | ~ (value(VAR_0,VAR_2)) | equal_value(VAR_1,VAR_2)), file('theBenchmark.p',unique_value)).
% 0.07/0.34 cnf(c_25, plain, ~value(A,B) | ~value(A,C) | equal_value(B,C), inference(clausify, [status(thm)], [unique_value])).
% 0.07/0.34 fof(equal_value1, axiom, (~ (equal_value(n0,n1))), file('theBenchmark.p',equal_value1)).
% 0.07/0.34 cnf(c_26, plain, ~equal_value(n0,n1), inference(clausify, [status(thm)], [equal_value1])).
% 0.07/0.34 cnf(c_28, plain, ~value(A,n0) | ~value(A,n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_25, c_26])).
% 0.07/0.34 fof(ok_or_abnormal, axiom, ! [VAR_0,VAR_1] : (~ (type(VAR_0,VAR_1)) | mode(VAR_0,ok) | mode(VAR_0,abnormal)), file('theBenchmark.p',ok_or_abnormal)).
% 0.07/0.34 cnf(c_30, plain, ~type(A,B) | mode(A,ok) | mode(A,abnormal), inference(clausify, [status(thm)], [ok_or_abnormal])).
% 0.07/0.34 fof(and_1_1x, axiom, ! [VAR_0] : (~ (mode(VAR_0,ok)) | ~ (type(VAR_0,and)) | ~ (value(out(n1,VAR_0),n1)) | value(in(n1,VAR_0),n1)), file('theBenchmark.p',and_1_1x)).
% 0.07/0.34 cnf(c_34, plain, ~mode(A,ok) | ~type(A,and) | ~value(out(n1,A),n1) | value(in(n1,A),n1), inference(clausify, [status(thm)], [and_1_1x])).
% 0.07/0.34 fof(and_1_x1, axiom, ! [VAR_0] : (~ (mode(VAR_0,ok)) | ~ (type(VAR_0,and)) | ~ (value(out(n1,VAR_0),n1)) | value(in(n2,VAR_0),n1)), file('theBenchmark.p',and_1_x1)).
% 0.07/0.34 cnf(c_35, plain, ~mode(A,ok) | ~type(A,and) | ~value(out(n1,A),n1) | value(in(n2,A),n1), inference(clausify, [status(thm)], [and_1_x1])).
% 0.07/0.34 fof(or_1_11, axiom, ! [VAR_0] : (~ (mode(VAR_0,ok)) | ~ (type(VAR_0,or)) | ~ (value(out(n1,VAR_0),n1)) | value(in(n1,VAR_0),n1) | value(in(n2,VAR_0),n1)), file('theBenchmark.p',or_1_11)).
% 0.07/0.34 cnf(c_38, plain, ~mode(A,ok) | ~type(A,or) | ~value(out(n1,A),n1) | value(in(n1,A),n1) | value(in(n2,A),n1), inference(clausify, [status(thm)], [or_1_11])).
% 0.07/0.34 fof(halfadder_and2, axiom, ! [VAR_0] : (~ (type(VAR_0,halfadder)) | type(and2(VAR_0),and)), file('theBenchmark.p',halfadder_and2)).
% 0.07/0.34 cnf(c_46, plain, ~type(A,halfadder) | type(and2(A),and), inference(clausify, [status(thm)], [halfadder_and2])).
% 0.07/0.34 fof(fulladder_halfadder1, axiom, ! [VAR_0] : (~ (type(VAR_0,fulladder)) | type(h1(VAR_0),halfadder)), file('theBenchmark.p',fulladder_halfadder1)).
% 0.07/0.34 cnf(c_49, plain, ~type(A,fulladder) | type(h1(A),halfadder), inference(clausify, [status(thm)], [fulladder_halfadder1])).
% 0.07/0.34 fof(fulladder_halfadder2, axiom, ! [VAR_0] : (~ (type(VAR_0,fulladder)) | type(h2(VAR_0),halfadder)), file('theBenchmark.p',fulladder_halfadder2)).
% 0.07/0.34 cnf(c_50, plain, ~type(A,fulladder) | type(h2(A),halfadder), inference(clausify, [status(thm)], [fulladder_halfadder2])).
% 0.07/0.34 fof(fulladder_or1, axiom, ! [VAR_0] : (~ (type(VAR_0,fulladder)) | type(or1(VAR_0),or)), file('theBenchmark.p',fulladder_or1)).
% 0.07/0.34 cnf(c_51, plain, ~type(A,fulladder) | type(or1(A),or), inference(clausify, [status(thm)], [fulladder_or1])).
% 0.07/0.34 fof(nbit_adder_fulladder1, axiom, ! [VAR_0] : (~ (type(VAR_0,nbit_adder(n1))) | type(n1 v VAR_0,fulladder)), file('theBenchmark.p',nbit_adder_fulladder1)).
% 0.07/0.34 cnf(c_52, plain, ~type(A,nbit_adder(n1)) | type(n1 v A,fulladder), inference(clausify, [status(thm)], [nbit_adder_fulladder1])).
% 0.07/0.34 fof(a_isa_1bit_adder, axiom, (type(a,nbit_adder(n1))), file('theBenchmark.p',a_isa_1bit_adder)).
% 0.07/0.34 cnf(c_53, plain, type(a,nbit_adder(n1)), inference(clausify, [status(thm)], [a_isa_1bit_adder])).
% 0.07/0.34 fof(ina1_0, axiom, (value(in(a1,a),n0)), file('theBenchmark.p',ina1_0)).
% 0.07/0.34 cnf(c_54, plain, value(in(a1,a),n0), inference(clausify, [status(thm)], [ina1_0])).
% 0.07/0.34 fof(inc_0, axiom, (value(in(c,a),n0)), file('theBenchmark.p',inc_0)).
% 0.07/0.34 cnf(c_56, plain, value(in(c,a),n0), inference(clausify, [status(thm)], [inc_0])).
% 0.07/0.34 fof(outc_0, axiom, (value(out(c,a),n1)), file('theBenchmark.p',outc_0)).
% 0.07/0.34 cnf(c_58, plain, value(out(c,a),n1), inference(clausify, [status(thm)], [outc_0])).
% 0.07/0.34 fof(diagnosis_or1v1, axiom, (~ (mode(or1(n1 v a),abnormal))), file('theBenchmark.p',diagnosis_or1v1)).
% 0.07/0.34 cnf(c_59, plain, ~mode(or1(n1 v a),abnormal), inference(clausify, [status(thm)], [diagnosis_or1v1])).
% 0.07/0.34 fof(diagnosis_and2h1v1, axiom, (~ (mode(and2(h1(n1 v a)),abnormal))), file('theBenchmark.p',diagnosis_and2h1v1)).
% 0.07/0.34 cnf(c_60, plain, ~mode(and2(h1(n1 v a)),abnormal), inference(clausify, [status(thm)], [diagnosis_and2h1v1])).
% 0.07/0.34 fof(diagnosis_and2h2v1, axiom, (~ (mode(and2(h2(n1 v a)),abnormal))), file('theBenchmark.p',diagnosis_and2h2v1)).
% 0.07/0.34 cnf(c_61, plain, ~mode(and2(h2(n1 v a)),abnormal), inference(clausify, [status(thm)], [diagnosis_and2h2v1])).
% 0.07/0.34 cnf(c_66, plain, ~type(A,halfadder) | ~value(in(n1,and2(A)),B) | value(in(n1,A),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_5, c_2])).
% 0.07/0.34 cnf(c_68, plain, ~type(A,halfadder) | ~value(in(n2,and2(A)),B) | value(in(n2,A),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_6, c_2])).
% 0.07/0.34 cnf(c_73, plain, ~type(A,halfadder) | ~value(out(c,A),B) | value(out(n1,and2(A)),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_8, c_3])).
% 0.07/0.34 cnf(c_82, plain, ~type(A,fulladder) | ~value(in(n2,or1(A)),B) | value(out(c,h1(A)),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_13, c_2])).
% 0.07/0.34 cnf(c_84, plain, ~type(A,fulladder) | ~value(in(n1,or1(A)),B) | value(out(c,h2(A)),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_14, c_2])).
% 0.07/0.34 cnf(c_86, plain, ~type(A,fulladder) | ~value(in(n1,h2(A)),B) | value(in(n1,A),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_15, c_2])).
% 0.07/0.34 cnf(c_90, plain, ~type(A,fulladder) | ~value(in(n2,h1(A)),B) | value(in(c,A),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_17, c_2])).
% 0.07/0.34 cnf(c_95, plain, ~type(A,fulladder) | ~value(out(c,A),B) | value(out(n1,or1(A)),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_19, c_3])).
% 0.07/0.34 cnf(c_99, plain, ~type(A,nbit_adder(n1)) | ~value(out(c,A),B) | value(out(c,n1 v A),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_21, c_3])).
% 0.07/0.34 cnf(c_100, plain, ~type(A,nbit_adder(n1)) | ~value(in(n1,n1 v A),B) | value(in(a1,A),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_22, c_2])).
% 0.07/0.34 cnf(c_104, plain, ~type(A,nbit_adder(n1)) | ~value(in(c,n1 v A),B) | value(in(c,A),B),
% 0.07/0.34 inference(resolve, [status(thm)], [c_24, c_2])).
% 0.07/0.34 cnf(c_106, plain, type(n1 v a,fulladder),
% 0.07/0.34 inference(resolve, [status(thm)], [c_53, c_52])).
% 0.07/0.34 cnf(c_108, plain, ~value(in(a1,a),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_54, c_28])).
% 0.07/0.34 cnf(c_110, plain, ~value(in(c,a),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_56, c_28])).
% 0.07/0.34 cnf(c_116, plain, ~value(out(c,a),A) | value(out(c,n1 v a),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_99, c_53])).
% 0.07/0.34 cnf(c_139, plain, type(or1(n1 v a),or),
% 0.07/0.34 inference(resolve, [status(thm)], [c_106, c_51])).
% 0.07/0.34 cnf(c_140, plain, type(h2(n1 v a),halfadder),
% 0.07/0.34 inference(resolve, [status(thm)], [c_106, c_50])).
% 0.07/0.34 cnf(c_141, plain, type(h1(n1 v a),halfadder),
% 0.07/0.34 inference(resolve, [status(thm)], [c_106, c_49])).
% 0.07/0.34 cnf(c_273, plain, ~value(in(n1,n1 v a),A) | value(in(a1,a),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_100, c_53])).
% 0.07/0.34 cnf(c_143, plain, ~value(in(n1,n1 v a),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_273, c_108])).
% 0.07/0.34 cnf(c_274, plain, ~value(in(c,n1 v a),A) | value(in(c,a),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_104, c_53])).
% 0.07/0.34 cnf(c_145, plain, ~value(in(c,n1 v a),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_274, c_110])).
% 0.07/0.34 cnf(c_275, plain, mode(or1(n1 v a),ok) | mode(or1(n1 v a),abnormal),
% 0.07/0.34 inference(resolve, [status(thm)], [c_139, c_30])).
% 0.07/0.34 cnf(c_147, plain, mode(or1(n1 v a),ok),
% 0.07/0.34 inference(resolve, [status(thm)], [c_59, c_275])).
% 0.07/0.34 cnf(c_168, plain, type(and2(h2(n1 v a)),and),
% 0.07/0.34 inference(resolve, [status(thm)], [c_140, c_46])).
% 0.07/0.34 cnf(c_191, plain, type(and2(h1(n1 v a)),and),
% 0.07/0.34 inference(resolve, [status(thm)], [c_141, c_46])).
% 0.07/0.34 cnf(c_276, plain, ~value(in(n1,h2(n1 v a)),A) | value(in(n1,n1 v a),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_86, c_106])).
% 0.07/0.34 cnf(c_195, plain, ~value(in(n1,h2(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_276, c_143])).
% 0.07/0.34 cnf(c_277, plain, ~value(in(n2,h1(n1 v a)),A) | value(in(c,n1 v a),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_90, c_106])).
% 0.07/0.34 cnf(c_197, plain, ~value(in(n2,h1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_277, c_145])).
% 0.07/0.34 cnf(c_278, plain, ~type(or1(n1 v a),or) | ~value(out(n1,or1(n1 v a)),n1) | value(in(n1,or1(n1 v a)),n1) | value(in(n2,or1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_147, c_38])).
% 0.07/0.34 cnf(c_205, plain, ~value(out(n1,or1(n1 v a)),n1) | value(in(n1,or1(n1 v a)),n1) | value(in(n2,or1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_139, c_278])).
% 0.07/0.34 cnf(c_279, plain, mode(and2(h2(n1 v a)),ok) | mode(and2(h2(n1 v a)),abnormal),
% 0.07/0.34 inference(resolve, [status(thm)], [c_168, c_30])).
% 0.07/0.34 cnf(c_213, plain, mode(and2(h2(n1 v a)),ok),
% 0.07/0.34 inference(resolve, [status(thm)], [c_61, c_279])).
% 0.07/0.34 cnf(c_280, plain, ~value(in(n1,and2(h2(n1 v a))),A) | value(in(n1,h2(n1 v a)),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_66, c_140])).
% 0.07/0.34 cnf(c_218, plain, ~value(in(n1,and2(h2(n1 v a))),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_280, c_195])).
% 0.07/0.34 cnf(c_281, plain, ~value(in(n2,and2(h1(n1 v a))),A) | value(in(n2,h1(n1 v a)),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_68, c_141])).
% 0.07/0.34 cnf(c_222, plain, ~value(in(n2,and2(h1(n1 v a))),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_281, c_197])).
% 0.07/0.34 cnf(c_282, plain, mode(and2(h1(n1 v a)),ok) | mode(and2(h1(n1 v a)),abnormal),
% 0.07/0.34 inference(resolve, [status(thm)], [c_191, c_30])).
% 0.07/0.34 cnf(c_227, plain, mode(and2(h1(n1 v a)),ok),
% 0.07/0.34 inference(resolve, [status(thm)], [c_60, c_282])).
% 0.07/0.34 cnf(c_283, plain, ~type(and2(h2(n1 v a)),and) | ~value(out(n1,and2(h2(n1 v a))),n1) | value(in(n1,and2(h2(n1 v a))),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_213, c_34])).
% 0.07/0.34 cnf(c_284, plain, ~value(out(n1,and2(h2(n1 v a))),n1) | value(in(n1,and2(h2(n1 v a))),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_168, c_283])).
% 0.07/0.34 cnf(c_240, plain, ~value(out(n1,and2(h2(n1 v a))),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_218, c_284])).
% 0.07/0.34 cnf(c_285, plain, ~type(and2(h1(n1 v a)),and) | ~value(out(n1,and2(h1(n1 v a))),n1) | value(in(n2,and2(h1(n1 v a))),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_227, c_35])).
% 0.07/0.34 cnf(c_286, plain, ~value(out(n1,and2(h1(n1 v a))),n1) | value(in(n2,and2(h1(n1 v a))),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_191, c_285])).
% 0.07/0.34 cnf(c_253, plain, ~value(out(n1,and2(h1(n1 v a))),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_222, c_286])).
% 0.07/0.34 cnf(c_258, plain, value(out(c,n1 v a),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_116, c_58])).
% 0.07/0.34 cnf(c_287, plain, ~value(out(c,h2(n1 v a)),A) | value(out(n1,and2(h2(n1 v a))),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_73, c_140])).
% 0.07/0.34 cnf(c_261, plain, ~value(out(c,h2(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_287, c_240])).
% 0.07/0.34 cnf(c_288, plain, ~value(in(n1,or1(n1 v a)),A) | value(out(c,h2(n1 v a)),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_84, c_106])).
% 0.07/0.34 cnf(c_262, plain, ~value(in(n1,or1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_288, c_261])).
% 0.07/0.34 cnf(c_264, plain, ~value(out(n1,or1(n1 v a)),n1) | value(in(n2,or1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_262, c_205])).
% 0.07/0.34 cnf(c_289, plain, ~value(out(c,h1(n1 v a)),A) | value(out(n1,and2(h1(n1 v a))),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_73, c_141])).
% 0.07/0.34 cnf(c_267, plain, ~value(out(c,h1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_289, c_253])).
% 0.07/0.34 cnf(c_290, plain, ~value(in(n2,or1(n1 v a)),A) | value(out(c,h1(n1 v a)),A),
% 0.07/0.34 inference(resolve, [status(thm)], [c_82, c_106])).
% 0.07/0.34 cnf(c_268, plain, ~value(in(n2,or1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_290, c_267])).
% 0.07/0.34 cnf(c_269, plain, ~value(out(n1,or1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_268, c_264])).
% 0.07/0.34 cnf(c_291, plain, ~type(n1 v a,fulladder) | value(out(n1,or1(n1 v a)),n1),
% 0.07/0.34 inference(resolve, [status(thm)], [c_95, c_258])).
% 0.07/0.34 cnf(c_292, plain, ~type(n1 v a,fulladder),
% 0.07/0.34 inference(resolve, [status(thm)], [c_291, c_269])).
% 0.07/0.34 cnf(c_272, plain, $false,
% 0.07/0.34 inference(resolve, [status(thm)], [c_106, c_292])).
% 0.07/0.34 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------