%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV006-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 : n008.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.19s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HWV006-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.39 % Computer : n008.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sun Sep 20 20:47:55 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.42 % Drodi V4.1.1
% 0.19/0.46 % Refutation found
% 0.19/0.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.19/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.46 fof(f1,axiom,(
% 0.19/0.46 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P1,V)| value(P2,V) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f2,axiom,(
% 0.19/0.46 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P2,V)| value(P1,V) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f3,axiom,(
% 0.19/0.46 (![P,V1,V2]: (( ~ value(P,V1)| ~ value(P,V2)| equal_value(V1,V2) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f5,axiom,(
% 0.19/0.46 ~ equal_value(n1,n0) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f7,axiom,(
% 0.19/0.46 (![K,Any]: (( ~ type(K,Any)| mode(K,ok)| mode(K,abnormal) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f8,axiom,(
% 0.19/0.46 (![K,Any]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(in(Any,K),n0)| value(out(n1,K),n0) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f9,axiom,(
% 0.19/0.46 (![K]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(in(n1,K),n1)| ~ value(in(n2,K),n1)| value(out(n1,K),n1) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f13,axiom,(
% 0.19/0.46 (![K,Any]: (( ~ mode(K,ok)| ~ type(K,or)| ~ value(in(Any,K),n1)| value(out(n1,K),n1) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f16,axiom,(
% 0.19/0.46 (![K]: (( ~ mode(K,ok)| ~ type(K,or)| ~ value(out(n1,K),n0)| value(in(n1,K),n0) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f18,axiom,(
% 0.19/0.46 (![K]: (( ~ mode(K,ok)| ~ type(K,not)| ~ value(in(n1,K),n0)| value(out(n1,K),n1) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f19,axiom,(
% 0.19/0.46 (![K]: (( ~ mode(K,ok)| ~ type(K,not)| ~ value(in(n1,K),n1)| value(out(n1,K),n0) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f22,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| type(and1(X),and) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f23,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| type(and2(X),and) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f24,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| type(not1(X),not) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f25,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| type(or1(X),or) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f27,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| connection(in(n2,X),in(n2,or1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f28,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| connection(in(n1,X),in(n1,and2(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f29,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| connection(in(n2,X),in(n2,and2(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f30,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| connection(out(s,X),out(n1,and1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f31,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| connection(out(c,X),out(n1,and2(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f32,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| connection(out(n1,or1(X)),in(n1,and1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f33,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| connection(out(n1,and2(X)),in(n1,not1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f34,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,halfadder)| connection(out(n1,not1(X)),in(n2,and1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f35,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| type(h1(X),halfadder) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f36,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| type(h2(X),halfadder) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f37,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| type(or1(X),or) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f38,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| connection(out(s,h1(X)),in(n2,h2(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f40,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| connection(out(c,h2(X)),in(n1,or1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f41,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| connection(in(n1,X),in(n1,h2(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f42,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| connection(in(n2,X),in(n1,h1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f43,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| connection(in(c,X),in(n2,h1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f44,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| connection(out(s,X),out(s,h2(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f45,axiom,(
% 0.19/0.46 (![X]: (( ~ type(X,fulladder)| connection(out(c,X),out(n1,or1(X))) ) ))),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f46,hypothesis,(
% 0.19/0.46 type(f,fulladder) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f47,hypothesis,(
% 0.19/0.46 value(in(n1,f),n1) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f48,hypothesis,(
% 0.19/0.46 value(in(n2,f),n0) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f49,hypothesis,(
% 0.19/0.46 value(in(c,f),n1) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f50,hypothesis,(
% 0.19/0.46 value(out(s,f),n1) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f51,hypothesis,(
% 0.19/0.46 value(out(c,f),n0) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f52,negated_conjecture,(
% 0.19/0.46 ( ~ mode(or1(f),abnormal)| ~ mode(not1(h2(f)),abnormal) ) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f53,negated_conjecture,(
% 0.19/0.46 ~ mode(and2(h2(f)),abnormal) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f54,negated_conjecture,(
% 0.19/0.46 ( ~ mode(or1(f),abnormal)| ~ mode(and1(h2(f)),abnormal) ) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f55,negated_conjecture,(
% 0.19/0.46 ~ mode(or1(h1(f)),abnormal) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f56,negated_conjecture,(
% 0.19/0.46 ~ mode(not1(h1(f)),abnormal) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f57,negated_conjecture,(
% 0.19/0.46 ~ mode(and2(h1(f)),abnormal) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f58,negated_conjecture,(
% 0.19/0.46 ~ mode(and1(h1(f)),abnormal) ),
% 0.19/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.46 fof(f59,plain,(
% 0.19/0.46 ![P2,V]: ((![P1]: (~connection(P1,P2)|~value(P1,V)))|value(P2,V))),
% 0.19/0.46 inference(miniscoping,[status(thm)],[f1])).
% 0.19/0.46 fof(f60,plain,(
% 0.19/0.46 ![X0,X1,X2]: (~connection(X0,X1)|~value(X0,X2)|value(X1,X2))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f59])).
% 0.19/0.46 fof(f61,plain,(
% 0.19/0.46 ![P1,V]: ((![P2]: (~connection(P1,P2)|~value(P2,V)))|value(P1,V))),
% 0.19/0.46 inference(miniscoping,[status(thm)],[f2])).
% 0.19/0.46 fof(f62,plain,(
% 0.19/0.46 ![X0,X1,X2]: (~connection(X0,X1)|~value(X1,X2)|value(X0,X2))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f61])).
% 0.19/0.46 fof(f63,plain,(
% 0.19/0.46 ![V1,V2]: ((![P]: (~value(P,V1)|~value(P,V2)))|equal_value(V1,V2))),
% 0.19/0.46 inference(miniscoping,[status(thm)],[f3])).
% 0.19/0.46 fof(f64,plain,(
% 0.19/0.46 ![X0,X1,X2]: (~value(X0,X1)|~value(X0,X2)|equal_value(X1,X2))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f63])).
% 0.19/0.46 fof(f66,plain,(
% 0.19/0.46 ~equal_value(n1,n0)),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.19/0.46 fof(f68,plain,(
% 0.19/0.46 ![K]: (((![Any]: ~type(K,Any))|mode(K,ok))|mode(K,abnormal))),
% 0.19/0.46 inference(miniscoping,[status(thm)],[f7])).
% 0.19/0.46 fof(f69,plain,(
% 0.19/0.46 ![X0,X1]: (~type(X0,X1)|mode(X0,ok)|mode(X0,abnormal))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f68])).
% 0.19/0.46 fof(f70,plain,(
% 0.19/0.46 ![K]: (((~mode(K,ok)|~type(K,and))|(![Any]: ~value(in(Any,K),n0)))|value(out(n1,K),n0))),
% 0.19/0.46 inference(miniscoping,[status(thm)],[f8])).
% 0.19/0.46 fof(f71,plain,(
% 0.19/0.46 ![X0,X1]: (~mode(X0,ok)|~type(X0,and)|~value(in(X1,X0),n0)|value(out(n1,X0),n0))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f70])).
% 0.19/0.46 fof(f72,plain,(
% 0.19/0.46 ![X0]: (~mode(X0,ok)|~type(X0,and)|~value(in(n1,X0),n1)|~value(in(n2,X0),n1)|value(out(n1,X0),n1))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f9])).
% 0.19/0.46 fof(f76,plain,(
% 0.19/0.46 ![K]: (((~mode(K,ok)|~type(K,or))|(![Any]: ~value(in(Any,K),n1)))|value(out(n1,K),n1))),
% 0.19/0.46 inference(miniscoping,[status(thm)],[f13])).
% 0.19/0.46 fof(f77,plain,(
% 0.19/0.46 ![X0,X1]: (~mode(X0,ok)|~type(X0,or)|~value(in(X1,X0),n1)|value(out(n1,X0),n1))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f76])).
% 0.19/0.46 fof(f80,plain,(
% 0.19/0.46 ![X0]: (~mode(X0,ok)|~type(X0,or)|~value(out(n1,X0),n0)|value(in(n1,X0),n0))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f16])).
% 0.19/0.46 fof(f82,plain,(
% 0.19/0.46 ![X0]: (~mode(X0,ok)|~type(X0,not)|~value(in(n1,X0),n0)|value(out(n1,X0),n1))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f18])).
% 0.19/0.46 fof(f83,plain,(
% 0.19/0.46 ![X0]: (~mode(X0,ok)|~type(X0,not)|~value(in(n1,X0),n1)|value(out(n1,X0),n0))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f19])).
% 0.19/0.46 fof(f86,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|type(and1(X0),and))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f22])).
% 0.19/0.46 fof(f87,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|type(and2(X0),and))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f23])).
% 0.19/0.46 fof(f88,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|type(not1(X0),not))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f24])).
% 0.19/0.46 fof(f89,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|type(or1(X0),or))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f25])).
% 0.19/0.46 fof(f91,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|connection(in(n2,X0),in(n2,or1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f27])).
% 0.19/0.46 fof(f92,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|connection(in(n1,X0),in(n1,and2(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f28])).
% 0.19/0.46 fof(f93,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|connection(in(n2,X0),in(n2,and2(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f29])).
% 0.19/0.46 fof(f94,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|connection(out(s,X0),out(n1,and1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f30])).
% 0.19/0.46 fof(f95,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|connection(out(c,X0),out(n1,and2(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f31])).
% 0.19/0.46 fof(f96,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|connection(out(n1,or1(X0)),in(n1,and1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f32])).
% 0.19/0.46 fof(f97,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|connection(out(n1,and2(X0)),in(n1,not1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f33])).
% 0.19/0.46 fof(f98,plain,(
% 0.19/0.46 ![X0]: (~type(X0,halfadder)|connection(out(n1,not1(X0)),in(n2,and1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f34])).
% 0.19/0.46 fof(f99,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|type(h1(X0),halfadder))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f35])).
% 0.19/0.46 fof(f100,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|type(h2(X0),halfadder))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f36])).
% 0.19/0.46 fof(f101,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|type(or1(X0),or))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f37])).
% 0.19/0.46 fof(f102,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|connection(out(s,h1(X0)),in(n2,h2(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f38])).
% 0.19/0.46 fof(f104,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|connection(out(c,h2(X0)),in(n1,or1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f40])).
% 0.19/0.46 fof(f105,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|connection(in(n1,X0),in(n1,h2(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f41])).
% 0.19/0.46 fof(f106,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|connection(in(n2,X0),in(n1,h1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f42])).
% 0.19/0.46 fof(f107,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|connection(in(c,X0),in(n2,h1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f43])).
% 0.19/0.46 fof(f108,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|connection(out(s,X0),out(s,h2(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f44])).
% 0.19/0.46 fof(f109,plain,(
% 0.19/0.46 ![X0]: (~type(X0,fulladder)|connection(out(c,X0),out(n1,or1(X0))))),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f45])).
% 0.19/0.46 fof(f110,plain,(
% 0.19/0.46 type(f,fulladder)),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f46])).
% 0.19/0.46 fof(f111,plain,(
% 0.19/0.46 value(in(n1,f),n1)),
% 0.19/0.46 inference(cnf_transformation,[status(thm)],[f47])).
% 0.19/0.47 fof(f112,plain,(
% 0.19/0.47 value(in(n2,f),n0)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f48])).
% 0.19/0.47 fof(f113,plain,(
% 0.19/0.47 value(in(c,f),n1)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f49])).
% 0.19/0.47 fof(f114,plain,(
% 0.19/0.47 value(out(s,f),n1)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f50])).
% 0.19/0.47 fof(f115,plain,(
% 0.19/0.47 value(out(c,f),n0)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f51])).
% 0.19/0.47 fof(f116,plain,(
% 0.19/0.47 ~mode(or1(f),abnormal)|~mode(not1(h2(f)),abnormal)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f52])).
% 0.19/0.47 fof(f117,plain,(
% 0.19/0.47 ~mode(and2(h2(f)),abnormal)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f53])).
% 0.19/0.47 fof(f118,plain,(
% 0.19/0.47 ~mode(or1(f),abnormal)|~mode(and1(h2(f)),abnormal)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f54])).
% 0.19/0.47 fof(f119,plain,(
% 0.19/0.47 ~mode(or1(h1(f)),abnormal)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f55])).
% 0.19/0.47 fof(f120,plain,(
% 0.19/0.47 ~mode(not1(h1(f)),abnormal)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f56])).
% 0.19/0.47 fof(f121,plain,(
% 0.19/0.47 ~mode(and2(h1(f)),abnormal)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f57])).
% 0.19/0.47 fof(f122,plain,(
% 0.19/0.47 ~mode(and1(h1(f)),abnormal)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f58])).
% 0.19/0.47 fof(f123,definition,(
% 0.19/0.47 sQ0_spl <=> (mode(or1(f),abnormal))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f126,definition,(
% 0.19/0.47 sQ1_spl <=> (mode(not1(h2(f)),abnormal))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f129,plain,(
% 0.19/0.47 ~sQ0_spl|~sQ1_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f116,f123,f126])).
% 0.19/0.47 fof(f130,definition,(
% 0.19/0.47 sQ2_spl <=> (mode(and1(h2(f)),abnormal))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f133,plain,(
% 0.19/0.47 ~sQ0_spl|~sQ2_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f118,f123,f130])).
% 0.19/0.47 fof(f162,plain,(
% 0.19/0.47 type(h1(f),halfadder)),
% 0.19/0.47 inference(resolution,[status(thm)],[f99,f110])).
% 0.19/0.47 fof(f163,plain,(
% 0.19/0.47 type(h2(f),halfadder)),
% 0.19/0.47 inference(resolution,[status(thm)],[f100,f110])).
% 0.19/0.47 fof(f164,plain,(
% 0.19/0.47 connection(in(n1,f),in(n1,h2(f)))),
% 0.19/0.47 inference(resolution,[status(thm)],[f105,f110])).
% 0.19/0.47 fof(f165,plain,(
% 0.19/0.47 connection(in(n2,f),in(n1,h1(f)))),
% 0.19/0.47 inference(resolution,[status(thm)],[f106,f110])).
% 0.19/0.47 fof(f168,plain,(
% 0.19/0.47 connection(out(n1,not1(h1(f))),in(n2,and1(h1(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f162,f98])).
% 0.19/0.47 fof(f169,plain,(
% 0.19/0.47 connection(out(n1,and2(h1(f))),in(n1,not1(h1(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f162,f97])).
% 0.19/0.47 fof(f170,plain,(
% 0.19/0.47 connection(out(n1,or1(h1(f))),in(n1,and1(h1(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f162,f96])).
% 0.19/0.47 fof(f173,plain,(
% 0.19/0.47 connection(in(n1,h1(f)),in(n1,and2(h1(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f162,f92])).
% 0.19/0.47 fof(f174,plain,(
% 0.19/0.47 connection(in(n2,h1(f)),in(n2,or1(h1(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f162,f91])).
% 0.19/0.47 fof(f176,plain,(
% 0.19/0.47 type(not1(h1(f)),not)),
% 0.19/0.47 inference(resolution,[status(thm)],[f162,f88])).
% 0.19/0.47 fof(f177,plain,(
% 0.19/0.47 type(and2(h1(f)),and)),
% 0.19/0.47 inference(resolution,[status(thm)],[f162,f87])).
% 0.19/0.47 fof(f178,plain,(
% 0.19/0.47 type(and1(h1(f)),and)),
% 0.19/0.47 inference(resolution,[status(thm)],[f162,f86])).
% 0.19/0.47 fof(f187,plain,(
% 0.19/0.47 connection(out(n1,not1(h2(f))),in(n2,and1(h2(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f163,f98])).
% 0.19/0.47 fof(f188,plain,(
% 0.19/0.47 connection(out(n1,and2(h2(f))),in(n1,not1(h2(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f163,f97])).
% 0.19/0.47 fof(f190,plain,(
% 0.19/0.47 connection(out(c,h2(f)),out(n1,and2(h2(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f163,f95])).
% 0.19/0.47 fof(f191,plain,(
% 0.19/0.47 connection(in(n2,h2(f)),in(n2,and2(h2(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f163,f93])).
% 0.19/0.47 fof(f192,plain,(
% 0.19/0.47 connection(in(n1,h2(f)),in(n1,and2(h2(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f163,f92])).
% 0.19/0.47 fof(f195,plain,(
% 0.19/0.47 type(not1(h2(f)),not)),
% 0.19/0.47 inference(resolution,[status(thm)],[f163,f88])).
% 0.19/0.47 fof(f196,plain,(
% 0.19/0.47 type(and2(h2(f)),and)),
% 0.19/0.47 inference(resolution,[status(thm)],[f163,f87])).
% 0.19/0.47 fof(f197,plain,(
% 0.19/0.47 type(and1(h2(f)),and)),
% 0.19/0.47 inference(resolution,[status(thm)],[f163,f86])).
% 0.19/0.47 fof(f207,plain,(
% 0.19/0.47 ![X0]: (~value(in(n1,f),X0)|value(in(n1,h2(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f164,f60])).
% 0.19/0.47 fof(f209,plain,(
% 0.19/0.47 ![X0]: (~value(in(n2,f),X0)|value(in(n1,h1(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f165,f60])).
% 0.19/0.47 fof(f211,plain,(
% 0.19/0.47 ![X0]: (~value(out(n1,not1(h1(f))),X0)|value(in(n2,and1(h1(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f168,f60])).
% 0.19/0.47 fof(f213,plain,(
% 0.19/0.47 ![X0]: (~value(out(n1,and2(h1(f))),X0)|value(in(n1,not1(h1(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f169,f60])).
% 0.19/0.47 fof(f215,plain,(
% 0.19/0.47 ![X0]: (~value(out(n1,or1(h1(f))),X0)|value(in(n1,and1(h1(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f170,f60])).
% 0.19/0.47 fof(f218,plain,(
% 0.19/0.47 mode(not1(h1(f)),ok)|mode(not1(h1(f)),abnormal)),
% 0.19/0.47 inference(resolution,[status(thm)],[f176,f69])).
% 0.19/0.47 fof(f219,definition,(
% 0.19/0.47 sQ13_spl <=> (mode(not1(h1(f)),ok))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f222,definition,(
% 0.19/0.47 sQ14_spl <=> (mode(not1(h1(f)),abnormal))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f223,plain,(
% 0.19/0.47 mode(not1(h1(f)),abnormal)|~sQ14_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f222])).
% 0.19/0.47 fof(f225,plain,(
% 0.19/0.47 sQ13_spl|sQ14_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f218,f219,f222])).
% 0.19/0.47 fof(f226,plain,(
% 0.19/0.47 mode(and2(h1(f)),ok)|mode(and2(h1(f)),abnormal)),
% 0.19/0.47 inference(resolution,[status(thm)],[f177,f69])).
% 0.19/0.47 fof(f227,definition,(
% 0.19/0.47 sQ15_spl <=> (mode(and2(h1(f)),ok))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f230,definition,(
% 0.19/0.47 sQ16_spl <=> (mode(and2(h1(f)),abnormal))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f231,plain,(
% 0.19/0.47 mode(and2(h1(f)),abnormal)|~sQ16_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f230])).
% 0.19/0.47 fof(f233,plain,(
% 0.19/0.47 sQ15_spl|sQ16_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f226,f227,f230])).
% 0.19/0.47 fof(f234,plain,(
% 0.19/0.47 mode(and1(h1(f)),ok)|mode(and1(h1(f)),abnormal)),
% 0.19/0.47 inference(resolution,[status(thm)],[f178,f69])).
% 0.19/0.47 fof(f235,definition,(
% 0.19/0.47 sQ17_spl <=> (mode(and1(h1(f)),ok))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f238,definition,(
% 0.19/0.47 sQ18_spl <=> (mode(and1(h1(f)),abnormal))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f239,plain,(
% 0.19/0.47 mode(and1(h1(f)),abnormal)|~sQ18_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f238])).
% 0.19/0.47 fof(f241,plain,(
% 0.19/0.47 sQ17_spl|sQ18_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f234,f235,f238])).
% 0.19/0.47 fof(f242,plain,(
% 0.19/0.47 mode(not1(h2(f)),ok)|mode(not1(h2(f)),abnormal)),
% 0.19/0.47 inference(resolution,[status(thm)],[f195,f69])).
% 0.19/0.47 fof(f243,definition,(
% 0.19/0.47 sQ19_spl <=> (mode(not1(h2(f)),ok))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f246,plain,(
% 0.19/0.47 sQ19_spl|sQ1_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f242,f243,f126])).
% 0.19/0.47 fof(f247,plain,(
% 0.19/0.47 mode(and2(h2(f)),ok)|mode(and2(h2(f)),abnormal)),
% 0.19/0.47 inference(resolution,[status(thm)],[f196,f69])).
% 0.19/0.47 fof(f248,definition,(
% 0.19/0.47 sQ20_spl <=> (mode(and2(h2(f)),ok))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f251,definition,(
% 0.19/0.47 sQ21_spl <=> (mode(and2(h2(f)),abnormal))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f252,plain,(
% 0.19/0.47 mode(and2(h2(f)),abnormal)|~sQ21_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f251])).
% 0.19/0.47 fof(f254,plain,(
% 0.19/0.47 sQ20_spl|sQ21_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f247,f248,f251])).
% 0.19/0.47 fof(f255,plain,(
% 0.19/0.47 mode(and1(h2(f)),ok)|mode(and1(h2(f)),abnormal)),
% 0.19/0.47 inference(resolution,[status(thm)],[f197,f69])).
% 0.19/0.47 fof(f256,definition,(
% 0.19/0.47 sQ22_spl <=> (mode(and1(h2(f)),ok))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f259,plain,(
% 0.19/0.47 sQ22_spl|sQ2_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f255,f256,f130])).
% 0.19/0.47 fof(f263,plain,(
% 0.19/0.47 ![X0]: (~value(in(n1,h1(f)),X0)|value(in(n1,and2(h1(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f173,f60])).
% 0.19/0.47 fof(f265,plain,(
% 0.19/0.47 ![X0]: (~value(in(n2,h1(f)),X0)|value(in(n2,or1(h1(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f174,f60])).
% 0.19/0.47 fof(f269,plain,(
% 0.19/0.47 ![X0]: (~value(out(n1,not1(h2(f))),X0)|value(in(n2,and1(h2(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f187,f60])).
% 0.19/0.47 fof(f271,plain,(
% 0.19/0.47 ![X0]: (~value(out(n1,and2(h2(f))),X0)|value(in(n1,not1(h2(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f188,f60])).
% 0.19/0.47 fof(f274,plain,(
% 0.19/0.47 ![X0]: (~value(out(n1,and2(h2(f))),X0)|value(out(c,h2(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f190,f62])).
% 0.19/0.47 fof(f277,plain,(
% 0.19/0.47 ![X0]: (~value(in(n2,h2(f)),X0)|value(in(n2,and2(h2(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f191,f60])).
% 0.19/0.47 fof(f279,plain,(
% 0.19/0.47 ![X0]: (~value(in(n1,h2(f)),X0)|value(in(n1,and2(h2(f))),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f192,f60])).
% 0.19/0.47 fof(f284,plain,(
% 0.19/0.47 value(in(n1,h2(f)),n1)),
% 0.19/0.47 inference(resolution,[status(thm)],[f207,f111])).
% 0.19/0.47 fof(f285,plain,(
% 0.19/0.47 value(in(n1,h1(f)),n0)),
% 0.19/0.47 inference(resolution,[status(thm)],[f209,f112])).
% 0.19/0.47 fof(f299,plain,(
% 0.19/0.47 value(in(n1,and2(h1(f))),n0)),
% 0.19/0.47 inference(resolution,[status(thm)],[f263,f285])).
% 0.19/0.47 fof(f301,plain,(
% 0.19/0.47 ![X0]: (~value(out(s,f),X0)|equal_value(n1,X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f114,f64])).
% 0.19/0.47 fof(f352,plain,(
% 0.19/0.47 ~mode(and2(h1(f)),ok)|~type(and2(h1(f)),and)|value(out(n1,and2(h1(f))),n0)),
% 0.19/0.47 inference(resolution,[status(thm)],[f299,f71])).
% 0.19/0.47 fof(f361,definition,(
% 0.19/0.47 sQ36_spl <=> (type(and2(h1(f)),and))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f363,plain,(
% 0.19/0.47 ~type(and2(h1(f)),and)|sQ36_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f361])).
% 0.19/0.47 fof(f364,definition,(
% 0.19/0.47 sQ37_spl <=> (value(out(n1,and2(h1(f))),n0))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f365,plain,(
% 0.19/0.47 value(out(n1,and2(h1(f))),n0)|~sQ37_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f364])).
% 0.19/0.47 fof(f367,plain,(
% 0.19/0.47 ~sQ15_spl|~sQ36_spl|sQ37_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f352,f227,f361,f364])).
% 0.19/0.47 fof(f368,plain,(
% 0.19/0.47 $false|sQ36_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f363,f177])).
% 0.19/0.47 fof(f369,plain,(
% 0.19/0.47 sQ36_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f368])).
% 0.19/0.47 fof(f370,plain,(
% 0.19/0.47 $false|~sQ16_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f231,f121])).
% 0.19/0.47 fof(f371,plain,(
% 0.19/0.47 ~sQ16_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f370])).
% 0.19/0.47 fof(f372,plain,(
% 0.19/0.47 value(in(n1,and2(h2(f))),n1)),
% 0.19/0.47 inference(resolution,[status(thm)],[f279,f284])).
% 0.19/0.47 fof(f380,definition,(
% 0.19/0.47 sQ38_spl <=> (mode(or1(h1(f)),ok))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f386,definition,(
% 0.19/0.47 sQ40_spl <=> (value(out(n1,or1(h1(f))),n1))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f387,plain,(
% 0.19/0.47 value(out(n1,or1(h1(f))),n1)|~sQ40_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f386])).
% 0.19/0.47 fof(f398,plain,(
% 0.19/0.47 value(in(n1,not1(h1(f))),n0)|~sQ37_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f365,f213])).
% 0.19/0.47 fof(f423,definition,(
% 0.19/0.47 sQ47_spl <=> (value(out(n1,and2(h2(f))),n1))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f424,plain,(
% 0.19/0.47 value(out(n1,and2(h2(f))),n1)|~sQ47_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f423])).
% 0.19/0.47 fof(f427,plain,(
% 0.19/0.47 $false|~sQ21_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f252,f117])).
% 0.19/0.47 fof(f428,plain,(
% 0.19/0.47 ~sQ21_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f427])).
% 0.19/0.47 fof(f450,plain,(
% 0.19/0.47 ~mode(not1(h1(f)),ok)|~type(not1(h1(f)),not)|value(out(n1,not1(h1(f))),n1)|~sQ37_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f398,f82])).
% 0.19/0.47 fof(f453,definition,(
% 0.19/0.47 sQ51_spl <=> (type(not1(h1(f)),not))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f455,plain,(
% 0.19/0.47 ~type(not1(h1(f)),not)|sQ51_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f453])).
% 0.19/0.47 fof(f456,definition,(
% 0.19/0.47 sQ52_spl <=> (value(out(n1,not1(h1(f))),n1))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f457,plain,(
% 0.19/0.47 value(out(n1,not1(h1(f))),n1)|~sQ52_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f456])).
% 0.19/0.47 fof(f459,plain,(
% 0.19/0.47 ~sQ13_spl|~sQ51_spl|sQ52_spl|~sQ37_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f450,f219,f453,f456,f364])).
% 0.19/0.47 fof(f467,plain,(
% 0.19/0.47 $false|sQ51_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f455,f176])).
% 0.19/0.47 fof(f468,plain,(
% 0.19/0.47 sQ51_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f467])).
% 0.19/0.47 fof(f469,plain,(
% 0.19/0.47 $false|~sQ14_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f223,f120])).
% 0.19/0.47 fof(f470,plain,(
% 0.19/0.47 ~sQ14_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f469])).
% 0.19/0.47 fof(f507,plain,(
% 0.19/0.47 value(in(n2,and1(h1(f))),n1)|~sQ52_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f457,f211])).
% 0.19/0.47 fof(f525,plain,(
% 0.19/0.47 ~mode(and1(h1(f)),ok)|~type(and1(h1(f)),and)|~value(in(n1,and1(h1(f))),n1)|value(out(n1,and1(h1(f))),n1)|~sQ52_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f507,f72])).
% 0.19/0.47 fof(f528,definition,(
% 0.19/0.47 sQ61_spl <=> (type(and1(h1(f)),and))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f530,plain,(
% 0.19/0.47 ~type(and1(h1(f)),and)|sQ61_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f528])).
% 0.19/0.47 fof(f531,definition,(
% 0.19/0.47 sQ62_spl <=> (value(in(n1,and1(h1(f))),n1))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f533,plain,(
% 0.19/0.47 ~value(in(n1,and1(h1(f))),n1)|sQ62_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f531])).
% 0.19/0.47 fof(f534,definition,(
% 0.19/0.47 sQ63_spl <=> (value(out(n1,and1(h1(f))),n1))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f535,plain,(
% 0.19/0.47 value(out(n1,and1(h1(f))),n1)|~sQ63_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f534])).
% 0.19/0.47 fof(f537,plain,(
% 0.19/0.47 ~sQ17_spl|~sQ61_spl|~sQ62_spl|sQ63_spl|~sQ52_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f525,f235,f528,f531,f534,f456])).
% 0.19/0.47 fof(f565,plain,(
% 0.19/0.47 $false|sQ61_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f530,f178])).
% 0.19/0.47 fof(f566,plain,(
% 0.19/0.47 sQ61_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f565])).
% 0.19/0.47 fof(f614,plain,(
% 0.19/0.47 type(or1(h1(f)),or)),
% 0.19/0.47 inference(resolution,[status(thm)],[f89,f162])).
% 0.19/0.47 fof(f618,plain,(
% 0.19/0.47 mode(or1(h1(f)),ok)|mode(or1(h1(f)),abnormal)),
% 0.19/0.47 inference(resolution,[status(thm)],[f614,f69])).
% 0.19/0.47 fof(f619,definition,(
% 0.19/0.47 sQ75_spl <=> (mode(or1(h1(f)),abnormal))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f620,plain,(
% 0.19/0.47 mode(or1(h1(f)),abnormal)|~sQ75_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f619])).
% 0.19/0.47 fof(f622,plain,(
% 0.19/0.47 sQ38_spl|sQ75_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f618,f380,f619])).
% 0.19/0.47 fof(f623,plain,(
% 0.19/0.47 connection(out(s,h2(f)),out(n1,and1(h2(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f94,f163])).
% 0.19/0.47 fof(f624,plain,(
% 0.19/0.47 connection(out(s,h1(f)),out(n1,and1(h1(f))))),
% 0.19/0.47 inference(resolution,[status(thm)],[f94,f162])).
% 0.19/0.47 fof(f625,plain,(
% 0.19/0.47 type(or1(f),or)),
% 0.19/0.47 inference(resolution,[status(thm)],[f101,f110])).
% 0.19/0.47 fof(f626,plain,(
% 0.19/0.47 connection(out(s,h1(f)),in(n2,h2(f)))),
% 0.19/0.47 inference(resolution,[status(thm)],[f102,f110])).
% 0.19/0.47 fof(f628,plain,(
% 0.19/0.47 connection(out(c,h2(f)),in(n1,or1(f)))),
% 0.19/0.47 inference(resolution,[status(thm)],[f104,f110])).
% 0.19/0.47 fof(f629,plain,(
% 0.19/0.47 connection(in(c,f),in(n2,h1(f)))),
% 0.19/0.47 inference(resolution,[status(thm)],[f107,f110])).
% 0.19/0.47 fof(f635,plain,(
% 0.19/0.47 ![X0]: (~value(out(n1,and1(h2(f))),X0)|value(out(s,h2(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f623,f62])).
% 0.19/0.47 fof(f637,plain,(
% 0.19/0.47 ![X0]: (~value(out(n1,and1(h1(f))),X0)|value(out(s,h1(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f624,f62])).
% 0.19/0.47 fof(f640,plain,(
% 0.19/0.47 mode(or1(f),ok)|mode(or1(f),abnormal)),
% 0.19/0.47 inference(resolution,[status(thm)],[f625,f69])).
% 0.19/0.47 fof(f641,definition,(
% 0.19/0.47 sQ77_spl <=> (mode(or1(f),ok))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f644,plain,(
% 0.19/0.47 sQ77_spl|sQ0_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f640,f641,f123])).
% 0.19/0.47 fof(f649,plain,(
% 0.19/0.47 ![X0]: (~value(in(c,f),X0)|value(in(n2,h1(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f629,f60])).
% 0.19/0.47 fof(f651,plain,(
% 0.19/0.47 ![X0]: (~value(out(s,h1(f)),X0)|value(in(n2,h2(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f626,f60])).
% 0.19/0.47 fof(f654,plain,(
% 0.19/0.47 connection(out(s,f),out(s,h2(f)))),
% 0.19/0.47 inference(resolution,[status(thm)],[f108,f110])).
% 0.19/0.47 fof(f655,plain,(
% 0.19/0.47 connection(out(c,f),out(n1,or1(f)))),
% 0.19/0.47 inference(resolution,[status(thm)],[f109,f110])).
% 0.19/0.47 fof(f657,plain,(
% 0.19/0.47 ![X0]: (~value(out(c,h2(f)),X0)|value(in(n1,or1(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f628,f60])).
% 0.19/0.47 fof(f658,plain,(
% 0.19/0.47 ![X0]: (~value(out(s,h2(f)),X0)|value(out(s,f),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f654,f62])).
% 0.19/0.47 fof(f661,plain,(
% 0.19/0.47 ![X0]: (~value(out(c,f),X0)|value(out(n1,or1(f)),X0))),
% 0.19/0.47 inference(resolution,[status(thm)],[f655,f60])).
% 0.19/0.47 fof(f662,plain,(
% 0.19/0.47 value(in(n2,h1(f)),n1)),
% 0.19/0.47 inference(resolution,[status(thm)],[f649,f113])).
% 0.19/0.47 fof(f668,definition,(
% 0.19/0.47 sQ78_spl <=> (type(or1(f),or))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f670,plain,(
% 0.19/0.47 ~type(or1(f),or)|sQ78_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f668])).
% 0.19/0.47 fof(f671,definition,(
% 0.19/0.47 sQ79_spl <=> (value(in(n1,or1(f)),n0))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f672,plain,(
% 0.19/0.47 value(in(n1,or1(f)),n0)|~sQ79_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f671])).
% 0.19/0.47 fof(f674,definition,(
% 0.19/0.47 sQ80_spl <=> (value(out(n1,or1(f)),n0))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f675,plain,(
% 0.19/0.47 value(out(n1,or1(f)),n0)|~sQ80_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f674])).
% 0.19/0.47 fof(f676,plain,(
% 0.19/0.47 ~value(out(n1,or1(f)),n0)|sQ80_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f674])).
% 0.19/0.47 fof(f685,plain,(
% 0.19/0.47 ~mode(or1(f),ok)|~type(or1(f),or)|value(in(n1,or1(f)),n0)|~sQ80_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f675,f80])).
% 0.19/0.47 fof(f699,plain,(
% 0.19/0.47 ~sQ77_spl|~sQ78_spl|sQ79_spl|~sQ80_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f685,f641,f668,f671,f674])).
% 0.19/0.47 fof(f701,plain,(
% 0.19/0.47 $false|sQ78_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f670,f625])).
% 0.19/0.47 fof(f702,plain,(
% 0.19/0.47 sQ78_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f701])).
% 0.19/0.47 fof(f721,plain,(
% 0.19/0.47 value(in(n2,or1(h1(f))),n1)),
% 0.19/0.47 inference(resolution,[status(thm)],[f662,f265])).
% 0.19/0.47 fof(f751,plain,(
% 0.19/0.47 ~mode(or1(h1(f)),ok)|~type(or1(h1(f)),or)|value(out(n1,or1(h1(f))),n1)),
% 0.19/0.47 inference(resolution,[status(thm)],[f721,f77])).
% 0.19/0.47 fof(f757,definition,(
% 0.19/0.47 sQ91_spl <=> (type(or1(h1(f)),or))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f759,plain,(
% 0.19/0.47 ~type(or1(h1(f)),or)|sQ91_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f757])).
% 0.19/0.47 fof(f760,plain,(
% 0.19/0.47 ~sQ38_spl|~sQ91_spl|sQ40_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f751,f380,f757,f386])).
% 0.19/0.47 fof(f767,plain,(
% 0.19/0.47 value(in(n1,and1(h1(f))),n1)|~sQ40_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f387,f215])).
% 0.19/0.47 fof(f773,plain,(
% 0.19/0.47 $false|sQ62_spl|~sQ40_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f767,f533])).
% 0.19/0.47 fof(f774,plain,(
% 0.19/0.47 sQ62_spl|~sQ40_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f773])).
% 0.19/0.47 fof(f785,plain,(
% 0.19/0.47 $false|~sQ18_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f239,f122])).
% 0.19/0.47 fof(f786,plain,(
% 0.19/0.47 ~sQ18_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f785])).
% 0.19/0.47 fof(f787,plain,(
% 0.19/0.47 $false|~sQ75_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f620,f119])).
% 0.19/0.47 fof(f788,plain,(
% 0.19/0.47 ~sQ75_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f787])).
% 0.19/0.47 fof(f789,plain,(
% 0.19/0.47 $false|sQ91_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f759,f614])).
% 0.19/0.47 fof(f790,plain,(
% 0.19/0.47 sQ91_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f789])).
% 0.19/0.47 fof(f827,plain,(
% 0.19/0.47 value(out(s,h1(f)),n1)|~sQ63_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f535,f637])).
% 0.19/0.47 fof(f841,plain,(
% 0.19/0.47 value(in(n2,h2(f)),n1)|~sQ63_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f827,f651])).
% 0.19/0.47 fof(f846,plain,(
% 0.19/0.47 value(in(n2,and2(h2(f))),n1)|~sQ63_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f841,f277])).
% 0.19/0.47 fof(f860,plain,(
% 0.19/0.47 ~mode(and2(h2(f)),ok)|~type(and2(h2(f)),and)|~value(in(n1,and2(h2(f))),n1)|value(out(n1,and2(h2(f))),n1)|~sQ63_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f846,f72])).
% 0.19/0.47 fof(f863,definition,(
% 0.19/0.47 sQ97_spl <=> (type(and2(h2(f)),and))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f865,plain,(
% 0.19/0.47 ~type(and2(h2(f)),and)|sQ97_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f863])).
% 0.19/0.47 fof(f866,definition,(
% 0.19/0.47 sQ98_spl <=> (value(in(n1,and2(h2(f))),n1))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f868,plain,(
% 0.19/0.47 ~value(in(n1,and2(h2(f))),n1)|sQ98_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f866])).
% 0.19/0.47 fof(f869,plain,(
% 0.19/0.47 ~sQ20_spl|~sQ97_spl|~sQ98_spl|sQ47_spl|~sQ63_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f860,f248,f863,f866,f423,f534])).
% 0.19/0.47 fof(f871,plain,(
% 0.19/0.47 value(out(c,h2(f)),n1)|~sQ47_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f424,f274])).
% 0.19/0.47 fof(f872,plain,(
% 0.19/0.47 value(in(n1,not1(h2(f))),n1)|~sQ47_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f424,f271])).
% 0.19/0.47 fof(f888,plain,(
% 0.19/0.47 $false|sQ97_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f865,f196])).
% 0.19/0.47 fof(f889,plain,(
% 0.19/0.47 sQ97_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f888])).
% 0.19/0.48 fof(f904,plain,(
% 0.19/0.48 ~mode(not1(h2(f)),ok)|~type(not1(h2(f)),not)|value(out(n1,not1(h2(f))),n0)|~sQ47_spl),
% 0.19/0.48 inference(resolution,[status(thm)],[f872,f83])).
% 0.19/0.48 fof(f907,definition,(
% 0.19/0.48 sQ101_spl <=> (type(not1(h2(f)),not))),
% 0.19/0.48 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.19/0.48 fof(f909,plain,(
% 0.19/0.48 ~type(not1(h2(f)),not)|sQ101_spl),
% 0.19/0.48 inference(component_clause,[status(thm)],[f907])).
% 0.19/0.48 fof(f910,definition,(
% 0.19/0.48 sQ102_spl <=> (value(out(n1,not1(h2(f))),n0))),
% 0.19/0.48 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.19/0.48 fof(f911,plain,(
% 0.19/0.48 value(out(n1,not1(h2(f))),n0)|~sQ102_spl),
% 0.19/0.48 inference(component_clause,[status(thm)],[f910])).
% 0.19/0.48 fof(f913,plain,(
% 0.19/0.48 ~sQ19_spl|~sQ101_spl|sQ102_spl|~sQ47_spl),
% 0.19/0.48 inference(split_clause,[status(thm)],[f904,f243,f907,f910,f423])).
% 0.19/0.48 fof(f921,plain,(
% 0.19/0.48 $false|sQ101_spl),
% 0.19/0.48 inference(forward_subsumption_resolution,[status(thm)],[f909,f195])).
% 0.19/0.48 fof(f922,plain,(
% 0.19/0.48 sQ101_spl),
% 0.19/0.48 inference(contradiction_clause,[status(thm)],[f921])).
% 0.19/0.48 fof(f927,plain,(
% 0.19/0.48 value(in(n1,or1(f)),n1)|~sQ47_spl),
% 0.19/0.48 inference(resolution,[status(thm)],[f657,f871])).
% 0.19/0.48 fof(f929,plain,(
% 0.19/0.48 value(out(n1,or1(f)),n0)),
% 0.19/0.48 inference(resolution,[status(thm)],[f661,f115])).
% 0.19/0.48 fof(f930,plain,(
% 0.19/0.48 $false|sQ80_spl),
% 0.19/0.48 inference(forward_subsumption_resolution,[status(thm)],[f929,f676])).
% 0.19/0.48 fof(f931,plain,(
% 0.19/0.48 sQ80_spl),
% 0.19/0.48 inference(contradiction_clause,[status(thm)],[f930])).
% 0.19/0.48 fof(f935,plain,(
% 0.19/0.48 ![X0]: (~value(in(n1,or1(f)),X0)|equal_value(n1,X0)|~sQ47_spl)),
% 0.19/0.48 inference(resolution,[status(thm)],[f927,f64])).
% 0.19/0.48 fof(f956,plain,(
% 0.19/0.48 equal_value(n1,n0)|~sQ47_spl|~sQ79_spl),
% 0.19/0.48 inference(resolution,[status(thm)],[f935,f672])).
% 0.19/0.48 fof(f958,plain,(
% 0.19/0.48 $false|~sQ47_spl|~sQ79_spl),
% 0.19/0.48 inference(forward_subsumption_resolution,[status(thm)],[f956,f66])).
% 0.19/0.48 fof(f959,plain,(
% 0.19/0.48 ~sQ47_spl|~sQ79_spl),
% 0.19/0.48 inference(contradiction_clause,[status(thm)],[f958])).
% 0.19/0.48 fof(f961,plain,(
% 0.19/0.48 value(in(n2,and1(h2(f))),n0)|~sQ102_spl),
% 0.19/0.48 inference(resolution,[status(thm)],[f911,f269])).
% 0.19/0.48 fof(f985,plain,(
% 0.19/0.48 ~mode(and1(h2(f)),ok)|~type(and1(h2(f)),and)|value(out(n1,and1(h2(f))),n0)|~sQ102_spl),
% 0.19/0.48 inference(resolution,[status(thm)],[f961,f71])).
% 0.19/0.48 fof(f993,definition,(
% 0.19/0.48 sQ111_spl <=> (value(out(n1,and1(h2(f))),n0))),
% 0.19/0.48 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.19/0.48 fof(f994,plain,(
% 0.19/0.48 value(out(n1,and1(h2(f))),n0)|~sQ111_spl),
% 0.19/0.48 inference(component_clause,[status(thm)],[f993])).
% 0.19/0.48 fof(f997,definition,(
% 0.19/0.48 sQ112_spl <=> (type(and1(h2(f)),and))),
% 0.19/0.48 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.19/0.48 fof(f999,plain,(
% 0.19/0.48 ~type(and1(h2(f)),and)|sQ112_spl),
% 0.19/0.48 inference(component_clause,[status(thm)],[f997])).
% 0.19/0.48 fof(f1000,plain,(
% 0.19/0.48 ~sQ22_spl|~sQ112_spl|sQ111_spl|~sQ102_spl),
% 0.19/0.48 inference(split_clause,[status(thm)],[f985,f256,f997,f993,f910])).
% 0.19/0.48 fof(f1009,plain,(
% 0.19/0.48 value(out(s,h2(f)),n0)|~sQ111_spl),
% 0.19/0.48 inference(resolution,[status(thm)],[f994,f635])).
% 0.19/0.48 fof(f1028,plain,(
% 0.19/0.48 $false|sQ112_spl),
% 0.19/0.48 inference(forward_subsumption_resolution,[status(thm)],[f999,f197])).
% 0.19/0.48 fof(f1029,plain,(
% 0.19/0.48 sQ112_spl),
% 0.19/0.48 inference(contradiction_clause,[status(thm)],[f1028])).
% 0.19/0.48 fof(f1040,plain,(
% 0.19/0.48 value(out(s,f),n0)|~sQ111_spl),
% 0.19/0.48 inference(resolution,[status(thm)],[f1009,f658])).
% 0.19/0.48 fof(f1045,plain,(
% 0.19/0.48 equal_value(n1,n0)|~sQ111_spl),
% 0.19/0.48 inference(resolution,[status(thm)],[f1040,f301])).
% 0.19/0.48 fof(f1047,plain,(
% 0.19/0.48 $false|~sQ111_spl),
% 0.19/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1045,f66])).
% 0.19/0.48 fof(f1048,plain,(
% 0.19/0.48 ~sQ111_spl),
% 0.19/0.48 inference(contradiction_clause,[status(thm)],[f1047])).
% 0.19/0.48 fof(f1049,plain,(
% 0.19/0.48 $false|sQ98_spl),
% 0.19/0.48 inference(forward_subsumption_resolution,[status(thm)],[f868,f372])).
% 0.19/0.48 fof(f1050,plain,(
% 0.19/0.48 sQ98_spl),
% 0.19/0.48 inference(contradiction_clause,[status(thm)],[f1049])).
% 0.19/0.48 fof(f1051,plain,(
% 0.19/0.48 $false),
% 0.19/0.48 inference(sat_refutation,[status(thm)],[f129,f133,f225,f233,f241,f246,f254,f259,f367,f369,f371,f428,f459,f468,f470,f537,f566,f622,f644,f699,f702,f760,f774,f786,f788,f790,f869,f889,f913,f922,f931,f959,f1000,f1029,f1048,f1050])).
% 0.19/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.50 % Elapsed time: 0.095535 seconds
% 0.19/0.50 % CPU time: 0.293895 seconds
% 0.19/0.50 % Total memory used: 13.461 MB
% 0.19/0.50 % Net memory used: 13.352 MB
%------------------------------------------------------------------------------