%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV006-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 : Thu Sep 24 12:45:54 PM UTC 2026
% Result : Unsatisfiable 0.50s 0.55s
% Output : CNFRefutation 0.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 98
% Syntax : Number of formulae : 360 ( 51 unt; 52 def)
% Number of atoms : 802 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 866 ( 424 ~; 390 |; 0 &)
% ( 52 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 58 ( 57 usr; 53 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% Number of variables : 191 ( 191 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [P1,P2,V] :
( value(P2,V)
| ~ value(P1,V)
| ~ connection(P1,P2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [P1,P2,V] :
( value(P1,V)
| ~ value(P2,V)
| ~ connection(P1,P2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [P,V1,V2] :
( equal_value(V1,V2)
| ~ value(P,V2)
| ~ value(P,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
~ equal_value(n1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [K,Any] :
( mode(K,abnormal)
| mode(K,ok)
| ~ type(K,Any) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [K,Any] :
( value(out(n1,K),n0)
| ~ value(in(Any,K),n0)
| ~ type(K,and)
| ~ mode(K,ok) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [K] :
( value(out(n1,K),n1)
| ~ value(in(n2,K),n1)
| ~ value(in(n1,K),n1)
| ~ type(K,and)
| ~ mode(K,ok) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [K,Any] :
( value(out(n1,K),n1)
| ~ value(in(Any,K),n1)
| ~ type(K,or)
| ~ mode(K,ok) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [K] :
( value(in(n1,K),n0)
| ~ value(out(n1,K),n0)
| ~ type(K,or)
| ~ mode(K,ok) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [K] :
( value(out(n1,K),n1)
| ~ value(in(n1,K),n0)
| ~ type(K,not)
| ~ mode(K,ok) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [K] :
( value(out(n1,K),n0)
| ~ value(in(n1,K),n1)
| ~ type(K,not)
| ~ mode(K,ok) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] :
( type(and1(X),and)
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X] :
( type(and2(X),and)
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X] :
( type(not1(X),not)
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X] :
( type(or1(X),or)
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X] :
( connection(in(n2,X),in(n2,or1(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X] :
( connection(in(n1,X),in(n1,and2(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X] :
( connection(in(n2,X),in(n2,and2(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] :
( connection(out(s,X),out(n1,and1(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X] :
( connection(out(c,X),out(n1,and2(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [X] :
( connection(out(n1,or1(X)),in(n1,and1(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X] :
( connection(out(n1,and2(X)),in(n1,not1(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X] :
( connection(out(n1,not1(X)),in(n2,and1(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X] :
( type(h1(X),halfadder)
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X] :
( type(h2(X),halfadder)
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X] :
( type(or1(X),or)
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [X] :
( connection(out(s,h1(X)),in(n2,h2(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] :
( connection(out(c,h2(X)),in(n1,or1(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] :
( connection(in(n1,X),in(n1,h2(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [X] :
( connection(in(n2,X),in(n1,h1(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [X] :
( connection(in(c,X),in(n2,h1(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [X] :
( connection(out(s,X),out(s,h2(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X] :
( connection(out(c,X),out(n1,or1(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
type(f,fulladder),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
value(in(n1,f),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
value(in(n2,f),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
value(in(c,f),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
value(out(s,f),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
value(out(c,f),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
( ~ mode(not1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
~ mode(and2(h2(f)),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
( ~ mode(and1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,negated_conjecture,
~ mode(or1(h1(f)),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
~ mode(not1(h1(f)),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ mode(and2(h1(f)),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,negated_conjecture,
~ mode(and1(h1(f)),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,plain,
! [P2,V] :
( value(P2,V)
| ! [P1] :
( ~ value(P1,V)
| ~ connection(P1,P2) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f60,plain,
! [X0,X1,X2] :
( value(X1,X2)
| ~ value(X0,X2)
| ~ connection(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [P1,V] :
( value(P1,V)
| ! [P2] :
( ~ value(P2,V)
| ~ connection(P1,P2) ) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f62,plain,
! [X0,X1,X2] :
( value(X0,X2)
| ~ value(X1,X2)
| ~ connection(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [V1,V2] :
( equal_value(V1,V2)
| ! [P] :
( ~ value(P,V2)
| ~ value(P,V1) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f64,plain,
! [X0,X1,X2] :
( equal_value(X1,X2)
| ~ value(X0,X2)
| ~ value(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f66,plain,
~ equal_value(n1,n0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f68,plain,
! [K] :
( mode(K,abnormal)
| mode(K,ok)
| ! [Any] : ~ type(K,Any) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f69,plain,
! [X0,X1] :
( mode(X0,abnormal)
| mode(X0,ok)
| ~ type(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
! [K] :
( value(out(n1,K),n0)
| ! [Any] : ~ value(in(Any,K),n0)
| ~ type(K,and)
| ~ mode(K,ok) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f71,plain,
! [X0,X1] :
( value(out(n1,X0),n0)
| ~ value(in(X1,X0),n0)
| ~ type(X0,and)
| ~ mode(X0,ok) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f72,plain,
! [X0] :
( value(out(n1,X0),n1)
| ~ value(in(n2,X0),n1)
| ~ value(in(n1,X0),n1)
| ~ type(X0,and)
| ~ mode(X0,ok) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f76,plain,
! [K] :
( value(out(n1,K),n1)
| ! [Any] : ~ value(in(Any,K),n1)
| ~ type(K,or)
| ~ mode(K,ok) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f77,plain,
! [X0,X1] :
( value(out(n1,X0),n1)
| ~ value(in(X1,X0),n1)
| ~ type(X0,or)
| ~ mode(X0,ok) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f80,plain,
! [X0] :
( value(in(n1,X0),n0)
| ~ value(out(n1,X0),n0)
| ~ type(X0,or)
| ~ mode(X0,ok) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f82,plain,
! [X0] :
( value(out(n1,X0),n1)
| ~ value(in(n1,X0),n0)
| ~ type(X0,not)
| ~ mode(X0,ok) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f83,plain,
! [X0] :
( value(out(n1,X0),n0)
| ~ value(in(n1,X0),n1)
| ~ type(X0,not)
| ~ mode(X0,ok) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f86,plain,
! [X0] :
( type(and1(X0),and)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f87,plain,
! [X0] :
( type(and2(X0),and)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f88,plain,
! [X0] :
( type(not1(X0),not)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f89,plain,
! [X0] :
( type(or1(X0),or)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f91,plain,
! [X0] :
( connection(in(n2,X0),in(n2,or1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f92,plain,
! [X0] :
( connection(in(n1,X0),in(n1,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f93,plain,
! [X0] :
( connection(in(n2,X0),in(n2,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f94,plain,
! [X0] :
( connection(out(s,X0),out(n1,and1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f95,plain,
! [X0] :
( connection(out(c,X0),out(n1,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f96,plain,
! [X0] :
( connection(out(n1,or1(X0)),in(n1,and1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f97,plain,
! [X0] :
( connection(out(n1,and2(X0)),in(n1,not1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f98,plain,
! [X0] :
( connection(out(n1,not1(X0)),in(n2,and1(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f99,plain,
! [X0] :
( type(h1(X0),halfadder)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f100,plain,
! [X0] :
( type(h2(X0),halfadder)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f101,plain,
! [X0] :
( type(or1(X0),or)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f102,plain,
! [X0] :
( connection(out(s,h1(X0)),in(n2,h2(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f104,plain,
! [X0] :
( connection(out(c,h2(X0)),in(n1,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f105,plain,
! [X0] :
( connection(in(n1,X0),in(n1,h2(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f106,plain,
! [X0] :
( connection(in(n2,X0),in(n1,h1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f107,plain,
! [X0] :
( connection(in(c,X0),in(n2,h1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f108,plain,
! [X0] :
( connection(out(s,X0),out(s,h2(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f109,plain,
! [X0] :
( connection(out(c,X0),out(n1,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f110,plain,
type(f,fulladder),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f111,plain,
value(in(n1,f),n1),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f112,plain,
value(in(n2,f),n0),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f113,plain,
value(in(c,f),n1),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f114,plain,
value(out(s,f),n1),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f115,plain,
value(out(c,f),n0),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f116,plain,
( ~ mode(not1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f117,plain,
~ mode(and2(h2(f)),abnormal),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f118,plain,
( ~ mode(and1(h2(f)),abnormal)
| ~ mode(or1(f),abnormal) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f119,plain,
~ mode(or1(h1(f)),abnormal),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f120,plain,
~ mode(not1(h1(f)),abnormal),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f121,plain,
~ mode(and2(h1(f)),abnormal),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f122,plain,
~ mode(and1(h1(f)),abnormal),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f123,definition,
( sQ0_spl
<=> mode(or1(f),abnormal) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f126,definition,
( sQ1_spl
<=> mode(not1(h2(f)),abnormal) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f129,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f116,f123,f126]) ).
fof(f130,definition,
( sQ2_spl
<=> mode(and1(h2(f)),abnormal) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f133,plain,
( ~ sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f118,f123,f130]) ).
fof(f134,plain,
! [X0] :
( ~ value(X0,n0)
| ~ value(X0,n1) ),
inference(resolution,[status(thm)],[f64,f66]) ).
fof(f139,plain,
! [X0,X1] :
( value(in(n2,or1(X0)),X1)
| ~ value(in(n2,X0),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f91,f60]) ).
fof(f141,plain,
! [X0,X1] :
( value(in(n1,and2(X0)),X1)
| ~ value(in(n1,X0),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f92,f60]) ).
fof(f144,plain,
! [X0,X1] :
( ~ value(out(n1,X0),n1)
| ~ value(in(X1,X0),n0)
| ~ type(X0,and)
| ~ mode(X0,ok) ),
inference(resolution,[status(thm)],[f71,f134]) ).
fof(f148,plain,
! [X0,X1] :
( value(in(n2,and2(X0)),X1)
| ~ value(in(n2,X0),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f93,f60]) ).
fof(f150,plain,
! [X0,X1] :
( value(out(n1,and2(X0)),X1)
| ~ value(out(c,X0),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f95,f60]) ).
fof(f152,plain,
! [X0,X1] :
( value(in(n1,and1(X0)),X1)
| ~ value(out(n1,or1(X0)),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f96,f60]) ).
fof(f153,plain,
connection(in(n1,f),in(n1,h2(f))),
inference(resolution,[status(thm)],[f105,f110]) ).
fof(f155,plain,
! [X0] :
( value(in(n1,h2(f)),X0)
| ~ value(in(n1,f),X0) ),
inference(resolution,[status(thm)],[f153,f60]) ).
fof(f156,plain,
connection(in(n2,f),in(n1,h1(f))),
inference(resolution,[status(thm)],[f106,f110]) ).
fof(f158,plain,
! [X0] :
( value(in(n1,h1(f)),X0)
| ~ value(in(n2,f),X0) ),
inference(resolution,[status(thm)],[f156,f60]) ).
fof(f159,plain,
! [X0,X1] :
( value(out(n1,and2(X0)),X1)
| ~ value(in(n1,not1(X0)),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f97,f62]) ).
fof(f160,plain,
! [X0,X1] :
( value(in(n1,not1(X0)),X1)
| ~ value(out(n1,and2(X0)),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f97,f60]) ).
fof(f162,plain,
! [X0,X1] :
( value(in(n2,and1(X0)),X1)
| ~ value(out(n1,not1(X0)),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f98,f60]) ).
fof(f163,plain,
! [X0,X1] :
( value(out(s,X0),X1)
| ~ value(out(n1,and1(X0)),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f94,f62]) ).
fof(f164,plain,
! [X0,X1] :
( value(out(n1,and1(X0)),X1)
| ~ value(out(s,X0),X1)
| ~ type(X0,halfadder) ),
inference(resolution,[status(thm)],[f94,f60]) ).
fof(f165,plain,
connection(in(c,f),in(n2,h1(f))),
inference(resolution,[status(thm)],[f107,f110]) ).
fof(f167,plain,
! [X0] :
( value(in(n2,h1(f)),X0)
| ~ value(in(c,f),X0) ),
inference(resolution,[status(thm)],[f165,f60]) ).
fof(f168,plain,
connection(out(s,f),out(s,h2(f))),
inference(resolution,[status(thm)],[f108,f110]) ).
fof(f170,plain,
! [X0] :
( value(out(s,h2(f)),X0)
| ~ value(out(s,f),X0) ),
inference(resolution,[status(thm)],[f168,f60]) ).
fof(f171,plain,
connection(out(c,f),out(n1,or1(f))),
inference(resolution,[status(thm)],[f109,f110]) ).
fof(f201,definition,
( sQ10_spl
<=> value(in(n2,h2(f)),n1) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( ~ sQ10_spl
| value(in(n2,h2(f)),n1) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f231,plain,
value(in(n1,h2(f)),n1),
inference(resolution,[status(thm)],[f155,f111]) ).
fof(f266,plain,
! [X0,X1] :
( ~ type(X0,fulladder)
| value(in(n1,and2(h2(X0))),X1)
| ~ value(in(n1,h2(X0)),X1) ),
inference(resolution,[status(thm)],[f141,f100]) ).
fof(f267,plain,
! [X0,X1] :
( ~ type(X0,fulladder)
| value(in(n1,and2(h1(X0))),X1)
| ~ value(in(n1,h1(X0)),X1) ),
inference(resolution,[status(thm)],[f141,f99]) ).
fof(f290,plain,
! [X0] :
( ~ type(X0,halfadder)
| value(out(n1,not1(X0)),n0)
| ~ value(in(n1,not1(X0)),n1)
| ~ mode(not1(X0),ok) ),
inference(resolution,[status(thm)],[f83,f88]) ).
fof(f351,plain,
connection(out(s,h1(f)),in(n2,h2(f))),
inference(resolution,[status(thm)],[f102,f110]) ).
fof(f447,plain,
connection(out(c,h2(f)),in(n1,or1(f))),
inference(resolution,[status(thm)],[f104,f110]) ).
fof(f456,plain,
! [X0,X1] :
( ~ type(X0,fulladder)
| value(in(n1,and1(h1(X0))),X1)
| ~ value(out(n1,or1(h1(X0))),X1) ),
inference(resolution,[status(thm)],[f152,f99]) ).
fof(f483,plain,
! [X0,X1] :
( ~ type(X0,fulladder)
| value(in(n1,not1(h2(X0))),X1)
| ~ value(out(n1,and2(h2(X0))),X1) ),
inference(resolution,[status(thm)],[f160,f100]) ).
fof(f484,plain,
! [X0,X1] :
( ~ type(X0,fulladder)
| value(in(n1,not1(h1(X0))),X1)
| ~ value(out(n1,and2(h1(X0))),X1) ),
inference(resolution,[status(thm)],[f160,f99]) ).
fof(f542,plain,
! [X0,X1] :
( ~ type(X0,fulladder)
| value(in(n2,and1(h2(X0))),X1)
| ~ value(out(n1,not1(h2(X0))),X1) ),
inference(resolution,[status(thm)],[f162,f100]) ).
fof(f543,plain,
! [X0,X1] :
( ~ type(X0,fulladder)
| value(in(n2,and1(h1(X0))),X1)
| ~ value(out(n1,not1(h1(X0))),X1) ),
inference(resolution,[status(thm)],[f162,f99]) ).
fof(f653,plain,
! [X0,X1] :
( ~ type(X0,fulladder)
| value(out(n1,and1(h2(X0))),X1)
| ~ value(out(s,h2(X0)),X1) ),
inference(resolution,[status(thm)],[f164,f100]) ).
fof(f656,plain,
! [X0] :
( value(out(n1,or1(f)),X0)
| ~ value(out(c,f),X0) ),
inference(resolution,[status(thm)],[f171,f60]) ).
fof(f671,definition,
( sQ88_spl
<=> value(in(n2,h1(f)),n1) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f672,plain,
( ~ sQ88_spl
| value(in(n2,h1(f)),n1) ),
inference(component_clause,[status(thm)],[f671]) ).
fof(f673,plain,
( sQ88_spl
| ~ value(in(n2,h1(f)),n1) ),
inference(component_clause,[status(thm)],[f671]) ).
fof(f677,plain,
value(in(n1,h1(f)),n0),
inference(resolution,[status(thm)],[f158,f112]) ).
fof(f770,plain,
! [X0] :
( value(in(n1,and2(h2(f))),X0)
| ~ value(in(n1,h2(f)),X0) ),
inference(resolution,[status(thm)],[f266,f110]) ).
fof(f813,plain,
! [X0] :
( value(in(n2,h2(f)),X0)
| ~ value(out(s,h1(f)),X0) ),
inference(resolution,[status(thm)],[f351,f60]) ).
fof(f824,plain,
! [X0] :
( value(in(n1,and2(h1(f))),X0)
| ~ value(in(n1,h1(f)),X0) ),
inference(resolution,[status(thm)],[f267,f110]) ).
fof(f943,plain,
! [X0] :
( value(out(c,h2(f)),X0)
| ~ value(in(n1,or1(f)),X0) ),
inference(resolution,[status(thm)],[f447,f62]) ).
fof(f955,plain,
! [X0] :
( value(in(n1,and1(h1(f))),X0)
| ~ value(out(n1,or1(h1(f))),X0) ),
inference(resolution,[status(thm)],[f456,f110]) ).
fof(f1013,plain,
value(in(n2,h1(f)),n1),
inference(resolution,[status(thm)],[f167,f113]) ).
fof(f1014,plain,
( sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1013,f673]) ).
fof(f1015,plain,
sQ88_spl,
inference(contradiction_clause,[status(thm)],[f1014]) ).
fof(f1020,definition,
( sQ138_spl
<=> type(h2(f),halfadder) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1022,plain,
( sQ138_spl
| ~ type(h2(f),halfadder) ),
inference(component_clause,[status(thm)],[f1020]) ).
fof(f1029,definition,
( sQ140_spl
<=> value(out(s,h2(f)),n1) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1030,plain,
( ~ sQ140_spl
| value(out(s,h2(f)),n1) ),
inference(component_clause,[status(thm)],[f1029]) ).
fof(f1031,plain,
( sQ140_spl
| ~ value(out(s,h2(f)),n1) ),
inference(component_clause,[status(thm)],[f1029]) ).
fof(f1035,plain,
( ~ sQ88_spl
| value(in(n2,or1(h1(f))),n1)
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f672,f139]) ).
fof(f1036,definition,
( sQ141_spl
<=> type(h1(f),halfadder) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1038,plain,
( sQ141_spl
| ~ type(h1(f),halfadder) ),
inference(component_clause,[status(thm)],[f1036]) ).
fof(f1043,definition,
( sQ143_spl
<=> value(in(n2,or1(h1(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1044,plain,
( ~ sQ143_spl
| value(in(n2,or1(h1(f))),n1) ),
inference(component_clause,[status(thm)],[f1043]) ).
fof(f1046,plain,
( ~ sQ88_spl
| sQ143_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1035,f1036,f1043,f671]) ).
fof(f1047,plain,
( sQ141_spl
| ~ type(f,fulladder) ),
inference(resolution,[status(thm)],[f1038,f99]) ).
fof(f1048,plain,
( sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1047,f110]) ).
fof(f1049,plain,
sQ141_spl,
inference(contradiction_clause,[status(thm)],[f1048]) ).
fof(f1087,plain,
! [X0] :
( value(in(n1,not1(h2(f))),X0)
| ~ value(out(n1,and2(h2(f))),X0) ),
inference(resolution,[status(thm)],[f483,f110]) ).
fof(f1088,plain,
! [X0] :
( value(in(n1,not1(h1(f))),X0)
| ~ value(out(n1,and2(h1(f))),X0) ),
inference(resolution,[status(thm)],[f484,f110]) ).
fof(f1089,plain,
( sQ138_spl
| ~ type(f,fulladder) ),
inference(resolution,[status(thm)],[f1022,f100]) ).
fof(f1090,plain,
( sQ138_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1089,f110]) ).
fof(f1091,plain,
sQ138_spl,
inference(contradiction_clause,[status(thm)],[f1090]) ).
fof(f1104,plain,
( sQ140_spl
| ~ value(out(s,f),n1) ),
inference(resolution,[status(thm)],[f1031,f170]) ).
fof(f1106,plain,
( sQ140_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1104,f114]) ).
fof(f1107,plain,
sQ140_spl,
inference(contradiction_clause,[status(thm)],[f1106]) ).
fof(f1108,plain,
! [X0] :
( value(in(n2,and1(h2(f))),X0)
| ~ value(out(n1,not1(h2(f))),X0) ),
inference(resolution,[status(thm)],[f542,f110]) ).
fof(f1109,plain,
! [X0] :
( value(in(n2,and1(h1(f))),X0)
| ~ value(out(n1,not1(h1(f))),X0) ),
inference(resolution,[status(thm)],[f543,f110]) ).
fof(f1148,plain,
! [X0] :
( value(out(n1,and1(h2(f))),X0)
| ~ value(out(s,h2(f)),X0) ),
inference(resolution,[status(thm)],[f653,f110]) ).
fof(f1188,plain,
value(out(n1,or1(f)),n0),
inference(resolution,[status(thm)],[f656,f115]) ).
fof(f1252,definition,
( sQ173_spl
<=> mode(or1(f),ok) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1254,plain,
( sQ173_spl
| ~ mode(or1(f),ok) ),
inference(component_clause,[status(thm)],[f1252]) ).
fof(f1255,definition,
( sQ174_spl
<=> type(or1(f),or) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1257,plain,
( sQ174_spl
| ~ type(or1(f),or) ),
inference(component_clause,[status(thm)],[f1255]) ).
fof(f1272,plain,
! [X0] :
( sQ173_spl
| mode(or1(f),abnormal)
| ~ type(or1(f),X0) ),
inference(resolution,[status(thm)],[f1254,f69]) ).
fof(f1273,definition,
! [X0] :
( sQ179_spl
<=> ~ type(or1(f),X0) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1274,plain,
! [X0] :
( ~ sQ179_spl
| ~ type(or1(f),X0) ),
inference(component_clause,[status(thm)],[f1273]) ).
fof(f1276,plain,
( sQ173_spl
| sQ0_spl
| sQ179_spl ),
inference(split_clause,[status(thm)],[f1272,f1273,f123,f1252]) ).
fof(f1277,plain,
( ~ sQ179_spl
| ~ type(f,fulladder) ),
inference(resolution,[status(thm)],[f1274,f101]) ).
fof(f1279,plain,
( ~ sQ179_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1277,f110]) ).
fof(f1280,plain,
~ sQ179_spl,
inference(contradiction_clause,[status(thm)],[f1279]) ).
fof(f1296,definition,
( sQ180_spl
<=> mode(or1(h1(f)),ok) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f1298,plain,
( sQ180_spl
| ~ mode(or1(h1(f)),ok) ),
inference(component_clause,[status(thm)],[f1296]) ).
fof(f1306,definition,
( sQ183_spl
<=> type(or1(h1(f)),or) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f1308,plain,
( sQ183_spl
| ~ type(or1(h1(f)),or) ),
inference(component_clause,[status(thm)],[f1306]) ).
fof(f1325,plain,
! [X0] :
( sQ180_spl
| mode(or1(h1(f)),abnormal)
| ~ type(or1(h1(f)),X0) ),
inference(resolution,[status(thm)],[f1298,f69]) ).
fof(f1326,definition,
! [X0] :
( sQ188_spl
<=> ~ type(or1(h1(f)),X0) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f1327,plain,
! [X0] :
( ~ sQ188_spl
| ~ type(or1(h1(f)),X0) ),
inference(component_clause,[status(thm)],[f1326]) ).
fof(f1329,definition,
( sQ189_spl
<=> mode(or1(h1(f)),abnormal) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f1330,plain,
( ~ sQ189_spl
| mode(or1(h1(f)),abnormal) ),
inference(component_clause,[status(thm)],[f1329]) ).
fof(f1332,plain,
( sQ180_spl
| sQ189_spl
| sQ188_spl ),
inference(split_clause,[status(thm)],[f1325,f1326,f1329,f1296]) ).
fof(f1333,plain,
( ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1330,f119]) ).
fof(f1334,plain,
~ sQ189_spl,
inference(contradiction_clause,[status(thm)],[f1333]) ).
fof(f1335,plain,
value(in(n1,and2(h2(f))),n1),
inference(resolution,[status(thm)],[f770,f231]) ).
fof(f1337,definition,
( sQ190_spl
<=> value(in(n1,and2(h2(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f1339,plain,
( sQ190_spl
| ~ value(in(n1,and2(h2(f))),n1) ),
inference(component_clause,[status(thm)],[f1337]) ).
fof(f1341,plain,
value(in(n1,and2(h1(f))),n0),
inference(resolution,[status(thm)],[f824,f677]) ).
fof(f1347,plain,
( sQ174_spl
| ~ type(f,fulladder) ),
inference(resolution,[status(thm)],[f1257,f101]) ).
fof(f1349,plain,
( sQ174_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1347,f110]) ).
fof(f1350,plain,
sQ174_spl,
inference(contradiction_clause,[status(thm)],[f1349]) ).
fof(f1356,plain,
( ~ sQ188_spl
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f1327,f89]) ).
fof(f1357,plain,
( ~ sQ188_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1356,f1036,f1326]) ).
fof(f1360,plain,
( sQ183_spl
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f1308,f89]) ).
fof(f1361,plain,
( sQ183_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1360,f1036,f1306]) ).
fof(f1377,definition,
! [X0] :
( sQ195_spl
<=> ~ value(in(X0,or1(h1(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1378,plain,
! [X0] :
( ~ sQ195_spl
| ~ value(in(X0,or1(h1(f))),n1) ),
inference(component_clause,[status(thm)],[f1377]) ).
fof(f1424,plain,
( value(in(n1,or1(f)),n0)
| ~ type(or1(f),or)
| ~ mode(or1(f),ok) ),
inference(resolution,[status(thm)],[f1188,f80]) ).
fof(f1432,definition,
( sQ204_spl
<=> value(in(n1,or1(f)),n0) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f1433,plain,
( ~ sQ204_spl
| value(in(n1,or1(f)),n0) ),
inference(component_clause,[status(thm)],[f1432]) ).
fof(f1435,plain,
( sQ204_spl
| ~ sQ174_spl
| ~ sQ173_spl ),
inference(split_clause,[status(thm)],[f1424,f1252,f1255,f1432]) ).
fof(f1443,plain,
! [X0] :
( ~ value(out(n1,and1(h1(f))),X0)
| ~ type(h1(f),halfadder)
| value(in(n2,h2(f)),X0) ),
inference(resolution,[status(thm)],[f813,f163]) ).
fof(f1444,definition,
! [X0] :
( sQ205_spl
<=> ( ~ value(out(n1,and1(h1(f))),X0)
| value(in(n2,h2(f)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f1445,plain,
! [X0] :
( ~ sQ205_spl
| ~ value(out(n1,and1(h1(f))),X0)
| value(in(n2,h2(f)),X0) ),
inference(component_clause,[status(thm)],[f1444]) ).
fof(f1447,plain,
( ~ sQ141_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f1443,f1444,f1036]) ).
fof(f1506,plain,
! [X0] :
( ~ value(in(X0,or1(h1(f))),n1)
| ~ type(or1(h1(f)),or)
| ~ mode(or1(h1(f)),ok)
| value(in(n1,and1(h1(f))),n1) ),
inference(resolution,[status(thm)],[f955,f77]) ).
fof(f1509,definition,
( sQ217_spl
<=> value(in(n1,and1(h1(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f1512,plain,
( sQ195_spl
| ~ sQ183_spl
| ~ sQ180_spl
| sQ217_spl ),
inference(split_clause,[status(thm)],[f1506,f1509,f1296,f1306,f1377]) ).
fof(f1522,plain,
( ~ value(in(n2,and2(h2(f))),n1)
| ~ value(in(n1,and2(h2(f))),n1)
| ~ type(and2(h2(f)),and)
| ~ mode(and2(h2(f)),ok)
| value(in(n1,not1(h2(f))),n1) ),
inference(resolution,[status(thm)],[f1087,f72]) ).
fof(f1524,definition,
( sQ220_spl
<=> value(in(n1,not1(h2(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f1525,plain,
( ~ sQ220_spl
| value(in(n1,not1(h2(f))),n1) ),
inference(component_clause,[status(thm)],[f1524]) ).
fof(f1527,definition,
( sQ221_spl
<=> mode(and2(h2(f)),ok) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f1529,plain,
( sQ221_spl
| ~ mode(and2(h2(f)),ok) ),
inference(component_clause,[status(thm)],[f1527]) ).
fof(f1537,definition,
( sQ224_spl
<=> type(and2(h2(f)),and) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f1539,plain,
( sQ224_spl
| ~ type(and2(h2(f)),and) ),
inference(component_clause,[status(thm)],[f1537]) ).
fof(f1540,definition,
( sQ225_spl
<=> value(in(n2,and2(h2(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f1543,plain,
( ~ sQ225_spl
| ~ sQ190_spl
| ~ sQ224_spl
| ~ sQ221_spl
| sQ220_spl ),
inference(split_clause,[status(thm)],[f1522,f1524,f1527,f1537,f1337,f1540]) ).
fof(f1556,plain,
! [X0] :
( sQ221_spl
| mode(and2(h2(f)),abnormal)
| ~ type(and2(h2(f)),X0) ),
inference(resolution,[status(thm)],[f1529,f69]) ).
fof(f1557,definition,
! [X0] :
( sQ228_spl
<=> ~ type(and2(h2(f)),X0) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f1558,plain,
! [X0] :
( ~ sQ228_spl
| ~ type(and2(h2(f)),X0) ),
inference(component_clause,[status(thm)],[f1557]) ).
fof(f1560,definition,
( sQ229_spl
<=> mode(and2(h2(f)),abnormal) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f1561,plain,
( ~ sQ229_spl
| mode(and2(h2(f)),abnormal) ),
inference(component_clause,[status(thm)],[f1560]) ).
fof(f1563,plain,
( sQ221_spl
| sQ229_spl
| sQ228_spl ),
inference(split_clause,[status(thm)],[f1556,f1557,f1560,f1527]) ).
fof(f1564,plain,
( ~ sQ229_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1561,f117]) ).
fof(f1565,plain,
~ sQ229_spl,
inference(contradiction_clause,[status(thm)],[f1564]) ).
fof(f1567,definition,
( sQ230_spl
<=> value(out(n1,and2(h2(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f1571,plain,
( ~ sQ228_spl
| ~ type(h2(f),halfadder) ),
inference(resolution,[status(thm)],[f1558,f87]) ).
fof(f1572,plain,
( ~ sQ228_spl
| ~ sQ138_spl ),
inference(split_clause,[status(thm)],[f1571,f1020,f1557]) ).
fof(f1576,plain,
! [X0] :
( value(out(n1,and2(h2(f))),X0)
| ~ type(h2(f),halfadder)
| ~ value(in(n1,or1(f)),X0) ),
inference(resolution,[status(thm)],[f943,f150]) ).
fof(f1578,definition,
! [X0] :
( sQ231_spl
<=> ( value(out(n1,and2(h2(f))),X0)
| ~ value(in(n1,or1(f)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f1579,plain,
! [X0] :
( ~ sQ231_spl
| value(out(n1,and2(h2(f))),X0)
| ~ value(in(n1,or1(f)),X0) ),
inference(component_clause,[status(thm)],[f1578]) ).
fof(f1581,plain,
( ~ sQ138_spl
| sQ231_spl ),
inference(split_clause,[status(thm)],[f1576,f1578,f1020]) ).
fof(f1583,plain,
( sQ224_spl
| ~ type(h2(f),halfadder) ),
inference(resolution,[status(thm)],[f1539,f87]) ).
fof(f1584,plain,
( sQ224_spl
| ~ sQ138_spl ),
inference(split_clause,[status(thm)],[f1583,f1020,f1537]) ).
fof(f1587,plain,
! [X0] :
( ~ value(in(X0,and2(h1(f))),n0)
| ~ type(and2(h1(f)),and)
| ~ mode(and2(h1(f)),ok)
| value(in(n1,not1(h1(f))),n0) ),
inference(resolution,[status(thm)],[f1088,f71]) ).
fof(f1591,definition,
( sQ233_spl
<=> mode(and2(h1(f)),ok) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f1593,plain,
( sQ233_spl
| ~ mode(and2(h1(f)),ok) ),
inference(component_clause,[status(thm)],[f1591]) ).
fof(f1601,definition,
( sQ236_spl
<=> type(and2(h1(f)),and) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f1603,plain,
( sQ236_spl
| ~ type(and2(h1(f)),and) ),
inference(component_clause,[status(thm)],[f1601]) ).
fof(f1605,definition,
( sQ237_spl
<=> value(in(n1,not1(h1(f))),n0) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f1606,plain,
( ~ sQ237_spl
| value(in(n1,not1(h1(f))),n0) ),
inference(component_clause,[status(thm)],[f1605]) ).
fof(f1608,definition,
! [X0] :
( sQ238_spl
<=> ~ value(in(X0,and2(h1(f))),n0) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f1609,plain,
! [X0] :
( ~ sQ238_spl
| ~ value(in(X0,and2(h1(f))),n0) ),
inference(component_clause,[status(thm)],[f1608]) ).
fof(f1611,plain,
( sQ238_spl
| ~ sQ236_spl
| ~ sQ233_spl
| sQ237_spl ),
inference(split_clause,[status(thm)],[f1587,f1605,f1591,f1601,f1608]) ).
fof(f1618,plain,
! [X0] :
( sQ233_spl
| mode(and2(h1(f)),abnormal)
| ~ type(and2(h1(f)),X0) ),
inference(resolution,[status(thm)],[f1593,f69]) ).
fof(f1619,definition,
! [X0] :
( sQ239_spl
<=> ~ type(and2(h1(f)),X0) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f1620,plain,
! [X0] :
( ~ sQ239_spl
| ~ type(and2(h1(f)),X0) ),
inference(component_clause,[status(thm)],[f1619]) ).
fof(f1622,definition,
( sQ240_spl
<=> mode(and2(h1(f)),abnormal) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f1623,plain,
( ~ sQ240_spl
| mode(and2(h1(f)),abnormal) ),
inference(component_clause,[status(thm)],[f1622]) ).
fof(f1625,plain,
( sQ233_spl
| sQ240_spl
| sQ239_spl ),
inference(split_clause,[status(thm)],[f1618,f1619,f1622,f1591]) ).
fof(f1626,plain,
( ~ sQ240_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1623,f121]) ).
fof(f1627,plain,
~ sQ240_spl,
inference(contradiction_clause,[status(thm)],[f1626]) ).
fof(f1634,definition,
( sQ242_spl
<=> mode(not1(h2(f)),ok) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f1635,plain,
( ~ sQ242_spl
| mode(not1(h2(f)),ok) ),
inference(component_clause,[status(thm)],[f1634]) ).
fof(f1636,plain,
( sQ242_spl
| ~ mode(not1(h2(f)),ok) ),
inference(component_clause,[status(thm)],[f1634]) ).
fof(f1661,definition,
( sQ249_spl
<=> value(in(n2,and1(h1(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f1664,definition,
( sQ250_spl
<=> mode(not1(h1(f)),ok) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f1666,plain,
( sQ250_spl
| ~ mode(not1(h1(f)),ok) ),
inference(component_clause,[status(thm)],[f1664]) ).
fof(f1695,plain,
( ~ sQ239_spl
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f1620,f87]) ).
fof(f1696,plain,
( ~ sQ239_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1695,f1036,f1619]) ).
fof(f1699,plain,
( sQ236_spl
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f1603,f87]) ).
fof(f1700,plain,
( sQ236_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1699,f1036,f1601]) ).
fof(f1701,plain,
! [X0] :
( sQ242_spl
| mode(not1(h2(f)),abnormal)
| ~ type(not1(h2(f)),X0) ),
inference(resolution,[status(thm)],[f1636,f69]) ).
fof(f1702,definition,
! [X0] :
( sQ258_spl
<=> ~ type(not1(h2(f)),X0) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f1703,plain,
! [X0] :
( ~ sQ258_spl
| ~ type(not1(h2(f)),X0) ),
inference(component_clause,[status(thm)],[f1702]) ).
fof(f1705,plain,
( sQ242_spl
| sQ1_spl
| sQ258_spl ),
inference(split_clause,[status(thm)],[f1701,f1702,f126,f1634]) ).
fof(f1718,plain,
( ~ sQ258_spl
| ~ type(h2(f),halfadder) ),
inference(resolution,[status(thm)],[f1703,f88]) ).
fof(f1719,plain,
( ~ sQ258_spl
| ~ sQ138_spl ),
inference(split_clause,[status(thm)],[f1718,f1020,f1702]) ).
fof(f1721,plain,
( ~ sQ242_spl
| ~ type(h2(f),halfadder)
| value(out(n1,not1(h2(f))),n0)
| ~ value(in(n1,not1(h2(f))),n1) ),
inference(resolution,[status(thm)],[f1635,f290]) ).
fof(f1726,definition,
( sQ260_spl
<=> value(out(n1,not1(h2(f))),n0) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f1727,plain,
( ~ sQ260_spl
| value(out(n1,not1(h2(f))),n0) ),
inference(component_clause,[status(thm)],[f1726]) ).
fof(f1729,plain,
( ~ sQ242_spl
| ~ sQ138_spl
| sQ260_spl
| ~ sQ220_spl ),
inference(split_clause,[status(thm)],[f1721,f1524,f1726,f1020,f1634]) ).
fof(f1730,plain,
! [X0] :
( sQ250_spl
| mode(not1(h1(f)),abnormal)
| ~ type(not1(h1(f)),X0) ),
inference(resolution,[status(thm)],[f1666,f69]) ).
fof(f1731,definition,
! [X0] :
( sQ261_spl
<=> ~ type(not1(h1(f)),X0) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f1732,plain,
! [X0] :
( ~ sQ261_spl
| ~ type(not1(h1(f)),X0) ),
inference(component_clause,[status(thm)],[f1731]) ).
fof(f1734,definition,
( sQ262_spl
<=> mode(not1(h1(f)),abnormal) ),
introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition]) ).
fof(f1735,plain,
( ~ sQ262_spl
| mode(not1(h1(f)),abnormal) ),
inference(component_clause,[status(thm)],[f1734]) ).
fof(f1737,plain,
( sQ250_spl
| sQ262_spl
| sQ261_spl ),
inference(split_clause,[status(thm)],[f1730,f1731,f1734,f1664]) ).
fof(f1738,plain,
( ~ sQ262_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1735,f120]) ).
fof(f1739,plain,
~ sQ262_spl,
inference(contradiction_clause,[status(thm)],[f1738]) ).
fof(f1742,definition,
( sQ263_spl
<=> value(out(n1,not1(h1(f))),n1) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f1743,plain,
( ~ sQ263_spl
| value(out(n1,not1(h1(f))),n1) ),
inference(component_clause,[status(thm)],[f1742]) ).
fof(f1754,plain,
( ~ sQ261_spl
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f1732,f88]) ).
fof(f1755,plain,
( ~ sQ261_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1754,f1036,f1731]) ).
fof(f1773,plain,
( ~ sQ140_spl
| value(out(n1,and1(h2(f))),n1) ),
inference(resolution,[status(thm)],[f1148,f1030]) ).
fof(f1810,plain,
( ~ sQ143_spl
| ~ sQ195_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1044,f1378]) ).
fof(f1814,plain,
( ~ sQ143_spl
| ~ sQ195_spl ),
inference(contradiction_clause,[status(thm)],[f1810]) ).
fof(f1851,plain,
( ~ sQ205_spl
| ~ value(in(n2,and1(h1(f))),n1)
| ~ value(in(n1,and1(h1(f))),n1)
| ~ type(and1(h1(f)),and)
| ~ mode(and1(h1(f)),ok)
| value(in(n2,h2(f)),n1) ),
inference(resolution,[status(thm)],[f1445,f72]) ).
fof(f1853,definition,
( sQ269_spl
<=> mode(and1(h1(f)),ok) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f1855,plain,
( sQ269_spl
| ~ mode(and1(h1(f)),ok) ),
inference(component_clause,[status(thm)],[f1853]) ).
fof(f1863,definition,
( sQ272_spl
<=> type(and1(h1(f)),and) ),
introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition]) ).
fof(f1865,plain,
( sQ272_spl
| ~ type(and1(h1(f)),and) ),
inference(component_clause,[status(thm)],[f1863]) ).
fof(f1866,plain,
( ~ sQ205_spl
| ~ sQ249_spl
| ~ sQ217_spl
| ~ sQ272_spl
| ~ sQ269_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f1851,f201,f1853,f1863,f1509,f1661,f1444]) ).
fof(f1941,plain,
! [X0] :
( sQ269_spl
| mode(and1(h1(f)),abnormal)
| ~ type(and1(h1(f)),X0) ),
inference(resolution,[status(thm)],[f1855,f69]) ).
fof(f1942,definition,
! [X0] :
( sQ282_spl
<=> ~ type(and1(h1(f)),X0) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f1943,plain,
! [X0] :
( ~ sQ282_spl
| ~ type(and1(h1(f)),X0) ),
inference(component_clause,[status(thm)],[f1942]) ).
fof(f1945,definition,
( sQ283_spl
<=> mode(and1(h1(f)),abnormal) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f1946,plain,
( ~ sQ283_spl
| mode(and1(h1(f)),abnormal) ),
inference(component_clause,[status(thm)],[f1945]) ).
fof(f1948,plain,
( sQ269_spl
| sQ283_spl
| sQ282_spl ),
inference(split_clause,[status(thm)],[f1941,f1942,f1945,f1853]) ).
fof(f1949,plain,
( ~ sQ283_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1946,f122]) ).
fof(f1950,plain,
~ sQ283_spl,
inference(contradiction_clause,[status(thm)],[f1949]) ).
fof(f1956,plain,
( ~ sQ282_spl
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f1943,f86]) ).
fof(f1957,plain,
( ~ sQ282_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1956,f1036,f1942]) ).
fof(f1958,plain,
( sQ272_spl
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f1865,f86]) ).
fof(f1959,plain,
( sQ272_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f1958,f1036,f1863]) ).
fof(f2024,plain,
( ~ sQ231_spl
| ~ sQ204_spl
| value(out(n1,and2(h2(f))),n0) ),
inference(resolution,[status(thm)],[f1433,f1579]) ).
fof(f2079,plain,
( ~ sQ238_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1341,f1609]) ).
fof(f2080,plain,
~ sQ238_spl,
inference(contradiction_clause,[status(thm)],[f2079]) ).
fof(f2119,definition,
( sQ293_spl
<=> mode(and1(h2(f)),ok) ),
introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition]) ).
fof(f2121,plain,
( sQ293_spl
| ~ mode(and1(h2(f)),ok) ),
inference(component_clause,[status(thm)],[f2119]) ).
fof(f2134,definition,
( sQ297_spl
<=> type(and1(h2(f)),and) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f2136,plain,
( sQ297_spl
| ~ type(and1(h2(f)),and) ),
inference(component_clause,[status(thm)],[f2134]) ).
fof(f2142,plain,
! [X0] :
( sQ293_spl
| mode(and1(h2(f)),abnormal)
| ~ type(and1(h2(f)),X0) ),
inference(resolution,[status(thm)],[f2121,f69]) ).
fof(f2143,definition,
! [X0] :
( sQ298_spl
<=> ~ type(and1(h2(f)),X0) ),
introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition]) ).
fof(f2144,plain,
! [X0] :
( ~ sQ298_spl
| ~ type(and1(h2(f)),X0) ),
inference(component_clause,[status(thm)],[f2143]) ).
fof(f2146,plain,
( sQ293_spl
| sQ2_spl
| sQ298_spl ),
inference(split_clause,[status(thm)],[f2142,f2143,f130,f2119]) ).
fof(f2149,plain,
( ~ sQ298_spl
| ~ type(h2(f),halfadder) ),
inference(resolution,[status(thm)],[f2144,f86]) ).
fof(f2150,plain,
( ~ sQ298_spl
| ~ sQ138_spl ),
inference(split_clause,[status(thm)],[f2149,f1020,f2143]) ).
fof(f2151,plain,
( sQ297_spl
| ~ type(h2(f),halfadder) ),
inference(resolution,[status(thm)],[f2136,f86]) ).
fof(f2152,plain,
( sQ297_spl
| ~ sQ138_spl ),
inference(split_clause,[status(thm)],[f2151,f1020,f2134]) ).
fof(f2182,definition,
! [X0] :
( sQ302_spl
<=> ~ value(in(X0,and1(h2(f))),n0) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f2183,plain,
! [X0] :
( ~ sQ302_spl
| ~ value(in(X0,and1(h2(f))),n0) ),
inference(component_clause,[status(thm)],[f2182]) ).
fof(f2267,plain,
( ~ sQ260_spl
| value(in(n2,and1(h2(f))),n0) ),
inference(resolution,[status(thm)],[f1727,f1108]) ).
fof(f2273,plain,
( ~ sQ260_spl
| ~ sQ302_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2267,f2183]) ).
fof(f2274,plain,
( ~ sQ260_spl
| ~ sQ302_spl ),
inference(contradiction_clause,[status(thm)],[f2273]) ).
fof(f2291,definition,
( sQ307_spl
<=> type(not1(h1(f)),not) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f2293,plain,
( sQ307_spl
| ~ type(not1(h1(f)),not) ),
inference(component_clause,[status(thm)],[f2291]) ).
fof(f2301,plain,
( sQ307_spl
| ~ type(h1(f),halfadder) ),
inference(resolution,[status(thm)],[f2293,f88]) ).
fof(f2302,plain,
( sQ307_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f2301,f1036,f2291]) ).
fof(f2321,plain,
! [X0] :
( ~ sQ140_spl
| ~ value(in(X0,and1(h2(f))),n0)
| ~ type(and1(h2(f)),and)
| ~ mode(and1(h2(f)),ok) ),
inference(resolution,[status(thm)],[f1773,f144]) ).
fof(f2325,plain,
( ~ sQ140_spl
| sQ302_spl
| ~ sQ297_spl
| ~ sQ293_spl ),
inference(split_clause,[status(thm)],[f2321,f2119,f2134,f2182,f1029]) ).
fof(f2483,plain,
( ~ sQ10_spl
| value(in(n2,and2(h2(f))),n1)
| ~ type(h2(f),halfadder) ),
inference(resolution,[status(thm)],[f202,f148]) ).
fof(f2489,plain,
( ~ sQ10_spl
| sQ225_spl
| ~ sQ138_spl ),
inference(split_clause,[status(thm)],[f2483,f1020,f1540,f201]) ).
fof(f2491,plain,
( sQ190_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1339,f1335]) ).
fof(f2492,plain,
sQ190_spl,
inference(contradiction_clause,[status(thm)],[f2491]) ).
fof(f2527,plain,
( ~ sQ237_spl
| value(out(n1,not1(h1(f))),n1)
| ~ type(not1(h1(f)),not)
| ~ mode(not1(h1(f)),ok) ),
inference(resolution,[status(thm)],[f1606,f82]) ).
fof(f2534,plain,
( ~ sQ237_spl
| sQ263_spl
| ~ sQ307_spl
| ~ sQ250_spl ),
inference(split_clause,[status(thm)],[f2527,f1664,f2291,f1742,f1605]) ).
fof(f2604,plain,
( ~ sQ220_spl
| value(out(n1,and2(h2(f))),n1)
| ~ type(h2(f),halfadder) ),
inference(resolution,[status(thm)],[f1525,f159]) ).
fof(f2606,plain,
( ~ sQ220_spl
| sQ230_spl
| ~ sQ138_spl ),
inference(split_clause,[status(thm)],[f2604,f1020,f1567,f1524]) ).
fof(f2668,plain,
( ~ sQ231_spl
| ~ sQ204_spl
| ~ value(out(n1,and2(h2(f))),n1) ),
inference(resolution,[status(thm)],[f2024,f134]) ).
fof(f2680,plain,
( ~ sQ231_spl
| ~ sQ204_spl
| ~ sQ230_spl ),
inference(split_clause,[status(thm)],[f2668,f1567,f1432,f1578]) ).
fof(f2821,plain,
( ~ sQ263_spl
| value(in(n2,and1(h1(f))),n1) ),
inference(resolution,[status(thm)],[f1743,f1109]) ).
fof(f2825,plain,
( ~ sQ263_spl
| sQ249_spl ),
inference(split_clause,[status(thm)],[f2821,f1661,f1742]) ).
fof(f2829,plain,
$false,
inference(sat_refutation,[status(thm)],[f129,f133,f1015,f1046,f1049,f1091,f1107,f1276,f1280,f1332,f1334,f1350,f1357,f1361,f1435,f1447,f1512,f1543,f1563,f1565,f1572,f1581,f1584,f1611,f1625,f1627,f1696,f1700,f1705,f1719,f1729,f1737,f1739,f1755,f1814,f1866,f1948,f1950,f1957,f1959,f2080,f2146,f2150,f2152,f2274,f2302,f2325,f2489,f2492,f2534,f2606,f2680,f2825]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV006-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n017.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 : Sun Sep 20 20:42:26 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.50/0.55 % Refutation found
% 0.50/0.55 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.50/0.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.50/0.58 % Elapsed time: 0.196043 seconds
% 0.50/0.58 % CPU time: 1.253852 seconds
% 0.50/0.58 % Total memory used: 31.719 MB
% 0.50/0.58 % Net memory used: 30.602 MB
%------------------------------------------------------------------------------