%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV008-1.002 : TPTP v9.3.1. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV008-1.002 : TPTP v9.3.1. Bugfixed v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n002.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 20:50:32 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f1,axiom,(
% 0.14/0.40 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P1,V)| value(P2,V) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f2,axiom,(
% 0.14/0.40 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P2,V)| value(P1,V) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f3,axiom,(
% 0.14/0.40 (![P,V1,V2]: (( ~ value(P,V1)| ~ value(P,V2)| equal_value(V1,V2) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f5,axiom,(
% 0.14/0.40 ~ equal_value(n1,n0) ),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f7,axiom,(
% 0.14/0.40 (![K,Any]: (( ~ type(K,Any)| mode(K,ok)| mode(K,abnormal) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f8,axiom,(
% 0.14/0.40 (![K,Any]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(in(Any,K),n0)| value(out(n1,K),n0) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f11,axiom,(
% 0.14/0.40 (![K]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(out(n1,K),n1)| value(in(n1,K),n1) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f15,axiom,(
% 0.14/0.40 (![K]: (( ~ mode(K,ok)| ~ type(K,or)| ~ value(out(n1,K),n1)| value(in(n1,K),n1)| value(in(n2,K),n1) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f23,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,halfadder)| type(and2(X),and) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f28,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,halfadder)| connection(in(n1,X),in(n1,and2(X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f31,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,halfadder)| connection(out(c,X),out(n1,and2(X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f35,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,fulladder)| type(h1(X),halfadder) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f36,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,fulladder)| type(h2(X),halfadder) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f37,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,fulladder)| type(or1(X),or) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f39,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,fulladder)| connection(out(c,h1(X)),in(n2,or1(X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f40,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,fulladder)| connection(out(c,h2(X)),in(n1,or1(X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f41,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,fulladder)| connection(in(n1,X),in(n1,h2(X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f42,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,fulladder)| connection(in(n2,X),in(n1,h1(X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f45,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,fulladder)| connection(out(c,X),out(n1,or1(X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f47,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,nbit_adder(n2))| type(f(n2,X),fulladder) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f50,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,nbit_adder(n2))| connection(out(c,X),out(c,f(n2,X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f53,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,nbit_adder(n2))| connection(in(a2,X),in(n1,f(n2,X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f54,axiom,(
% 0.14/0.40 (![X]: (( ~ type(X,nbit_adder(n2))| connection(in(b2,X),in(n2,f(n2,X))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f57,hypothesis,(
% 0.14/0.40 type(a,nbit_adder(n2)) ),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f59,hypothesis,(
% 0.14/0.40 value(in(a2,a),n0) ),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f61,hypothesis,(
% 0.14/0.40 value(in(b2,a),n0) ),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f65,hypothesis,(
% 0.14/0.40 value(out(c,a),n1) ),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f66,negated_conjecture,(
% 0.14/0.40 ~ mode(or1(f(n2,a)),abnormal) ),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f67,negated_conjecture,(
% 0.14/0.41 ~ mode(and2(h1(f(n2,a))),abnormal) ),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f68,negated_conjecture,(
% 0.14/0.41 ~ mode(and2(h2(f(n2,a))),abnormal) ),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f69,plain,(
% 0.14/0.41 ![P2,V]: ((![P1]: (~connection(P1,P2)|~value(P1,V)))|value(P2,V))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f1])).
% 0.14/0.41 fof(f70,plain,(
% 0.14/0.41 ![X0,X1,X2]: (~connection(X0,X1)|~value(X0,X2)|value(X1,X2))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/0.41 fof(f71,plain,(
% 0.14/0.41 ![P1,V]: ((![P2]: (~connection(P1,P2)|~value(P2,V)))|value(P1,V))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f2])).
% 0.14/0.41 fof(f72,plain,(
% 0.14/0.41 ![X0,X1,X2]: (~connection(X0,X1)|~value(X1,X2)|value(X0,X2))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.14/0.41 fof(f73,plain,(
% 0.14/0.41 ![V1,V2]: ((![P]: (~value(P,V1)|~value(P,V2)))|equal_value(V1,V2))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f3])).
% 0.14/0.41 fof(f74,plain,(
% 0.14/0.41 ![X0,X1,X2]: (~value(X0,X1)|~value(X0,X2)|equal_value(X1,X2))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.41 fof(f76,plain,(
% 0.14/0.41 ~equal_value(n1,n0)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.41 fof(f78,plain,(
% 0.14/0.41 ![K]: (((![Any]: ~type(K,Any))|mode(K,ok))|mode(K,abnormal))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f7])).
% 0.14/0.41 fof(f79,plain,(
% 0.14/0.41 ![X0,X1]: (~type(X0,X1)|mode(X0,ok)|mode(X0,abnormal))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.41 fof(f80,plain,(
% 0.14/0.41 ![K]: (((~mode(K,ok)|~type(K,and))|(![Any]: ~value(in(Any,K),n0)))|value(out(n1,K),n0))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f8])).
% 0.14/0.41 fof(f81,plain,(
% 0.14/0.41 ![X0,X1]: (~mode(X0,ok)|~type(X0,and)|~value(in(X1,X0),n0)|value(out(n1,X0),n0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.41 fof(f84,plain,(
% 0.14/0.41 ![X0]: (~mode(X0,ok)|~type(X0,and)|~value(out(n1,X0),n1)|value(in(n1,X0),n1))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f11])).
% 0.14/0.41 fof(f89,plain,(
% 0.14/0.41 ![X0]: (~mode(X0,ok)|~type(X0,or)|~value(out(n1,X0),n1)|value(in(n1,X0),n1)|value(in(n2,X0),n1))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.14/0.41 fof(f97,plain,(
% 0.14/0.41 ![X0]: (~type(X0,halfadder)|type(and2(X0),and))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/0.41 fof(f102,plain,(
% 0.14/0.41 ![X0]: (~type(X0,halfadder)|connection(in(n1,X0),in(n1,and2(X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/0.41 fof(f105,plain,(
% 0.14/0.41 ![X0]: (~type(X0,halfadder)|connection(out(c,X0),out(n1,and2(X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f31])).
% 0.14/0.41 fof(f109,plain,(
% 0.14/0.41 ![X0]: (~type(X0,fulladder)|type(h1(X0),halfadder))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f35])).
% 0.14/0.41 fof(f110,plain,(
% 0.14/0.41 ![X0]: (~type(X0,fulladder)|type(h2(X0),halfadder))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f36])).
% 0.14/0.41 fof(f111,plain,(
% 0.14/0.41 ![X0]: (~type(X0,fulladder)|type(or1(X0),or))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f37])).
% 0.14/0.41 fof(f113,plain,(
% 0.14/0.41 ![X0]: (~type(X0,fulladder)|connection(out(c,h1(X0)),in(n2,or1(X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/0.41 fof(f114,plain,(
% 0.14/0.41 ![X0]: (~type(X0,fulladder)|connection(out(c,h2(X0)),in(n1,or1(X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f40])).
% 0.14/0.41 fof(f115,plain,(
% 0.14/0.41 ![X0]: (~type(X0,fulladder)|connection(in(n1,X0),in(n1,h2(X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/0.41 fof(f116,plain,(
% 0.14/0.41 ![X0]: (~type(X0,fulladder)|connection(in(n2,X0),in(n1,h1(X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/0.41 fof(f119,plain,(
% 0.14/0.41 ![X0]: (~type(X0,fulladder)|connection(out(c,X0),out(n1,or1(X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.41 fof(f121,plain,(
% 0.14/0.41 ![X0]: (~type(X0,nbit_adder(n2))|type(f(n2,X0),fulladder))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f47])).
% 0.14/0.41 fof(f124,plain,(
% 0.14/0.41 ![X0]: (~type(X0,nbit_adder(n2))|connection(out(c,X0),out(c,f(n2,X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/0.41 fof(f127,plain,(
% 0.14/0.41 ![X0]: (~type(X0,nbit_adder(n2))|connection(in(a2,X0),in(n1,f(n2,X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f53])).
% 0.14/0.41 fof(f128,plain,(
% 0.14/0.41 ![X0]: (~type(X0,nbit_adder(n2))|connection(in(b2,X0),in(n2,f(n2,X0))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f54])).
% 0.14/0.41 fof(f131,plain,(
% 0.14/0.41 type(a,nbit_adder(n2))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/0.41 fof(f133,plain,(
% 0.14/0.41 value(in(a2,a),n0)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.14/0.41 fof(f135,plain,(
% 0.14/0.41 value(in(b2,a),n0)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f61])).
% 0.14/0.41 fof(f139,plain,(
% 0.14/0.41 value(out(c,a),n1)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f65])).
% 0.14/0.41 fof(f140,plain,(
% 0.14/0.41 ~mode(or1(f(n2,a)),abnormal)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f66])).
% 0.14/0.41 fof(f141,plain,(
% 0.14/0.41 ~mode(and2(h1(f(n2,a))),abnormal)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f67])).
% 0.14/0.41 fof(f142,plain,(
% 0.14/0.41 ~mode(and2(h2(f(n2,a))),abnormal)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f68])).
% 0.14/0.41 fof(f144,plain,(
% 0.14/0.41 ![X0]: (~connection(in(b2,a),X0)|value(X0,n0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f70,f135])).
% 0.14/0.41 fof(f146,plain,(
% 0.14/0.41 ![X0]: (~connection(in(a2,a),X0)|value(X0,n0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f70,f133])).
% 0.14/0.41 fof(f185,plain,(
% 0.14/0.41 ![X0]: (~connection(out(c,a),X0)|value(X0,n1))),
% 0.14/0.41 inference(resolution,[status(thm)],[f139,f70])).
% 0.14/0.41 fof(f358,plain,(
% 0.14/0.41 type(f(n2,a),fulladder)),
% 0.14/0.41 inference(resolution,[status(thm)],[f121,f131])).
% 0.14/0.41 fof(f359,plain,(
% 0.14/0.41 type(or1(f(n2,a)),or)),
% 0.14/0.41 inference(resolution,[status(thm)],[f358,f111])).
% 0.14/0.41 fof(f360,plain,(
% 0.14/0.41 connection(out(c,f(n2,a)),out(n1,or1(f(n2,a))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f358,f119])).
% 0.14/0.41 fof(f362,plain,(
% 0.14/0.41 connection(in(n2,f(n2,a)),in(n1,h1(f(n2,a))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f358,f116])).
% 0.14/0.41 fof(f363,plain,(
% 0.14/0.41 connection(in(n1,f(n2,a)),in(n1,h2(f(n2,a))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f358,f115])).
% 0.14/0.41 fof(f364,plain,(
% 0.14/0.41 connection(out(c,h2(f(n2,a))),in(n1,or1(f(n2,a))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f358,f114])).
% 0.14/0.41 fof(f365,plain,(
% 0.14/0.41 connection(out(c,h1(f(n2,a))),in(n2,or1(f(n2,a))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f358,f113])).
% 0.14/0.41 fof(f366,plain,(
% 0.14/0.41 type(h2(f(n2,a)),halfadder)),
% 0.14/0.41 inference(resolution,[status(thm)],[f358,f110])).
% 0.14/0.41 fof(f367,plain,(
% 0.14/0.41 type(h1(f(n2,a)),halfadder)),
% 0.14/0.41 inference(resolution,[status(thm)],[f358,f109])).
% 0.14/0.41 fof(f377,plain,(
% 0.14/0.41 mode(or1(f(n2,a)),ok)|mode(or1(f(n2,a)),abnormal)),
% 0.14/0.41 inference(resolution,[status(thm)],[f359,f79])).
% 0.14/0.41 fof(f378,definition,(
% 0.14/0.41 sQ32_spl <=> (mode(or1(f(n2,a)),ok))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f381,definition,(
% 0.14/0.41 sQ33_spl <=> (mode(or1(f(n2,a)),abnormal))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f382,plain,(
% 0.14/0.41 mode(or1(f(n2,a)),abnormal)|~sQ33_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f381])).
% 0.14/0.41 fof(f384,plain,(
% 0.14/0.41 sQ32_spl|sQ33_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f377,f378,f381])).
% 0.14/0.41 fof(f388,plain,(
% 0.14/0.41 connection(out(c,h2(f(n2,a))),out(n1,and2(h2(f(n2,a)))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f366,f105])).
% 0.14/0.41 fof(f390,plain,(
% 0.14/0.41 connection(in(n1,h2(f(n2,a))),in(n1,and2(h2(f(n2,a)))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f366,f102])).
% 0.14/0.41 fof(f393,plain,(
% 0.14/0.41 type(and2(h2(f(n2,a))),and)),
% 0.14/0.41 inference(resolution,[status(thm)],[f366,f97])).
% 0.14/0.41 fof(f405,plain,(
% 0.14/0.41 connection(out(c,h1(f(n2,a))),out(n1,and2(h1(f(n2,a)))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f367,f105])).
% 0.14/0.41 fof(f407,plain,(
% 0.14/0.41 connection(in(n1,h1(f(n2,a))),in(n1,and2(h1(f(n2,a)))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f367,f102])).
% 0.14/0.41 fof(f410,plain,(
% 0.14/0.41 type(and2(h1(f(n2,a))),and)),
% 0.14/0.41 inference(resolution,[status(thm)],[f367,f97])).
% 0.14/0.41 fof(f446,plain,(
% 0.14/0.41 mode(and2(h2(f(n2,a))),ok)|mode(and2(h2(f(n2,a))),abnormal)),
% 0.14/0.41 inference(resolution,[status(thm)],[f393,f79])).
% 0.14/0.41 fof(f447,definition,(
% 0.14/0.41 sQ44_spl <=> (mode(and2(h2(f(n2,a))),ok))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f450,definition,(
% 0.14/0.41 sQ45_spl <=> (mode(and2(h2(f(n2,a))),abnormal))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f451,plain,(
% 0.14/0.41 mode(and2(h2(f(n2,a))),abnormal)|~sQ45_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f450])).
% 0.14/0.41 fof(f453,plain,(
% 0.14/0.41 sQ44_spl|sQ45_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f446,f447,f450])).
% 0.14/0.41 fof(f478,plain,(
% 0.14/0.41 mode(and2(h1(f(n2,a))),ok)|mode(and2(h1(f(n2,a))),abnormal)),
% 0.14/0.41 inference(resolution,[status(thm)],[f410,f79])).
% 0.14/0.41 fof(f479,definition,(
% 0.14/0.41 sQ52_spl <=> (mode(and2(h1(f(n2,a))),ok))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f482,definition,(
% 0.14/0.41 sQ53_spl <=> (mode(and2(h1(f(n2,a))),abnormal))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f483,plain,(
% 0.14/0.41 mode(and2(h1(f(n2,a))),abnormal)|~sQ53_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f482])).
% 0.14/0.41 fof(f485,plain,(
% 0.14/0.41 sQ52_spl|sQ53_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f478,f479,f482])).
% 0.14/0.41 fof(f623,plain,(
% 0.14/0.41 connection(out(c,a),out(c,f(n2,a)))),
% 0.14/0.41 inference(resolution,[status(thm)],[f124,f131])).
% 0.14/0.41 fof(f624,plain,(
% 0.14/0.41 value(out(c,f(n2,a)),n1)),
% 0.14/0.41 inference(resolution,[status(thm)],[f623,f185])).
% 0.14/0.41 fof(f627,plain,(
% 0.14/0.41 ![X0]: (~connection(out(c,f(n2,a)),X0)|value(X0,n1))),
% 0.14/0.41 inference(resolution,[status(thm)],[f624,f70])).
% 0.14/0.41 fof(f630,plain,(
% 0.14/0.41 value(out(n1,or1(f(n2,a))),n1)),
% 0.14/0.41 inference(resolution,[status(thm)],[f627,f360])).
% 0.14/0.41 fof(f634,plain,(
% 0.14/0.41 ~mode(or1(f(n2,a)),ok)|~type(or1(f(n2,a)),or)|value(in(n1,or1(f(n2,a))),n1)|value(in(n2,or1(f(n2,a))),n1)),
% 0.14/0.41 inference(resolution,[status(thm)],[f630,f89])).
% 0.14/0.41 fof(f648,definition,(
% 0.14/0.41 sQ75_spl <=> (value(in(n2,or1(f(n2,a))),n1))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f649,plain,(
% 0.14/0.41 value(in(n2,or1(f(n2,a))),n1)|~sQ75_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f648])).
% 0.14/0.41 fof(f652,definition,(
% 0.14/0.41 sQ76_spl <=> (value(in(n1,or1(f(n2,a))),n1))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f653,plain,(
% 0.14/0.41 value(in(n1,or1(f(n2,a))),n1)|~sQ76_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f652])).
% 0.14/0.41 fof(f656,definition,(
% 0.14/0.41 sQ77_spl <=> (type(or1(f(n2,a)),or))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f658,plain,(
% 0.14/0.41 ~type(or1(f(n2,a)),or)|sQ77_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f656])).
% 0.14/0.41 fof(f659,plain,(
% 0.14/0.41 ~sQ32_spl|~sQ77_spl|sQ76_spl|sQ75_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f634,f378,f656,f652,f648])).
% 0.14/0.41 fof(f664,plain,(
% 0.14/0.41 ![X0]: (~connection(X0,in(n2,or1(f(n2,a))))|value(X0,n1)|~sQ75_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f649,f72])).
% 0.14/0.41 fof(f670,plain,(
% 0.14/0.41 $false|sQ77_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f658,f359])).
% 0.14/0.41 fof(f671,plain,(
% 0.14/0.41 sQ77_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f670])).
% 0.14/0.41 fof(f676,plain,(
% 0.14/0.41 ![X0]: (~connection(X0,in(n1,or1(f(n2,a))))|value(X0,n1)|~sQ76_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f653,f72])).
% 0.14/0.41 fof(f685,plain,(
% 0.14/0.41 value(out(c,h2(f(n2,a))),n1)|~sQ76_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f676,f364])).
% 0.14/0.41 fof(f688,plain,(
% 0.14/0.41 ![X0]: (~connection(out(c,h2(f(n2,a))),X0)|value(X0,n1)|~sQ76_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f685,f70])).
% 0.14/0.41 fof(f690,plain,(
% 0.14/0.41 value(out(n1,and2(h2(f(n2,a)))),n1)|~sQ76_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f688,f388])).
% 0.14/0.41 fof(f706,definition,(
% 0.14/0.41 sQ82_spl <=> (type(and2(h2(f(n2,a))),and))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f708,plain,(
% 0.14/0.41 ~type(and2(h2(f(n2,a))),and)|sQ82_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f706])).
% 0.14/0.41 fof(f721,plain,(
% 0.14/0.41 $false|sQ82_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f708,f393])).
% 0.14/0.41 fof(f722,plain,(
% 0.14/0.41 sQ82_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f721])).
% 0.14/0.41 fof(f723,plain,(
% 0.14/0.41 $false|~sQ33_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f382,f140])).
% 0.14/0.41 fof(f724,plain,(
% 0.14/0.41 ~sQ33_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f723])).
% 0.14/0.41 fof(f725,plain,(
% 0.14/0.41 $false|~sQ45_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f451,f142])).
% 0.14/0.41 fof(f726,plain,(
% 0.14/0.41 ~sQ45_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f725])).
% 0.14/0.41 fof(f743,plain,(
% 0.14/0.41 value(out(c,h1(f(n2,a))),n1)|~sQ75_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f664,f365])).
% 0.14/0.41 fof(f746,plain,(
% 0.14/0.41 ![X0]: (~connection(out(c,h1(f(n2,a))),X0)|value(X0,n1)|~sQ75_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f743,f70])).
% 0.14/0.41 fof(f753,definition,(
% 0.14/0.41 sQ87_spl <=> (value(out(n1,and2(h2(f(n2,a)))),n0))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f754,plain,(
% 0.14/0.41 value(out(n1,and2(h2(f(n2,a)))),n0)|~sQ87_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f753])).
% 0.14/0.41 fof(f789,plain,(
% 0.14/0.41 connection(in(a2,a),in(n1,f(n2,a)))),
% 0.14/0.41 inference(resolution,[status(thm)],[f127,f131])).
% 0.14/0.41 fof(f794,plain,(
% 0.14/0.41 ![X0]: (~value(out(n1,and2(h2(f(n2,a)))),X0)|equal_value(X0,n0)|~sQ87_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f754,f74])).
% 0.14/0.41 fof(f820,plain,(
% 0.14/0.41 value(in(n1,f(n2,a)),n0)),
% 0.14/0.41 inference(resolution,[status(thm)],[f789,f146])).
% 0.14/0.41 fof(f826,plain,(
% 0.14/0.41 ![X0]: (~connection(in(n1,f(n2,a)),X0)|value(X0,n0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f820,f70])).
% 0.14/0.41 fof(f935,plain,(
% 0.14/0.41 value(in(n1,h2(f(n2,a))),n0)),
% 0.14/0.41 inference(resolution,[status(thm)],[f826,f363])).
% 0.14/0.41 fof(f941,plain,(
% 0.14/0.41 ![X0]: (~connection(in(n1,h2(f(n2,a))),X0)|value(X0,n0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f935,f70])).
% 0.14/0.41 fof(f1191,plain,(
% 0.14/0.41 value(in(n1,and2(h2(f(n2,a)))),n0)),
% 0.14/0.41 inference(resolution,[status(thm)],[f941,f390])).
% 0.14/0.41 fof(f1276,plain,(
% 0.14/0.41 value(out(n1,and2(h1(f(n2,a)))),n1)|~sQ75_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f746,f405])).
% 0.14/0.41 fof(f1280,plain,(
% 0.14/0.41 ~mode(and2(h1(f(n2,a))),ok)|~type(and2(h1(f(n2,a))),and)|value(in(n1,and2(h1(f(n2,a)))),n1)|~sQ75_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f1276,f84])).
% 0.14/0.41 fof(f1292,definition,(
% 0.14/0.41 sQ156_spl <=> (type(and2(h1(f(n2,a))),and))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1294,plain,(
% 0.14/0.41 ~type(and2(h1(f(n2,a))),and)|sQ156_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f1292])).
% 0.14/0.41 fof(f1299,definition,(
% 0.14/0.41 sQ158_spl <=> (value(in(n1,and2(h1(f(n2,a)))),n1))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1300,plain,(
% 0.14/0.41 value(in(n1,and2(h1(f(n2,a)))),n1)|~sQ158_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f1299])).
% 0.14/0.41 fof(f1302,plain,(
% 0.14/0.41 ~sQ52_spl|~sQ156_spl|sQ158_spl|~sQ75_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f1280,f479,f1292,f1299,f648])).
% 0.14/0.41 fof(f1307,plain,(
% 0.14/0.41 $false|sQ156_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1294,f410])).
% 0.14/0.41 fof(f1308,plain,(
% 0.14/0.41 sQ156_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1307])).
% 0.14/0.41 fof(f1309,plain,(
% 0.14/0.41 $false|~sQ53_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f483,f141])).
% 0.14/0.41 fof(f1310,plain,(
% 0.14/0.41 ~sQ53_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1309])).
% 0.14/0.41 fof(f1321,plain,(
% 0.14/0.41 connection(in(b2,a),in(n2,f(n2,a)))),
% 0.14/0.41 inference(resolution,[status(thm)],[f128,f131])).
% 0.14/0.41 fof(f1347,plain,(
% 0.14/0.41 value(in(n2,f(n2,a)),n0)),
% 0.14/0.41 inference(resolution,[status(thm)],[f1321,f144])).
% 0.14/0.41 fof(f1351,plain,(
% 0.14/0.41 ![X0]: (~connection(in(n2,f(n2,a)),X0)|value(X0,n0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f1347,f70])).
% 0.14/0.41 fof(f1361,plain,(
% 0.14/0.41 value(in(n1,h1(f(n2,a))),n0)),
% 0.14/0.41 inference(resolution,[status(thm)],[f1351,f362])).
% 0.14/0.41 fof(f1367,plain,(
% 0.14/0.41 ![X0]: (~connection(in(n1,h1(f(n2,a))),X0)|value(X0,n0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f1361,f70])).
% 0.14/0.41 fof(f1422,plain,(
% 0.14/0.41 value(in(n1,and2(h1(f(n2,a)))),n0)),
% 0.14/0.41 inference(resolution,[status(thm)],[f1367,f407])).
% 0.14/0.41 fof(f1457,plain,(
% 0.14/0.41 ![X0]: (~value(in(n1,and2(h1(f(n2,a)))),X0)|equal_value(X0,n0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f1422,f74])).
% 0.14/0.41 fof(f1613,plain,(
% 0.14/0.41 equal_value(n1,n0)|~sQ87_spl|~sQ76_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f794,f690])).
% 0.14/0.41 fof(f1615,plain,(
% 0.14/0.41 $false|~sQ87_spl|~sQ76_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1613,f76])).
% 0.14/0.41 fof(f1616,plain,(
% 0.14/0.41 ~sQ87_spl|~sQ76_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1615])).
% 0.14/0.41 fof(f1619,plain,(
% 0.14/0.41 ~mode(and2(h2(f(n2,a))),ok)|~type(and2(h2(f(n2,a))),and)|value(out(n1,and2(h2(f(n2,a)))),n0)),
% 0.14/0.41 inference(resolution,[status(thm)],[f1191,f81])).
% 0.14/0.41 fof(f1625,plain,(
% 0.14/0.41 ~sQ44_spl|~sQ82_spl|sQ87_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f1619,f447,f706,f753])).
% 0.14/0.41 fof(f1647,plain,(
% 0.14/0.41 equal_value(n1,n0)|~sQ158_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f1300,f1457])).
% 0.14/0.41 fof(f1654,plain,(
% 0.14/0.41 $false|~sQ158_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1647,f76])).
% 0.14/0.41 fof(f1655,plain,(
% 0.14/0.41 ~sQ158_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1654])).
% 0.14/0.41 fof(f1656,plain,(
% 0.14/0.41 $false),
% 0.14/0.41 inference(sat_refutation,[status(thm)],[f384,f453,f485,f659,f671,f722,f724,f726,f1302,f1308,f1310,f1616,f1625,f1655])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.43 % Elapsed time: 0.062916 seconds
% 0.14/0.43 % CPU time: 0.260945 seconds
% 0.14/0.43 % Total memory used: 24.135 MB
% 0.14/0.43 % Net memory used: 23.982 MB
%------------------------------------------------------------------------------