%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV007-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 12:46:39 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV007-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n026.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 20:50:37 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.39 % Refutation found
% 0.10/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.39 fof(f1,axiom,(
% 0.10/0.39 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P1,V)| value(P2,V) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f2,axiom,(
% 0.10/0.39 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P2,V)| value(P1,V) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f3,axiom,(
% 0.10/0.39 (![P,V1,V2]: (( ~ value(P,V1)| ~ value(P,V2)| equal_value(V1,V2) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f4,axiom,(
% 0.10/0.39 ~ equal_value(n0,n1) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f5,axiom,(
% 0.10/0.39 ~ equal_value(n1,n0) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f7,axiom,(
% 0.10/0.39 (![K,Any]: (( ~ type(K,Any)| mode(K,ok)| mode(K,abnormal) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f8,axiom,(
% 0.10/0.39 (![K,Any]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(in(Any,K),n0)| value(out(n1,K),n0) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f9,axiom,(
% 0.10/0.39 (![K]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(in(n1,K),n1)| ~ value(in(n2,K),n1)| value(out(n1,K),n1) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f13,axiom,(
% 0.10/0.39 (![K,Any]: (( ~ mode(K,ok)| ~ type(K,or)| ~ value(in(Any,K),n1)| value(out(n1,K),n1) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f14,axiom,(
% 0.10/0.39 (![K]: (( ~ mode(K,ok)| ~ type(K,or)| ~ value(in(n1,K),n0)| ~ value(in(n2,K),n0)| value(out(n1,K),n0) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f19,axiom,(
% 0.10/0.39 (![K]: (( ~ mode(K,ok)| ~ type(K,not)| ~ value(in(n1,K),n1)| value(out(n1,K),n0) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f22,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| type(and1(X),and) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f23,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| type(and2(X),and) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f24,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| type(not1(X),not) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f25,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| type(or1(X),or) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f26,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(in(n1,X),in(n1,or1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f27,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(in(n2,X),in(n2,or1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f28,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(in(n1,X),in(n1,and2(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f29,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(in(n2,X),in(n2,and2(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f30,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(out(s,X),out(n1,and1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f31,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(out(c,X),out(n1,and2(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f32,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(out(n1,or1(X)),in(n1,and1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f33,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(out(n1,and2(X)),in(n1,not1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f34,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,halfadder)| connection(out(n1,not1(X)),in(n2,and1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f35,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| type(h1(X),halfadder) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f36,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| type(h2(X),halfadder) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f37,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| type(or1(X),or) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f38,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| connection(out(s,h1(X)),in(n2,h2(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f39,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| connection(out(c,h1(X)),in(n2,or1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f41,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| connection(in(n1,X),in(n1,h2(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f42,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| connection(in(n2,X),in(n1,h1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f43,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| connection(in(c,X),in(n2,h1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f44,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| connection(out(s,X),out(s,h2(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f45,axiom,(
% 0.10/0.39 (![X]: (( ~ type(X,fulladder)| connection(out(c,X),out(n1,or1(X))) ) ))),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f46,hypothesis,(
% 0.10/0.39 type(f,fulladder) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f47,hypothesis,(
% 0.10/0.39 value(in(n1,f),n0) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f48,hypothesis,(
% 0.10/0.39 value(in(n2,f),n1) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f49,hypothesis,(
% 0.10/0.39 value(in(c,f),n1) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f50,hypothesis,(
% 0.10/0.39 value(out(s,f),n1) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f51,hypothesis,(
% 0.10/0.39 value(out(c,f),n0) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f52,negated_conjecture,(
% 0.10/0.39 ~ mode(and2(h1(f)),abnormal) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f53,negated_conjecture,(
% 0.10/0.39 ( ~ mode(or1(f),abnormal)| ~ mode(and1(h1(f)),abnormal) ) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f54,negated_conjecture,(
% 0.10/0.39 ( ~ mode(or1(f),abnormal)| ~ mode(not1(h1(f)),abnormal) ) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f55,negated_conjecture,(
% 0.10/0.39 ( ~ mode(or1(f),abnormal)| ~ mode(and1(h2(f)),abnormal) ) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f56,negated_conjecture,(
% 0.10/0.39 ( ~ mode(or1(f),abnormal)| ~ mode(or1(h2(f)),abnormal) ) ),
% 0.10/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.39 fof(f57,plain,(
% 0.10/0.39 ![P2,V]: ((![P1]: (~connection(P1,P2)|~value(P1,V)))|value(P2,V))),
% 0.10/0.39 inference(miniscoping,[status(thm)],[f1])).
% 0.10/0.39 fof(f58,plain,(
% 0.10/0.39 ![X0,X1,X2]: (~connection(X0,X1)|~value(X0,X2)|value(X1,X2))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f57])).
% 0.10/0.39 fof(f59,plain,(
% 0.10/0.39 ![P1,V]: ((![P2]: (~connection(P1,P2)|~value(P2,V)))|value(P1,V))),
% 0.10/0.39 inference(miniscoping,[status(thm)],[f2])).
% 0.10/0.39 fof(f60,plain,(
% 0.10/0.39 ![X0,X1,X2]: (~connection(X0,X1)|~value(X1,X2)|value(X0,X2))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f59])).
% 0.10/0.39 fof(f61,plain,(
% 0.10/0.39 ![V1,V2]: ((![P]: (~value(P,V1)|~value(P,V2)))|equal_value(V1,V2))),
% 0.10/0.39 inference(miniscoping,[status(thm)],[f3])).
% 0.10/0.39 fof(f62,plain,(
% 0.10/0.39 ![X0,X1,X2]: (~value(X0,X1)|~value(X0,X2)|equal_value(X1,X2))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f61])).
% 0.10/0.39 fof(f63,plain,(
% 0.10/0.39 ~equal_value(n0,n1)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.39 fof(f64,plain,(
% 0.10/0.39 ~equal_value(n1,n0)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.39 fof(f66,plain,(
% 0.10/0.39 ![K]: (((![Any]: ~type(K,Any))|mode(K,ok))|mode(K,abnormal))),
% 0.10/0.39 inference(miniscoping,[status(thm)],[f7])).
% 0.10/0.39 fof(f67,plain,(
% 0.10/0.39 ![X0,X1]: (~type(X0,X1)|mode(X0,ok)|mode(X0,abnormal))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f66])).
% 0.10/0.39 fof(f68,plain,(
% 0.10/0.39 ![K]: (((~mode(K,ok)|~type(K,and))|(![Any]: ~value(in(Any,K),n0)))|value(out(n1,K),n0))),
% 0.10/0.39 inference(miniscoping,[status(thm)],[f8])).
% 0.10/0.39 fof(f69,plain,(
% 0.10/0.39 ![X0,X1]: (~mode(X0,ok)|~type(X0,and)|~value(in(X1,X0),n0)|value(out(n1,X0),n0))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f68])).
% 0.10/0.39 fof(f70,plain,(
% 0.10/0.39 ![X0]: (~mode(X0,ok)|~type(X0,and)|~value(in(n1,X0),n1)|~value(in(n2,X0),n1)|value(out(n1,X0),n1))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/0.39 fof(f74,plain,(
% 0.10/0.39 ![K]: (((~mode(K,ok)|~type(K,or))|(![Any]: ~value(in(Any,K),n1)))|value(out(n1,K),n1))),
% 0.10/0.39 inference(miniscoping,[status(thm)],[f13])).
% 0.10/0.39 fof(f75,plain,(
% 0.10/0.39 ![X0,X1]: (~mode(X0,ok)|~type(X0,or)|~value(in(X1,X0),n1)|value(out(n1,X0),n1))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f74])).
% 0.10/0.39 fof(f76,plain,(
% 0.10/0.39 ![X0]: (~mode(X0,ok)|~type(X0,or)|~value(in(n1,X0),n0)|~value(in(n2,X0),n0)|value(out(n1,X0),n0))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.39 fof(f81,plain,(
% 0.10/0.39 ![X0]: (~mode(X0,ok)|~type(X0,not)|~value(in(n1,X0),n1)|value(out(n1,X0),n0))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f19])).
% 0.10/0.39 fof(f84,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|type(and1(X0),and))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.39 fof(f85,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|type(and2(X0),and))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f23])).
% 0.10/0.39 fof(f86,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|type(not1(X0),not))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f24])).
% 0.10/0.39 fof(f87,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|type(or1(X0),or))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f25])).
% 0.10/0.39 fof(f88,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(in(n1,X0),in(n1,or1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f26])).
% 0.10/0.39 fof(f89,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(in(n2,X0),in(n2,or1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f27])).
% 0.10/0.39 fof(f90,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(in(n1,X0),in(n1,and2(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f28])).
% 0.10/0.39 fof(f91,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(in(n2,X0),in(n2,and2(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f29])).
% 0.10/0.39 fof(f92,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(out(s,X0),out(n1,and1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f30])).
% 0.10/0.39 fof(f93,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(out(c,X0),out(n1,and2(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f31])).
% 0.10/0.39 fof(f94,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(out(n1,or1(X0)),in(n1,and1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f32])).
% 0.10/0.39 fof(f95,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(out(n1,and2(X0)),in(n1,not1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f33])).
% 0.10/0.39 fof(f96,plain,(
% 0.10/0.39 ![X0]: (~type(X0,halfadder)|connection(out(n1,not1(X0)),in(n2,and1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f34])).
% 0.10/0.39 fof(f97,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|type(h1(X0),halfadder))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f35])).
% 0.10/0.39 fof(f98,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|type(h2(X0),halfadder))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f36])).
% 0.10/0.39 fof(f99,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|type(or1(X0),or))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f37])).
% 0.10/0.39 fof(f100,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|connection(out(s,h1(X0)),in(n2,h2(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f38])).
% 0.10/0.39 fof(f101,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|connection(out(c,h1(X0)),in(n2,or1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f39])).
% 0.10/0.39 fof(f103,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|connection(in(n1,X0),in(n1,h2(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f41])).
% 0.10/0.39 fof(f104,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|connection(in(n2,X0),in(n1,h1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.10/0.39 fof(f105,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|connection(in(c,X0),in(n2,h1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/0.39 fof(f106,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|connection(out(s,X0),out(s,h2(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.39 fof(f107,plain,(
% 0.10/0.39 ![X0]: (~type(X0,fulladder)|connection(out(c,X0),out(n1,or1(X0))))),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f45])).
% 0.10/0.39 fof(f108,plain,(
% 0.10/0.39 type(f,fulladder)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f46])).
% 0.10/0.39 fof(f109,plain,(
% 0.10/0.39 value(in(n1,f),n0)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f47])).
% 0.10/0.39 fof(f110,plain,(
% 0.10/0.39 value(in(n2,f),n1)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f48])).
% 0.10/0.39 fof(f111,plain,(
% 0.10/0.39 value(in(c,f),n1)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f49])).
% 0.10/0.39 fof(f112,plain,(
% 0.10/0.39 value(out(s,f),n1)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f50])).
% 0.10/0.39 fof(f113,plain,(
% 0.10/0.39 value(out(c,f),n0)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f51])).
% 0.10/0.39 fof(f114,plain,(
% 0.10/0.39 ~mode(and2(h1(f)),abnormal)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f52])).
% 0.10/0.39 fof(f115,plain,(
% 0.10/0.39 ~mode(or1(f),abnormal)|~mode(and1(h1(f)),abnormal)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f53])).
% 0.10/0.39 fof(f116,plain,(
% 0.10/0.39 ~mode(or1(f),abnormal)|~mode(not1(h1(f)),abnormal)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f54])).
% 0.10/0.39 fof(f117,plain,(
% 0.10/0.39 ~mode(or1(f),abnormal)|~mode(and1(h2(f)),abnormal)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f55])).
% 0.10/0.39 fof(f118,plain,(
% 0.10/0.39 ~mode(or1(f),abnormal)|~mode(or1(h2(f)),abnormal)),
% 0.10/0.39 inference(cnf_transformation,[status(thm)],[f56])).
% 0.10/0.39 fof(f119,definition,(
% 0.10/0.39 sQ0_spl <=> (mode(or1(f),abnormal))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f122,definition,(
% 0.10/0.39 sQ1_spl <=> (mode(and1(h1(f)),abnormal))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f125,plain,(
% 0.10/0.39 ~sQ0_spl|~sQ1_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f115,f119,f122])).
% 0.10/0.39 fof(f126,definition,(
% 0.10/0.39 sQ2_spl <=> (mode(not1(h1(f)),abnormal))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f129,plain,(
% 0.10/0.39 ~sQ0_spl|~sQ2_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f116,f119,f126])).
% 0.10/0.39 fof(f130,definition,(
% 0.10/0.39 sQ3_spl <=> (mode(and1(h2(f)),abnormal))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f133,plain,(
% 0.10/0.39 ~sQ0_spl|~sQ3_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f117,f119,f130])).
% 0.10/0.39 fof(f134,definition,(
% 0.10/0.39 sQ4_spl <=> (mode(or1(h2(f)),abnormal))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f137,plain,(
% 0.10/0.39 ~sQ0_spl|~sQ4_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f118,f119,f134])).
% 0.10/0.39 fof(f138,plain,(
% 0.10/0.39 ![X0]: (~connection(out(c,f),X0)|value(X0,n0))),
% 0.10/0.39 inference(resolution,[status(thm)],[f58,f113])).
% 0.10/0.39 fof(f139,plain,(
% 0.10/0.39 ![X0]: (~connection(out(s,f),X0)|value(X0,n1))),
% 0.10/0.39 inference(resolution,[status(thm)],[f58,f112])).
% 0.10/0.39 fof(f140,plain,(
% 0.10/0.39 ![X0]: (~connection(in(c,f),X0)|value(X0,n1))),
% 0.10/0.39 inference(resolution,[status(thm)],[f58,f111])).
% 0.10/0.39 fof(f141,plain,(
% 0.10/0.39 ![X0]: (~connection(in(n2,f),X0)|value(X0,n1))),
% 0.10/0.39 inference(resolution,[status(thm)],[f58,f110])).
% 0.10/0.39 fof(f142,plain,(
% 0.10/0.39 ![X0]: (~connection(in(n1,f),X0)|value(X0,n0))),
% 0.10/0.39 inference(resolution,[status(thm)],[f58,f109])).
% 0.10/0.39 fof(f162,plain,(
% 0.10/0.39 type(h1(f),halfadder)),
% 0.10/0.39 inference(resolution,[status(thm)],[f97,f108])).
% 0.10/0.39 fof(f164,plain,(
% 0.10/0.39 type(not1(h1(f)),not)),
% 0.10/0.39 inference(resolution,[status(thm)],[f162,f86])).
% 0.10/0.39 fof(f165,plain,(
% 0.10/0.39 type(and2(h1(f)),and)),
% 0.10/0.39 inference(resolution,[status(thm)],[f162,f85])).
% 0.10/0.39 fof(f166,plain,(
% 0.10/0.39 type(and1(h1(f)),and)),
% 0.10/0.39 inference(resolution,[status(thm)],[f162,f84])).
% 0.10/0.39 fof(f177,plain,(
% 0.10/0.39 connection(in(n1,h1(f)),in(n1,and2(h1(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f90,f162])).
% 0.10/0.39 fof(f178,plain,(
% 0.10/0.39 connection(in(n2,h1(f)),in(n2,and2(h1(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f91,f162])).
% 0.10/0.39 fof(f179,plain,(
% 0.10/0.39 connection(out(c,h1(f)),out(n1,and2(h1(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f93,f162])).
% 0.10/0.39 fof(f180,plain,(
% 0.10/0.39 mode(not1(h1(f)),ok)|mode(not1(h1(f)),abnormal)),
% 0.10/0.39 inference(resolution,[status(thm)],[f164,f67])).
% 0.10/0.39 fof(f181,definition,(
% 0.10/0.39 sQ9_spl <=> (mode(not1(h1(f)),ok))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f184,plain,(
% 0.10/0.39 sQ9_spl|sQ2_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f180,f181,f126])).
% 0.10/0.39 fof(f185,plain,(
% 0.10/0.39 mode(and2(h1(f)),ok)|mode(and2(h1(f)),abnormal)),
% 0.10/0.39 inference(resolution,[status(thm)],[f165,f67])).
% 0.10/0.39 fof(f186,definition,(
% 0.10/0.39 sQ10_spl <=> (mode(and2(h1(f)),ok))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f189,definition,(
% 0.10/0.39 sQ11_spl <=> (mode(and2(h1(f)),abnormal))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f190,plain,(
% 0.10/0.39 mode(and2(h1(f)),abnormal)|~sQ11_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f189])).
% 0.10/0.39 fof(f192,plain,(
% 0.10/0.39 sQ10_spl|sQ11_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f185,f186,f189])).
% 0.10/0.39 fof(f193,plain,(
% 0.10/0.39 mode(and1(h1(f)),ok)|mode(and1(h1(f)),abnormal)),
% 0.10/0.39 inference(resolution,[status(thm)],[f166,f67])).
% 0.10/0.39 fof(f194,definition,(
% 0.10/0.39 sQ12_spl <=> (mode(and1(h1(f)),ok))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f197,plain,(
% 0.10/0.39 sQ12_spl|sQ1_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f193,f194,f122])).
% 0.10/0.39 fof(f201,plain,(
% 0.10/0.39 type(h2(f),halfadder)),
% 0.10/0.39 inference(resolution,[status(thm)],[f98,f108])).
% 0.10/0.39 fof(f205,plain,(
% 0.10/0.39 connection(in(n2,h2(f)),in(n2,or1(h2(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f201,f89])).
% 0.10/0.39 fof(f206,plain,(
% 0.10/0.39 connection(in(n1,h2(f)),in(n1,or1(h2(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f201,f88])).
% 0.10/0.39 fof(f209,plain,(
% 0.10/0.39 type(and1(h2(f)),and)),
% 0.10/0.39 inference(resolution,[status(thm)],[f201,f84])).
% 0.10/0.39 fof(f235,plain,(
% 0.10/0.39 mode(and1(h2(f)),ok)|mode(and1(h2(f)),abnormal)),
% 0.10/0.39 inference(resolution,[status(thm)],[f209,f67])).
% 0.10/0.39 fof(f236,definition,(
% 0.10/0.39 sQ19_spl <=> (mode(and1(h2(f)),ok))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f239,plain,(
% 0.10/0.39 sQ19_spl|sQ3_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f235,f236,f130])).
% 0.10/0.39 fof(f240,plain,(
% 0.10/0.39 connection(out(n1,or1(h2(f))),in(n1,and1(h2(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f94,f201])).
% 0.10/0.39 fof(f243,plain,(
% 0.10/0.39 connection(out(n1,and2(h1(f))),in(n1,not1(h1(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f95,f162])).
% 0.10/0.39 fof(f245,plain,(
% 0.10/0.39 connection(out(n1,not1(h1(f))),in(n2,and1(h1(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f96,f162])).
% 0.10/0.39 fof(f247,plain,(
% 0.10/0.39 connection(in(n1,f),in(n1,h2(f)))),
% 0.10/0.39 inference(resolution,[status(thm)],[f103,f108])).
% 0.10/0.39 fof(f248,plain,(
% 0.10/0.39 connection(in(n2,f),in(n1,h1(f)))),
% 0.10/0.39 inference(resolution,[status(thm)],[f104,f108])).
% 0.10/0.39 fof(f254,plain,(
% 0.10/0.39 value(in(n1,h2(f)),n0)),
% 0.10/0.39 inference(resolution,[status(thm)],[f247,f142])).
% 0.10/0.39 fof(f257,plain,(
% 0.10/0.39 ![X0]: (~connection(in(n1,h2(f)),X0)|value(X0,n0))),
% 0.10/0.39 inference(resolution,[status(thm)],[f254,f58])).
% 0.10/0.39 fof(f258,plain,(
% 0.10/0.39 value(in(n1,h1(f)),n1)),
% 0.10/0.39 inference(resolution,[status(thm)],[f248,f141])).
% 0.10/0.39 fof(f261,plain,(
% 0.10/0.39 ![X0]: (~connection(in(n1,h1(f)),X0)|value(X0,n1))),
% 0.10/0.39 inference(resolution,[status(thm)],[f258,f58])).
% 0.10/0.39 fof(f267,plain,(
% 0.10/0.39 value(in(n1,and2(h1(f))),n1)),
% 0.10/0.39 inference(resolution,[status(thm)],[f177,f261])).
% 0.10/0.39 fof(f269,plain,(
% 0.10/0.39 value(in(n1,or1(h2(f))),n0)),
% 0.10/0.39 inference(resolution,[status(thm)],[f206,f257])).
% 0.10/0.39 fof(f284,plain,(
% 0.10/0.39 type(or1(h2(f)),or)),
% 0.10/0.39 inference(resolution,[status(thm)],[f87,f201])).
% 0.10/0.39 fof(f286,plain,(
% 0.10/0.39 mode(or1(h2(f)),ok)|mode(or1(h2(f)),abnormal)),
% 0.10/0.39 inference(resolution,[status(thm)],[f284,f67])).
% 0.10/0.39 fof(f287,definition,(
% 0.10/0.39 sQ20_spl <=> (mode(or1(h2(f)),ok))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f290,plain,(
% 0.10/0.39 sQ20_spl|sQ4_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f286,f287,f134])).
% 0.10/0.39 fof(f315,definition,(
% 0.10/0.39 sQ26_spl <=> (value(out(n1,or1(h2(f))),n0))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f316,plain,(
% 0.10/0.39 value(out(n1,or1(h2(f))),n0)|~sQ26_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f315])).
% 0.10/0.39 fof(f333,plain,(
% 0.10/0.39 ~mode(and2(h1(f)),ok)|~type(and2(h1(f)),and)|~value(in(n2,and2(h1(f))),n1)|value(out(n1,and2(h1(f))),n1)),
% 0.10/0.39 inference(resolution,[status(thm)],[f70,f267])).
% 0.10/0.39 fof(f336,definition,(
% 0.10/0.39 sQ31_spl <=> (type(and2(h1(f)),and))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f338,plain,(
% 0.10/0.39 ~type(and2(h1(f)),and)|sQ31_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f336])).
% 0.10/0.39 fof(f339,definition,(
% 0.10/0.39 sQ32_spl <=> (value(in(n2,and2(h1(f))),n1))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f341,plain,(
% 0.10/0.39 ~value(in(n2,and2(h1(f))),n1)|sQ32_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f339])).
% 0.10/0.39 fof(f342,definition,(
% 0.10/0.39 sQ33_spl <=> (value(out(n1,and2(h1(f))),n1))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f343,plain,(
% 0.10/0.39 value(out(n1,and2(h1(f))),n1)|~sQ33_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f342])).
% 0.10/0.39 fof(f345,plain,(
% 0.10/0.39 ~sQ10_spl|~sQ31_spl|~sQ32_spl|sQ33_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f333,f186,f336,f339,f342])).
% 0.10/0.39 fof(f366,plain,(
% 0.10/0.39 $false|~sQ11_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f190,f114])).
% 0.10/0.39 fof(f367,plain,(
% 0.10/0.39 ~sQ11_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f366])).
% 0.10/0.39 fof(f368,plain,(
% 0.10/0.39 $false|sQ31_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f338,f165])).
% 0.10/0.39 fof(f369,plain,(
% 0.10/0.39 sQ31_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f368])).
% 0.10/0.39 fof(f432,plain,(
% 0.10/0.39 ![X0]: (~connection(out(n1,or1(h2(f))),X0)|value(X0,n0)|~sQ26_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f316,f58])).
% 0.10/0.39 fof(f436,definition,(
% 0.10/0.39 sQ47_spl <=> (value(in(n2,or1(h2(f))),n0))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f471,plain,(
% 0.10/0.39 type(or1(f),or)),
% 0.10/0.39 inference(resolution,[status(thm)],[f99,f108])).
% 0.10/0.39 fof(f472,plain,(
% 0.10/0.39 mode(or1(f),ok)|mode(or1(f),abnormal)),
% 0.10/0.39 inference(resolution,[status(thm)],[f471,f67])).
% 0.10/0.39 fof(f473,definition,(
% 0.10/0.39 sQ52_spl <=> (mode(or1(f),ok))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f476,plain,(
% 0.10/0.39 sQ52_spl|sQ0_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f472,f473,f119])).
% 0.10/0.39 fof(f503,plain,(
% 0.10/0.39 ![X0]: (~connection(X0,out(n1,and2(h1(f))))|value(X0,n1)|~sQ33_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f343,f60])).
% 0.10/0.39 fof(f504,plain,(
% 0.10/0.39 ![X0]: (~connection(out(n1,and2(h1(f))),X0)|value(X0,n1)|~sQ33_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f343,f58])).
% 0.10/0.39 fof(f512,plain,(
% 0.10/0.39 ~mode(or1(h2(f)),ok)|~type(or1(h2(f)),or)|~value(in(n2,or1(h2(f))),n0)|value(out(n1,or1(h2(f))),n0)),
% 0.10/0.39 inference(resolution,[status(thm)],[f76,f269])).
% 0.10/0.39 fof(f519,definition,(
% 0.10/0.39 sQ58_spl <=> (type(or1(h2(f)),or))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f521,plain,(
% 0.10/0.39 ~type(or1(h2(f)),or)|sQ58_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f519])).
% 0.10/0.39 fof(f522,plain,(
% 0.10/0.39 ~sQ20_spl|~sQ58_spl|~sQ47_spl|sQ26_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f512,f287,f519,f436,f315])).
% 0.10/0.39 fof(f528,plain,(
% 0.10/0.39 $false|sQ58_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f521,f284])).
% 0.10/0.39 fof(f529,plain,(
% 0.10/0.39 sQ58_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f528])).
% 0.10/0.39 fof(f536,plain,(
% 0.10/0.39 value(in(n1,and1(h2(f))),n0)|~sQ26_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f432,f240])).
% 0.10/0.39 fof(f538,plain,(
% 0.10/0.39 ~mode(and1(h2(f)),ok)|~type(and1(h2(f)),and)|value(out(n1,and1(h2(f))),n0)|~sQ26_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f536,f69])).
% 0.10/0.39 fof(f548,definition,(
% 0.10/0.39 sQ62_spl <=> (value(out(n1,and1(h2(f))),n0))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f549,plain,(
% 0.10/0.39 value(out(n1,and1(h2(f))),n0)|~sQ62_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f548])).
% 0.10/0.39 fof(f552,definition,(
% 0.10/0.39 sQ63_spl <=> (type(and1(h2(f)),and))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f554,plain,(
% 0.10/0.39 ~type(and1(h2(f)),and)|sQ63_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f552])).
% 0.10/0.39 fof(f555,plain,(
% 0.10/0.39 ~sQ19_spl|~sQ63_spl|sQ62_spl|~sQ26_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f538,f236,f552,f548,f315])).
% 0.10/0.39 fof(f556,plain,(
% 0.10/0.39 $false|sQ63_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f554,f209])).
% 0.10/0.39 fof(f557,plain,(
% 0.10/0.39 sQ63_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f556])).
% 0.10/0.39 fof(f563,plain,(
% 0.10/0.39 ![X0]: (~connection(X0,out(n1,and1(h2(f))))|value(X0,n0)|~sQ62_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f549,f60])).
% 0.10/0.39 fof(f729,plain,(
% 0.10/0.39 connection(out(s,h2(f)),out(n1,and1(h2(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f92,f201])).
% 0.10/0.39 fof(f730,plain,(
% 0.10/0.39 connection(out(s,h1(f)),out(n1,and1(h1(f))))),
% 0.10/0.39 inference(resolution,[status(thm)],[f92,f162])).
% 0.10/0.39 fof(f736,plain,(
% 0.10/0.39 connection(out(s,h1(f)),in(n2,h2(f)))),
% 0.10/0.39 inference(resolution,[status(thm)],[f100,f108])).
% 0.10/0.39 fof(f737,plain,(
% 0.10/0.39 connection(out(c,h1(f)),in(n2,or1(f)))),
% 0.10/0.39 inference(resolution,[status(thm)],[f101,f108])).
% 0.10/0.39 fof(f738,plain,(
% 0.10/0.39 connection(in(c,f),in(n2,h1(f)))),
% 0.10/0.39 inference(resolution,[status(thm)],[f105,f108])).
% 0.10/0.39 fof(f739,plain,(
% 0.10/0.39 connection(out(s,f),out(s,h2(f)))),
% 0.10/0.39 inference(resolution,[status(thm)],[f106,f108])).
% 0.10/0.39 fof(f740,plain,(
% 0.10/0.39 connection(out(c,f),out(n1,or1(f)))),
% 0.10/0.39 inference(resolution,[status(thm)],[f107,f108])).
% 0.10/0.39 fof(f741,plain,(
% 0.10/0.39 value(in(n2,h1(f)),n1)),
% 0.10/0.39 inference(resolution,[status(thm)],[f738,f140])).
% 0.10/0.39 fof(f742,plain,(
% 0.10/0.39 value(out(s,h2(f)),n1)),
% 0.10/0.39 inference(resolution,[status(thm)],[f739,f139])).
% 0.10/0.39 fof(f746,plain,(
% 0.10/0.39 ![X0]: (~connection(in(n2,h1(f)),X0)|value(X0,n1))),
% 0.10/0.39 inference(resolution,[status(thm)],[f741,f58])).
% 0.10/0.39 fof(f751,plain,(
% 0.10/0.39 value(out(n1,or1(f)),n0)),
% 0.10/0.39 inference(resolution,[status(thm)],[f740,f138])).
% 0.10/0.39 fof(f766,definition,(
% 0.10/0.39 sQ87_spl <=> (type(or1(f),or))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f768,plain,(
% 0.10/0.39 ~type(or1(f),or)|sQ87_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f766])).
% 0.10/0.39 fof(f781,plain,(
% 0.10/0.39 $false|sQ87_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f768,f471])).
% 0.10/0.39 fof(f782,plain,(
% 0.10/0.39 sQ87_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f781])).
% 0.10/0.39 fof(f795,plain,(
% 0.10/0.39 value(in(n2,and2(h1(f))),n1)),
% 0.10/0.39 inference(resolution,[status(thm)],[f746,f178])).
% 0.10/0.39 fof(f797,plain,(
% 0.10/0.39 $false|sQ32_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f795,f341])).
% 0.10/0.39 fof(f798,plain,(
% 0.10/0.39 sQ32_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f797])).
% 0.10/0.39 fof(f843,plain,(
% 0.10/0.39 value(out(s,h2(f)),n0)|~sQ62_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f563,f729])).
% 0.10/0.39 fof(f847,plain,(
% 0.10/0.39 ![X0]: (~value(out(s,h2(f)),X0)|equal_value(X0,n0)|~sQ62_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f843,f62])).
% 0.10/0.39 fof(f851,plain,(
% 0.10/0.39 equal_value(n1,n0)|~sQ62_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f847,f742])).
% 0.10/0.39 fof(f852,plain,(
% 0.10/0.39 $false|~sQ62_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f851,f64])).
% 0.10/0.39 fof(f853,plain,(
% 0.10/0.39 ~sQ62_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f852])).
% 0.10/0.39 fof(f856,plain,(
% 0.10/0.39 value(out(c,h1(f)),n1)|~sQ33_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f503,f179])).
% 0.10/0.39 fof(f859,plain,(
% 0.10/0.39 ![X0]: (~connection(out(c,h1(f)),X0)|value(X0,n1)|~sQ33_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f856,f58])).
% 0.10/0.39 fof(f861,plain,(
% 0.10/0.39 value(in(n2,or1(f)),n1)|~sQ33_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f859,f737])).
% 0.10/0.39 fof(f864,plain,(
% 0.10/0.39 value(in(n1,not1(h1(f))),n1)|~sQ33_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f504,f243])).
% 0.10/0.39 fof(f867,plain,(
% 0.10/0.39 ~mode(or1(f),ok)|~type(or1(f),or)|value(out(n1,or1(f)),n1)|~sQ33_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f861,f75])).
% 0.10/0.39 fof(f871,definition,(
% 0.10/0.39 sQ94_spl <=> (value(out(n1,or1(f)),n1))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f872,plain,(
% 0.10/0.39 value(out(n1,or1(f)),n1)|~sQ94_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f871])).
% 0.10/0.39 fof(f874,plain,(
% 0.10/0.39 ~sQ52_spl|~sQ87_spl|sQ94_spl|~sQ33_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f867,f473,f766,f871,f342])).
% 0.10/0.39 fof(f876,plain,(
% 0.10/0.39 ~mode(not1(h1(f)),ok)|~type(not1(h1(f)),not)|value(out(n1,not1(h1(f))),n0)|~sQ33_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f864,f81])).
% 0.10/0.39 fof(f882,definition,(
% 0.10/0.39 sQ95_spl <=> (type(not1(h1(f)),not))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f884,plain,(
% 0.10/0.39 ~type(not1(h1(f)),not)|sQ95_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f882])).
% 0.10/0.39 fof(f885,definition,(
% 0.10/0.39 sQ96_spl <=> (value(out(n1,not1(h1(f))),n0))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f886,plain,(
% 0.10/0.39 value(out(n1,not1(h1(f))),n0)|~sQ96_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f885])).
% 0.10/0.39 fof(f888,plain,(
% 0.10/0.39 ~sQ9_spl|~sQ95_spl|sQ96_spl|~sQ33_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f876,f181,f882,f885,f342])).
% 0.10/0.39 fof(f903,plain,(
% 0.10/0.39 $false|sQ95_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f884,f164])).
% 0.10/0.39 fof(f904,plain,(
% 0.10/0.39 sQ95_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f903])).
% 0.10/0.39 fof(f928,plain,(
% 0.10/0.39 ![X0]: (~connection(out(n1,not1(h1(f))),X0)|value(X0,n0)|~sQ96_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f886,f58])).
% 0.10/0.39 fof(f950,plain,(
% 0.10/0.39 value(in(n2,and1(h1(f))),n0)|~sQ96_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f928,f245])).
% 0.10/0.39 fof(f951,plain,(
% 0.10/0.39 ~mode(and1(h1(f)),ok)|~type(and1(h1(f)),and)|value(out(n1,and1(h1(f))),n0)|~sQ96_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f950,f69])).
% 0.10/0.39 fof(f955,definition,(
% 0.10/0.39 sQ104_spl <=> (type(and1(h1(f)),and))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f957,plain,(
% 0.10/0.39 ~type(and1(h1(f)),and)|sQ104_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f955])).
% 0.10/0.39 fof(f958,definition,(
% 0.10/0.39 sQ105_spl <=> (value(out(n1,and1(h1(f))),n0))),
% 0.10/0.39 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.10/0.39 fof(f959,plain,(
% 0.10/0.39 value(out(n1,and1(h1(f))),n0)|~sQ105_spl),
% 0.10/0.39 inference(component_clause,[status(thm)],[f958])).
% 0.10/0.39 fof(f961,plain,(
% 0.10/0.39 ~sQ12_spl|~sQ104_spl|sQ105_spl|~sQ96_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f951,f194,f955,f958,f885])).
% 0.10/0.39 fof(f962,plain,(
% 0.10/0.39 $false|sQ104_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f957,f166])).
% 0.10/0.39 fof(f963,plain,(
% 0.10/0.39 sQ104_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f962])).
% 0.10/0.39 fof(f971,plain,(
% 0.10/0.39 ![X0]: (~connection(X0,out(n1,and1(h1(f))))|value(X0,n0)|~sQ105_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f959,f60])).
% 0.10/0.39 fof(f993,plain,(
% 0.10/0.39 value(out(s,h1(f)),n0)|~sQ105_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f971,f730])).
% 0.10/0.39 fof(f996,plain,(
% 0.10/0.39 ![X0]: (~connection(out(s,h1(f)),X0)|value(X0,n0)|~sQ105_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f993,f58])).
% 0.10/0.39 fof(f1010,plain,(
% 0.10/0.39 value(in(n2,h2(f)),n0)|~sQ105_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f996,f736])).
% 0.10/0.39 fof(f1015,plain,(
% 0.10/0.39 ![X0]: (~connection(in(n2,h2(f)),X0)|value(X0,n0)|~sQ105_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f1010,f58])).
% 0.10/0.39 fof(f1032,plain,(
% 0.10/0.39 ![X0]: (~value(out(n1,or1(f)),X0)|equal_value(X0,n1)|~sQ94_spl)),
% 0.10/0.39 inference(resolution,[status(thm)],[f872,f62])).
% 0.10/0.39 fof(f1120,plain,(
% 0.10/0.39 value(in(n2,or1(h2(f))),n0)|~sQ105_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f1015,f205])).
% 0.10/0.39 fof(f1122,plain,(
% 0.10/0.39 sQ47_spl|~sQ105_spl),
% 0.10/0.39 inference(split_clause,[status(thm)],[f1120,f436,f958])).
% 0.10/0.39 fof(f1146,plain,(
% 0.10/0.39 equal_value(n0,n1)|~sQ94_spl),
% 0.10/0.39 inference(resolution,[status(thm)],[f1032,f751])).
% 0.10/0.39 fof(f1147,plain,(
% 0.10/0.39 $false|~sQ94_spl),
% 0.10/0.39 inference(forward_subsumption_resolution,[status(thm)],[f1146,f63])).
% 0.10/0.39 fof(f1148,plain,(
% 0.10/0.39 ~sQ94_spl),
% 0.10/0.39 inference(contradiction_clause,[status(thm)],[f1147])).
% 0.10/0.39 fof(f1149,plain,(
% 0.10/0.39 $false),
% 0.10/0.39 inference(sat_refutation,[status(thm)],[f125,f129,f133,f137,f184,f192,f197,f239,f290,f345,f367,f369,f476,f522,f529,f555,f557,f782,f798,f853,f874,f888,f904,f961,f963,f1122,f1148])).
% 0.10/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.42 % Elapsed time: 0.051682 seconds
% 0.10/0.42 % CPU time: 0.177549 seconds
% 0.10/0.42 % Total memory used: 18.524 MB
% 0.10/0.42 % Net memory used: 18.454 MB
%------------------------------------------------------------------------------