%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HWV006-1 : TPTP v9.3.1. Released v2.1.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:54 PM UTC 2026
% Result : Unsatisfiable 4.57s 1.53s
% Output : CNFRefutation 4.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 46
% Syntax : Number of formulae : 257 ( 25 unt; 0 def)
% Number of atoms : 639 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 770 ( 388 ~; 382 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 9 usr; 5 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% Number of variables : 210 ( 0 sgn 210 !; 0 ?; 169 :)
% 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(f9,axiom,
! [X0] :
( value(out(n1,X0),n1)
| ~ value(in(n2,X0),n1)
| ~ value(in(n1,X0),n1)
| ~ type(X0,and)
| ~ mode(X0,ok) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_11_1) ).
fof(f12,axiom,
! [X0] :
( value(in(n2,X0),n1)
| ~ value(out(n1,X0),n1)
| ~ type(X0,and)
| ~ mode(X0,ok) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_1_x1) ).
fof(f13,axiom,
! [X0,X1] :
( value(out(n1,X0),n1)
| ~ value(in(X1,X0),n1)
| ~ type(X0,or)
| ~ mode(X0,ok) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',or_1x_1) ).
fof(f18,axiom,
! [X0] :
( value(out(n1,X0),n1)
| ~ value(in(n1,X0),n0)
| ~ type(X0,not)
| ~ mode(X0,ok) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',not_0_1_fw) ).
fof(f21,axiom,
! [X0] :
( value(in(n1,X0),n0)
| ~ value(out(n1,X0),n1)
| ~ type(X0,not)
| ~ mode(X0,ok) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',not_1_0_bw) ).
fof(f22,axiom,
! [X0] :
( type(and1(X0),and)
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_and1) ).
fof(f23,axiom,
! [X0] :
( type(and2(X0),and)
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_and2) ).
fof(f24,axiom,
! [X0] :
( type(not1(X0),not)
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_not1) ).
fof(f25,axiom,
! [X0] :
( type(or1(X0),or)
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_or1) ).
fof(f27,axiom,
! [X0] :
( connection(in(n2,X0),in(n2,or1(X0)))
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in2_in2or1) ).
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(f29,axiom,
! [X0] :
( connection(in(n2,X0),in(n2,and2(X0)))
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in2_in2and2) ).
fof(f30,axiom,
! [X0] :
( connection(out(s,X0),out(n1,and1(X0)))
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outs_out1and1) ).
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(f32,axiom,
! [X0] :
( connection(out(n1,or1(X0)),in(n1,and1(X0)))
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1or1_in1_and1) ).
fof(f33,axiom,
! [X0] :
( connection(out(n1,and2(X0)),in(n1,not1(X0)))
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1and2_in1not1) ).
fof(f34,axiom,
! [X0] :
( connection(out(n1,not1(X0)),in(n2,and1(X0)))
| ~ type(X0,halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1not1_in2and1) ).
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(f38,axiom,
! [X0] :
( connection(out(s,h1(X0)),in(n2,h2(X0)))
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outsh1_in2h2) ).
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(f43,axiom,
! [X0] :
( connection(in(c,X0),in(n2,h1(X0)))
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_inc_in2h1) ).
fof(f44,axiom,
! [X0] :
( connection(out(s,X0),out(s,h2(X0)))
| ~ type(X0,fulladder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outs_outsh2) ).
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(f46,axiom,
type(f,fulladder),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_isa_fulladder) ).
fof(f47,axiom,
value(in(n1,f),n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',in1_1) ).
fof(f48,axiom,
value(in(n2,f),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',in2_0) ).
fof(f49,axiom,
value(in(c,f),n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inc_1) ).
fof(f50,axiom,
value(out(s,f),n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outs_1) ).
fof(f51,axiom,
value(out(c,f),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outc_0) ).
fof(f52,negated_conjecture,
( ~ mode(not1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1_not1h2) ).
fof(f53,negated_conjecture,
~ mode(and2(h2(f)),abnormal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_and2) ).
fof(f54,negated_conjecture,
( ~ mode(and1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1_and1h2) ).
fof(f55,negated_conjecture,
~ mode(or1(h1(f)),abnormal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_or1h1) ).
fof(f56,negated_conjecture,
~ mode(not1(h1(f)),abnormal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_not1h1) ).
fof(f57,negated_conjecture,
~ mode(and2(h1(f)),abnormal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_and2h1) ).
fof(f58,negated_conjecture,
~ mode(and1(h1(f)),abnormal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diagnosis_and1h1) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] :
( value(X2,X1)
| ~ connection(X0,X2)
| ~ value(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i] :
( value(X2,X1)
| ~ connection(X2,X0)
| ~ value(X0,X1) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] :
( equal_value(X1,X2)
| ~ value(X0,X2)
| ~ value(X0,X1) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_110,plain,
~ equal_value(n0,n1),
inference(cnf_transformation,[],[f4]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i] :
( mode(X0,ok)
| mode(X0,abnormal)
| ~ type(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_114,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_115,plain,
! [X0: $i] :
( value(out(n1,X0),n1)
| ~ mode(X0,ok)
| ~ type(X0,and)
| ~ value(in(n2,X0),n1)
| ~ value(in(n1,X0),n1) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_118,plain,
! [X0: $i] :
( value(in(n2,X0),n1)
| ~ mode(X0,ok)
| ~ type(X0,and)
| ~ value(out(n1,X0),n1) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] :
( value(out(n1,X1),n1)
| ~ mode(X1,ok)
| ~ type(X1,or)
| ~ value(in(X0,X1),n1) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_124,plain,
! [X0: $i] :
( value(out(n1,X0),n1)
| ~ mode(X0,ok)
| ~ type(X0,not)
| ~ value(in(n1,X0),n0) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_127,plain,
! [X0: $i] :
( value(in(n1,X0),n0)
| ~ mode(X0,ok)
| ~ type(X0,not)
| ~ value(out(n1,X0),n1) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_128,plain,
! [X0: $i] :
( type(and1(X0),and)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_129,plain,
! [X0: $i] :
( type(and2(X0),and)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_130,plain,
! [X0: $i] :
( type(not1(X0),not)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_131,plain,
! [X0: $i] :
( type(or1(X0),or)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_133,plain,
! [X0: $i] :
( connection(in(n2,X0),in(n2,or1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_134,plain,
! [X0: $i] :
( connection(in(n1,X0),in(n1,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_135,plain,
! [X0: $i] :
( connection(in(n2,X0),in(n2,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_136,plain,
! [X0: $i] :
( connection(out(s,X0),out(n1,and1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_137,plain,
! [X0: $i] :
( connection(out(c,X0),out(n1,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_138,plain,
! [X0: $i] :
( connection(out(n1,or1(X0)),in(n1,and1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_139,plain,
! [X0: $i] :
( connection(out(n1,and2(X0)),in(n1,not1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_140,plain,
! [X0: $i] :
( connection(out(n1,not1(X0)),in(n2,and1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_141,plain,
! [X0: $i] :
( type(h1(X0),halfadder)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_142,plain,
! [X0: $i] :
( type(h2(X0),halfadder)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_143,plain,
! [X0: $i] :
( type(or1(X0),or)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_144,plain,
! [X0: $i] :
( connection(out(s,h1(X0)),in(n2,h2(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_146,plain,
! [X0: $i] :
( connection(out(c,h2(X0)),in(n1,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_147,plain,
! [X0: $i] :
( connection(in(n1,X0),in(n1,h2(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_148,plain,
! [X0: $i] :
( connection(in(n2,X0),in(n1,h1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_149,plain,
! [X0: $i] :
( connection(in(c,X0),in(n2,h1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_150,plain,
! [X0: $i] :
( connection(out(s,X0),out(s,h2(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_151,plain,
! [X0: $i] :
( connection(out(c,X0),out(n1,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_152,plain,
type(f,fulladder),
inference(cnf_transformation,[],[f46]) ).
tcf(c_153,plain,
value(in(n1,f),n1),
inference(cnf_transformation,[],[f47]) ).
tcf(c_154,plain,
value(in(n2,f),n0),
inference(cnf_transformation,[],[f48]) ).
tcf(c_155,plain,
value(in(c,f),n1),
inference(cnf_transformation,[],[f49]) ).
tcf(c_156,plain,
value(out(s,f),n1),
inference(cnf_transformation,[],[f50]) ).
tcf(c_157,plain,
value(out(c,f),n0),
inference(cnf_transformation,[],[f51]) ).
tcf(c_158,negated_conjecture,
( ~ mode(or1(f),abnormal)
| ~ mode(not1(h2(f)),abnormal) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_159,negated_conjecture,
~ mode(and2(h2(f)),abnormal),
inference(cnf_transformation,[],[f53]) ).
tcf(c_160,negated_conjecture,
( ~ mode(or1(f),abnormal)
| ~ mode(and1(h2(f)),abnormal) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_161,negated_conjecture,
~ mode(or1(h1(f)),abnormal),
inference(cnf_transformation,[],[f55]) ).
tcf(c_162,negated_conjecture,
~ mode(not1(h1(f)),abnormal),
inference(cnf_transformation,[],[f56]) ).
tcf(c_163,negated_conjecture,
~ mode(and2(h1(f)),abnormal),
inference(cnf_transformation,[],[f57]) ).
tcf(c_164,negated_conjecture,
~ mode(and1(h1(f)),abnormal),
inference(cnf_transformation,[],[f58]) ).
tcf(c_484,plain,
! [X0: $i] :
( ~ value(X0,n0)
| ~ value(X0,n1) ),
inference(resolution,[status(thm)],[c_109,c_110]) ).
tcf(c_1685,plain,
! [X0_iProver_value_1: iProver_value_1] :
( ~ value(X0_iProver_value_1,n0)
| ~ value(X0_iProver_value_1,n1) ),
inference(subtyping,[status(esa)],[c_484]) ).
tcf(c_1686,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n1,X0_iProver_type_1),n0)
| ~ mode(X0_iProver_type_1,ok)
| ~ type(X0_iProver_type_1,not)
| ~ value(out(n1,X0_iProver_type_1),n1) ),
inference(subtyping,[status(esa)],[c_127]) ).
tcf(c_1689,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(out(n1,X0_iProver_type_1),n1)
| ~ mode(X0_iProver_type_1,ok)
| ~ type(X0_iProver_type_1,not)
| ~ value(in(n1,X0_iProver_type_1),n0) ),
inference(subtyping,[status(esa)],[c_124]) ).
tcf(c_1694,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(n1,X0_iProver_type_1),n1)
| ~ mode(X0_iProver_type_1,ok)
| ~ type(X0_iProver_type_1,or)
| ~ value(in(X0_iProver_value_2,X0_iProver_type_1),n1) ),
inference(subtyping,[status(esa)],[c_119]) ).
tcf(c_1695,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n2,X0_iProver_type_1),n1)
| ~ mode(X0_iProver_type_1,ok)
| ~ type(X0_iProver_type_1,and)
| ~ value(out(n1,X0_iProver_type_1),n1) ),
inference(subtyping,[status(esa)],[c_118]) ).
tcf(c_1698,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(out(n1,X0_iProver_type_1),n1)
| ~ mode(X0_iProver_type_1,ok)
| ~ type(X0_iProver_type_1,and)
| ~ value(in(n2,X0_iProver_type_1),n1)
| ~ value(in(n1,X0_iProver_type_1),n1) ),
inference(subtyping,[status(esa)],[c_115]) ).
tcf(c_1699,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(n1,X0_iProver_type_1),n0)
| ~ mode(X0_iProver_type_1,ok)
| ~ type(X0_iProver_type_1,and)
| ~ value(in(X0_iProver_value_2,X0_iProver_type_1),n0) ),
inference(subtyping,[status(esa)],[c_114]) ).
tcf(c_1700,plain,
! [X0_iProver_type_1: iProver_type_1,X0_iProver_type_2: iProver_type_2] :
( mode(X0_iProver_type_1,ok)
| mode(X0_iProver_type_1,abnormal)
| ~ type(X0_iProver_type_1,X0_iProver_type_2) ),
inference(subtyping,[status(esa)],[c_113]) ).
tcf(c_1702,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_value_2: iProver_value_2,X1_iProver_value_1: iProver_value_1] :
( value(X1_iProver_value_1,X0_iProver_value_2)
| ~ connection(X1_iProver_value_1,X0_iProver_value_1)
| ~ value(X0_iProver_value_1,X0_iProver_value_2) ),
inference(subtyping,[status(esa)],[c_108]) ).
tcf(c_1703,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_value_2: iProver_value_2,X1_iProver_value_1: iProver_value_1] :
( value(X1_iProver_value_1,X0_iProver_value_2)
| ~ connection(X0_iProver_value_1,X1_iProver_value_1)
| ~ value(X0_iProver_value_1,X0_iProver_value_2) ),
inference(subtyping,[status(esa)],[c_107]) ).
tcf(c_1704,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(n1,not1(X0_iProver_type_1)),in(n2,and1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_140]) ).
tcf(c_1705,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(n1,and2(X0_iProver_type_1)),in(n1,not1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_139]) ).
tcf(c_1706,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(n1,or1(X0_iProver_type_1)),in(n1,and1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_138]) ).
tcf(c_1707,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(c,X0_iProver_type_1),out(n1,and2(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_137]) ).
tcf(c_1708,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(s,X0_iProver_type_1),out(n1,and1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_136]) ).
tcf(c_1709,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n2,X0_iProver_type_1),in(n2,and2(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_135]) ).
tcf(c_1710,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n1,X0_iProver_type_1),in(n1,and2(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_134]) ).
tcf(c_1711,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n2,X0_iProver_type_1),in(n2,or1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_133]) ).
tcf(c_1713,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(or1(X0_iProver_type_1),or)
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_131]) ).
tcf(c_1714,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(not1(X0_iProver_type_1),not)
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_130]) ).
tcf(c_1715,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(and2(X0_iProver_type_1),and)
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_129]) ).
tcf(c_1716,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(and1(X0_iProver_type_1),and)
| ~ type(X0_iProver_type_1,halfadder) ),
inference(subtyping,[status(esa)],[c_128]) ).
tcf(c_1717,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(c,X0_iProver_type_1),out(n1,or1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_151]) ).
tcf(c_1718,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(s,X0_iProver_type_1),out(s,h2(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_150]) ).
tcf(c_1719,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(c,X0_iProver_type_1),in(n2,h1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_149]) ).
tcf(c_1720,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n2,X0_iProver_type_1),in(n1,h1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_148]) ).
tcf(c_1721,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n1,X0_iProver_type_1),in(n1,h2(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_147]) ).
tcf(c_1722,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(c,h2(X0_iProver_type_1)),in(n1,or1(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_146]) ).
tcf(c_1724,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(s,h1(X0_iProver_type_1)),in(n2,h2(X0_iProver_type_1)))
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_144]) ).
tcf(c_1725,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(or1(X0_iProver_type_1),or)
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_143]) ).
tcf(c_1726,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(h2(X0_iProver_type_1),halfadder)
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_142]) ).
tcf(c_1727,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(h1(X0_iProver_type_1),halfadder)
| ~ type(X0_iProver_type_1,fulladder) ),
inference(subtyping,[status(esa)],[c_141]) ).
tcf(c_1732,negated_conjecture,
( ~ mode(or1(f),abnormal)
| ~ mode(and1(h2(f)),abnormal) ),
inference(subtyping,[status(esa)],[c_160]) ).
tcf(c_1734,negated_conjecture,
( ~ mode(or1(f),abnormal)
| ~ mode(not1(h2(f)),abnormal) ),
inference(subtyping,[status(esa)],[c_158]) ).
tcf(c_1747,plain,
( type(or1(f),or)
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1725]) ).
tcf(c_1748,plain,
( type(h2(f),halfadder)
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1726]) ).
tcf(c_1749,plain,
( type(h1(f),halfadder)
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1727]) ).
tcf(c_1757,plain,
( connection(out(c,f),out(n1,or1(f)))
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1717]) ).
tcf(c_1758,plain,
( connection(out(s,f),out(s,h2(f)))
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1718]) ).
tcf(c_1759,plain,
( connection(in(c,f),in(n2,h1(f)))
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1719]) ).
tcf(c_1760,plain,
( connection(in(n2,f),in(n1,h1(f)))
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1720]) ).
tcf(c_1761,plain,
( connection(in(n1,f),in(n1,h2(f)))
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1721]) ).
tcf(c_1767,plain,
( connection(out(s,h1(f)),in(n2,h2(f)))
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_1724]) ).
tcf(c_1777,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(n1,or1(X0_iProver_type_1)),n1)
| ~ mode(or1(X0_iProver_type_1),ok)
| ~ type(or1(X0_iProver_type_1),or)
| ~ value(in(X0_iProver_value_2,or1(X0_iProver_type_1)),n1) ),
inference(instantiation,[status(thm)],[c_1694]) ).
tcf(c_1782,plain,
( value(out(n1,or1(f)),n1)
| ~ mode(or1(f),ok)
| ~ type(or1(f),or)
| ~ value(in(n1,or1(f)),n1) ),
inference(instantiation,[status(thm)],[c_1777]) ).
tcf(c_1783,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(and1(h2(X0_iProver_type_1)),and)
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1716]) ).
tcf(c_1784,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(and2(h2(X0_iProver_type_1)),and)
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1715]) ).
tcf(c_1785,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(not1(h2(X0_iProver_type_1)),not)
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1714]) ).
tcf(c_1789,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n1,h2(X0_iProver_type_1)),in(n1,and2(h2(X0_iProver_type_1))))
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1710]) ).
tcf(c_1790,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n2,h2(X0_iProver_type_1)),in(n2,and2(h2(X0_iProver_type_1))))
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1709]) ).
tcf(c_1791,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(s,h2(X0_iProver_type_1)),out(n1,and1(h2(X0_iProver_type_1))))
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1708]) ).
tcf(c_1792,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(c,h2(X0_iProver_type_1)),out(n1,and2(h2(X0_iProver_type_1))))
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1707]) ).
tcf(c_1794,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(n1,and2(h2(X0_iProver_type_1))),in(n1,not1(h2(X0_iProver_type_1))))
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1705]) ).
tcf(c_1795,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(n1,not1(h2(X0_iProver_type_1))),in(n2,and1(h2(X0_iProver_type_1))))
| ~ type(h2(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1704]) ).
tcf(c_1796,plain,
( connection(out(n1,not1(h2(f))),in(n2,and1(h2(f))))
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1795]) ).
tcf(c_1797,plain,
( connection(out(n1,and2(h2(f))),in(n1,not1(h2(f))))
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1794]) ).
tcf(c_1799,plain,
( connection(out(c,h2(f)),out(n1,and2(h2(f))))
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1792]) ).
tcf(c_1800,plain,
( connection(out(s,h2(f)),out(n1,and1(h2(f))))
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1791]) ).
tcf(c_1801,plain,
( connection(in(n2,h2(f)),in(n2,and2(h2(f))))
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1790]) ).
tcf(c_1802,plain,
( connection(in(n1,h2(f)),in(n1,and2(h2(f))))
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1789]) ).
tcf(c_1806,plain,
( type(not1(h2(f)),not)
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1785]) ).
tcf(c_1807,plain,
( type(and2(h2(f)),and)
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1784]) ).
tcf(c_1808,plain,
( type(and1(h2(f)),and)
| ~ type(h2(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1783]) ).
tcf(c_1809,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(and1(h1(X0_iProver_type_1)),and)
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1716]) ).
tcf(c_1810,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(and2(h1(X0_iProver_type_1)),and)
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1715]) ).
tcf(c_1811,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(not1(h1(X0_iProver_type_1)),not)
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1714]) ).
tcf(c_1812,plain,
! [X0_iProver_type_1: iProver_type_1] :
( type(or1(h1(X0_iProver_type_1)),or)
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1713]) ).
tcf(c_1814,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n2,h1(X0_iProver_type_1)),in(n2,or1(h1(X0_iProver_type_1))))
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1711]) ).
tcf(c_1815,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(in(n1,h1(X0_iProver_type_1)),in(n1,and2(h1(X0_iProver_type_1))))
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1710]) ).
tcf(c_1817,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(s,h1(X0_iProver_type_1)),out(n1,and1(h1(X0_iProver_type_1))))
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1708]) ).
tcf(c_1819,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(n1,or1(h1(X0_iProver_type_1))),in(n1,and1(h1(X0_iProver_type_1))))
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1706]) ).
tcf(c_1820,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(n1,and2(h1(X0_iProver_type_1))),in(n1,not1(h1(X0_iProver_type_1))))
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1705]) ).
tcf(c_1821,plain,
! [X0_iProver_type_1: iProver_type_1] :
( connection(out(n1,not1(h1(X0_iProver_type_1))),in(n2,and1(h1(X0_iProver_type_1))))
| ~ type(h1(X0_iProver_type_1),halfadder) ),
inference(instantiation,[status(thm)],[c_1704]) ).
tcf(c_1822,plain,
( connection(out(n1,not1(h1(f))),in(n2,and1(h1(f))))
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1821]) ).
tcf(c_1823,plain,
( connection(out(n1,and2(h1(f))),in(n1,not1(h1(f))))
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1820]) ).
tcf(c_1824,plain,
( connection(out(n1,or1(h1(f))),in(n1,and1(h1(f))))
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1819]) ).
tcf(c_1826,plain,
( connection(out(s,h1(f)),out(n1,and1(h1(f))))
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1817]) ).
tcf(c_1828,plain,
( connection(in(n1,h1(f)),in(n1,and2(h1(f))))
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1815]) ).
tcf(c_1829,plain,
( connection(in(n2,h1(f)),in(n2,or1(h1(f))))
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1814]) ).
tcf(c_1831,plain,
( type(or1(h1(f)),or)
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1812]) ).
tcf(c_1832,plain,
( type(not1(h1(f)),not)
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1811]) ).
tcf(c_1833,plain,
( type(and2(h1(f)),and)
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1810]) ).
tcf(c_1834,plain,
( type(and1(h1(f)),and)
| ~ type(h1(f),halfadder) ),
inference(instantiation,[status(thm)],[c_1809]) ).
tcf(c_1843,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(c,X0_iProver_type_1),X0_iProver_value_2)
| ~ value(out(n1,or1(X0_iProver_type_1)),X0_iProver_value_2)
| ~ connection(out(c,X0_iProver_type_1),out(n1,or1(X0_iProver_type_1))) ),
inference(instantiation,[status(thm)],[c_1702]) ).
tcf(c_1844,plain,
( value(out(c,f),n1)
| ~ value(out(n1,or1(f)),n1)
| ~ connection(out(c,f),out(n1,or1(f))) ),
inference(instantiation,[status(thm)],[c_1843]) ).
tcf(c_1858,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(s,h2(X0_iProver_type_1)),X0_iProver_value_2)
| ~ value(out(s,X0_iProver_type_1),X0_iProver_value_2)
| ~ connection(out(s,X0_iProver_type_1),out(s,h2(X0_iProver_type_1))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1859,plain,
( value(out(s,h2(f)),n1)
| ~ value(out(s,f),n1)
| ~ connection(out(s,f),out(s,h2(f))) ),
inference(instantiation,[status(thm)],[c_1858]) ).
tcf(c_1860,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n2,h1(X0_iProver_type_1)),X0_iProver_value_2)
| ~ value(in(c,X0_iProver_type_1),X0_iProver_value_2)
| ~ connection(in(c,X0_iProver_type_1),in(n2,h1(X0_iProver_type_1))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1861,plain,
( value(in(n2,h1(f)),n1)
| ~ value(in(c,f),n1)
| ~ connection(in(c,f),in(n2,h1(f))) ),
inference(instantiation,[status(thm)],[c_1860]) ).
tcf(c_1862,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n1,h1(X0_iProver_type_1)),X0_iProver_value_2)
| ~ value(in(n2,X0_iProver_type_1),X0_iProver_value_2)
| ~ connection(in(n2,X0_iProver_type_1),in(n1,h1(X0_iProver_type_1))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1864,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n1,h2(X0_iProver_type_1)),X0_iProver_value_2)
| ~ value(in(n1,X0_iProver_type_1),X0_iProver_value_2)
| ~ connection(in(n1,X0_iProver_type_1),in(n1,h2(X0_iProver_type_1))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1865,plain,
( value(in(n1,h2(f)),n1)
| ~ value(in(n1,f),n1)
| ~ connection(in(n1,f),in(n1,h2(f))) ),
inference(instantiation,[status(thm)],[c_1864]) ).
tcf(c_1870,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n2,h2(X0_iProver_type_1)),X0_iProver_value_2)
| ~ value(out(s,h1(X0_iProver_type_1)),X0_iProver_value_2)
| ~ connection(out(s,h1(X0_iProver_type_1)),in(n2,h2(X0_iProver_type_1))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1871,plain,
( value(in(n2,h2(f)),n1)
| ~ value(out(s,h1(f)),n1)
| ~ connection(out(s,h1(f)),in(n2,h2(f))) ),
inference(instantiation,[status(thm)],[c_1870]) ).
tcf(c_1872,plain,
( ~ value(out(c,f),n0)
| ~ value(out(c,f),n1) ),
inference(instantiation,[status(thm)],[c_1685]) ).
tcf(c_1877,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n2,and1(h2(X0_iProver_type_1))),n1)
| ~ mode(and1(h2(X0_iProver_type_1)),ok)
| ~ type(and1(h2(X0_iProver_type_1)),and)
| ~ value(out(n1,and1(h2(X0_iProver_type_1))),n1) ),
inference(instantiation,[status(thm)],[c_1695]) ).
tcf(c_1878,plain,
( value(in(n2,and1(h2(f))),n1)
| ~ mode(and1(h2(f)),ok)
| ~ type(and1(h2(f)),and)
| ~ value(out(n1,and1(h2(f))),n1) ),
inference(instantiation,[status(thm)],[c_1877]) ).
tcf(c_1884,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(out(n1,and2(h2(X0_iProver_type_1))),n1)
| ~ mode(and2(h2(X0_iProver_type_1)),ok)
| ~ type(and2(h2(X0_iProver_type_1)),and)
| ~ value(in(n2,and2(h2(X0_iProver_type_1))),n1)
| ~ value(in(n1,and2(h2(X0_iProver_type_1))),n1) ),
inference(instantiation,[status(thm)],[c_1698]) ).
tcf(c_1887,plain,
( value(out(n1,and2(h2(f))),n1)
| ~ mode(and2(h2(f)),ok)
| ~ type(and2(h2(f)),and)
| ~ value(in(n2,and2(h2(f))),n1)
| ~ value(in(n1,and2(h2(f))),n1) ),
inference(instantiation,[status(thm)],[c_1884]) ).
tcf(c_1889,plain,
! [X0_iProver_type_1: iProver_type_1] :
( mode(and2(h2(X0_iProver_type_1)),ok)
| mode(and2(h2(X0_iProver_type_1)),abnormal)
| ~ type(and2(h2(X0_iProver_type_1)),and) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_1890,plain,
( mode(and2(h2(f)),ok)
| mode(and2(h2(f)),abnormal)
| ~ type(and2(h2(f)),and) ),
inference(instantiation,[status(thm)],[c_1889]) ).
tcf(c_1893,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n1,not1(h2(X0_iProver_type_1))),n0)
| ~ mode(not1(h2(X0_iProver_type_1)),ok)
| ~ type(not1(h2(X0_iProver_type_1)),not)
| ~ value(out(n1,not1(h2(X0_iProver_type_1))),n1) ),
inference(instantiation,[status(thm)],[c_1686]) ).
tcf(c_1894,plain,
( value(in(n1,not1(h2(f))),n0)
| ~ mode(not1(h2(f)),ok)
| ~ type(not1(h2(f)),not)
| ~ value(out(n1,not1(h2(f))),n1) ),
inference(instantiation,[status(thm)],[c_1893]) ).
tcf(c_1901,plain,
! [X0_iProver_type_2: iProver_type_2] :
( mode(or1(h1(f)),ok)
| mode(or1(h1(f)),abnormal)
| ~ type(or1(h1(f)),X0_iProver_type_2) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_1903,plain,
! [X0_iProver_type_2: iProver_type_2] :
( mode(not1(h1(f)),ok)
| mode(not1(h1(f)),abnormal)
| ~ type(not1(h1(f)),X0_iProver_type_2) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_1905,plain,
! [X0_iProver_type_2: iProver_type_2] :
( mode(and2(h1(f)),ok)
| mode(and2(h1(f)),abnormal)
| ~ type(and2(h1(f)),X0_iProver_type_2) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_1907,plain,
! [X0_iProver_type_2: iProver_type_2] :
( mode(and1(h1(f)),ok)
| mode(and1(h1(f)),abnormal)
| ~ type(and1(h1(f)),X0_iProver_type_2) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_1922,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n1,and2(h2(X0_iProver_type_1))),X0_iProver_value_2)
| ~ value(in(n1,h2(X0_iProver_type_1)),X0_iProver_value_2)
| ~ connection(in(n1,h2(X0_iProver_type_1)),in(n1,and2(h2(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1923,plain,
( value(in(n1,and2(h2(f))),n1)
| ~ value(in(n1,h2(f)),n1)
| ~ connection(in(n1,h2(f)),in(n1,and2(h2(f)))) ),
inference(instantiation,[status(thm)],[c_1922]) ).
tcf(c_1926,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n2,and2(h2(X0_iProver_type_1))),X0_iProver_value_2)
| ~ value(in(n2,h2(X0_iProver_type_1)),X0_iProver_value_2)
| ~ connection(in(n2,h2(X0_iProver_type_1)),in(n2,and2(h2(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1927,plain,
( value(in(n2,and2(h2(f))),n1)
| ~ value(in(n2,h2(f)),n1)
| ~ connection(in(n2,h2(f)),in(n2,and2(h2(f)))) ),
inference(instantiation,[status(thm)],[c_1926]) ).
tcf(c_1930,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(n1,and1(h2(X0_iProver_type_1))),X0_iProver_value_2)
| ~ value(out(s,h2(X0_iProver_type_1)),X0_iProver_value_2)
| ~ connection(out(s,h2(X0_iProver_type_1)),out(n1,and1(h2(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1931,plain,
( value(out(n1,and1(h2(f))),n1)
| ~ value(out(s,h2(f)),n1)
| ~ connection(out(s,h2(f)),out(n1,and1(h2(f)))) ),
inference(instantiation,[status(thm)],[c_1930]) ).
tcf(c_1936,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(c,h2(X0_iProver_type_1)),X0_iProver_value_2)
| ~ value(out(n1,and2(h2(X0_iProver_type_1))),X0_iProver_value_2)
| ~ connection(out(c,h2(X0_iProver_type_1)),out(n1,and2(h2(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_1702]) ).
tcf(c_1937,plain,
( value(out(c,h2(f)),n1)
| ~ value(out(n1,and2(h2(f))),n1)
| ~ connection(out(c,h2(f)),out(n1,and2(h2(f)))) ),
inference(instantiation,[status(thm)],[c_1936]) ).
tcf(c_1942,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n1,not1(h2(X0_iProver_type_1))),X0_iProver_value_2)
| ~ value(out(n1,and2(h2(X0_iProver_type_1))),X0_iProver_value_2)
| ~ connection(out(n1,and2(h2(X0_iProver_type_1))),in(n1,not1(h2(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_1943,plain,
( value(in(n1,not1(h2(f))),n1)
| ~ value(out(n1,and2(h2(f))),n1)
| ~ connection(out(n1,and2(h2(f))),in(n1,not1(h2(f)))) ),
inference(instantiation,[status(thm)],[c_1942]) ).
tcf(c_1971,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(out(n1,and1(h1(X0_iProver_type_1))),n1)
| ~ mode(and1(h1(X0_iProver_type_1)),ok)
| ~ type(and1(h1(X0_iProver_type_1)),and)
| ~ value(in(n2,and1(h1(X0_iProver_type_1))),n1)
| ~ value(in(n1,and1(h1(X0_iProver_type_1))),n1) ),
inference(instantiation,[status(thm)],[c_1698]) ).
tcf(c_1974,plain,
( value(out(n1,and1(h1(f))),n1)
| ~ mode(and1(h1(f)),ok)
| ~ type(and1(h1(f)),and)
| ~ value(in(n2,and1(h1(f))),n1)
| ~ value(in(n1,and1(h1(f))),n1) ),
inference(instantiation,[status(thm)],[c_1971]) ).
tcf(c_1976,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(n1,and2(h1(X0_iProver_type_1))),n0)
| ~ mode(and2(h1(X0_iProver_type_1)),ok)
| ~ type(and2(h1(X0_iProver_type_1)),and)
| ~ value(in(X0_iProver_value_2,and2(h1(X0_iProver_type_1))),n0) ),
inference(instantiation,[status(thm)],[c_1699]) ).
tcf(c_1981,plain,
( value(out(n1,and2(h1(f))),n0)
| ~ mode(and2(h1(f)),ok)
| ~ type(and2(h1(f)),and)
| ~ value(in(n1,and2(h1(f))),n0) ),
inference(instantiation,[status(thm)],[c_1976]) ).
tcf(c_1982,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(out(n1,not1(h1(X0_iProver_type_1))),n1)
| ~ mode(not1(h1(X0_iProver_type_1)),ok)
| ~ type(not1(h1(X0_iProver_type_1)),not)
| ~ value(in(n1,not1(h1(X0_iProver_type_1))),n0) ),
inference(instantiation,[status(thm)],[c_1689]) ).
tcf(c_1987,plain,
( value(out(n1,not1(h1(f))),n1)
| ~ mode(not1(h1(f)),ok)
| ~ type(not1(h1(f)),not)
| ~ value(in(n1,not1(h1(f))),n0) ),
inference(instantiation,[status(thm)],[c_1982]) ).
tcf(c_2028,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(X0_iProver_value_1,X0_iProver_value_2)
| ~ connection(in(n2,h1(X0_iProver_type_1)),X0_iProver_value_1)
| ~ value(in(n2,h1(X0_iProver_type_1)),X0_iProver_value_2) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_2032,plain,
( value(in(n1,h1(f)),n0)
| ~ value(in(n2,f),n0)
| ~ connection(in(n2,f),in(n1,h1(f))) ),
inference(instantiation,[status(thm)],[c_1862]) ).
tcf(c_2052,plain,
( mode(or1(h1(f)),ok)
| mode(or1(h1(f)),abnormal)
| ~ type(or1(h1(f)),or) ),
inference(instantiation,[status(thm)],[c_1901]) ).
tcf(c_2055,plain,
! [X0_iProver_type_1: iProver_type_1] :
( mode(or1(X0_iProver_type_1),ok)
| mode(or1(X0_iProver_type_1),abnormal)
| ~ type(X0_iProver_type_1,fulladder) ),
inference(superposition,[status(thm)],[c_1725,c_1700]) ).
tcf(c_2057,plain,
! [X0_iProver_type_1: iProver_type_1] :
( mode(not1(X0_iProver_type_1),ok)
| mode(not1(X0_iProver_type_1),abnormal)
| ~ type(X0_iProver_type_1,halfadder) ),
inference(superposition,[status(thm)],[c_1714,c_1700]) ).
tcf(c_2059,plain,
! [X0_iProver_type_1: iProver_type_1] :
( mode(and1(X0_iProver_type_1),ok)
| mode(and1(X0_iProver_type_1),abnormal)
| ~ type(X0_iProver_type_1,halfadder) ),
inference(superposition,[status(thm)],[c_1716,c_1700]) ).
tcf(c_2068,plain,
( mode(or1(f),ok)
| mode(or1(f),abnormal)
| ~ type(f,fulladder) ),
inference(instantiation,[status(thm)],[c_2055]) ).
tcf(c_2069,plain,
( mode(not1(h1(f)),ok)
| mode(not1(h1(f)),abnormal)
| ~ type(not1(h1(f)),not) ),
inference(instantiation,[status(thm)],[c_1903]) ).
tcf(c_2070,plain,
( mode(and2(h1(f)),ok)
| mode(and2(h1(f)),abnormal)
| ~ type(and2(h1(f)),and) ),
inference(instantiation,[status(thm)],[c_1905]) ).
tcf(c_2071,plain,
( mode(and1(h1(f)),ok)
| mode(and1(h1(f)),abnormal)
| ~ type(and1(h1(f)),and) ),
inference(instantiation,[status(thm)],[c_1907]) ).
tcf(c_2259,plain,
( mode(not1(h2(f)),ok)
| ~ mode(or1(f),abnormal)
| ~ type(h2(f),halfadder) ),
inference(superposition,[status(thm)],[c_2057,c_1734]) ).
tcf(c_2333,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n2,or1(h1(X0_iProver_type_1))),X0_iProver_value_2)
| ~ value(in(n2,h1(X0_iProver_type_1)),X0_iProver_value_2)
| ~ connection(in(n2,h1(X0_iProver_type_1)),in(n2,or1(h1(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_2028]) ).
tcf(c_2334,plain,
( value(in(n2,or1(h1(f))),n1)
| ~ value(in(n2,h1(f)),n1)
| ~ connection(in(n2,h1(f)),in(n2,or1(h1(f)))) ),
inference(instantiation,[status(thm)],[c_2333]) ).
tcf(c_2337,plain,
( mode(and1(h2(f)),ok)
| ~ mode(or1(f),abnormal)
| ~ type(h2(f),halfadder) ),
inference(superposition,[status(thm)],[c_2059,c_1732]) ).
tcf(c_2397,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(in(n1,or1(X0_iProver_type_1)),X0_iProver_value_2)
| ~ type(X0_iProver_type_1,fulladder)
| ~ value(out(c,h2(X0_iProver_type_1)),X0_iProver_value_2) ),
inference(superposition,[status(thm)],[c_1722,c_1703]) ).
tcf(c_2398,plain,
( value(in(n1,or1(f)),n1)
| ~ type(f,fulladder)
| ~ value(out(c,h2(f)),n1) ),
inference(instantiation,[status(thm)],[c_2397]) ).
tcf(c_2537,plain,
! [X0_iProver_value_2: iProver_value_2,X0_iProver_type_1: iProver_type_1] :
( value(out(n1,or1(X0_iProver_type_1)),n1)
| ~ mode(or1(X0_iProver_type_1),ok)
| ~ type(or1(X0_iProver_type_1),or)
| ~ value(in(X0_iProver_value_2,or1(X0_iProver_type_1)),n1) ),
inference(instantiation,[status(thm)],[c_1694]) ).
tcf(c_2640,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_type_1: iProver_type_1] :
( value(X0_iProver_value_1,n1)
| ~ value(in(n2,and1(h2(X0_iProver_type_1))),n1)
| ~ connection(X0_iProver_value_1,in(n2,and1(h2(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_1702]) ).
tcf(c_2703,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_type_1: iProver_type_1] :
( value(X0_iProver_value_1,n0)
| ~ value(in(n1,h1(X0_iProver_type_1)),n0)
| ~ connection(in(n1,h1(X0_iProver_type_1)),X0_iProver_value_1) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_2710,plain,
! [X0_iProver_value_2: iProver_value_2] :
( value(out(n1,or1(h1(f))),n1)
| ~ mode(or1(h1(f)),ok)
| ~ type(or1(h1(f)),or)
| ~ value(in(X0_iProver_value_2,or1(h1(f))),n1) ),
inference(instantiation,[status(thm)],[c_2537]) ).
tcf(c_2733,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(out(n1,not1(h2(X0_iProver_type_1))),n1)
| ~ value(in(n2,and1(h2(X0_iProver_type_1))),n1)
| ~ connection(out(n1,not1(h2(X0_iProver_type_1))),in(n2,and1(h2(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_2640]) ).
tcf(c_2734,plain,
( value(out(n1,not1(h2(f))),n1)
| ~ value(in(n2,and1(h2(f))),n1)
| ~ connection(out(n1,not1(h2(f))),in(n2,and1(h2(f)))) ),
inference(instantiation,[status(thm)],[c_2733]) ).
tcf(c_2793,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n1,and2(h1(X0_iProver_type_1))),n0)
| ~ value(in(n1,h1(X0_iProver_type_1)),n0)
| ~ connection(in(n1,h1(X0_iProver_type_1)),in(n1,and2(h1(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_2703]) ).
tcf(c_2794,plain,
( value(in(n1,and2(h1(f))),n0)
| ~ value(in(n1,h1(f)),n0)
| ~ connection(in(n1,h1(f)),in(n1,and2(h1(f)))) ),
inference(instantiation,[status(thm)],[c_2793]) ).
tcf(c_2817,plain,
! [X0_iProver_type_1: iProver_type_1] :
( ~ value(in(n1,not1(h2(X0_iProver_type_1))),n0)
| ~ value(in(n1,not1(h2(X0_iProver_type_1))),n1) ),
inference(instantiation,[status(thm)],[c_1685]) ).
tcf(c_2818,plain,
( ~ value(in(n1,not1(h2(f))),n0)
| ~ value(in(n1,not1(h2(f))),n1) ),
inference(instantiation,[status(thm)],[c_2817]) ).
tcf(c_2833,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_type_1: iProver_type_1] :
( value(X0_iProver_value_1,n0)
| ~ value(out(n1,and2(h1(X0_iProver_type_1))),n0)
| ~ connection(out(n1,and2(h1(X0_iProver_type_1))),X0_iProver_value_1) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_2949,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_type_1: iProver_type_1] :
( value(in(n2,X0_iProver_type_1),n1)
| ~ value(X0_iProver_value_1,n1)
| ~ connection(X0_iProver_value_1,in(n2,X0_iProver_type_1)) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_2998,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_type_1: iProver_type_1] :
( value(in(n1,and1(X0_iProver_type_1)),n1)
| ~ value(X0_iProver_value_1,n1)
| ~ connection(X0_iProver_value_1,in(n1,and1(X0_iProver_type_1))) ),
inference(instantiation,[status(thm)],[c_1703]) ).
tcf(c_3045,plain,
( value(out(n1,or1(h1(f))),n1)
| ~ mode(or1(h1(f)),ok)
| ~ type(or1(h1(f)),or)
| ~ value(in(n2,or1(h1(f))),n1) ),
inference(instantiation,[status(thm)],[c_2710]) ).
tcf(c_3071,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n1,not1(h1(X0_iProver_type_1))),n0)
| ~ value(out(n1,and2(h1(X0_iProver_type_1))),n0)
| ~ connection(out(n1,and2(h1(X0_iProver_type_1))),in(n1,not1(h1(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_2833]) ).
tcf(c_3072,plain,
( value(in(n1,not1(h1(f))),n0)
| ~ value(out(n1,and2(h1(f))),n0)
| ~ connection(out(n1,and2(h1(f))),in(n1,not1(h1(f)))) ),
inference(instantiation,[status(thm)],[c_3071]) ).
tcf(c_3122,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n2,and1(X0_iProver_type_1)),n1)
| ~ value(out(n1,not1(X0_iProver_type_1)),n1)
| ~ connection(out(n1,not1(X0_iProver_type_1)),in(n2,and1(X0_iProver_type_1))) ),
inference(instantiation,[status(thm)],[c_2949]) ).
tcf(c_3333,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n1,and1(h1(X0_iProver_type_1))),n1)
| ~ value(out(n1,or1(h1(X0_iProver_type_1))),n1)
| ~ connection(out(n1,or1(h1(X0_iProver_type_1))),in(n1,and1(h1(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_2998]) ).
tcf(c_3334,plain,
( value(in(n1,and1(h1(f))),n1)
| ~ value(out(n1,or1(h1(f))),n1)
| ~ connection(out(n1,or1(h1(f))),in(n1,and1(h1(f)))) ),
inference(instantiation,[status(thm)],[c_3333]) ).
tcf(c_3439,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(in(n2,and1(h1(X0_iProver_type_1))),n1)
| ~ value(out(n1,not1(h1(X0_iProver_type_1))),n1)
| ~ connection(out(n1,not1(h1(X0_iProver_type_1))),in(n2,and1(h1(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_3122]) ).
tcf(c_3440,plain,
( value(in(n2,and1(h1(f))),n1)
| ~ value(out(n1,not1(h1(f))),n1)
| ~ connection(out(n1,not1(h1(f))),in(n2,and1(h1(f)))) ),
inference(instantiation,[status(thm)],[c_3439]) ).
tcf(c_3451,plain,
! [X0_iProver_value_1: iProver_value_1,X0_iProver_type_1: iProver_type_1] :
( value(out(s,h1(X0_iProver_type_1)),n1)
| ~ value(X0_iProver_value_1,n1)
| ~ connection(out(s,h1(X0_iProver_type_1)),X0_iProver_value_1) ),
inference(instantiation,[status(thm)],[c_1702]) ).
tcf(c_3619,plain,
! [X0_iProver_type_1: iProver_type_1] :
( value(out(s,h1(X0_iProver_type_1)),n1)
| ~ value(out(n1,and1(h1(X0_iProver_type_1))),n1)
| ~ connection(out(s,h1(X0_iProver_type_1)),out(n1,and1(h1(X0_iProver_type_1)))) ),
inference(instantiation,[status(thm)],[c_3451]) ).
tcf(c_3620,plain,
( value(out(s,h1(f)),n1)
| ~ value(out(n1,and1(h1(f))),n1)
| ~ connection(out(s,h1(f)),out(n1,and1(h1(f)))) ),
inference(instantiation,[status(thm)],[c_3619]) ).
tcf(c_3621,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_3620,c_3440,c_3334,c_3072,c_3045,c_2818,c_2794,c_2734,c_2398,c_2337,c_2334,c_2259,c_2071,c_2070,c_2069,c_2068,c_2052,c_2032,c_1987,c_1981,c_1974,c_1943,c_1937,c_1931,c_1927,c_1923,c_1894,c_1890,c_1887,c_1878,c_1872,c_1871,c_1865,c_1861,c_1859,c_1844,c_1834,c_1833,c_1832,c_1831,c_1829,c_1828,c_1826,c_1824,c_1823,c_1822,c_1808,c_1807,c_1806,c_1802,c_1801,c_1800,c_1799,c_1797,c_1796,c_1782,c_1767,c_1761,c_1760,c_1759,c_1758,c_1757,c_1749,c_1748,c_1747,c_159,c_161,c_162,c_163,c_164,c_153,c_154,c_155,c_156,c_157,c_152]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HWV006-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.19/0.45 % Computer : n026.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Wed Sep 23 16:23:23 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.24/0.52 Running first-order theorem proving
% 0.24/0.52 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.24/0.54
% 0.24/0.54 % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.54
% 0.24/0.54 % Detected problem language: tptp
% 0.24/0.56 % Proving...
% 4.57/1.53 % SZS status Started for theBenchmark.p
% 4.57/1.53 % SZS status Unsatisfiable for theBenchmark.p
% 4.57/1.53
% 4.57/1.53 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.57/1.53
% 4.57/1.53 % ------ iProver source info
% 4.57/1.53
% 4.57/1.53 % git: date: 2026-07-19 20:42:38 +0200
% 4.57/1.53 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.57/1.53 % git: non_committed_changes: false
% 4.57/1.53
% 4.57/1.53 % ------ Parsing...% successful
% 4.57/1.53
% 4.57/1.53
% 4.57/1.53 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.57/1.53
% 4.57/1.53 % ------ 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 %
% 4.57/1.53
% 4.57/1.53 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 4.57/1.53 % ------ Proving...
% 4.57/1.53 % ------ Problem Properties
% 4.57/1.53
% 4.57/1.53 %
% 4.57/1.53 % clauses 56
% 4.57/1.53 % conjectures 7
% 4.57/1.53 % EPR 6
% 4.57/1.53 % Horn 53
% 4.57/1.53 % unary 11
% 4.57/1.53 % binary 28
% 4.57/1.53 % lits 136
% 4.57/1.53 % lits eq 0
% 4.57/1.53 % fd_pure 0
% 4.57/1.53 % fd_pseudo 0
% 4.57/1.53 % fd_cond 0
% 4.57/1.53 % fd_pseudo_cond 0
% 4.57/1.53 % AC symbols 0
% 4.57/1.53
% 4.57/1.53 % ------ Input Options Time Limit: Unbounded
% 4.57/1.53
% 4.57/1.53
% 4.57/1.53 % ------
% 4.57/1.53 % Current options:
% 4.57/1.53 % ------
% 4.57/1.53
% 4.57/1.53
% 4.57/1.53 %
% 4.57/1.53
% 4.57/1.53 % ------ Proving...
% 4.57/1.53 %
% 4.57/1.53
% 4.57/1.53 % SZS status Unsatisfiable for theBenchmark.p
% 4.57/1.53
% 4.57/1.53 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.57/1.54
% 4.57/1.54
%------------------------------------------------------------------------------