%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV007-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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.02s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV007-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 20:45:51 UTC 2026
% 0.02/0.37 % CPUTime :
% 0.02/0.38 % Drodi V4.1.1
% 0.02/0.40 % Refutation found
% 0.02/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.02/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.02/0.40 fof(f1,axiom,(
% 0.02/0.40 (![P1,P2]: (( ~ connection(P1,P2)| ~ zero(P1)| zero(P2) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f2,axiom,(
% 0.02/0.40 (![P1,P2]: (( ~ connection(P1,P2)| ~ one(P1)| one(P2) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f3,axiom,(
% 0.02/0.40 (![P1,P2]: (( ~ connection(P1,P2)| ~ zero(P2)| zero(P1) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f4,axiom,(
% 0.02/0.40 (![P1,P2]: (( ~ connection(P1,P2)| ~ one(P2)| one(P1) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f5,axiom,(
% 0.02/0.40 (![P]: (( ~ zero(P)| ~ one(P) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f7,axiom,(
% 0.02/0.40 (![K]: (( ~ and_ok(K)| ~ zero(in2(K))| zero(out1(K)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f8,axiom,(
% 0.02/0.40 (![K]: (( ~ and_ok(K)| ~ one(in1(K))| ~ one(in2(K))| one(out1(K)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f10,axiom,(
% 0.02/0.40 (![K]: (( ~ and_ok(K)| ~ one(out1(K))| one(in1(K)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f13,axiom,(
% 0.02/0.40 (![K]: (( ~ logic_and(K)| and_ok(K)| abnormal(K) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f15,axiom,(
% 0.02/0.40 (![K]: (( ~ or_ok(K)| ~ one(in2(K))| one(out1(K)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f16,axiom,(
% 0.02/0.40 (![K]: (( ~ or_ok(K)| ~ zero(in1(K))| ~ zero(in2(K))| zero(out1(K)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f21,axiom,(
% 0.02/0.40 (![K]: (( ~ logic_or(K)| or_ok(K)| abnormal(K) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f23,axiom,(
% 0.02/0.40 (![K]: (( ~ not_ok(K)| ~ one(in1(K))| zero(out1(K)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f27,axiom,(
% 0.02/0.40 (![K]: (( ~ logic_not(K)| not_ok(K)| abnormal(K) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f28,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| logic_and(and1(X)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f29,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| logic_and(and2(X)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f30,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| logic_not(not1(X)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f31,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| logic_or(or1(X)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f32,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(in1(X),in1(or1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f33,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(in2(X),in2(or1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f34,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(in1(X),in1(and2(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f35,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(in2(X),in2(and2(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f36,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(outs(X),out1(and1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f37,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(outc(X),out1(and2(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f38,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(out1(or1(X)),in1(and1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f39,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(out1(and2(X)),in1(not1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f40,axiom,(
% 0.02/0.40 (![X]: (( ~ halfadder(X)| connection(out1(not1(X)),in2(and1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f41,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| halfadder(h1(X)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f42,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| halfadder(h2(X)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f43,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| logic_or(or1(X)) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f44,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| connection(outs(h1(X)),in2(h2(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f45,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| connection(outc(h1(X)),in2(or1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f47,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| connection(in1(X),in1(h2(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f48,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| connection(in2(X),in1(h1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f49,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| connection(inc(X),in2(h1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f50,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| connection(outs(X),outs(h2(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f51,axiom,(
% 0.02/0.40 (![X]: (( ~ fulladder(X)| connection(outc(X),out1(or1(X))) ) ))),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f52,hypothesis,(
% 0.02/0.40 fulladder(f) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f53,hypothesis,(
% 0.02/0.40 zero(in1(f)) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f54,hypothesis,(
% 0.02/0.40 one(in2(f)) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f55,hypothesis,(
% 0.02/0.40 one(inc(f)) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f56,hypothesis,(
% 0.02/0.40 one(outs(f)) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f57,hypothesis,(
% 0.02/0.40 zero(outc(f)) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f58,negated_conjecture,(
% 0.02/0.40 ~ abnormal(and2(h1(f))) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f59,negated_conjecture,(
% 0.02/0.40 ( ~ abnormal(or1(f))| ~ abnormal(and1(h1(f))) ) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f60,negated_conjecture,(
% 0.02/0.40 ( ~ abnormal(or1(f))| ~ abnormal(not1(h1(f))) ) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f61,negated_conjecture,(
% 0.02/0.40 ( ~ abnormal(or1(f))| ~ abnormal(and1(h2(f))) ) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f62,negated_conjecture,(
% 0.02/0.40 ( ~ abnormal(or1(f))| ~ abnormal(or1(h2(f))) ) ),
% 0.02/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.40 fof(f63,plain,(
% 0.02/0.40 ![P2]: ((![P1]: (~connection(P1,P2)|~zero(P1)))|zero(P2))),
% 0.02/0.40 inference(miniscoping,[status(thm)],[f1])).
% 0.02/0.40 fof(f64,plain,(
% 0.02/0.40 ![X0,X1]: (~connection(X0,X1)|~zero(X0)|zero(X1))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.02/0.40 fof(f65,plain,(
% 0.02/0.40 ![P2]: ((![P1]: (~connection(P1,P2)|~one(P1)))|one(P2))),
% 0.02/0.40 inference(miniscoping,[status(thm)],[f2])).
% 0.02/0.40 fof(f66,plain,(
% 0.02/0.40 ![X0,X1]: (~connection(X0,X1)|~one(X0)|one(X1))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f65])).
% 0.02/0.40 fof(f67,plain,(
% 0.02/0.40 ![P1]: ((![P2]: (~connection(P1,P2)|~zero(P2)))|zero(P1))),
% 0.02/0.40 inference(miniscoping,[status(thm)],[f3])).
% 0.02/0.40 fof(f68,plain,(
% 0.02/0.40 ![X0,X1]: (~connection(X0,X1)|~zero(X1)|zero(X0))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f67])).
% 0.02/0.40 fof(f69,plain,(
% 0.02/0.40 ![P1]: ((![P2]: (~connection(P1,P2)|~one(P2)))|one(P1))),
% 0.02/0.40 inference(miniscoping,[status(thm)],[f4])).
% 0.02/0.40 fof(f70,plain,(
% 0.02/0.40 ![X0,X1]: (~connection(X0,X1)|~one(X1)|one(X0))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f69])).
% 0.02/0.40 fof(f71,plain,(
% 0.02/0.40 ![X0]: (~zero(X0)|~one(X0))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f5])).
% 0.02/0.40 fof(f73,plain,(
% 0.02/0.40 ![X0]: (~and_ok(X0)|~zero(in2(X0))|zero(out1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.02/0.40 fof(f74,plain,(
% 0.02/0.40 ![X0]: (~and_ok(X0)|~one(in1(X0))|~one(in2(X0))|one(out1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f8])).
% 0.02/0.40 fof(f76,plain,(
% 0.02/0.40 ![X0]: (~and_ok(X0)|~one(out1(X0))|one(in1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f10])).
% 0.02/0.40 fof(f79,plain,(
% 0.02/0.40 ![X0]: (~logic_and(X0)|and_ok(X0)|abnormal(X0))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f13])).
% 0.02/0.40 fof(f81,plain,(
% 0.02/0.40 ![X0]: (~or_ok(X0)|~one(in2(X0))|one(out1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f15])).
% 0.02/0.40 fof(f82,plain,(
% 0.02/0.40 ![X0]: (~or_ok(X0)|~zero(in1(X0))|~zero(in2(X0))|zero(out1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f16])).
% 0.02/0.40 fof(f87,plain,(
% 0.02/0.40 ![X0]: (~logic_or(X0)|or_ok(X0)|abnormal(X0))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f21])).
% 0.02/0.40 fof(f89,plain,(
% 0.02/0.40 ![X0]: (~not_ok(X0)|~one(in1(X0))|zero(out1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f23])).
% 0.02/0.40 fof(f93,plain,(
% 0.02/0.40 ![X0]: (~logic_not(X0)|not_ok(X0)|abnormal(X0))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f27])).
% 0.02/0.40 fof(f94,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|logic_and(and1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f28])).
% 0.02/0.40 fof(f95,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|logic_and(and2(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f29])).
% 0.02/0.40 fof(f96,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|logic_not(not1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f30])).
% 0.02/0.40 fof(f97,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|logic_or(or1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f31])).
% 0.02/0.40 fof(f98,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(in1(X0),in1(or1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f32])).
% 0.02/0.40 fof(f99,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(in2(X0),in2(or1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f33])).
% 0.02/0.40 fof(f100,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(in1(X0),in1(and2(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f34])).
% 0.02/0.40 fof(f101,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(in2(X0),in2(and2(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f35])).
% 0.02/0.40 fof(f102,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(outs(X0),out1(and1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f36])).
% 0.02/0.40 fof(f103,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(outc(X0),out1(and2(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f37])).
% 0.02/0.40 fof(f104,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(out1(or1(X0)),in1(and1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f38])).
% 0.02/0.40 fof(f105,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(out1(and2(X0)),in1(not1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f39])).
% 0.02/0.40 fof(f106,plain,(
% 0.02/0.40 ![X0]: (~halfadder(X0)|connection(out1(not1(X0)),in2(and1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f40])).
% 0.02/0.40 fof(f107,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|halfadder(h1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f41])).
% 0.02/0.40 fof(f108,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|halfadder(h2(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.02/0.40 fof(f109,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|logic_or(or1(X0)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.02/0.40 fof(f110,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|connection(outs(h1(X0)),in2(h2(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f44])).
% 0.02/0.40 fof(f111,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|connection(outc(h1(X0)),in2(or1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f45])).
% 0.02/0.40 fof(f113,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|connection(in1(X0),in1(h2(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f47])).
% 0.02/0.40 fof(f114,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|connection(in2(X0),in1(h1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f48])).
% 0.02/0.40 fof(f115,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|connection(inc(X0),in2(h1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f49])).
% 0.02/0.40 fof(f116,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|connection(outs(X0),outs(h2(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f50])).
% 0.02/0.40 fof(f117,plain,(
% 0.02/0.40 ![X0]: (~fulladder(X0)|connection(outc(X0),out1(or1(X0))))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f51])).
% 0.02/0.40 fof(f118,plain,(
% 0.02/0.40 fulladder(f)),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f52])).
% 0.02/0.40 fof(f119,plain,(
% 0.02/0.40 zero(in1(f))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f53])).
% 0.02/0.40 fof(f120,plain,(
% 0.02/0.40 one(in2(f))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f54])).
% 0.02/0.40 fof(f121,plain,(
% 0.02/0.40 one(inc(f))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f55])).
% 0.02/0.40 fof(f122,plain,(
% 0.02/0.40 one(outs(f))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f56])).
% 0.02/0.40 fof(f123,plain,(
% 0.02/0.40 zero(outc(f))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f57])).
% 0.02/0.40 fof(f124,plain,(
% 0.02/0.40 ~abnormal(and2(h1(f)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f58])).
% 0.02/0.40 fof(f125,plain,(
% 0.02/0.40 ~abnormal(or1(f))|~abnormal(and1(h1(f)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f59])).
% 0.02/0.40 fof(f126,plain,(
% 0.02/0.40 ~abnormal(or1(f))|~abnormal(not1(h1(f)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f60])).
% 0.02/0.40 fof(f127,plain,(
% 0.02/0.40 ~abnormal(or1(f))|~abnormal(and1(h2(f)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f61])).
% 0.02/0.40 fof(f128,plain,(
% 0.02/0.40 ~abnormal(or1(f))|~abnormal(or1(h2(f)))),
% 0.02/0.40 inference(cnf_transformation,[status(thm)],[f62])).
% 0.02/0.40 fof(f129,definition,(
% 0.02/0.40 sQ0_spl <=> (abnormal(or1(f)))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f132,definition,(
% 0.02/0.40 sQ1_spl <=> (abnormal(and1(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f135,plain,(
% 0.02/0.40 ~sQ0_spl|~sQ1_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f125,f129,f132])).
% 0.02/0.40 fof(f136,definition,(
% 0.02/0.40 sQ2_spl <=> (abnormal(not1(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f139,plain,(
% 0.02/0.40 ~sQ0_spl|~sQ2_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f126,f129,f136])).
% 0.02/0.40 fof(f140,definition,(
% 0.02/0.40 sQ3_spl <=> (abnormal(and1(h2(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f143,plain,(
% 0.02/0.40 ~sQ0_spl|~sQ3_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f127,f129,f140])).
% 0.02/0.40 fof(f144,definition,(
% 0.02/0.40 sQ4_spl <=> (abnormal(or1(h2(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f147,plain,(
% 0.02/0.40 ~sQ0_spl|~sQ4_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f128,f129,f144])).
% 0.02/0.40 fof(f149,plain,(
% 0.02/0.40 halfadder(h1(f))),
% 0.02/0.40 inference(resolution,[status(thm)],[f107,f118])).
% 0.02/0.40 fof(f151,plain,(
% 0.02/0.40 connection(in2(h1(f)),in2(and2(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f149,f101])).
% 0.02/0.40 fof(f152,plain,(
% 0.02/0.40 connection(in1(h1(f)),in1(and2(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f149,f100])).
% 0.02/0.40 fof(f155,plain,(
% 0.02/0.40 halfadder(h2(f))),
% 0.02/0.40 inference(resolution,[status(thm)],[f108,f118])).
% 0.02/0.40 fof(f156,plain,(
% 0.02/0.40 connection(out1(or1(h2(f))),in1(and1(h2(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f155,f104])).
% 0.02/0.40 fof(f159,plain,(
% 0.02/0.40 connection(in2(h2(f)),in2(or1(h2(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f155,f99])).
% 0.02/0.40 fof(f160,plain,(
% 0.02/0.40 connection(in1(h2(f)),in1(or1(h2(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f155,f98])).
% 0.02/0.40 fof(f161,plain,(
% 0.02/0.40 connection(in1(f),in1(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f113,f118])).
% 0.02/0.40 fof(f164,plain,(
% 0.02/0.40 ~zero(in1(f))|zero(in1(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f161,f64])).
% 0.02/0.40 fof(f165,definition,(
% 0.02/0.40 sQ5_spl <=> (zero(in1(h2(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f168,definition,(
% 0.02/0.40 sQ6_spl <=> (zero(in1(f)))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f170,plain,(
% 0.02/0.40 ~zero(in1(f))|sQ6_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f168])).
% 0.02/0.40 fof(f179,plain,(
% 0.02/0.40 ~sQ6_spl|sQ5_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f164,f168,f165])).
% 0.02/0.40 fof(f180,plain,(
% 0.02/0.40 $false|sQ6_spl),
% 0.02/0.40 inference(forward_subsumption_resolution,[status(thm)],[f170,f119])).
% 0.02/0.40 fof(f181,plain,(
% 0.02/0.40 sQ6_spl),
% 0.02/0.40 inference(contradiction_clause,[status(thm)],[f180])).
% 0.02/0.40 fof(f183,plain,(
% 0.02/0.40 connection(out1(and2(h1(f))),in1(not1(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f105,f149])).
% 0.02/0.40 fof(f185,plain,(
% 0.02/0.40 connection(out1(not1(h1(f))),in2(and1(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f106,f149])).
% 0.02/0.40 fof(f186,plain,(
% 0.02/0.40 connection(in2(f),in1(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f114,f118])).
% 0.02/0.40 fof(f188,plain,(
% 0.02/0.40 ~one(in2(f))|one(in1(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f186,f66])).
% 0.02/0.40 fof(f197,definition,(
% 0.02/0.40 sQ11_spl <=> (one(in2(f)))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f199,plain,(
% 0.02/0.40 ~one(in2(f))|sQ11_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f197])).
% 0.02/0.40 fof(f200,definition,(
% 0.02/0.40 sQ12_spl <=> (one(in1(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f203,plain,(
% 0.02/0.40 ~sQ11_spl|sQ12_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f188,f197,f200])).
% 0.02/0.40 fof(f205,plain,(
% 0.02/0.40 $false|sQ11_spl),
% 0.02/0.40 inference(forward_subsumption_resolution,[status(thm)],[f199,f120])).
% 0.02/0.40 fof(f206,plain,(
% 0.02/0.40 sQ11_spl),
% 0.02/0.40 inference(contradiction_clause,[status(thm)],[f205])).
% 0.02/0.40 fof(f226,plain,(
% 0.02/0.40 ~one(in2(h1(f)))|one(in2(and2(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f151,f66])).
% 0.02/0.40 fof(f235,definition,(
% 0.02/0.40 sQ19_spl <=> (one(in2(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f238,definition,(
% 0.02/0.40 sQ20_spl <=> (one(in2(and2(h1(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f239,plain,(
% 0.02/0.40 one(in2(and2(h1(f))))|~sQ20_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f238])).
% 0.02/0.40 fof(f241,plain,(
% 0.02/0.40 ~sQ19_spl|sQ20_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f226,f235,f238])).
% 0.02/0.40 fof(f244,plain,(
% 0.02/0.40 ~one(in1(h1(f)))|one(in1(and2(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f152,f66])).
% 0.02/0.40 fof(f250,definition,(
% 0.02/0.40 sQ22_spl <=> (one(in1(and2(h1(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f253,plain,(
% 0.02/0.40 ~sQ12_spl|sQ22_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f244,f200,f250])).
% 0.02/0.40 fof(f283,plain,(
% 0.02/0.40 ~zero(out1(or1(h2(f))))|zero(in1(and1(h2(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f156,f64])).
% 0.02/0.40 fof(f284,definition,(
% 0.02/0.40 sQ27_spl <=> (zero(in1(and1(h2(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f287,definition,(
% 0.02/0.40 sQ28_spl <=> (zero(out1(or1(h2(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f294,definition,(
% 0.02/0.40 sQ30_spl <=> (one(in1(and1(h2(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f295,plain,(
% 0.02/0.40 one(in1(and1(h2(f))))|~sQ30_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f294])).
% 0.02/0.40 fof(f298,plain,(
% 0.02/0.40 ~sQ28_spl|sQ27_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f283,f287,f284])).
% 0.02/0.40 fof(f305,definition,(
% 0.02/0.40 sQ32_spl <=> (zero(in2(h2(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f331,plain,(
% 0.02/0.40 ~zero(in2(h2(f)))|zero(in2(or1(h2(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f159,f64])).
% 0.02/0.40 fof(f332,definition,(
% 0.02/0.40 sQ37_spl <=> (zero(in2(or1(h2(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f333,plain,(
% 0.02/0.40 zero(in2(or1(h2(f))))|~sQ37_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f332])).
% 0.02/0.40 fof(f340,plain,(
% 0.02/0.40 ~sQ32_spl|sQ37_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f331,f305,f332])).
% 0.02/0.40 fof(f343,plain,(
% 0.02/0.40 ~zero(in1(h2(f)))|zero(in1(or1(h2(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f160,f64])).
% 0.02/0.40 fof(f344,definition,(
% 0.02/0.40 sQ39_spl <=> (zero(in1(or1(h2(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f352,plain,(
% 0.02/0.40 ~sQ5_spl|sQ39_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f343,f165,f344])).
% 0.02/0.40 fof(f372,plain,(
% 0.02/0.40 ~one(out1(and2(h1(f))))|one(in1(not1(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f183,f66])).
% 0.02/0.40 fof(f381,definition,(
% 0.02/0.40 sQ47_spl <=> (one(out1(and2(h1(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f384,definition,(
% 0.02/0.40 sQ48_spl <=> (one(in1(not1(h1(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f385,plain,(
% 0.02/0.40 one(in1(not1(h1(f))))|~sQ48_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f384])).
% 0.02/0.40 fof(f387,plain,(
% 0.02/0.40 ~sQ47_spl|sQ48_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f372,f381,f384])).
% 0.02/0.40 fof(f409,plain,(
% 0.02/0.40 ~zero(out1(not1(h1(f))))|zero(in2(and1(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f185,f64])).
% 0.02/0.40 fof(f410,definition,(
% 0.02/0.40 sQ53_spl <=> (zero(in2(and1(h1(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f411,plain,(
% 0.02/0.40 zero(in2(and1(h1(f))))|~sQ53_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f410])).
% 0.02/0.40 fof(f413,definition,(
% 0.02/0.40 sQ54_spl <=> (zero(out1(not1(h1(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f424,plain,(
% 0.02/0.40 ~sQ54_spl|sQ53_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f409,f413,f410])).
% 0.02/0.40 fof(f548,plain,(
% 0.02/0.40 logic_and(and1(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f94,f155])).
% 0.02/0.40 fof(f549,plain,(
% 0.02/0.40 logic_and(and1(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f94,f149])).
% 0.02/0.40 fof(f568,plain,(
% 0.02/0.40 and_ok(and1(h2(f)))|abnormal(and1(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f548,f79])).
% 0.02/0.40 fof(f569,definition,(
% 0.02/0.40 sQ78_spl <=> (and_ok(and1(h2(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f572,plain,(
% 0.02/0.40 sQ78_spl|sQ3_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f568,f569,f140])).
% 0.02/0.40 fof(f573,plain,(
% 0.02/0.40 and_ok(and1(h1(f)))|abnormal(and1(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f549,f79])).
% 0.02/0.40 fof(f574,definition,(
% 0.02/0.40 sQ79_spl <=> (and_ok(and1(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f577,plain,(
% 0.02/0.40 sQ79_spl|sQ1_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f573,f574,f132])).
% 0.02/0.40 fof(f585,definition,(
% 0.02/0.40 sQ80_spl <=> (and_ok(and2(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f602,definition,(
% 0.02/0.40 sQ82_spl <=> (not_ok(not1(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f634,definition,(
% 0.02/0.40 sQ87_spl <=> (zero(out1(and1(h1(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f661,plain,(
% 0.02/0.40 ~and_ok(and1(h1(f)))|zero(out1(and1(h1(f))))|~sQ53_spl),
% 0.02/0.40 inference(resolution,[status(thm)],[f411,f73])).
% 0.02/0.40 fof(f666,plain,(
% 0.02/0.40 ~sQ79_spl|sQ87_spl|~sQ53_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f661,f574,f634,f410])).
% 0.02/0.40 fof(f689,plain,(
% 0.02/0.40 logic_and(and2(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f95,f149])).
% 0.02/0.40 fof(f695,plain,(
% 0.02/0.40 and_ok(and2(h1(f)))|abnormal(and2(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f689,f79])).
% 0.02/0.40 fof(f696,definition,(
% 0.02/0.40 sQ92_spl <=> (abnormal(and2(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f697,plain,(
% 0.02/0.40 abnormal(and2(h1(f)))|~sQ92_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f696])).
% 0.02/0.40 fof(f699,plain,(
% 0.02/0.40 sQ80_spl|sQ92_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f695,f585,f696])).
% 0.02/0.40 fof(f727,plain,(
% 0.02/0.40 logic_not(not1(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f96,f149])).
% 0.02/0.40 fof(f728,plain,(
% 0.02/0.40 logic_or(or1(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f97,f155])).
% 0.02/0.40 fof(f730,plain,(
% 0.02/0.40 logic_or(or1(f))),
% 0.02/0.40 inference(resolution,[status(thm)],[f109,f118])).
% 0.02/0.40 fof(f731,plain,(
% 0.02/0.40 connection(outs(h2(f)),out1(and1(h2(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f102,f155])).
% 0.02/0.40 fof(f732,plain,(
% 0.02/0.40 connection(outs(h1(f)),out1(and1(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f102,f149])).
% 0.02/0.40 fof(f734,plain,(
% 0.02/0.40 connection(outc(h1(f)),out1(and2(h1(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f103,f149])).
% 0.02/0.40 fof(f735,plain,(
% 0.02/0.40 connection(outs(h1(f)),in2(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f110,f118])).
% 0.02/0.40 fof(f744,plain,(
% 0.02/0.40 not_ok(not1(h1(f)))|abnormal(not1(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f727,f93])).
% 0.02/0.40 fof(f745,plain,(
% 0.02/0.40 sQ82_spl|sQ2_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f744,f602,f136])).
% 0.02/0.40 fof(f746,plain,(
% 0.02/0.40 or_ok(or1(h2(f)))|abnormal(or1(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f728,f87])).
% 0.02/0.40 fof(f747,definition,(
% 0.02/0.40 sQ95_spl <=> (or_ok(or1(h2(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f750,plain,(
% 0.02/0.40 sQ95_spl|sQ4_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f746,f747,f144])).
% 0.02/0.40 fof(f758,plain,(
% 0.02/0.40 ~one(outs(h2(f)))|one(out1(and1(h2(f))))),
% 0.02/0.40 inference(resolution,[status(thm)],[f731,f66])).
% 0.02/0.40 fof(f760,definition,(
% 0.02/0.40 sQ97_spl <=> (one(out1(and1(h2(f)))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f761,plain,(
% 0.02/0.40 one(out1(and1(h2(f))))|~sQ97_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f760])).
% 0.02/0.40 fof(f763,definition,(
% 0.02/0.40 sQ98_spl <=> (one(outs(h2(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f774,plain,(
% 0.02/0.40 ~sQ98_spl|sQ97_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f758,f763,f760])).
% 0.02/0.40 fof(f777,plain,(
% 0.02/0.40 ~zero(out1(and1(h1(f))))|zero(outs(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f732,f68])).
% 0.02/0.40 fof(f784,definition,(
% 0.02/0.40 sQ102_spl <=> (zero(outs(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f787,plain,(
% 0.02/0.40 ~sQ87_spl|sQ102_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f777,f634,f784])).
% 0.02/0.40 fof(f809,plain,(
% 0.02/0.40 ~one(out1(and2(h1(f))))|one(outc(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f734,f70])).
% 0.02/0.40 fof(f813,definition,(
% 0.02/0.40 sQ105_spl <=> (one(outc(h1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f816,plain,(
% 0.02/0.40 ~sQ47_spl|sQ105_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f809,f381,f813])).
% 0.02/0.40 fof(f823,plain,(
% 0.02/0.40 $false|~sQ92_spl),
% 0.02/0.40 inference(forward_subsumption_resolution,[status(thm)],[f697,f124])).
% 0.02/0.40 fof(f824,plain,(
% 0.02/0.40 ~sQ92_spl),
% 0.02/0.40 inference(contradiction_clause,[status(thm)],[f823])).
% 0.02/0.40 fof(f846,plain,(
% 0.02/0.40 connection(outc(h1(f)),in2(or1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f111,f118])).
% 0.02/0.40 fof(f848,plain,(
% 0.02/0.40 or_ok(or1(f))|abnormal(or1(f))),
% 0.02/0.40 inference(resolution,[status(thm)],[f730,f87])).
% 0.02/0.40 fof(f849,definition,(
% 0.02/0.40 sQ107_spl <=> (or_ok(or1(f)))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f852,plain,(
% 0.02/0.40 sQ107_spl|sQ0_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f848,f849,f129])).
% 0.02/0.40 fof(f854,plain,(
% 0.02/0.40 connection(inc(f),in2(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f115,f118])).
% 0.02/0.40 fof(f857,plain,(
% 0.02/0.40 ~one(inc(f))|one(in2(h1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f854,f66])).
% 0.02/0.40 fof(f859,definition,(
% 0.02/0.40 sQ108_spl <=> (one(inc(f)))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f861,plain,(
% 0.02/0.40 ~one(inc(f))|sQ108_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f859])).
% 0.02/0.40 fof(f867,plain,(
% 0.02/0.40 ~sQ108_spl|sQ19_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f857,f859,f235])).
% 0.02/0.40 fof(f869,plain,(
% 0.02/0.40 $false|sQ108_spl),
% 0.02/0.40 inference(forward_subsumption_resolution,[status(thm)],[f861,f121])).
% 0.02/0.40 fof(f870,plain,(
% 0.02/0.40 sQ108_spl),
% 0.02/0.40 inference(contradiction_clause,[status(thm)],[f869])).
% 0.02/0.40 fof(f872,plain,(
% 0.02/0.40 connection(outs(f),outs(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f116,f118])).
% 0.02/0.40 fof(f873,plain,(
% 0.02/0.40 connection(outc(f),out1(or1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f117,f118])).
% 0.02/0.40 fof(f877,plain,(
% 0.02/0.40 ~zero(outs(h1(f)))|zero(in2(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f735,f64])).
% 0.02/0.40 fof(f881,plain,(
% 0.02/0.40 ~sQ102_spl|sQ32_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f877,f784,f305])).
% 0.02/0.40 fof(f889,plain,(
% 0.02/0.40 ~and_ok(and2(h1(f)))|~one(in1(and2(h1(f))))|one(out1(and2(h1(f))))|~sQ20_spl),
% 0.02/0.40 inference(resolution,[status(thm)],[f239,f74])).
% 0.02/0.40 fof(f892,plain,(
% 0.02/0.40 ~sQ80_spl|~sQ22_spl|sQ47_spl|~sQ20_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f889,f585,f250,f381,f238])).
% 0.02/0.40 fof(f908,plain,(
% 0.02/0.40 ~not_ok(not1(h1(f)))|zero(out1(not1(h1(f))))|~sQ48_spl),
% 0.02/0.40 inference(resolution,[status(thm)],[f385,f89])).
% 0.02/0.40 fof(f911,plain,(
% 0.02/0.40 ~sQ82_spl|sQ54_spl|~sQ48_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f908,f602,f413,f384])).
% 0.02/0.40 fof(f928,plain,(
% 0.02/0.40 ~one(outc(h1(f)))|one(in2(or1(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f846,f66])).
% 0.02/0.40 fof(f930,definition,(
% 0.02/0.40 sQ110_spl <=> (one(in2(or1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f931,plain,(
% 0.02/0.40 one(in2(or1(f)))|~sQ110_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f930])).
% 0.02/0.40 fof(f938,plain,(
% 0.02/0.40 ~sQ105_spl|sQ110_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f928,f813,f930])).
% 0.02/0.40 fof(f956,plain,(
% 0.02/0.40 ~one(outs(f))|one(outs(h2(f)))),
% 0.02/0.40 inference(resolution,[status(thm)],[f872,f66])).
% 0.02/0.40 fof(f958,definition,(
% 0.02/0.40 sQ114_spl <=> (one(outs(f)))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f960,plain,(
% 0.02/0.40 ~one(outs(f))|sQ114_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f958])).
% 0.02/0.40 fof(f966,plain,(
% 0.02/0.40 ~sQ114_spl|sQ98_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f956,f958,f763])).
% 0.02/0.40 fof(f968,plain,(
% 0.02/0.40 $false|sQ114_spl),
% 0.02/0.40 inference(forward_subsumption_resolution,[status(thm)],[f960,f122])).
% 0.02/0.40 fof(f969,plain,(
% 0.02/0.40 sQ114_spl),
% 0.02/0.40 inference(contradiction_clause,[status(thm)],[f968])).
% 0.02/0.40 fof(f973,plain,(
% 0.02/0.40 ~and_ok(and1(h2(f)))|one(in1(and1(h2(f))))|~sQ97_spl),
% 0.02/0.40 inference(resolution,[status(thm)],[f761,f76])).
% 0.02/0.40 fof(f981,plain,(
% 0.02/0.40 ~sQ78_spl|sQ30_spl|~sQ97_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f973,f569,f294,f760])).
% 0.02/0.40 fof(f992,plain,(
% 0.02/0.40 ~or_ok(or1(f))|one(out1(or1(f)))|~sQ110_spl),
% 0.02/0.40 inference(resolution,[status(thm)],[f931,f81])).
% 0.02/0.40 fof(f995,definition,(
% 0.02/0.40 sQ118_spl <=> (one(out1(or1(f))))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f998,plain,(
% 0.02/0.40 ~sQ107_spl|sQ118_spl|~sQ110_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f992,f849,f995,f930])).
% 0.02/0.40 fof(f1003,plain,(
% 0.02/0.40 ~one(out1(or1(f)))|one(outc(f))),
% 0.02/0.40 inference(resolution,[status(thm)],[f873,f70])).
% 0.02/0.40 fof(f1007,definition,(
% 0.02/0.40 sQ120_spl <=> (one(outc(f)))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f1008,plain,(
% 0.02/0.40 one(outc(f))|~sQ120_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f1007])).
% 0.02/0.40 fof(f1010,plain,(
% 0.02/0.40 ~sQ118_spl|sQ120_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f1003,f995,f1007])).
% 0.02/0.40 fof(f1014,definition,(
% 0.02/0.40 sQ122_spl <=> (zero(outc(f)))),
% 0.02/0.40 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.02/0.40 fof(f1016,plain,(
% 0.02/0.40 ~zero(outc(f))|sQ122_spl),
% 0.02/0.40 inference(component_clause,[status(thm)],[f1014])).
% 0.02/0.40 fof(f1020,plain,(
% 0.02/0.40 $false|sQ122_spl),
% 0.02/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1016,f123])).
% 0.02/0.40 fof(f1021,plain,(
% 0.02/0.40 sQ122_spl),
% 0.02/0.40 inference(contradiction_clause,[status(thm)],[f1020])).
% 0.02/0.40 fof(f1022,plain,(
% 0.02/0.40 ~zero(outc(f))|~sQ120_spl),
% 0.02/0.40 inference(resolution,[status(thm)],[f1008,f71])).
% 0.02/0.40 fof(f1023,plain,(
% 0.02/0.40 ~sQ122_spl|~sQ120_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f1022,f1014,f1007])).
% 0.02/0.40 fof(f1045,plain,(
% 0.02/0.40 ~or_ok(or1(h2(f)))|~zero(in1(or1(h2(f))))|zero(out1(or1(h2(f))))|~sQ37_spl),
% 0.02/0.40 inference(resolution,[status(thm)],[f333,f82])).
% 0.02/0.40 fof(f1047,plain,(
% 0.02/0.40 ~sQ95_spl|~sQ39_spl|sQ28_spl|~sQ37_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f1045,f747,f344,f287,f332])).
% 0.02/0.40 fof(f1051,plain,(
% 0.02/0.40 ~zero(in1(and1(h2(f))))|~sQ30_spl),
% 0.02/0.40 inference(resolution,[status(thm)],[f295,f71])).
% 0.02/0.40 fof(f1054,plain,(
% 0.02/0.40 ~sQ27_spl|~sQ30_spl),
% 0.02/0.40 inference(split_clause,[status(thm)],[f1051,f284,f294])).
% 0.02/0.40 fof(f1055,plain,(
% 0.02/0.40 $false),
% 0.02/0.40 inference(sat_refutation,[status(thm)],[f135,f139,f143,f147,f179,f181,f203,f206,f241,f253,f298,f340,f352,f387,f424,f572,f577,f666,f699,f745,f750,f774,f787,f816,f824,f852,f867,f870,f881,f892,f911,f938,f966,f969,f981,f998,f1010,f1021,f1023,f1047,f1054])).
% 0.02/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.02/0.42 % Elapsed time: 0.048679 seconds
% 0.02/0.42 % CPU time: 0.147696 seconds
% 0.02/0.42 % Total memory used: 20.078 MB
% 0.02/0.42 % Net memory used: 20.020 MB
%------------------------------------------------------------------------------