%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HWV008-1.002 : TPTP v9.3.1. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n026.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 : Fri Sep 25 01:39:55 PM UTC 2026
% Result : Unsatisfiable 2.88s 1.29s
% Output : CNFRefutation 2.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 36
% Syntax : Number of formulae : 148 ( 59 unt; 6 def)
% Number of atoms : 413 ( 6 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 235 ( 120 ~; 115 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 11 usr; 7 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% Number of variables : 73 ( 0 sgn 73 !; 0 ?; 43 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( value(X1,X2)
| ~ value(X0,X2)
| ~ connection(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',value_propagation1) ).
fof(f2,axiom,
! [X2,X0,X1] :
( value(X0,X2)
| ~ value(X1,X2)
| ~ connection(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',value_propagation2) ).
fof(f3,axiom,
! [X2,X0,X1] :
( equal_value(X1,X2)
| ~ value(X0,X2)
| ~ value(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',unique_value) ).
fof(f4,axiom,
~ equal_value(n0,n1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',equal_value1) ).
fof(f7,axiom,
! [X0,X1] :
( mode(X0,abnormal)
| mode(X0,ok)
| ~ type(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',ok_or_abnormal) ).
fof(f8,axiom,
! [X0,X1] :
( value(out(n1,X0),n0)
| ~ value(in(X1,X0),n0)
| ~ type(X0,and)
| ~ mode(X0,ok) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_0x_0) ).
fof(f11,axiom,
! [X0] :
( value(in(n1,X0),n1)
| ~ value(out(n1,X0),n1)
| ~ type(X0,and)
| ~ mode(X0,ok) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_1_1x) ).
fof(f15,axiom,
! [X0] :
( value(in(n2,X0),n1)
| value(in(n1,X0),n1)
| ~ value(out(n1,X0),n1)
| ~ type(X0,or)
| ~ mode(X0,ok) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',or_1_11) ).
fof(f23,axiom,
! [X0] :
( type(and2(X0),and)
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_and2) ).
fof(f28,axiom,
! [X0] :
( connection(in(n1,X0),in(n1,and2(X0)))
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1and2) ).
fof(f31,axiom,
! [X0] :
( connection(out(c,X0),out(n1,and2(X0)))
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outc_out1and2) ).
fof(f35,axiom,
! [X0] :
( type(h1(X0),halfadder)
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_halfadder1) ).
fof(f36,axiom,
! [X0] :
( type(h2(X0),halfadder)
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_halfadder2) ).
fof(f37,axiom,
! [X0] :
( type(or1(X0),or)
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_or1) ).
fof(f39,axiom,
! [X0] :
( connection(out(c,h1(X0)),in(n2,or1(X0)))
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outch1_in2or1) ).
fof(f40,axiom,
! [X0] :
( connection(out(c,h2(X0)),in(n1,or1(X0)))
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outch2_in1or1) ).
fof(f41,axiom,
! [X0] :
( connection(in(n1,X0),in(n1,h2(X0)))
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_in1_in1h2) ).
fof(f42,axiom,
! [X0] :
( connection(in(n2,X0),in(n1,h1(X0)))
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_in2_in1h1) ).
fof(f45,axiom,
! [X0] :
( connection(out(c,X0),out(n1,or1(X0)))
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outc_out1or1) ).
fof(f47,axiom,
! [X0] :
( type(f(n2,X0),fulladder)
| ~ type(X0,nbit_adder(n2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nbit_adder_fulladder2) ).
fof(f50,axiom,
! [X0] :
( connection(out(c,X0),out(c,f(n2,X0)))
| ~ type(X0,nbit_adder(n2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nbit_adder_connection_outc_outcf1) ).
fof(f53,axiom,
! [X0] :
( connection(in(a2,X0),in(n1,f(n2,X0)))
| ~ type(X0,nbit_adder(n2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nbit_adder_connection_ina2_in1f2) ).
fof(f54,axiom,
! [X0] :
( connection(in(b2,X0),in(n2,f(n2,X0)))
| ~ type(X0,nbit_adder(n2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nbit_adder_connection_inb2_in2f2) ).
fof(f57,axiom,
type(a,nbit_adder(n2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_isa_2bit_adder) ).
fof(f59,axiom,
value(in(a2,a),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ina2_0) ).
fof(f61,axiom,
value(in(b2,a),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inb2_0) ).
fof(f65,axiom,
value(out(c,a),n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outc_1) ).
fof(f66,negated_conjecture,
~ mode(or1(f(n2,a)),abnormal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1f2a) ).
fof(f67,negated_conjecture,
~ mode(and2(h1(f(n2,a))),abnormal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_and2h2f2a) ).
fof(f68,negated_conjecture,
~ mode(and2(h2(f(n2,a))),abnormal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_and2h1f2a) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i] :
( value(X1,X2)
| ~ value(X0,X2)
| ~ connection(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] :
( value(X0,X2)
| ~ value(X1,X2)
| ~ connection(X0,X1) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i] :
( equal_value(X1,X2)
| ~ value(X0,X2)
| ~ value(X0,X1) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_120,plain,
~ equal_value(n0,n1),
inference(cnf_transformation,[],[f4]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i] :
( mode(X0,ok)
| mode(X0,abnormal)
| ~ type(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i] :
( value(out(n1,X1),n0)
| ~ mode(X1,ok)
| ~ type(X1,and)
| ~ value(in(X0,X1),n0) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_127,plain,
! [X0: $i] :
( value(in(n1,X0),n1)
| ~ mode(X0,ok)
| ~ type(X0,and)
| ~ value(out(n1,X0),n1) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_131,plain,
! [X0: $i] :
( value(in(n1,X0),n1)
| value(in(n2,X0),n1)
| ~ mode(X0,ok)
| ~ type(X0,or)
| ~ value(out(n1,X0),n1) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_139,plain,
! [X0: $i] :
( type(and2(X0),and)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_144,plain,
! [X0: $i] :
( connection(in(n1,X0),in(n1,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_147,plain,
! [X0: $i] :
( connection(out(c,X0),out(n1,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_151,plain,
! [X0: $i] :
( type(h1(X0),halfadder)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_152,plain,
! [X0: $i] :
( type(h2(X0),halfadder)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_153,plain,
! [X0: $i] :
( type(or1(X0),or)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_155,plain,
! [X0: $i] :
( connection(out(c,h1(X0)),in(n2,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_156,plain,
! [X0: $i] :
( connection(out(c,h2(X0)),in(n1,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_157,plain,
! [X0: $i] :
( connection(in(n1,X0),in(n1,h2(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_158,plain,
! [X0: $i] :
( connection(in(n2,X0),in(n1,h1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_161,plain,
! [X0: $i] :
( connection(out(c,X0),out(n1,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_163,plain,
! [X0: $i] :
( type(f(n2,X0),fulladder)
| ~ type(X0,nbit_adder(n2)) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_166,plain,
! [X0: $i] :
( connection(out(c,X0),out(c,f(n2,X0)))
| ~ type(X0,nbit_adder(n2)) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_169,plain,
! [X0: $i] :
( connection(in(a2,X0),in(n1,f(n2,X0)))
| ~ type(X0,nbit_adder(n2)) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_170,plain,
! [X0: $i] :
( connection(in(b2,X0),in(n2,f(n2,X0)))
| ~ type(X0,nbit_adder(n2)) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_173,plain,
type(a,nbit_adder(n2)),
inference(cnf_transformation,[],[f57]) ).
tcf(c_175,plain,
value(in(a2,a),n0),
inference(cnf_transformation,[],[f59]) ).
tcf(c_177,plain,
value(in(b2,a),n0),
inference(cnf_transformation,[],[f61]) ).
tcf(c_181,plain,
value(out(c,a),n1),
inference(cnf_transformation,[],[f65]) ).
tcf(c_182,negated_conjecture,
~ mode(or1(f(n2,a)),abnormal),
inference(cnf_transformation,[],[f66]) ).
tcf(c_183,negated_conjecture,
~ mode(and2(h1(f(n2,a))),abnormal),
inference(cnf_transformation,[],[f67]) ).
tcf(c_184,negated_conjecture,
~ mode(and2(h2(f(n2,a))),abnormal),
inference(cnf_transformation,[],[f68]) ).
tcf(c_553,plain,
! [X0: $i] :
( ~ value(X0,n0)
| ~ value(X0,n1) ),
inference(resolution,[status(thm)],[c_119,c_120]) ).
tcf(c_2278,definition,
iPr_def_10 = f(n2,a),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_2279,definition,
iPr_def_11 = h2(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_2280,definition,
iPr_def_12 = and2(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_2281,definition,
iPr_def_13 = h1(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_2282,definition,
iPr_def_14 = and2(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_2283,definition,
iPr_def_15 = or1(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_2284,negated_conjecture,
~ mode(iPr_def_12,abnormal),
inference(demodulation,[status(thm)],[c_184,c_2278,c_2279,c_2280]) ).
tcf(c_2285,negated_conjecture,
~ mode(iPr_def_14,abnormal),
inference(demodulation,[status(thm)],[c_183,c_2281,c_2282]) ).
tcf(c_2286,negated_conjecture,
~ mode(iPr_def_15,abnormal),
inference(demodulation,[status(thm)],[c_182,c_2283]) ).
tcf(c_3124,plain,
( type(iPr_def_12,and)
| ~ type(iPr_def_11,halfadder) ),
inference(superposition,[status(thm)],[c_2280,c_139]) ).
tcf(c_3125,plain,
( type(iPr_def_14,and)
| ~ type(iPr_def_13,halfadder) ),
inference(superposition,[status(thm)],[c_2282,c_139]) ).
tcf(c_3182,plain,
( type(iPr_def_13,halfadder)
| ~ type(iPr_def_10,fulladder) ),
inference(superposition,[status(thm)],[c_2281,c_151]) ).
tcf(c_3194,plain,
( type(iPr_def_11,halfadder)
| ~ type(iPr_def_10,fulladder) ),
inference(superposition,[status(thm)],[c_2279,c_152]) ).
tcf(c_3206,plain,
( type(iPr_def_15,or)
| ~ type(iPr_def_10,fulladder) ),
inference(superposition,[status(thm)],[c_2283,c_153]) ).
tcf(c_3251,plain,
~ value(in(b2,a),n1),
inference(superposition,[status(thm)],[c_177,c_553]) ).
tcf(c_3272,plain,
( type(iPr_def_10,fulladder)
| ~ type(a,nbit_adder(n2)) ),
inference(superposition,[status(thm)],[c_2278,c_163]) ).
tcf(c_3274,plain,
type(iPr_def_10,fulladder),
inference(forward_subsumption_resolution,[status(thm)],[c_3272,c_173]) ).
tcf(c_3278,plain,
type(iPr_def_15,or),
inference(backward_subsumption_resolution,[status(thm)],[c_3206,c_3274]) ).
tcf(c_3279,plain,
type(iPr_def_11,halfadder),
inference(backward_subsumption_resolution,[status(thm)],[c_3194,c_3274]) ).
tcf(c_3280,plain,
type(iPr_def_13,halfadder),
inference(backward_subsumption_resolution,[status(thm)],[c_3182,c_3274]) ).
tcf(c_3281,plain,
type(iPr_def_12,and),
inference(backward_subsumption_resolution,[status(thm)],[c_3124,c_3279]) ).
tcf(c_3282,plain,
type(iPr_def_14,and),
inference(backward_subsumption_resolution,[status(thm)],[c_3125,c_3280]) ).
tcf(c_3314,plain,
( mode(iPr_def_15,ok)
| mode(iPr_def_15,abnormal) ),
inference(superposition,[status(thm)],[c_3278,c_123]) ).
tcf(c_3315,plain,
mode(iPr_def_15,ok),
inference(forward_subsumption_resolution,[status(thm)],[c_3314,c_2286]) ).
tcf(c_3322,plain,
( mode(iPr_def_12,ok)
| mode(iPr_def_12,abnormal) ),
inference(superposition,[status(thm)],[c_3281,c_123]) ).
tcf(c_3323,plain,
mode(iPr_def_12,ok),
inference(forward_subsumption_resolution,[status(thm)],[c_3322,c_2284]) ).
tcf(c_3324,plain,
( mode(iPr_def_14,ok)
| mode(iPr_def_14,abnormal) ),
inference(superposition,[status(thm)],[c_3282,c_123]) ).
tcf(c_3325,plain,
mode(iPr_def_14,ok),
inference(forward_subsumption_resolution,[status(thm)],[c_3324,c_2285]) ).
tcf(c_3360,plain,
( connection(in(n1,iPr_def_11),in(n1,iPr_def_12))
| ~ type(iPr_def_11,halfadder) ),
inference(superposition,[status(thm)],[c_2280,c_144]) ).
tcf(c_3361,plain,
( connection(in(n1,iPr_def_13),in(n1,iPr_def_14))
| ~ type(iPr_def_13,halfadder) ),
inference(superposition,[status(thm)],[c_2282,c_144]) ).
tcf(c_3364,plain,
connection(in(n1,iPr_def_13),in(n1,iPr_def_14)),
inference(forward_subsumption_resolution,[status(thm)],[c_3361,c_3280]) ).
tcf(c_3365,plain,
connection(in(n1,iPr_def_11),in(n1,iPr_def_12)),
inference(forward_subsumption_resolution,[status(thm)],[c_3360,c_3279]) ).
tcf(c_3400,plain,
! [X0: $i] :
( value(in(n1,iPr_def_13),X0)
| ~ value(in(n1,iPr_def_14),X0) ),
inference(superposition,[status(thm)],[c_3364,c_118]) ).
tcf(c_3407,plain,
( value(in(n1,iPr_def_13),n1)
| ~ value(in(n1,iPr_def_14),n1) ),
inference(instantiation,[status(thm)],[c_3400]) ).
tcf(c_3409,plain,
! [X0: $i] :
( value(in(n1,iPr_def_12),X0)
| ~ value(in(n1,iPr_def_11),X0) ),
inference(superposition,[status(thm)],[c_3365,c_117]) ).
tcf(c_3498,plain,
( connection(out(c,iPr_def_11),out(n1,iPr_def_12))
| ~ type(iPr_def_11,halfadder) ),
inference(superposition,[status(thm)],[c_2280,c_147]) ).
tcf(c_3499,plain,
( connection(out(c,iPr_def_13),out(n1,iPr_def_14))
| ~ type(iPr_def_13,halfadder) ),
inference(superposition,[status(thm)],[c_2282,c_147]) ).
tcf(c_3502,plain,
connection(out(c,iPr_def_13),out(n1,iPr_def_14)),
inference(forward_subsumption_resolution,[status(thm)],[c_3499,c_3280]) ).
tcf(c_3503,plain,
connection(out(c,iPr_def_11),out(n1,iPr_def_12)),
inference(forward_subsumption_resolution,[status(thm)],[c_3498,c_3279]) ).
tcf(c_3514,plain,
( connection(in(n1,iPr_def_10),in(n1,iPr_def_11))
| ~ type(iPr_def_10,fulladder) ),
inference(superposition,[status(thm)],[c_2279,c_157]) ).
tcf(c_3517,plain,
connection(in(n1,iPr_def_10),in(n1,iPr_def_11)),
inference(forward_subsumption_resolution,[status(thm)],[c_3514,c_3274]) ).
tcf(c_3528,plain,
( connection(in(n2,iPr_def_10),in(n1,iPr_def_13))
| ~ type(iPr_def_10,fulladder) ),
inference(superposition,[status(thm)],[c_2281,c_158]) ).
tcf(c_3531,plain,
connection(in(n2,iPr_def_10),in(n1,iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_3528,c_3274]) ).
tcf(c_3553,plain,
! [X0: $i] :
( value(out(n1,iPr_def_14),X0)
| ~ value(out(c,iPr_def_13),X0) ),
inference(superposition,[status(thm)],[c_3502,c_117]) ).
tcf(c_3561,plain,
! [X0: $i] :
( value(out(n1,iPr_def_12),X0)
| ~ value(out(c,iPr_def_11),X0) ),
inference(superposition,[status(thm)],[c_3503,c_117]) ).
tcf(c_3566,plain,
( value(out(n1,iPr_def_12),n1)
| ~ value(out(c,iPr_def_11),n1) ),
inference(instantiation,[status(thm)],[c_3561]) ).
tcf(c_3569,plain,
! [X0: $i] :
( value(in(n1,iPr_def_11),X0)
| ~ value(in(n1,iPr_def_10),X0) ),
inference(superposition,[status(thm)],[c_3517,c_117]) ).
tcf(c_3577,plain,
! [X0: $i] :
( value(in(n2,iPr_def_10),X0)
| ~ value(in(n1,iPr_def_13),X0) ),
inference(superposition,[status(thm)],[c_3531,c_118]) ).
tcf(c_3584,plain,
( value(in(n2,iPr_def_10),n1)
| ~ value(in(n1,iPr_def_13),n1) ),
inference(instantiation,[status(thm)],[c_3577]) ).
tcf(c_3659,plain,
( connection(out(c,iPr_def_10),out(n1,iPr_def_15))
| ~ type(iPr_def_10,fulladder) ),
inference(superposition,[status(thm)],[c_2283,c_161]) ).
tcf(c_3662,plain,
connection(out(c,iPr_def_10),out(n1,iPr_def_15)),
inference(forward_subsumption_resolution,[status(thm)],[c_3659,c_3274]) ).
tcf(c_3733,plain,
! [X0: $i] :
( value(out(n1,iPr_def_15),X0)
| ~ value(out(c,iPr_def_10),X0) ),
inference(superposition,[status(thm)],[c_3662,c_117]) ).
tcf(c_3832,plain,
( connection(out(c,h1(iPr_def_10)),in(n2,iPr_def_15))
| ~ type(iPr_def_10,fulladder) ),
inference(superposition,[status(thm)],[c_2283,c_155]) ).
tcf(c_3835,plain,
( connection(out(c,iPr_def_13),in(n2,iPr_def_15))
| ~ type(iPr_def_10,fulladder) ),
inference(light_normalisation,[status(thm)],[c_3832,c_2281]) ).
tcf(c_3836,plain,
connection(out(c,iPr_def_13),in(n2,iPr_def_15)),
inference(forward_subsumption_resolution,[status(thm)],[c_3835,c_3274]) ).
tcf(c_3864,plain,
( connection(out(c,h2(iPr_def_10)),in(n1,iPr_def_15))
| ~ type(iPr_def_10,fulladder) ),
inference(superposition,[status(thm)],[c_2283,c_156]) ).
tcf(c_3867,plain,
( connection(out(c,iPr_def_11),in(n1,iPr_def_15))
| ~ type(iPr_def_10,fulladder) ),
inference(light_normalisation,[status(thm)],[c_3864,c_2279]) ).
tcf(c_3868,plain,
connection(out(c,iPr_def_11),in(n1,iPr_def_15)),
inference(forward_subsumption_resolution,[status(thm)],[c_3867,c_3274]) ).
tcf(c_3885,plain,
! [X0: $i] :
( value(out(c,iPr_def_13),X0)
| ~ value(in(n2,iPr_def_15),X0) ),
inference(superposition,[status(thm)],[c_3836,c_118]) ).
tcf(c_3893,plain,
! [X0: $i] :
( value(out(c,iPr_def_11),X0)
| ~ value(in(n1,iPr_def_15),X0) ),
inference(superposition,[status(thm)],[c_3868,c_118]) ).
tcf(c_3900,plain,
( value(out(c,iPr_def_11),n1)
| ~ value(in(n1,iPr_def_15),n1) ),
inference(instantiation,[status(thm)],[c_3893]) ).
tcf(c_3983,plain,
( connection(out(c,a),out(c,iPr_def_10))
| ~ type(a,nbit_adder(n2)) ),
inference(superposition,[status(thm)],[c_2278,c_166]) ).
tcf(c_3986,plain,
connection(out(c,a),out(c,iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_3983,c_173]) ).
tcf(c_4027,plain,
! [X0: $i] :
( value(out(c,iPr_def_10),X0)
| ~ value(out(c,a),X0) ),
inference(superposition,[status(thm)],[c_3986,c_117]) ).
tcf(c_4057,plain,
value(out(c,iPr_def_10),n1),
inference(superposition,[status(thm)],[c_181,c_4027]) ).
tcf(c_4059,plain,
value(out(n1,iPr_def_15),n1),
inference(superposition,[status(thm)],[c_4057,c_3733]) ).
tcf(c_4110,plain,
( connection(in(a2,a),in(n1,iPr_def_10))
| ~ type(a,nbit_adder(n2)) ),
inference(superposition,[status(thm)],[c_2278,c_169]) ).
tcf(c_4113,plain,
connection(in(a2,a),in(n1,iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_4110,c_173]) ).
tcf(c_4124,plain,
( connection(in(b2,a),in(n2,iPr_def_10))
| ~ type(a,nbit_adder(n2)) ),
inference(superposition,[status(thm)],[c_2278,c_170]) ).
tcf(c_4127,plain,
connection(in(b2,a),in(n2,iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_4124,c_173]) ).
tcf(c_4157,plain,
! [X0: $i] :
( value(in(n1,iPr_def_10),X0)
| ~ value(in(a2,a),X0) ),
inference(superposition,[status(thm)],[c_4113,c_117]) ).
tcf(c_4163,plain,
! [X0: $i] :
( value(in(b2,a),X0)
| ~ value(in(n2,iPr_def_10),X0) ),
inference(superposition,[status(thm)],[c_4127,c_118]) ).
tcf(c_4169,plain,
( value(in(b2,a),n1)
| ~ value(in(n2,iPr_def_10),n1) ),
inference(instantiation,[status(thm)],[c_4163]) ).
tcf(c_4219,plain,
value(in(n1,iPr_def_10),n0),
inference(superposition,[status(thm)],[c_175,c_4157]) ).
tcf(c_4223,plain,
value(in(n1,iPr_def_11),n0),
inference(superposition,[status(thm)],[c_4219,c_3569]) ).
tcf(c_4227,plain,
value(in(n1,iPr_def_12),n0),
inference(superposition,[status(thm)],[c_4223,c_3409]) ).
tcf(c_4305,plain,
( value(out(n1,iPr_def_12),n0)
| ~ mode(iPr_def_12,ok)
| ~ type(iPr_def_12,and) ),
inference(superposition,[status(thm)],[c_4227,c_124]) ).
tcf(c_4312,plain,
value(out(n1,iPr_def_12),n0),
inference(forward_subsumption_resolution,[status(thm)],[c_4305,c_3323,c_3281]) ).
tcf(c_4321,plain,
~ value(out(n1,iPr_def_12),n1),
inference(superposition,[status(thm)],[c_4312,c_553]) ).
tcf(c_4409,plain,
( value(in(n1,iPr_def_15),n1)
| value(in(n2,iPr_def_15),n1)
| ~ mode(iPr_def_15,ok)
| ~ type(iPr_def_15,or) ),
inference(superposition,[status(thm)],[c_4059,c_131]) ).
tcf(c_4410,plain,
( value(in(n1,iPr_def_15),n1)
| value(in(n2,iPr_def_15),n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4409,c_3315,c_3278]) ).
tcf(c_4457,plain,
value(in(n2,iPr_def_15),n1),
inference(global_subsumption_just,[status(thm)],[c_4410,c_3566,c_3900,c_4321,c_4410]) ).
tcf(c_4461,plain,
value(out(c,iPr_def_13),n1),
inference(superposition,[status(thm)],[c_4457,c_3885]) ).
tcf(c_4463,plain,
value(out(n1,iPr_def_14),n1),
inference(superposition,[status(thm)],[c_4461,c_3553]) ).
tcf(c_4467,plain,
( value(in(n1,iPr_def_14),n1)
| ~ mode(iPr_def_14,ok)
| ~ type(iPr_def_14,and) ),
inference(superposition,[status(thm)],[c_4463,c_127]) ).
tcf(c_4469,plain,
value(in(n1,iPr_def_14),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_4467,c_3325,c_3282]) ).
tcf(c_4474,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_4469,c_4169,c_3584,c_3407,c_3251]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV008-1.002 : TPTP v9.3.1. Bugfixed v2.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 16:23:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 2.88/1.29 % SZS status Started for theBenchmark.p
% 2.88/1.29 % SZS status Unsatisfiable for theBenchmark.p
% 2.88/1.29
% 2.88/1.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.88/1.29
% 2.88/1.29 % ------ iProver source info
% 2.88/1.29
% 2.88/1.29 % git: date: 2026-07-19 20:42:38 +0200
% 2.88/1.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.88/1.29 % git: non_committed_changes: false
% 2.88/1.29
% 2.88/1.29 % ------ Parsing...% successful
% 2.88/1.29
% 2.88/1.29
% 2.88/1.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.88/1.29
% 2.88/1.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.88/1.29
% 2.88/1.29 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.88/1.29
% 2.88/1.29 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.88/1.29 % ------ Proving...
% 2.88/1.29 % ------ Problem Properties
% 2.88/1.29
% 2.88/1.29 %
% 2.88/1.29 % clauses 72
% 2.88/1.29 % conjectures 3
% 2.88/1.29 % EPR 8
% 2.88/1.29 % Horn 69
% 2.88/1.29 % unary 18
% 2.88/1.29 % binary 37
% 2.88/1.29 % lits 161
% 2.88/1.29 % lits eq 6
% 2.88/1.29 % fd_pure 0
% 2.88/1.29 % fd_pseudo 0
% 2.88/1.29 % fd_cond 0
% 2.88/1.29 % fd_pseudo_cond 0
% 2.88/1.29 % AC symbols 0
% 2.88/1.29
% 2.88/1.29 % ------ Schedule dynamic 5 is on
% 2.88/1.29
% 2.88/1.29 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.88/1.29
% 2.88/1.29
% 2.88/1.29 % ------
% 2.88/1.29 % Current options:
% 2.88/1.29 % ------
% 2.88/1.29
% 2.88/1.29
% 2.88/1.29 %
% 2.88/1.29
% 2.88/1.29 % ------ Proving...
% 2.88/1.29 %
% 2.88/1.29
% 2.88/1.29 % SZS status Unsatisfiable for theBenchmark.p
% 2.88/1.29
% 2.88/1.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.88/1.29
% 2.88/1.29
%------------------------------------------------------------------------------