%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV008-1.001 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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.15s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV008-1.001 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n018.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 20:49:58 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.15/0.41 % Refutation found
% 0.15/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.41 fof(f1,axiom,(
% 0.15/0.41 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P1,V)| value(P2,V) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f2,axiom,(
% 0.15/0.41 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P2,V)| value(P1,V) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f3,axiom,(
% 0.15/0.41 (![P,V1,V2]: (( ~ value(P,V1)| ~ value(P,V2)| equal_value(V1,V2) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f4,axiom,(
% 0.15/0.41 ~ equal_value(n0,n1) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f5,axiom,(
% 0.15/0.41 ~ equal_value(n1,n0) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f7,axiom,(
% 0.15/0.41 (![K,Any]: (( ~ type(K,Any)| mode(K,ok)| mode(K,abnormal) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f8,axiom,(
% 0.15/0.41 (![K,Any]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(in(Any,K),n0)| value(out(n1,K),n0) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f11,axiom,(
% 0.15/0.41 (![K]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(out(n1,K),n1)| value(in(n1,K),n1) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f15,axiom,(
% 0.15/0.41 (![K]: (( ~ mode(K,ok)| ~ type(K,or)| ~ value(out(n1,K),n1)| value(in(n1,K),n1)| value(in(n2,K),n1) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f23,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,halfadder)| type(and2(X),and) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f28,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,halfadder)| connection(in(n1,X),in(n1,and2(X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f29,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,halfadder)| connection(in(n2,X),in(n2,and2(X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f31,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,halfadder)| connection(out(c,X),out(n1,and2(X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f35,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,fulladder)| type(h1(X),halfadder) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f36,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,fulladder)| type(h2(X),halfadder) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f37,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,fulladder)| type(or1(X),or) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f39,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,fulladder)| connection(out(c,h1(X)),in(n2,or1(X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f40,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,fulladder)| connection(out(c,h2(X)),in(n1,or1(X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f41,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,fulladder)| connection(in(n1,X),in(n1,h2(X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f43,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,fulladder)| connection(in(c,X),in(n2,h1(X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f45,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,fulladder)| connection(out(c,X),out(n1,or1(X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f46,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,nbit_adder(n1))| type(v(n1,X),fulladder) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f48,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,nbit_adder(n1))| connection(out(c,X),out(c,v(n1,X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f49,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,nbit_adder(n1))| connection(in(a1,X),in(n1,v(n1,X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f51,axiom,(
% 0.15/0.41 (![X]: (( ~ type(X,nbit_adder(n1))| connection(in(c,X),in(c,v(n1,X))) ) ))),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f52,hypothesis,(
% 0.15/0.41 type(a,nbit_adder(n1)) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f53,hypothesis,(
% 0.15/0.41 value(in(a1,a),n0) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f55,hypothesis,(
% 0.15/0.41 value(in(c,a),n0) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f57,hypothesis,(
% 0.15/0.41 value(out(c,a),n1) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f58,negated_conjecture,(
% 0.15/0.41 ~ mode(or1(v(n1,a)),abnormal) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f59,negated_conjecture,(
% 0.15/0.41 ~ mode(and2(h1(v(n1,a))),abnormal) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f60,negated_conjecture,(
% 0.15/0.41 ~ mode(and2(h2(v(n1,a))),abnormal) ),
% 0.15/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f61,plain,(
% 0.15/0.41 ![P2,V]: ((![P1]: (~connection(P1,P2)|~value(P1,V)))|value(P2,V))),
% 0.15/0.41 inference(miniscoping,[status(thm)],[f1])).
% 0.15/0.41 fof(f62,plain,(
% 0.15/0.41 ![X0,X1,X2]: (~connection(X0,X1)|~value(X0,X2)|value(X1,X2))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f61])).
% 0.15/0.41 fof(f63,plain,(
% 0.15/0.41 ![P1,V]: ((![P2]: (~connection(P1,P2)|~value(P2,V)))|value(P1,V))),
% 0.15/0.41 inference(miniscoping,[status(thm)],[f2])).
% 0.15/0.41 fof(f64,plain,(
% 0.15/0.41 ![X0,X1,X2]: (~connection(X0,X1)|~value(X1,X2)|value(X0,X2))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f63])).
% 0.15/0.41 fof(f65,plain,(
% 0.15/0.41 ![V1,V2]: ((![P]: (~value(P,V1)|~value(P,V2)))|equal_value(V1,V2))),
% 0.15/0.41 inference(miniscoping,[status(thm)],[f3])).
% 0.15/0.41 fof(f66,plain,(
% 0.15/0.41 ![X0,X1,X2]: (~value(X0,X1)|~value(X0,X2)|equal_value(X1,X2))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f65])).
% 0.15/0.41 fof(f67,plain,(
% 0.15/0.41 ~equal_value(n0,n1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f68,plain,(
% 0.15/0.41 ~equal_value(n1,n0)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f70,plain,(
% 0.15/0.41 ![K]: (((![Any]: ~type(K,Any))|mode(K,ok))|mode(K,abnormal))),
% 0.15/0.41 inference(miniscoping,[status(thm)],[f7])).
% 0.15/0.41 fof(f71,plain,(
% 0.15/0.41 ![X0,X1]: (~type(X0,X1)|mode(X0,ok)|mode(X0,abnormal))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f70])).
% 0.15/0.41 fof(f72,plain,(
% 0.15/0.41 ![K]: (((~mode(K,ok)|~type(K,and))|(![Any]: ~value(in(Any,K),n0)))|value(out(n1,K),n0))),
% 0.15/0.41 inference(miniscoping,[status(thm)],[f8])).
% 0.15/0.41 fof(f73,plain,(
% 0.15/0.41 ![X0,X1]: (~mode(X0,ok)|~type(X0,and)|~value(in(X1,X0),n0)|value(out(n1,X0),n0))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f72])).
% 0.15/0.41 fof(f76,plain,(
% 0.15/0.41 ![X0]: (~mode(X0,ok)|~type(X0,and)|~value(out(n1,X0),n1)|value(in(n1,X0),n1))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f11])).
% 0.15/0.41 fof(f81,plain,(
% 0.15/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.15/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.15/0.41 fof(f89,plain,(
% 0.15/0.41 ![X0]: (~type(X0,halfadder)|type(and2(X0),and))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f23])).
% 0.15/0.41 fof(f94,plain,(
% 0.15/0.41 ![X0]: (~type(X0,halfadder)|connection(in(n1,X0),in(n1,and2(X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f28])).
% 0.15/0.41 fof(f95,plain,(
% 0.15/0.41 ![X0]: (~type(X0,halfadder)|connection(in(n2,X0),in(n2,and2(X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f29])).
% 0.15/0.41 fof(f97,plain,(
% 0.15/0.41 ![X0]: (~type(X0,halfadder)|connection(out(c,X0),out(n1,and2(X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/0.41 fof(f101,plain,(
% 0.15/0.41 ![X0]: (~type(X0,fulladder)|type(h1(X0),halfadder))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f35])).
% 0.15/0.41 fof(f102,plain,(
% 0.15/0.41 ![X0]: (~type(X0,fulladder)|type(h2(X0),halfadder))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/0.41 fof(f103,plain,(
% 0.15/0.41 ![X0]: (~type(X0,fulladder)|type(or1(X0),or))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f37])).
% 0.15/0.41 fof(f105,plain,(
% 0.15/0.41 ![X0]: (~type(X0,fulladder)|connection(out(c,h1(X0)),in(n2,or1(X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f39])).
% 0.15/0.41 fof(f106,plain,(
% 0.15/0.41 ![X0]: (~type(X0,fulladder)|connection(out(c,h2(X0)),in(n1,or1(X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f40])).
% 0.15/0.41 fof(f107,plain,(
% 0.15/0.41 ![X0]: (~type(X0,fulladder)|connection(in(n1,X0),in(n1,h2(X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f41])).
% 0.15/0.41 fof(f109,plain,(
% 0.15/0.41 ![X0]: (~type(X0,fulladder)|connection(in(c,X0),in(n2,h1(X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f43])).
% 0.15/0.41 fof(f111,plain,(
% 0.15/0.41 ![X0]: (~type(X0,fulladder)|connection(out(c,X0),out(n1,or1(X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f45])).
% 0.15/0.41 fof(f112,plain,(
% 0.15/0.41 ![X0]: (~type(X0,nbit_adder(n1))|type(v(n1,X0),fulladder))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f46])).
% 0.15/0.41 fof(f114,plain,(
% 0.15/0.41 ![X0]: (~type(X0,nbit_adder(n1))|connection(out(c,X0),out(c,v(n1,X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f48])).
% 0.15/0.41 fof(f115,plain,(
% 0.15/0.41 ![X0]: (~type(X0,nbit_adder(n1))|connection(in(a1,X0),in(n1,v(n1,X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f49])).
% 0.15/0.41 fof(f117,plain,(
% 0.15/0.41 ![X0]: (~type(X0,nbit_adder(n1))|connection(in(c,X0),in(c,v(n1,X0))))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f51])).
% 0.15/0.41 fof(f118,plain,(
% 0.15/0.41 type(a,nbit_adder(n1))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f52])).
% 0.15/0.41 fof(f119,plain,(
% 0.15/0.41 value(in(a1,a),n0)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f53])).
% 0.15/0.41 fof(f121,plain,(
% 0.15/0.41 value(in(c,a),n0)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f55])).
% 0.15/0.41 fof(f123,plain,(
% 0.15/0.41 value(out(c,a),n1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f57])).
% 0.15/0.41 fof(f124,plain,(
% 0.15/0.41 ~mode(or1(v(n1,a)),abnormal)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f58])).
% 0.15/0.41 fof(f125,plain,(
% 0.15/0.41 ~mode(and2(h1(v(n1,a))),abnormal)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.15/0.41 fof(f126,plain,(
% 0.15/0.41 ~mode(and2(h2(v(n1,a))),abnormal)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f60])).
% 0.15/0.41 fof(f127,plain,(
% 0.15/0.41 ![X0]: (~connection(in(c,a),X0)|value(X0,n0))),
% 0.15/0.41 inference(resolution,[status(thm)],[f62,f121])).
% 0.15/0.41 fof(f155,plain,(
% 0.15/0.41 ![X0]: (~connection(out(c,a),X0)|value(X0,n1))),
% 0.15/0.41 inference(resolution,[status(thm)],[f123,f62])).
% 0.15/0.41 fof(f186,plain,(
% 0.15/0.41 ![X0]: (~connection(in(a1,a),X0)|value(X0,n0))),
% 0.15/0.41 inference(resolution,[status(thm)],[f119,f62])).
% 0.15/0.41 fof(f203,plain,(
% 0.15/0.41 type(v(n1,a),fulladder)),
% 0.15/0.41 inference(resolution,[status(thm)],[f112,f118])).
% 0.15/0.41 fof(f204,plain,(
% 0.15/0.41 type(or1(v(n1,a)),or)),
% 0.15/0.41 inference(resolution,[status(thm)],[f203,f103])).
% 0.15/0.41 fof(f205,plain,(
% 0.15/0.41 connection(out(c,v(n1,a)),out(n1,or1(v(n1,a))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f203,f111])).
% 0.15/0.41 fof(f206,plain,(
% 0.15/0.41 connection(in(c,v(n1,a)),in(n2,h1(v(n1,a))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f203,f109])).
% 0.15/0.41 fof(f208,plain,(
% 0.15/0.41 connection(in(n1,v(n1,a)),in(n1,h2(v(n1,a))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f203,f107])).
% 0.15/0.41 fof(f209,plain,(
% 0.15/0.41 connection(out(c,h2(v(n1,a))),in(n1,or1(v(n1,a))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f203,f106])).
% 0.15/0.41 fof(f210,plain,(
% 0.15/0.41 connection(out(c,h1(v(n1,a))),in(n2,or1(v(n1,a))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f203,f105])).
% 0.15/0.41 fof(f211,plain,(
% 0.15/0.41 type(h2(v(n1,a)),halfadder)),
% 0.15/0.41 inference(resolution,[status(thm)],[f203,f102])).
% 0.15/0.41 fof(f212,plain,(
% 0.15/0.41 type(h1(v(n1,a)),halfadder)),
% 0.15/0.41 inference(resolution,[status(thm)],[f203,f101])).
% 0.15/0.41 fof(f228,plain,(
% 0.15/0.41 connection(out(c,h2(v(n1,a))),out(n1,and2(h2(v(n1,a)))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f211,f97])).
% 0.15/0.41 fof(f230,plain,(
% 0.15/0.41 connection(in(n1,h2(v(n1,a))),in(n1,and2(h2(v(n1,a)))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f211,f94])).
% 0.15/0.41 fof(f233,plain,(
% 0.15/0.41 type(and2(h2(v(n1,a))),and)),
% 0.15/0.41 inference(resolution,[status(thm)],[f211,f89])).
% 0.15/0.41 fof(f249,plain,(
% 0.15/0.41 connection(out(c,h1(v(n1,a))),out(n1,and2(h1(v(n1,a)))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f212,f97])).
% 0.15/0.41 fof(f250,plain,(
% 0.15/0.41 connection(in(n2,h1(v(n1,a))),in(n2,and2(h1(v(n1,a)))))),
% 0.15/0.41 inference(resolution,[status(thm)],[f212,f95])).
% 0.15/0.41 fof(f254,plain,(
% 0.15/0.41 type(and2(h1(v(n1,a))),and)),
% 0.15/0.41 inference(resolution,[status(thm)],[f212,f89])).
% 0.15/0.41 fof(f287,plain,(
% 0.15/0.41 mode(and2(h2(v(n1,a))),ok)|mode(and2(h2(v(n1,a))),abnormal)),
% 0.15/0.41 inference(resolution,[status(thm)],[f233,f71])).
% 0.15/0.41 fof(f288,definition,(
% 0.15/0.41 sQ21_spl <=> (mode(and2(h2(v(n1,a))),ok))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f291,definition,(
% 0.15/0.41 sQ22_spl <=> (mode(and2(h2(v(n1,a))),abnormal))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f292,plain,(
% 0.15/0.41 mode(and2(h2(v(n1,a))),abnormal)|~sQ22_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f291])).
% 0.15/0.41 fof(f294,plain,(
% 0.15/0.41 sQ21_spl|sQ22_spl),
% 0.15/0.41 inference(split_clause,[status(thm)],[f287,f288,f291])).
% 0.15/0.41 fof(f319,plain,(
% 0.15/0.41 mode(and2(h1(v(n1,a))),ok)|mode(and2(h1(v(n1,a))),abnormal)),
% 0.15/0.41 inference(resolution,[status(thm)],[f254,f71])).
% 0.15/0.41 fof(f320,definition,(
% 0.15/0.41 sQ29_spl <=> (mode(and2(h1(v(n1,a))),ok))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f323,definition,(
% 0.15/0.41 sQ30_spl <=> (mode(and2(h1(v(n1,a))),abnormal))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f324,plain,(
% 0.15/0.41 mode(and2(h1(v(n1,a))),abnormal)|~sQ30_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f323])).
% 0.15/0.41 fof(f326,plain,(
% 0.15/0.41 sQ29_spl|sQ30_spl),
% 0.15/0.41 inference(split_clause,[status(thm)],[f319,f320,f323])).
% 0.15/0.41 fof(f327,plain,(
% 0.15/0.41 mode(or1(v(n1,a)),ok)|mode(or1(v(n1,a)),abnormal)),
% 0.15/0.41 inference(resolution,[status(thm)],[f204,f71])).
% 0.15/0.41 fof(f328,definition,(
% 0.15/0.41 sQ31_spl <=> (mode(or1(v(n1,a)),ok))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f331,definition,(
% 0.15/0.41 sQ32_spl <=> (mode(or1(v(n1,a)),abnormal))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f332,plain,(
% 0.15/0.41 mode(or1(v(n1,a)),abnormal)|~sQ32_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f331])).
% 0.15/0.41 fof(f334,plain,(
% 0.15/0.41 sQ31_spl|sQ32_spl),
% 0.15/0.41 inference(split_clause,[status(thm)],[f327,f328,f331])).
% 0.15/0.41 fof(f338,plain,(
% 0.15/0.41 connection(out(c,a),out(c,v(n1,a)))),
% 0.15/0.41 inference(resolution,[status(thm)],[f114,f118])).
% 0.15/0.41 fof(f339,plain,(
% 0.15/0.41 connection(in(a1,a),in(n1,v(n1,a)))),
% 0.15/0.41 inference(resolution,[status(thm)],[f115,f118])).
% 0.15/0.41 fof(f341,plain,(
% 0.15/0.41 connection(in(c,a),in(c,v(n1,a)))),
% 0.15/0.41 inference(resolution,[status(thm)],[f117,f118])).
% 0.15/0.41 fof(f348,plain,(
% 0.15/0.41 value(out(c,v(n1,a)),n1)),
% 0.15/0.41 inference(resolution,[status(thm)],[f338,f155])).
% 0.15/0.41 fof(f351,plain,(
% 0.15/0.41 ![X0]: (~connection(out(c,v(n1,a)),X0)|value(X0,n1))),
% 0.15/0.41 inference(resolution,[status(thm)],[f348,f62])).
% 0.15/0.41 fof(f354,plain,(
% 0.15/0.41 value(out(n1,or1(v(n1,a))),n1)),
% 0.15/0.41 inference(resolution,[status(thm)],[f351,f205])).
% 0.15/0.41 fof(f358,plain,(
% 0.15/0.41 ~mode(or1(v(n1,a)),ok)|~type(or1(v(n1,a)),or)|value(in(n1,or1(v(n1,a))),n1)|value(in(n2,or1(v(n1,a))),n1)),
% 0.15/0.41 inference(resolution,[status(thm)],[f354,f81])).
% 0.15/0.41 fof(f372,definition,(
% 0.15/0.41 sQ36_spl <=> (value(in(n2,or1(v(n1,a))),n1))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f373,plain,(
% 0.15/0.41 value(in(n2,or1(v(n1,a))),n1)|~sQ36_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f372])).
% 0.15/0.41 fof(f376,definition,(
% 0.15/0.41 sQ37_spl <=> (value(in(n1,or1(v(n1,a))),n1))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f377,plain,(
% 0.15/0.41 value(in(n1,or1(v(n1,a))),n1)|~sQ37_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f376])).
% 0.15/0.41 fof(f380,definition,(
% 0.15/0.41 sQ38_spl <=> (type(or1(v(n1,a)),or))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f382,plain,(
% 0.15/0.41 ~type(or1(v(n1,a)),or)|sQ38_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f380])).
% 0.15/0.41 fof(f383,plain,(
% 0.15/0.41 ~sQ31_spl|~sQ38_spl|sQ37_spl|sQ36_spl),
% 0.15/0.41 inference(split_clause,[status(thm)],[f358,f328,f380,f376,f372])).
% 0.15/0.41 fof(f388,plain,(
% 0.15/0.41 ![X0]: (~value(in(n2,or1(v(n1,a))),X0)|equal_value(X0,n1)|~sQ36_spl)),
% 0.15/0.41 inference(resolution,[status(thm)],[f373,f66])).
% 0.15/0.41 fof(f396,plain,(
% 0.15/0.41 $false|sQ38_spl),
% 0.15/0.41 inference(forward_subsumption_resolution,[status(thm)],[f382,f204])).
% 0.15/0.41 fof(f397,plain,(
% 0.15/0.41 sQ38_spl),
% 0.15/0.41 inference(contradiction_clause,[status(thm)],[f396])).
% 0.15/0.41 fof(f401,plain,(
% 0.15/0.41 ![X0]: (~connection(X0,in(n1,or1(v(n1,a))))|value(X0,n1)|~sQ37_spl)),
% 0.15/0.41 inference(resolution,[status(thm)],[f377,f64])).
% 0.15/0.41 fof(f409,plain,(
% 0.15/0.41 value(out(c,h2(v(n1,a))),n1)|~sQ37_spl),
% 0.15/0.41 inference(resolution,[status(thm)],[f401,f209])).
% 0.15/0.41 fof(f412,plain,(
% 0.15/0.41 ![X0]: (~connection(out(c,h2(v(n1,a))),X0)|value(X0,n1)|~sQ37_spl)),
% 0.15/0.41 inference(resolution,[status(thm)],[f409,f62])).
% 0.15/0.41 fof(f414,plain,(
% 0.15/0.41 value(out(n1,and2(h2(v(n1,a)))),n1)|~sQ37_spl),
% 0.15/0.41 inference(resolution,[status(thm)],[f412,f228])).
% 0.15/0.41 fof(f418,plain,(
% 0.15/0.41 ~mode(and2(h2(v(n1,a))),ok)|~type(and2(h2(v(n1,a))),and)|value(in(n1,and2(h2(v(n1,a)))),n1)|~sQ37_spl),
% 0.15/0.41 inference(resolution,[status(thm)],[f414,f76])).
% 0.15/0.41 fof(f430,definition,(
% 0.15/0.41 sQ43_spl <=> (type(and2(h2(v(n1,a))),and))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f432,plain,(
% 0.15/0.41 ~type(and2(h2(v(n1,a))),and)|sQ43_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f430])).
% 0.15/0.41 fof(f437,definition,(
% 0.15/0.41 sQ45_spl <=> (value(in(n1,and2(h2(v(n1,a)))),n1))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f438,plain,(
% 0.15/0.41 value(in(n1,and2(h2(v(n1,a)))),n1)|~sQ45_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f437])).
% 0.15/0.41 fof(f440,plain,(
% 0.15/0.41 ~sQ21_spl|~sQ43_spl|sQ45_spl|~sQ37_spl),
% 0.15/0.41 inference(split_clause,[status(thm)],[f418,f288,f430,f437,f376])).
% 0.15/0.41 fof(f445,plain,(
% 0.15/0.41 $false|sQ43_spl),
% 0.15/0.41 inference(forward_subsumption_resolution,[status(thm)],[f432,f233])).
% 0.15/0.41 fof(f446,plain,(
% 0.15/0.41 sQ43_spl),
% 0.15/0.41 inference(contradiction_clause,[status(thm)],[f445])).
% 0.15/0.41 fof(f447,plain,(
% 0.15/0.41 $false|~sQ22_spl),
% 0.15/0.41 inference(forward_subsumption_resolution,[status(thm)],[f292,f126])).
% 0.15/0.41 fof(f448,plain,(
% 0.15/0.41 ~sQ22_spl),
% 0.15/0.41 inference(contradiction_clause,[status(thm)],[f447])).
% 0.15/0.41 fof(f449,plain,(
% 0.15/0.41 $false|~sQ32_spl),
% 0.15/0.41 inference(forward_subsumption_resolution,[status(thm)],[f332,f124])).
% 0.15/0.41 fof(f450,plain,(
% 0.15/0.41 ~sQ32_spl),
% 0.15/0.41 inference(contradiction_clause,[status(thm)],[f449])).
% 0.15/0.41 fof(f490,plain,(
% 0.15/0.41 ![X0]: (~connection(X0,in(n1,and2(h2(v(n1,a)))))|value(X0,n1)|~sQ45_spl)),
% 0.15/0.41 inference(resolution,[status(thm)],[f438,f64])).
% 0.15/0.41 fof(f501,plain,(
% 0.15/0.41 value(in(n1,v(n1,a)),n0)),
% 0.15/0.41 inference(resolution,[status(thm)],[f339,f186])).
% 0.15/0.41 fof(f506,plain,(
% 0.15/0.41 ![X0]: (~connection(in(n1,v(n1,a)),X0)|value(X0,n0))),
% 0.15/0.41 inference(resolution,[status(thm)],[f501,f62])).
% 0.15/0.41 fof(f522,plain,(
% 0.15/0.41 value(in(c,v(n1,a)),n0)),
% 0.15/0.41 inference(resolution,[status(thm)],[f341,f127])).
% 0.15/0.41 fof(f526,plain,(
% 0.15/0.41 ![X0]: (~connection(in(c,v(n1,a)),X0)|value(X0,n0))),
% 0.15/0.41 inference(resolution,[status(thm)],[f522,f62])).
% 0.15/0.41 fof(f552,plain,(
% 0.15/0.41 value(in(n2,h1(v(n1,a))),n0)),
% 0.15/0.41 inference(resolution,[status(thm)],[f526,f206])).
% 0.15/0.41 fof(f557,plain,(
% 0.15/0.41 ![X0]: (~connection(in(n2,h1(v(n1,a))),X0)|value(X0,n0))),
% 0.15/0.41 inference(resolution,[status(thm)],[f552,f62])).
% 0.15/0.41 fof(f625,plain,(
% 0.15/0.41 value(in(n2,and2(h1(v(n1,a)))),n0)),
% 0.15/0.41 inference(resolution,[status(thm)],[f557,f250])).
% 0.15/0.41 fof(f646,plain,(
% 0.15/0.41 ~mode(and2(h1(v(n1,a))),ok)|~type(and2(h1(v(n1,a))),and)|value(out(n1,and2(h1(v(n1,a)))),n0)),
% 0.15/0.41 inference(resolution,[status(thm)],[f625,f73])).
% 0.15/0.41 fof(f656,definition,(
% 0.15/0.41 sQ72_spl <=> (value(out(n1,and2(h1(v(n1,a)))),n0))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f657,plain,(
% 0.15/0.41 value(out(n1,and2(h1(v(n1,a)))),n0)|~sQ72_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f656])).
% 0.15/0.41 fof(f660,definition,(
% 0.15/0.41 sQ73_spl <=> (type(and2(h1(v(n1,a))),and))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f662,plain,(
% 0.15/0.41 ~type(and2(h1(v(n1,a))),and)|sQ73_spl),
% 0.15/0.41 inference(component_clause,[status(thm)],[f660])).
% 0.15/0.41 fof(f663,plain,(
% 0.15/0.41 ~sQ29_spl|~sQ73_spl|sQ72_spl),
% 0.15/0.41 inference(split_clause,[status(thm)],[f646,f320,f660,f656])).
% 0.15/0.41 fof(f693,plain,(
% 0.15/0.41 ![X0]: (~connection(X0,out(n1,and2(h1(v(n1,a)))))|value(X0,n0)|~sQ72_spl)),
% 0.15/0.41 inference(resolution,[status(thm)],[f657,f64])).
% 0.15/0.41 fof(f708,plain,(
% 0.15/0.41 $false|sQ73_spl),
% 0.15/0.41 inference(forward_subsumption_resolution,[status(thm)],[f662,f254])).
% 0.15/0.41 fof(f709,plain,(
% 0.15/0.41 sQ73_spl),
% 0.15/0.41 inference(contradiction_clause,[status(thm)],[f708])).
% 0.15/0.41 fof(f710,plain,(
% 0.15/0.41 $false|~sQ30_spl),
% 0.15/0.41 inference(forward_subsumption_resolution,[status(thm)],[f324,f125])).
% 0.15/0.41 fof(f711,plain,(
% 0.15/0.41 ~sQ30_spl),
% 0.15/0.41 inference(contradiction_clause,[status(thm)],[f710])).
% 0.15/0.41 fof(f769,plain,(
% 0.15/0.41 value(out(c,h1(v(n1,a))),n0)|~sQ72_spl),
% 0.15/0.41 inference(resolution,[status(thm)],[f693,f249])).
% 0.15/0.41 fof(f835,plain,(
% 0.15/0.41 ![X0]: (~connection(out(c,h1(v(n1,a))),X0)|value(X0,n0)|~sQ72_spl)),
% 0.15/0.41 inference(resolution,[status(thm)],[f769,f62])).
% 0.15/0.41 fof(f1004,plain,(
% 0.15/0.41 value(in(n2,or1(v(n1,a))),n0)|~sQ72_spl),
% 0.15/0.41 inference(resolution,[status(thm)],[f835,f210])).
% 0.15/0.41 fof(f1010,plain,(
% 0.15/0.41 value(in(n1,h2(v(n1,a))),n1)|~sQ45_spl),
% 0.15/0.41 inference(resolution,[status(thm)],[f490,f230])).
% 0.15/0.41 fof(f1052,plain,(
% 0.15/0.41 value(in(n1,h2(v(n1,a))),n0)),
% 0.15/0.41 inference(resolution,[status(thm)],[f506,f208])).
% 0.15/0.42 fof(f1071,plain,(
% 0.15/0.42 ![X0]: (~value(in(n1,h2(v(n1,a))),X0)|equal_value(X0,n0))),
% 0.15/0.42 inference(resolution,[status(thm)],[f1052,f66])).
% 0.15/0.42 fof(f1085,plain,(
% 0.15/0.42 equal_value(n1,n0)|~sQ45_spl),
% 0.15/0.42 inference(resolution,[status(thm)],[f1071,f1010])).
% 0.15/0.42 fof(f1086,plain,(
% 0.15/0.42 $false|~sQ45_spl),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1085,f68])).
% 0.15/0.42 fof(f1087,plain,(
% 0.15/0.42 ~sQ45_spl),
% 0.15/0.42 inference(contradiction_clause,[status(thm)],[f1086])).
% 0.15/0.42 fof(f1136,plain,(
% 0.15/0.42 equal_value(n0,n1)|~sQ36_spl|~sQ72_spl),
% 0.15/0.42 inference(resolution,[status(thm)],[f388,f1004])).
% 0.15/0.42 fof(f1137,plain,(
% 0.15/0.42 $false|~sQ36_spl|~sQ72_spl),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1136,f67])).
% 0.15/0.42 fof(f1138,plain,(
% 0.15/0.42 ~sQ36_spl|~sQ72_spl),
% 0.15/0.42 inference(contradiction_clause,[status(thm)],[f1137])).
% 0.15/0.42 fof(f1139,plain,(
% 0.15/0.42 $false),
% 0.15/0.42 inference(sat_refutation,[status(thm)],[f294,f326,f334,f383,f397,f440,f446,f448,f450,f663,f709,f711,f1087,f1138])).
% 0.15/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.43 % Elapsed time: 0.060913 seconds
% 0.15/0.43 % CPU time: 0.259831 seconds
% 0.15/0.43 % Total memory used: 21.793 MB
% 0.15/0.43 % Net memory used: 21.630 MB
%------------------------------------------------------------------------------