%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV006-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV006-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n016.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:51:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.41 fof(f1,axiom,(
% 0.10/0.41 (![P1,P2]: (( ~ connection(P1,P2)| ~ zero(P1)| zero(P2) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f2,axiom,(
% 0.10/0.41 (![P1,P2]: (( ~ connection(P1,P2)| ~ one(P1)| one(P2) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f4,axiom,(
% 0.10/0.41 (![P1,P2]: (( ~ connection(P1,P2)| ~ one(P2)| one(P1) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f5,axiom,(
% 0.10/0.41 (![P]: (( ~ zero(P)| ~ one(P) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f6,axiom,(
% 0.10/0.41 (![K]: (( ~ and_ok(K)| ~ zero(in1(K))| zero(out1(K)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f8,axiom,(
% 0.10/0.41 (![K]: (( ~ and_ok(K)| ~ one(in1(K))| ~ one(in2(K))| one(out1(K)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f11,axiom,(
% 0.10/0.41 (![K]: (( ~ and_ok(K)| ~ one(out1(K))| one(in2(K)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f13,axiom,(
% 0.10/0.41 (![K]: (( ~ logic_and(K)| and_ok(K)| abnormal(K) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f14,axiom,(
% 0.10/0.41 (![K]: (( ~ or_ok(K)| ~ one(in1(K))| one(out1(K)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f15,axiom,(
% 0.10/0.41 (![K]: (( ~ or_ok(K)| ~ one(in2(K))| one(out1(K)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f21,axiom,(
% 0.10/0.41 (![K]: (( ~ logic_or(K)| or_ok(K)| abnormal(K) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f22,axiom,(
% 0.10/0.41 (![K]: (( ~ not_ok(K)| ~ zero(in1(K))| one(out1(K)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f25,axiom,(
% 0.10/0.41 (![K]: (( ~ not_ok(K)| ~ one(out1(K))| zero(in1(K)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f27,axiom,(
% 0.10/0.41 (![K]: (( ~ logic_not(K)| not_ok(K)| abnormal(K) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f28,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| logic_and(and1(X)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f29,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| logic_and(and2(X)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f30,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| logic_not(not1(X)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f31,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| logic_or(or1(X)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f33,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| connection(in2(X),in2(or1(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f34,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| connection(in1(X),in1(and2(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f35,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| connection(in2(X),in2(and2(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f36,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| connection(outs(X),out1(and1(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f37,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| connection(outc(X),out1(and2(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f38,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| connection(out1(or1(X)),in1(and1(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f39,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| connection(out1(and2(X)),in1(not1(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f40,axiom,(
% 0.10/0.41 (![X]: (( ~ halfadder(X)| connection(out1(not1(X)),in2(and1(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f41,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| halfadder(h1(X)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f42,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| halfadder(h2(X)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f43,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| logic_or(or1(X)) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f44,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| connection(outs(h1(X)),in2(h2(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f46,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| connection(outc(h2(X)),in1(or1(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f47,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| connection(in1(X),in1(h2(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f48,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| connection(in2(X),in1(h1(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f49,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| connection(inc(X),in2(h1(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f50,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| connection(outs(X),outs(h2(X))) ) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f51,axiom,(
% 0.10/0.41 (![X]: (( ~ fulladder(X)| connection(outc(X),out1(or1(X))) ) ))),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f52,hypothesis,(
% 0.10/0.42 fulladder(f) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f53,hypothesis,(
% 0.10/0.42 one(in1(f)) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f54,hypothesis,(
% 0.10/0.42 zero(in2(f)) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f55,hypothesis,(
% 0.10/0.42 one(inc(f)) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f56,hypothesis,(
% 0.10/0.42 one(outs(f)) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f57,hypothesis,(
% 0.10/0.42 zero(outc(f)) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f58,negated_conjecture,(
% 0.10/0.42 ( ~ abnormal(or1(f))| ~ abnormal(not1(h2(f))) ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f59,negated_conjecture,(
% 0.10/0.42 ~ abnormal(and2(h2(f))) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f60,negated_conjecture,(
% 0.10/0.42 ( ~ abnormal(or1(f))| ~ abnormal(and1(h2(f))) ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f61,negated_conjecture,(
% 0.10/0.42 ~ abnormal(or1(h1(f))) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f62,negated_conjecture,(
% 0.10/0.42 ~ abnormal(not1(h1(f))) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f63,negated_conjecture,(
% 0.10/0.42 ~ abnormal(and2(h1(f))) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f64,negated_conjecture,(
% 0.10/0.42 ~ abnormal(and1(h1(f))) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f65,plain,(
% 0.10/0.42 ![P2]: ((![P1]: (~connection(P1,P2)|~zero(P1)))|zero(P2))),
% 0.10/0.42 inference(miniscoping,[status(thm)],[f1])).
% 0.10/0.42 fof(f66,plain,(
% 0.10/0.42 ![X0,X1]: (~connection(X0,X1)|~zero(X0)|zero(X1))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f65])).
% 0.10/0.42 fof(f67,plain,(
% 0.10/0.42 ![P2]: ((![P1]: (~connection(P1,P2)|~one(P1)))|one(P2))),
% 0.10/0.42 inference(miniscoping,[status(thm)],[f2])).
% 0.10/0.42 fof(f68,plain,(
% 0.10/0.42 ![X0,X1]: (~connection(X0,X1)|~one(X0)|one(X1))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f67])).
% 0.10/0.42 fof(f71,plain,(
% 0.10/0.42 ![P1]: ((![P2]: (~connection(P1,P2)|~one(P2)))|one(P1))),
% 0.10/0.42 inference(miniscoping,[status(thm)],[f4])).
% 0.10/0.42 fof(f72,plain,(
% 0.10/0.42 ![X0,X1]: (~connection(X0,X1)|~one(X1)|one(X0))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f71])).
% 0.10/0.42 fof(f73,plain,(
% 0.10/0.42 ![X0]: (~zero(X0)|~one(X0))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.42 fof(f74,plain,(
% 0.10/0.42 ![X0]: (~and_ok(X0)|~zero(in1(X0))|zero(out1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.42 fof(f76,plain,(
% 0.10/0.42 ![X0]: (~and_ok(X0)|~one(in1(X0))|~one(in2(X0))|one(out1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.42 fof(f79,plain,(
% 0.10/0.42 ![X0]: (~and_ok(X0)|~one(out1(X0))|one(in2(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f11])).
% 0.10/0.42 fof(f81,plain,(
% 0.10/0.42 ![X0]: (~logic_and(X0)|and_ok(X0)|abnormal(X0))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.42 fof(f82,plain,(
% 0.10/0.42 ![X0]: (~or_ok(X0)|~one(in1(X0))|one(out1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.42 fof(f83,plain,(
% 0.10/0.42 ![X0]: (~or_ok(X0)|~one(in2(X0))|one(out1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.42 fof(f89,plain,(
% 0.10/0.42 ![X0]: (~logic_or(X0)|or_ok(X0)|abnormal(X0))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f21])).
% 0.10/0.42 fof(f90,plain,(
% 0.10/0.42 ![X0]: (~not_ok(X0)|~zero(in1(X0))|one(out1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.42 fof(f93,plain,(
% 0.10/0.42 ![X0]: (~not_ok(X0)|~one(out1(X0))|zero(in1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f25])).
% 0.10/0.42 fof(f95,plain,(
% 0.10/0.42 ![X0]: (~logic_not(X0)|not_ok(X0)|abnormal(X0))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f27])).
% 0.10/0.42 fof(f96,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|logic_and(and1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f28])).
% 0.10/0.42 fof(f97,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|logic_and(and2(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f29])).
% 0.10/0.42 fof(f98,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|logic_not(not1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f30])).
% 0.10/0.42 fof(f99,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|logic_or(or1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f31])).
% 0.10/0.42 fof(f101,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|connection(in2(X0),in2(or1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f33])).
% 0.10/0.42 fof(f102,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|connection(in1(X0),in1(and2(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f34])).
% 0.10/0.42 fof(f103,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|connection(in2(X0),in2(and2(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f35])).
% 0.10/0.42 fof(f104,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|connection(outs(X0),out1(and1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f36])).
% 0.10/0.42 fof(f105,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|connection(outc(X0),out1(and2(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f37])).
% 0.10/0.42 fof(f106,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|connection(out1(or1(X0)),in1(and1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f38])).
% 0.10/0.42 fof(f107,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|connection(out1(and2(X0)),in1(not1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f39])).
% 0.10/0.42 fof(f108,plain,(
% 0.10/0.42 ![X0]: (~halfadder(X0)|connection(out1(not1(X0)),in2(and1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f40])).
% 0.10/0.42 fof(f109,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|halfadder(h1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f41])).
% 0.10/0.42 fof(f110,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|halfadder(h2(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f42])).
% 0.10/0.42 fof(f111,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|logic_or(or1(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/0.42 fof(f112,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|connection(outs(h1(X0)),in2(h2(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f114,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|connection(outc(h2(X0)),in1(or1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f46])).
% 0.10/0.42 fof(f115,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|connection(in1(X0),in1(h2(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f47])).
% 0.10/0.42 fof(f116,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|connection(in2(X0),in1(h1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f48])).
% 0.10/0.42 fof(f117,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|connection(inc(X0),in2(h1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f49])).
% 0.10/0.42 fof(f118,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|connection(outs(X0),outs(h2(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f50])).
% 0.10/0.42 fof(f119,plain,(
% 0.10/0.42 ![X0]: (~fulladder(X0)|connection(outc(X0),out1(or1(X0))))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f51])).
% 0.10/0.42 fof(f120,plain,(
% 0.10/0.42 fulladder(f)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f52])).
% 0.10/0.42 fof(f121,plain,(
% 0.10/0.42 one(in1(f))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f53])).
% 0.10/0.42 fof(f122,plain,(
% 0.10/0.42 zero(in2(f))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f54])).
% 0.10/0.42 fof(f123,plain,(
% 0.10/0.42 one(inc(f))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f55])).
% 0.10/0.42 fof(f124,plain,(
% 0.10/0.42 one(outs(f))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f56])).
% 0.10/0.42 fof(f125,plain,(
% 0.10/0.42 zero(outc(f))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f57])).
% 0.10/0.42 fof(f126,plain,(
% 0.10/0.42 ~abnormal(or1(f))|~abnormal(not1(h2(f)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f58])).
% 0.10/0.42 fof(f127,plain,(
% 0.10/0.42 ~abnormal(and2(h2(f)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f59])).
% 0.10/0.42 fof(f128,plain,(
% 0.10/0.42 ~abnormal(or1(f))|~abnormal(and1(h2(f)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f60])).
% 0.10/0.42 fof(f129,plain,(
% 0.10/0.42 ~abnormal(or1(h1(f)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f61])).
% 0.10/0.42 fof(f130,plain,(
% 0.10/0.42 ~abnormal(not1(h1(f)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f62])).
% 0.10/0.42 fof(f131,plain,(
% 0.10/0.42 ~abnormal(and2(h1(f)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f63])).
% 0.10/0.42 fof(f132,plain,(
% 0.10/0.42 ~abnormal(and1(h1(f)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f64])).
% 0.10/0.42 fof(f133,definition,(
% 0.10/0.42 sQ0_spl <=> (abnormal(or1(f)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f136,definition,(
% 0.10/0.42 sQ1_spl <=> (abnormal(not1(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f139,plain,(
% 0.10/0.42 ~sQ0_spl|~sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f126,f133,f136])).
% 0.10/0.42 fof(f140,definition,(
% 0.10/0.42 sQ2_spl <=> (abnormal(and1(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f143,plain,(
% 0.10/0.42 ~sQ0_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f128,f133,f140])).
% 0.10/0.42 fof(f153,plain,(
% 0.10/0.42 halfadder(h1(f))),
% 0.10/0.42 inference(resolution,[status(thm)],[f109,f120])).
% 0.10/0.42 fof(f154,plain,(
% 0.10/0.42 connection(out1(not1(h1(f))),in2(and1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f153,f108])).
% 0.10/0.42 fof(f155,plain,(
% 0.10/0.42 connection(out1(and2(h1(f))),in1(not1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f153,f107])).
% 0.10/0.42 fof(f156,plain,(
% 0.10/0.42 connection(out1(or1(h1(f))),in1(and1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f153,f106])).
% 0.10/0.42 fof(f158,plain,(
% 0.10/0.42 connection(in1(h1(f)),in1(and2(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f153,f102])).
% 0.10/0.42 fof(f159,plain,(
% 0.10/0.42 connection(in2(h1(f)),in2(or1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f153,f101])).
% 0.10/0.42 fof(f161,plain,(
% 0.10/0.42 halfadder(h2(f))),
% 0.10/0.42 inference(resolution,[status(thm)],[f110,f120])).
% 0.10/0.42 fof(f162,plain,(
% 0.10/0.42 connection(out1(not1(h2(f))),in2(and1(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f161,f108])).
% 0.10/0.42 fof(f163,plain,(
% 0.10/0.42 connection(out1(and2(h2(f))),in1(not1(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f161,f107])).
% 0.10/0.42 fof(f165,plain,(
% 0.10/0.42 connection(in2(h2(f)),in2(and2(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f161,f103])).
% 0.10/0.42 fof(f166,plain,(
% 0.10/0.42 connection(in1(h2(f)),in1(and2(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f161,f102])).
% 0.10/0.42 fof(f169,plain,(
% 0.10/0.42 connection(in1(f),in1(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f115,f120])).
% 0.10/0.42 fof(f172,plain,(
% 0.10/0.42 ~one(in1(f))|one(in1(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f169,f68])).
% 0.10/0.42 fof(f174,definition,(
% 0.10/0.42 sQ5_spl <=> (one(in1(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f177,definition,(
% 0.10/0.42 sQ6_spl <=> (one(in1(f)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f179,plain,(
% 0.10/0.42 ~one(in1(f))|sQ6_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f177])).
% 0.10/0.42 fof(f188,plain,(
% 0.10/0.42 ~sQ6_spl|sQ5_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f172,f177,f174])).
% 0.10/0.42 fof(f190,plain,(
% 0.10/0.42 $false|sQ6_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f179,f121])).
% 0.10/0.42 fof(f191,plain,(
% 0.10/0.42 sQ6_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f190])).
% 0.10/0.42 fof(f192,plain,(
% 0.10/0.42 connection(in2(f),in1(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f116,f120])).
% 0.10/0.42 fof(f196,plain,(
% 0.10/0.42 ~zero(in2(f))|zero(in1(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f192,f66])).
% 0.10/0.42 fof(f204,definition,(
% 0.10/0.42 sQ11_spl <=> (zero(in1(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f207,definition,(
% 0.10/0.42 sQ12_spl <=> (zero(in2(f)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f209,plain,(
% 0.10/0.42 ~zero(in2(f))|sQ12_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f207])).
% 0.10/0.42 fof(f212,plain,(
% 0.10/0.42 ~sQ12_spl|sQ11_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f196,f207,f204])).
% 0.10/0.42 fof(f213,plain,(
% 0.10/0.42 $false|sQ12_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f209,f122])).
% 0.10/0.42 fof(f214,plain,(
% 0.10/0.42 sQ12_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f213])).
% 0.10/0.42 fof(f217,plain,(
% 0.10/0.42 ~one(out1(not1(h1(f))))|one(in2(and1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f154,f68])).
% 0.10/0.42 fof(f219,definition,(
% 0.10/0.42 sQ13_spl <=> (one(in2(and1(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f220,plain,(
% 0.10/0.42 one(in2(and1(h1(f))))|~sQ13_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f219])).
% 0.10/0.42 fof(f222,definition,(
% 0.10/0.42 sQ14_spl <=> (one(out1(not1(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f233,plain,(
% 0.10/0.42 ~sQ14_spl|sQ13_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f217,f222,f219])).
% 0.10/0.42 fof(f238,plain,(
% 0.10/0.42 ~zero(out1(and2(h1(f))))|zero(in1(not1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f155,f66])).
% 0.10/0.42 fof(f246,definition,(
% 0.10/0.42 sQ19_spl <=> (zero(in1(not1(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f247,plain,(
% 0.10/0.42 zero(in1(not1(h1(f))))|~sQ19_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f246])).
% 0.10/0.42 fof(f249,definition,(
% 0.10/0.42 sQ20_spl <=> (zero(out1(and2(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f254,plain,(
% 0.10/0.42 ~sQ20_spl|sQ19_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f238,f249,f246])).
% 0.10/0.42 fof(f257,plain,(
% 0.10/0.42 ~one(out1(or1(h1(f))))|one(in1(and1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f156,f68])).
% 0.10/0.42 fof(f259,definition,(
% 0.10/0.42 sQ21_spl <=> (one(in1(and1(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f262,definition,(
% 0.10/0.42 sQ22_spl <=> (one(out1(or1(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f273,plain,(
% 0.10/0.42 ~sQ22_spl|sQ21_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f257,f262,f259])).
% 0.10/0.42 fof(f282,definition,(
% 0.10/0.42 sQ26_spl <=> (one(in2(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f298,plain,(
% 0.10/0.42 ~zero(in1(h1(f)))|zero(in1(and2(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f158,f66])).
% 0.10/0.42 fof(f303,definition,(
% 0.10/0.42 sQ30_spl <=> (zero(in1(and2(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f304,plain,(
% 0.10/0.42 zero(in1(and2(h1(f))))|~sQ30_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f303])).
% 0.10/0.42 fof(f308,plain,(
% 0.10/0.42 ~sQ11_spl|sQ30_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f298,f204,f303])).
% 0.10/0.42 fof(f311,plain,(
% 0.10/0.42 ~one(in2(h1(f)))|one(in2(or1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f159,f68])).
% 0.10/0.42 fof(f313,definition,(
% 0.10/0.42 sQ31_spl <=> (one(in2(or1(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f314,plain,(
% 0.10/0.42 one(in2(or1(h1(f))))|~sQ31_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f313])).
% 0.10/0.42 fof(f321,plain,(
% 0.10/0.42 ~sQ26_spl|sQ31_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f311,f282,f313])).
% 0.10/0.42 fof(f337,plain,(
% 0.10/0.42 ~one(in2(and1(h2(f))))|one(out1(not1(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f162,f72])).
% 0.10/0.42 fof(f341,definition,(
% 0.10/0.42 sQ35_spl <=> (one(in2(and1(h2(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f344,definition,(
% 0.10/0.42 sQ36_spl <=> (one(out1(not1(h2(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f345,plain,(
% 0.10/0.42 one(out1(not1(h2(f))))|~sQ36_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f344])).
% 0.10/0.42 fof(f347,plain,(
% 0.10/0.42 ~sQ35_spl|sQ36_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f337,f341,f344])).
% 0.10/0.42 fof(f359,plain,(
% 0.10/0.42 ~one(out1(and2(h2(f))))|one(in1(not1(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f163,f68])).
% 0.10/0.42 fof(f361,definition,(
% 0.10/0.42 sQ39_spl <=> (one(in1(not1(h2(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f362,plain,(
% 0.10/0.42 one(in1(not1(h2(f))))|~sQ39_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f361])).
% 0.10/0.42 fof(f364,definition,(
% 0.10/0.42 sQ40_spl <=> (one(out1(and2(h2(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f368,definition,(
% 0.10/0.42 sQ41_spl <=> (zero(in1(not1(h2(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f375,plain,(
% 0.10/0.42 ~sQ40_spl|sQ39_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f359,f364,f361])).
% 0.10/0.42 fof(f399,plain,(
% 0.10/0.42 ~one(in2(h2(f)))|one(in2(and2(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f165,f68])).
% 0.10/0.42 fof(f401,definition,(
% 0.10/0.42 sQ47_spl <=> (one(in2(and2(h2(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f402,plain,(
% 0.10/0.42 one(in2(and2(h2(f))))|~sQ47_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f401])).
% 0.10/0.42 fof(f404,definition,(
% 0.10/0.42 sQ48_spl <=> (one(in2(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f415,plain,(
% 0.10/0.42 ~sQ48_spl|sQ47_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f399,f404,f401])).
% 0.10/0.42 fof(f419,plain,(
% 0.10/0.42 ~one(in1(h2(f)))|one(in1(and2(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f166,f68])).
% 0.10/0.42 fof(f421,definition,(
% 0.10/0.42 sQ51_spl <=> (one(in1(and2(h2(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f429,plain,(
% 0.10/0.42 ~sQ5_spl|sQ51_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f419,f174,f421])).
% 0.10/0.42 fof(f468,plain,(
% 0.10/0.42 ~and_ok(and2(h1(f)))|zero(out1(and2(h1(f))))|~sQ30_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f304,f74])).
% 0.10/0.42 fof(f469,definition,(
% 0.10/0.42 sQ59_spl <=> (and_ok(and2(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f472,plain,(
% 0.10/0.42 ~sQ59_spl|sQ20_spl|~sQ30_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f468,f469,f249,f303])).
% 0.10/0.42 fof(f521,definition,(
% 0.10/0.42 sQ67_spl <=> (and_ok(and2(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f528,plain,(
% 0.10/0.42 ~zero(in1(not1(h2(f))))|~sQ39_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f362,f73])).
% 0.10/0.42 fof(f548,definition,(
% 0.10/0.42 sQ71_spl <=> (one(out1(and1(h2(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f549,plain,(
% 0.10/0.42 one(out1(and1(h2(f))))|~sQ71_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f548])).
% 0.10/0.42 fof(f569,definition,(
% 0.10/0.42 sQ74_spl <=> (and_ok(and1(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f574,plain,(
% 0.10/0.42 logic_and(and1(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f96,f161])).
% 0.10/0.42 fof(f575,plain,(
% 0.10/0.42 logic_and(and1(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f96,f153])).
% 0.10/0.42 fof(f576,plain,(
% 0.10/0.42 and_ok(and1(h2(f)))|abnormal(and1(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f574,f81])).
% 0.10/0.42 fof(f577,plain,(
% 0.10/0.42 sQ74_spl|sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f576,f569,f140])).
% 0.10/0.42 fof(f578,plain,(
% 0.10/0.42 and_ok(and1(h1(f)))|abnormal(and1(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f575,f81])).
% 0.10/0.42 fof(f579,definition,(
% 0.10/0.42 sQ75_spl <=> (and_ok(and1(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f582,definition,(
% 0.10/0.42 sQ76_spl <=> (abnormal(and1(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f583,plain,(
% 0.10/0.42 abnormal(and1(h1(f)))|~sQ76_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f582])).
% 0.10/0.42 fof(f585,plain,(
% 0.10/0.42 sQ75_spl|sQ76_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f578,f579,f582])).
% 0.10/0.42 fof(f586,plain,(
% 0.10/0.42 logic_and(and2(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f97,f161])).
% 0.10/0.42 fof(f587,plain,(
% 0.10/0.42 logic_and(and2(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f97,f153])).
% 0.10/0.42 fof(f588,plain,(
% 0.10/0.42 and_ok(and2(h2(f)))|abnormal(and2(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f586,f81])).
% 0.10/0.42 fof(f589,definition,(
% 0.10/0.42 sQ77_spl <=> (abnormal(and2(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f590,plain,(
% 0.10/0.42 abnormal(and2(h2(f)))|~sQ77_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f589])).
% 0.10/0.42 fof(f592,plain,(
% 0.10/0.42 sQ67_spl|sQ77_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f588,f521,f589])).
% 0.10/0.42 fof(f593,plain,(
% 0.10/0.42 and_ok(and2(h1(f)))|abnormal(and2(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f587,f81])).
% 0.10/0.42 fof(f594,definition,(
% 0.10/0.42 sQ78_spl <=> (abnormal(and2(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f595,plain,(
% 0.10/0.42 abnormal(and2(h1(f)))|~sQ78_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f594])).
% 0.10/0.42 fof(f597,plain,(
% 0.10/0.42 sQ59_spl|sQ78_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f593,f469,f594])).
% 0.10/0.42 fof(f598,plain,(
% 0.10/0.42 $false|~sQ78_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f595,f131])).
% 0.10/0.42 fof(f599,plain,(
% 0.10/0.42 ~sQ78_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f598])).
% 0.10/0.42 fof(f601,plain,(
% 0.10/0.42 ~and_ok(and2(h2(f)))|~one(in1(and2(h2(f))))|one(out1(and2(h2(f))))|~sQ47_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f402,f76])).
% 0.10/0.42 fof(f604,plain,(
% 0.10/0.42 ~sQ67_spl|~sQ51_spl|sQ40_spl|~sQ47_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f601,f521,f421,f364,f401])).
% 0.10/0.42 fof(f657,plain,(
% 0.10/0.42 $false|~sQ76_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f583,f132])).
% 0.10/0.42 fof(f658,plain,(
% 0.10/0.42 ~sQ76_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f657])).
% 0.10/0.42 fof(f688,definition,(
% 0.10/0.42 sQ86_spl <=> (or_ok(or1(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f694,plain,(
% 0.10/0.42 logic_not(not1(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f98,f161])).
% 0.10/0.42 fof(f695,plain,(
% 0.10/0.42 logic_not(not1(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f98,f153])).
% 0.10/0.42 fof(f697,plain,(
% 0.10/0.42 logic_or(or1(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f99,f153])).
% 0.10/0.42 fof(f698,plain,(
% 0.10/0.42 logic_or(or1(f))),
% 0.10/0.42 inference(resolution,[status(thm)],[f111,f120])).
% 0.10/0.42 fof(f700,plain,(
% 0.10/0.42 ~not_ok(not1(h1(f)))|one(out1(not1(h1(f))))|~sQ19_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f90,f247])).
% 0.10/0.42 fof(f707,definition,(
% 0.10/0.42 sQ88_spl <=> (one(out1(and1(h1(f)))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f711,definition,(
% 0.10/0.42 sQ89_spl <=> (not_ok(not1(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f714,plain,(
% 0.10/0.42 ~sQ89_spl|sQ14_spl|~sQ19_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f700,f711,f222,f246])).
% 0.10/0.42 fof(f735,definition,(
% 0.10/0.42 sQ94_spl <=> (not_ok(not1(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f759,plain,(
% 0.10/0.42 ~sQ41_spl|~sQ39_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f528,f368,f361])).
% 0.10/0.42 fof(f768,plain,(
% 0.10/0.42 connection(outs(h2(f)),out1(and1(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f104,f161])).
% 0.10/0.42 fof(f769,plain,(
% 0.10/0.42 connection(outs(h1(f)),out1(and1(h1(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f104,f153])).
% 0.10/0.42 fof(f770,plain,(
% 0.10/0.42 connection(outc(h2(f)),out1(and2(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f105,f161])).
% 0.10/0.42 fof(f780,plain,(
% 0.10/0.42 not_ok(not1(h2(f)))|abnormal(not1(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f694,f95])).
% 0.10/0.42 fof(f781,plain,(
% 0.10/0.42 sQ94_spl|sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f780,f735,f136])).
% 0.10/0.42 fof(f782,plain,(
% 0.10/0.42 not_ok(not1(h1(f)))|abnormal(not1(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f695,f95])).
% 0.10/0.42 fof(f783,definition,(
% 0.10/0.42 sQ100_spl <=> (abnormal(not1(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f784,plain,(
% 0.10/0.42 abnormal(not1(h1(f)))|~sQ100_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f783])).
% 0.10/0.42 fof(f786,plain,(
% 0.10/0.42 sQ89_spl|sQ100_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f782,f711,f783])).
% 0.10/0.42 fof(f787,plain,(
% 0.10/0.42 $false|~sQ100_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f784,f130])).
% 0.10/0.42 fof(f788,plain,(
% 0.10/0.42 ~sQ100_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f787])).
% 0.10/0.42 fof(f794,plain,(
% 0.10/0.42 or_ok(or1(h1(f)))|abnormal(or1(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f697,f89])).
% 0.10/0.42 fof(f795,definition,(
% 0.10/0.42 sQ102_spl <=> (abnormal(or1(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f796,plain,(
% 0.10/0.42 abnormal(or1(h1(f)))|~sQ102_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f795])).
% 0.10/0.42 fof(f798,plain,(
% 0.10/0.42 sQ86_spl|sQ102_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f794,f688,f795])).
% 0.10/0.42 fof(f801,plain,(
% 0.10/0.42 ~one(outs(h2(f)))|one(out1(and1(h2(f))))),
% 0.10/0.42 inference(resolution,[status(thm)],[f768,f68])).
% 0.10/0.42 fof(f803,definition,(
% 0.10/0.42 sQ103_spl <=> (one(outs(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f814,plain,(
% 0.10/0.42 ~sQ103_spl|sQ71_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f801,f803,f548])).
% 0.10/0.42 fof(f816,plain,(
% 0.10/0.42 ~one(out1(and1(h1(f))))|one(outs(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f769,f72])).
% 0.10/0.42 fof(f820,definition,(
% 0.10/0.42 sQ106_spl <=> (one(outs(h1(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f823,plain,(
% 0.10/0.42 ~sQ88_spl|sQ106_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f816,f707,f820])).
% 0.10/0.42 fof(f830,plain,(
% 0.10/0.42 ~one(out1(and2(h2(f))))|one(outc(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f770,f72])).
% 0.10/0.42 fof(f834,definition,(
% 0.10/0.42 sQ108_spl <=> (one(outc(h2(f))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f837,plain,(
% 0.10/0.42 ~sQ40_spl|sQ108_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f830,f364,f834])).
% 0.10/0.42 fof(f844,plain,(
% 0.10/0.42 $false|~sQ77_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f590,f127])).
% 0.10/0.42 fof(f845,plain,(
% 0.10/0.42 ~sQ77_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f844])).
% 0.10/0.42 fof(f874,plain,(
% 0.10/0.42 ~and_ok(and1(h1(f)))|~one(in1(and1(h1(f))))|one(out1(and1(h1(f))))|~sQ13_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f220,f76])).
% 0.10/0.42 fof(f877,plain,(
% 0.10/0.42 ~sQ75_spl|~sQ21_spl|sQ88_spl|~sQ13_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f874,f579,f259,f707,f219])).
% 0.10/0.42 fof(f911,plain,(
% 0.10/0.42 $false|~sQ102_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f796,f129])).
% 0.10/0.42 fof(f912,plain,(
% 0.10/0.42 ~sQ102_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f911])).
% 0.10/0.42 fof(f935,plain,(
% 0.10/0.42 ~and_ok(and1(h2(f)))|one(in2(and1(h2(f))))|~sQ71_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f549,f79])).
% 0.10/0.42 fof(f940,plain,(
% 0.10/0.42 ~sQ74_spl|sQ35_spl|~sQ71_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f935,f569,f341,f548])).
% 0.10/0.42 fof(f943,plain,(
% 0.10/0.42 ~not_ok(not1(h2(f)))|zero(in1(not1(h2(f))))|~sQ36_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f345,f93])).
% 0.10/0.42 fof(f948,plain,(
% 0.10/0.42 ~sQ94_spl|sQ41_spl|~sQ36_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f943,f735,f368,f344])).
% 0.10/0.42 fof(f953,plain,(
% 0.10/0.42 or_ok(or1(f))|abnormal(or1(f))),
% 0.10/0.42 inference(resolution,[status(thm)],[f698,f89])).
% 0.10/0.42 fof(f954,definition,(
% 0.10/0.42 sQ115_spl <=> (or_ok(or1(f)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f957,plain,(
% 0.10/0.42 sQ115_spl|sQ0_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f953,f954,f133])).
% 0.10/0.42 fof(f959,plain,(
% 0.10/0.42 connection(outs(h1(f)),in2(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f112,f120])).
% 0.10/0.42 fof(f961,plain,(
% 0.10/0.42 connection(outc(h2(f)),in1(or1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f114,f120])).
% 0.10/0.42 fof(f962,plain,(
% 0.10/0.42 connection(inc(f),in2(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f117,f120])).
% 0.10/0.42 fof(f963,plain,(
% 0.10/0.42 connection(outs(f),outs(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f118,f120])).
% 0.10/0.42 fof(f964,plain,(
% 0.10/0.42 connection(outc(f),out1(or1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f119,f120])).
% 0.10/0.42 fof(f967,plain,(
% 0.10/0.42 ~one(inc(f))|one(in2(h1(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f962,f68])).
% 0.10/0.42 fof(f969,definition,(
% 0.10/0.42 sQ116_spl <=> (one(inc(f)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f971,plain,(
% 0.10/0.42 ~one(inc(f))|sQ116_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f969])).
% 0.10/0.42 fof(f977,plain,(
% 0.10/0.42 ~sQ116_spl|sQ26_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f967,f969,f282])).
% 0.10/0.42 fof(f979,plain,(
% 0.10/0.42 $false|sQ116_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f971,f123])).
% 0.10/0.42 fof(f980,plain,(
% 0.10/0.42 sQ116_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f979])).
% 0.10/0.42 fof(f998,plain,(
% 0.10/0.42 ~or_ok(or1(h1(f)))|one(out1(or1(h1(f))))|~sQ31_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f314,f83])).
% 0.10/0.42 fof(f1001,plain,(
% 0.10/0.42 ~sQ86_spl|sQ22_spl|~sQ31_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f998,f688,f262,f313])).
% 0.10/0.42 fof(f1044,plain,(
% 0.10/0.42 ~one(outs(f))|one(outs(h2(f)))),
% 0.10/0.42 inference(resolution,[status(thm)],[f963,f68])).
% 0.10/0.43 fof(f1046,definition,(
% 0.10/0.43 sQ119_spl <=> (one(outs(f)))),
% 0.10/0.43 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.10/0.43 fof(f1048,plain,(
% 0.10/0.43 ~one(outs(f))|sQ119_spl),
% 0.10/0.43 inference(component_clause,[status(thm)],[f1046])).
% 0.10/0.43 fof(f1054,plain,(
% 0.10/0.43 ~sQ119_spl|sQ103_spl),
% 0.10/0.43 inference(split_clause,[status(thm)],[f1044,f1046,f803])).
% 0.10/0.43 fof(f1056,plain,(
% 0.10/0.43 $false|sQ119_spl),
% 0.10/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1048,f124])).
% 0.10/0.43 fof(f1057,plain,(
% 0.10/0.43 sQ119_spl),
% 0.10/0.43 inference(contradiction_clause,[status(thm)],[f1056])).
% 0.10/0.43 fof(f1070,plain,(
% 0.10/0.43 ~one(outs(h1(f)))|one(in2(h2(f)))),
% 0.10/0.43 inference(resolution,[status(thm)],[f959,f68])).
% 0.10/0.43 fof(f1074,plain,(
% 0.10/0.43 ~sQ106_spl|sQ48_spl),
% 0.10/0.43 inference(split_clause,[status(thm)],[f1070,f820,f404])).
% 0.10/0.43 fof(f1134,plain,(
% 0.10/0.43 ~one(outc(h2(f)))|one(in1(or1(f)))),
% 0.10/0.43 inference(resolution,[status(thm)],[f961,f68])).
% 0.10/0.43 fof(f1136,definition,(
% 0.10/0.43 sQ123_spl <=> (one(in1(or1(f))))),
% 0.10/0.43 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.10/0.43 fof(f1137,plain,(
% 0.10/0.43 one(in1(or1(f)))|~sQ123_spl),
% 0.10/0.43 inference(component_clause,[status(thm)],[f1136])).
% 0.10/0.43 fof(f1144,plain,(
% 0.10/0.43 ~sQ108_spl|sQ123_spl),
% 0.10/0.43 inference(split_clause,[status(thm)],[f1134,f834,f1136])).
% 0.10/0.43 fof(f1146,plain,(
% 0.10/0.43 ~one(out1(or1(f)))|one(outc(f))),
% 0.10/0.43 inference(resolution,[status(thm)],[f964,f72])).
% 0.10/0.43 fof(f1150,definition,(
% 0.10/0.43 sQ125_spl <=> (one(out1(or1(f))))),
% 0.10/0.43 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.10/0.43 fof(f1153,definition,(
% 0.10/0.43 sQ126_spl <=> (one(outc(f)))),
% 0.10/0.43 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.10/0.43 fof(f1154,plain,(
% 0.10/0.43 one(outc(f))|~sQ126_spl),
% 0.10/0.43 inference(component_clause,[status(thm)],[f1153])).
% 0.10/0.43 fof(f1156,plain,(
% 0.10/0.43 ~sQ125_spl|sQ126_spl),
% 0.10/0.43 inference(split_clause,[status(thm)],[f1146,f1150,f1153])).
% 0.10/0.43 fof(f1160,definition,(
% 0.10/0.43 sQ128_spl <=> (zero(outc(f)))),
% 0.10/0.43 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.10/0.43 fof(f1162,plain,(
% 0.10/0.43 ~zero(outc(f))|sQ128_spl),
% 0.10/0.43 inference(component_clause,[status(thm)],[f1160])).
% 0.10/0.43 fof(f1166,plain,(
% 0.10/0.43 $false|sQ128_spl),
% 0.10/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1162,f125])).
% 0.10/0.43 fof(f1167,plain,(
% 0.10/0.43 sQ128_spl),
% 0.10/0.43 inference(contradiction_clause,[status(thm)],[f1166])).
% 0.10/0.43 fof(f1176,plain,(
% 0.10/0.43 ~or_ok(or1(f))|one(out1(or1(f)))|~sQ123_spl),
% 0.10/0.43 inference(resolution,[status(thm)],[f1137,f82])).
% 0.10/0.43 fof(f1182,plain,(
% 0.10/0.43 ~sQ115_spl|sQ125_spl|~sQ123_spl),
% 0.10/0.43 inference(split_clause,[status(thm)],[f1176,f954,f1150,f1136])).
% 0.10/0.43 fof(f1183,plain,(
% 0.10/0.43 ~zero(outc(f))|~sQ126_spl),
% 0.10/0.43 inference(resolution,[status(thm)],[f1154,f73])).
% 0.10/0.43 fof(f1184,plain,(
% 0.10/0.43 ~sQ128_spl|~sQ126_spl),
% 0.10/0.43 inference(split_clause,[status(thm)],[f1183,f1160,f1153])).
% 0.10/0.43 fof(f1185,plain,(
% 0.10/0.43 $false),
% 0.10/0.43 inference(sat_refutation,[status(thm)],[f139,f143,f188,f191,f212,f214,f233,f254,f273,f308,f321,f347,f375,f415,f429,f472,f577,f585,f592,f597,f599,f604,f658,f714,f759,f781,f786,f788,f798,f814,f823,f837,f845,f877,f912,f940,f948,f957,f977,f980,f1001,f1054,f1057,f1074,f1144,f1156,f1167,f1182,f1184])).
% 0.10/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.46 % Elapsed time: 0.069391 seconds
% 0.10/0.46 % CPU time: 0.257516 seconds
% 0.10/0.46 % Total memory used: 21.586 MB
% 0.10/0.46 % Net memory used: 21.521 MB
%------------------------------------------------------------------------------