%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV008-1.001 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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 : Fri Sep 25 01:37:38 PM UTC 2026
% Result : Unsatisfiable 4.62s 1.19s
% Output : Proof 4.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 29
% Syntax : Number of formulae : 175 ( 61 unt; 0 def)
% Number of atoms : 330 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 306 ( 151 ~; 155 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% Number of variables : 134 ( 8 sgn 58 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f30,axiom,
( connection(out(c,X),out(n1,and2(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',halfadder_connection_outc_out1and2) ).
fof(f30_nnf,plain,
! [X] :
( connection(out(c,X),out(n1,and2(X)))
| ~ type(X,halfadder) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X] :
( connection(out(c,X),out(n1,and2(X)))
| ~ type(X,halfadder) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( connection(out(c,X0),out(n1,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f45,axiom,
( type(v(n1,X),fulladder)
| ~ type(X,nbit_adder(n1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nbit_adder_fulladder1) ).
fof(f45_nnf,plain,
! [X] :
( type(v(n1,X),fulladder)
| ~ type(X,nbit_adder(n1)) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [X] :
( type(v(n1,X),fulladder)
| ~ type(X,nbit_adder(n1)) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( type(v(n1,X0),fulladder)
| ~ type(X0,nbit_adder(n1)) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(f51,hypothesis,
type(a,nbit_adder(n1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_isa_1bit_adder) ).
fof(f51_nnf,plain,
type(a,nbit_adder(n1)),
inference(nnf_transformation,[status(thm)],[f51]) ).
cnf(c51,plain,
type(a,nbit_adder(n1)),
inference(cnf_transformation,[status(esa)],[f51_nnf]) ).
cnf(p69,plain,
type(v(n1,a),fulladder),
inference(resolution,[status(thm)],[c45,c51]) ).
cnf(f35,axiom,
( type(h2(X),halfadder)
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fulladder_halfadder2) ).
fof(f35_nnf,plain,
! [X] :
( type(h2(X),halfadder)
| ~ type(X,fulladder) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [X] :
( type(h2(X),halfadder)
| ~ type(X,fulladder) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( type(h2(X0),halfadder)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p72,plain,
type(h2(v(n1,a)),halfadder),
inference(resolution,[status(thm)],[p69,c35]) ).
cnf(p104,plain,
connection(out(c,h2(v(n1,a))),out(n1,and2(h2(v(n1,a))))),
inference(resolution,[status(thm)],[c30,p72]) ).
cnf(f0,axiom,
( value(P2,V)
| ~ value(P1,V)
| ~ connection(P1,P2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',value_propagation1) ).
fof(f0_nnf,plain,
! [P1,P2,V] :
( value(P2,V)
| ~ value(P1,V)
| ~ connection(P1,P2) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [P1,P2,V] :
( value(P2,V)
| ~ value(P1,V)
| ~ connection(P1,P2) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( value(X1,X2)
| ~ value(X0,X2)
| ~ connection(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p242,plain,
( value(out(n1,and2(h2(v(n1,a)))),X0)
| ~ value(out(c,h2(v(n1,a))),X0) ),
inference(resolution,[status(thm)],[p104,c0]) ).
cnf(f34,axiom,
( type(h1(X),halfadder)
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fulladder_halfadder1) ).
fof(f34_nnf,plain,
! [X] :
( type(h1(X),halfadder)
| ~ type(X,fulladder) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [X] :
( type(h1(X),halfadder)
| ~ type(X,fulladder) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( type(h1(X0),halfadder)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p71,plain,
type(h1(v(n1,a)),halfadder),
inference(resolution,[status(thm)],[p69,c34]) ).
cnf(p103,plain,
connection(out(c,h1(v(n1,a))),out(n1,and2(h1(v(n1,a))))),
inference(resolution,[status(thm)],[c30,p71]) ).
cnf(p240,plain,
( value(out(n1,and2(h1(v(n1,a)))),X0)
| ~ value(out(c,h1(v(n1,a))),X0) ),
inference(resolution,[status(thm)],[p103,c0]) ).
cnf(f38,axiom,
( connection(out(c,h1(X)),in(n2,or1(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fulladder_connection_outch1_in2or1) ).
fof(f38_nnf,plain,
! [X] :
( connection(out(c,h1(X)),in(n2,or1(X)))
| ~ type(X,fulladder) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X] :
( connection(out(c,h1(X)),in(n2,or1(X)))
| ~ type(X,fulladder) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( connection(out(c,h1(X0)),in(n2,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p127,plain,
connection(out(c,h1(v(n1,a))),in(n2,or1(v(n1,a)))),
inference(resolution,[status(thm)],[c38,p69]) ).
cnf(f1,axiom,
( value(P1,V)
| ~ value(P2,V)
| ~ connection(P1,P2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',value_propagation2) ).
fof(f1_nnf,plain,
! [P1,P2,V] :
( value(P1,V)
| ~ value(P2,V)
| ~ connection(P1,P2) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [P1,P2,V] :
( value(P1,V)
| ~ value(P2,V)
| ~ connection(P1,P2) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( value(X0,X2)
| ~ value(X1,X2)
| ~ connection(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p164,plain,
( value(out(c,h1(v(n1,a))),X0)
| ~ value(in(n2,or1(v(n1,a))),X0) ),
inference(resolution,[status(thm)],[p127,c1]) ).
cnf(f44,axiom,
( connection(out(c,X),out(n1,or1(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fulladder_connection_outc_out1or1) ).
fof(f44_nnf,plain,
! [X] :
( connection(out(c,X),out(n1,or1(X)))
| ~ type(X,fulladder) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [X] :
( connection(out(c,X),out(n1,or1(X)))
| ~ type(X,fulladder) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( connection(out(c,X0),out(n1,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p109,plain,
connection(out(c,v(n1,a)),out(n1,or1(v(n1,a)))),
inference(resolution,[status(thm)],[c44,p69]) ).
cnf(p118,plain,
( value(out(n1,or1(v(n1,a))),X0)
| ~ value(out(c,v(n1,a)),X0) ),
inference(resolution,[status(thm)],[p109,c0]) ).
cnf(f47,axiom,
( connection(out(c,X),out(c,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nbit_adder_connection_outc_outcv1) ).
fof(f47_nnf,plain,
! [X] :
( connection(out(c,X),out(c,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [X] :
( connection(out(c,X),out(c,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
( connection(out(c,X0),out(c,v(n1,X0)))
| ~ type(X0,nbit_adder(n1)) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p148,plain,
connection(out(c,a),out(c,v(n1,a))),
inference(resolution,[status(thm)],[c47,c51]) ).
cnf(p154,plain,
( value(out(c,v(n1,a)),X0)
| ~ value(out(c,a),X0) ),
inference(resolution,[status(thm)],[p148,c0]) ).
cnf(f56,hypothesis,
value(out(c,a),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outc_0) ).
fof(f56_nnf,plain,
value(out(c,a),n1),
inference(nnf_transformation,[status(thm)],[f56]) ).
cnf(c56,plain,
value(out(c,a),n1),
inference(cnf_transformation,[status(esa)],[f56_nnf]) ).
cnf(p172,plain,
value(out(c,v(n1,a)),n1),
inference(resolution,[status(thm)],[p154,c56]) ).
cnf(p264,plain,
value(out(n1,or1(v(n1,a))),n1),
inference(resolution,[status(thm)],[p118,p172]) ).
cnf(f36,axiom,
( type(or1(X),or)
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fulladder_or1) ).
fof(f36_nnf,plain,
! [X] :
( type(or1(X),or)
| ~ type(X,fulladder) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X] :
( type(or1(X),or)
| ~ type(X,fulladder) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( type(or1(X0),or)
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p73,plain,
type(or1(v(n1,a)),or),
inference(resolution,[status(thm)],[p69,c36]) ).
cnf(f6,axiom,
( mode(K,abnormal)
| mode(K,ok)
| ~ type(K,Any) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ok_or_abnormal) ).
fof(f6_nnf,plain,
! [K,Any] :
( mode(K,abnormal)
| mode(K,ok)
| ~ type(K,Any) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [K,Any] :
( mode(K,abnormal)
| mode(K,ok)
| ~ type(K,Any) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( mode(X0,abnormal)
| mode(X0,ok)
| ~ type(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p84,plain,
( mode(or1(v(n1,a)),abnormal)
| mode(or1(v(n1,a)),ok) ),
inference(resolution,[status(thm)],[p73,c6]) ).
cnf(f57,negated_conjecture,
~ mode(or1(v(n1,a)),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_or1v1) ).
fof(f57_nnf,plain,
~ mode(or1(v(n1,a)),abnormal),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
~ mode(or1(v(n1,a)),abnormal),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c57,plain,
~ mode(or1(v(n1,a)),abnormal),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p129,plain,
mode(or1(v(n1,a)),ok),
inference(resolution,[status(thm)],[p84,c57]) ).
cnf(f14,axiom,
( value(in(n2,K),n1)
| value(in(n1,K),n1)
| ~ value(out(n1,K),n1)
| ~ type(K,or)
| ~ mode(K,ok) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_1_11) ).
fof(f14_nnf,plain,
! [K] :
( value(in(n2,K),n1)
| value(in(n1,K),n1)
| ~ value(out(n1,K),n1)
| ~ type(K,or)
| ~ mode(K,ok) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [K] :
( value(in(n2,K),n1)
| value(in(n1,K),n1)
| ~ value(out(n1,K),n1)
| ~ type(K,or)
| ~ mode(K,ok) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( value(in(n2,X0),n1)
| value(in(n1,X0),n1)
| ~ value(out(n1,X0),n1)
| ~ type(X0,or)
| ~ mode(X0,ok) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p137,plain,
( value(in(n2,or1(v(n1,a))),n1)
| value(in(n1,or1(v(n1,a))),n1)
| ~ value(out(n1,or1(v(n1,a))),n1)
| ~ type(or1(v(n1,a)),or) ),
inference(resolution,[status(thm)],[p129,c14]) ).
cnf(p150,plain,
( value(in(n2,or1(v(n1,a))),n1)
| value(in(n1,or1(v(n1,a))),n1)
| ~ value(out(n1,or1(v(n1,a))),n1) ),
inference(resolution,[status(thm)],[p137,p73]) ).
cnf(p266,plain,
( value(in(n2,or1(v(n1,a))),n1)
| value(in(n1,or1(v(n1,a))),n1) ),
inference(resolution,[status(thm)],[p264,p150]) ).
cnf(p268,plain,
( value(in(n1,or1(v(n1,a))),n1)
| value(out(c,h1(v(n1,a))),n1) ),
inference(resolution,[status(thm)],[p164,p266]) ).
cnf(p288,plain,
( value(in(n1,or1(v(n1,a))),n1)
| value(out(n1,and2(h1(v(n1,a)))),n1) ),
inference(resolution,[status(thm)],[p240,p268]) ).
cnf(f27,axiom,
( connection(in(n1,X),in(n1,and2(X)))
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',halfadder_connection_in1_in1and2) ).
fof(f27_nnf,plain,
! [X] :
( connection(in(n1,X),in(n1,and2(X)))
| ~ type(X,halfadder) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [X] :
( connection(in(n1,X),in(n1,and2(X)))
| ~ type(X,halfadder) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( connection(in(n1,X0),in(n1,and2(X0)))
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p97,plain,
connection(in(n1,h1(v(n1,a))),in(n1,and2(h1(v(n1,a))))),
inference(resolution,[status(thm)],[c27,p71]) ).
cnf(p226,plain,
( value(in(n1,and2(h1(v(n1,a)))),X0)
| ~ value(in(n1,h1(v(n1,a))),X0) ),
inference(resolution,[status(thm)],[p97,c0]) ).
cnf(f41,axiom,
( connection(in(n2,X),in(n1,h1(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fulladder_connection_in2_in1h1) ).
fof(f41_nnf,plain,
! [X] :
( connection(in(n2,X),in(n1,h1(X)))
| ~ type(X,fulladder) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X] :
( connection(in(n2,X),in(n1,h1(X)))
| ~ type(X,fulladder) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( connection(in(n2,X0),in(n1,h1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p106,plain,
connection(in(n2,v(n1,a)),in(n1,h1(v(n1,a)))),
inference(resolution,[status(thm)],[c41,p69]) ).
cnf(p112,plain,
( value(in(n1,h1(v(n1,a))),X0)
| ~ value(in(n2,v(n1,a)),X0) ),
inference(resolution,[status(thm)],[p106,c0]) ).
cnf(f49,axiom,
( connection(in(b1,X),in(n2,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nbit_adder_connection_inb1_in2v1) ).
fof(f49_nnf,plain,
! [X] :
( connection(in(b1,X),in(n2,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [X] :
( connection(in(b1,X),in(n2,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
( connection(in(b1,X0),in(n2,v(n1,X0)))
| ~ type(X0,nbit_adder(n1)) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p158,plain,
connection(in(b1,a),in(n2,v(n1,a))),
inference(resolution,[status(thm)],[c49,c51]) ).
cnf(p159,plain,
( value(in(n2,v(n1,a)),X0)
| ~ value(in(b1,a),X0) ),
inference(resolution,[status(thm)],[p158,c0]) ).
cnf(f53,hypothesis,
value(in(b1,a),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inb1_0) ).
fof(f53_nnf,plain,
value(in(b1,a),n0),
inference(nnf_transformation,[status(thm)],[f53]) ).
cnf(c53,plain,
value(in(b1,a),n0),
inference(cnf_transformation,[status(esa)],[f53_nnf]) ).
cnf(p224,plain,
value(in(n2,v(n1,a)),n0),
inference(resolution,[status(thm)],[p159,c53]) ).
cnf(p258,plain,
value(in(n1,h1(v(n1,a))),n0),
inference(resolution,[status(thm)],[p112,p224]) ).
cnf(p276,plain,
value(in(n1,and2(h1(v(n1,a)))),n0),
inference(resolution,[status(thm)],[p226,p258]) ).
cnf(f22,axiom,
( type(and2(X),and)
| ~ type(X,halfadder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',halfadder_and2) ).
fof(f22_nnf,plain,
! [X] :
( type(and2(X),and)
| ~ type(X,halfadder) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X] :
( type(and2(X),and)
| ~ type(X,halfadder) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( type(and2(X0),and)
| ~ type(X0,halfadder) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p76,plain,
type(and2(h1(v(n1,a))),and),
inference(resolution,[status(thm)],[p71,c22]) ).
cnf(p86,plain,
( mode(and2(h1(v(n1,a))),abnormal)
| mode(and2(h1(v(n1,a))),ok) ),
inference(resolution,[status(thm)],[p76,c6]) ).
cnf(f58,negated_conjecture,
~ mode(and2(h1(v(n1,a))),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_and2h1v1) ).
fof(f58_nnf,plain,
~ mode(and2(h1(v(n1,a))),abnormal),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
~ mode(and2(h1(v(n1,a))),abnormal),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
~ mode(and2(h1(v(n1,a))),abnormal),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(p174,plain,
mode(and2(h1(v(n1,a))),ok),
inference(resolution,[status(thm)],[p86,c58]) ).
cnf(f7,axiom,
( value(out(n1,K),n0)
| ~ value(in(Any,K),n0)
| ~ type(K,and)
| ~ mode(K,ok) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_0x_0) ).
fof(f7_nnf,plain,
! [K,Any] :
( value(out(n1,K),n0)
| ~ value(in(Any,K),n0)
| ~ type(K,and)
| ~ mode(K,ok) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [K,Any] :
( value(out(n1,K),n0)
| ~ value(in(Any,K),n0)
| ~ type(K,and)
| ~ mode(K,ok) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( value(out(n1,X0),n0)
| ~ value(in(X1,X0),n0)
| ~ type(X0,and)
| ~ mode(X0,ok) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p175,plain,
( value(out(n1,and2(h1(v(n1,a)))),n0)
| ~ value(in(X0,and2(h1(v(n1,a)))),n0)
| ~ type(and2(h1(v(n1,a))),and) ),
inference(resolution,[status(thm)],[p174,c7]) ).
cnf(p189,plain,
( value(out(n1,and2(h1(v(n1,a)))),n0)
| ~ value(in(X0,and2(h1(v(n1,a)))),n0) ),
inference(resolution,[status(thm)],[p175,p76]) ).
cnf(p278,plain,
value(out(n1,and2(h1(v(n1,a)))),n0),
inference(resolution,[status(thm)],[p276,p189]) ).
cnf(f2,axiom,
( equal_value(V1,V2)
| ~ value(P,V2)
| ~ value(P,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_value) ).
fof(f2_nnf,plain,
! [P,V1,V2] :
( equal_value(V1,V2)
| ~ value(P,V2)
| ~ value(P,V1) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [P,V1,V2] :
( equal_value(V1,V2)
| ~ value(P,V2)
| ~ value(P,V1) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( equal_value(X1,X2)
| ~ value(X0,X2)
| ~ value(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p279,plain,
( equal_value(n0,X0)
| ~ value(out(n1,and2(h1(v(n1,a)))),X0) ),
inference(resolution,[status(thm)],[p278,c2]) ).
cnf(p292,plain,
( equal_value(n0,n1)
| value(in(n1,or1(v(n1,a))),n1) ),
inference(resolution,[status(thm)],[p288,p279]) ).
cnf(f39,axiom,
( connection(out(c,h2(X)),in(n1,or1(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fulladder_connection_outch2_in1or1) ).
fof(f39_nnf,plain,
! [X] :
( connection(out(c,h2(X)),in(n1,or1(X)))
| ~ type(X,fulladder) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X] :
( connection(out(c,h2(X)),in(n1,or1(X)))
| ~ type(X,fulladder) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( connection(out(c,h2(X0)),in(n1,or1(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p128,plain,
connection(out(c,h2(v(n1,a))),in(n1,or1(v(n1,a)))),
inference(resolution,[status(thm)],[c39,p69]) ).
cnf(p166,plain,
( value(out(c,h2(v(n1,a))),X0)
| ~ value(in(n1,or1(v(n1,a))),X0) ),
inference(resolution,[status(thm)],[p128,c1]) ).
cnf(p294,plain,
( value(out(c,h2(v(n1,a))),n1)
| equal_value(n0,n1) ),
inference(resolution,[status(thm)],[p292,p166]) ).
cnf(p301,plain,
( equal_value(n0,n1)
| value(out(n1,and2(h2(v(n1,a)))),n1) ),
inference(resolution,[status(thm)],[p242,p294]) ).
cnf(p98,plain,
connection(in(n1,h2(v(n1,a))),in(n1,and2(h2(v(n1,a))))),
inference(resolution,[status(thm)],[c27,p72]) ).
cnf(p230,plain,
( value(in(n1,and2(h2(v(n1,a)))),X0)
| ~ value(in(n1,h2(v(n1,a))),X0) ),
inference(resolution,[status(thm)],[p98,c0]) ).
cnf(f40,axiom,
( connection(in(n1,X),in(n1,h2(X)))
| ~ type(X,fulladder) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fulladder_connection_in1_in1h2) ).
fof(f40_nnf,plain,
! [X] :
( connection(in(n1,X),in(n1,h2(X)))
| ~ type(X,fulladder) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [X] :
( connection(in(n1,X),in(n1,h2(X)))
| ~ type(X,fulladder) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( connection(in(n1,X0),in(n1,h2(X0)))
| ~ type(X0,fulladder) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p105,plain,
connection(in(n1,v(n1,a)),in(n1,h2(v(n1,a)))),
inference(resolution,[status(thm)],[c40,p69]) ).
cnf(p110,plain,
( value(in(n1,h2(v(n1,a))),X0)
| ~ value(in(n1,v(n1,a)),X0) ),
inference(resolution,[status(thm)],[p105,c0]) ).
cnf(f48,axiom,
( connection(in(a1,X),in(n1,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nbit_adder_connection_ina1_in1v1) ).
fof(f48_nnf,plain,
! [X] :
( connection(in(a1,X),in(n1,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [X] :
( connection(in(a1,X),in(n1,v(n1,X)))
| ~ type(X,nbit_adder(n1)) ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
( connection(in(a1,X0),in(n1,v(n1,X0)))
| ~ type(X0,nbit_adder(n1)) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p151,plain,
connection(in(a1,a),in(n1,v(n1,a))),
inference(resolution,[status(thm)],[c48,c51]) ).
cnf(p156,plain,
( value(in(n1,v(n1,a)),X0)
| ~ value(in(a1,a),X0) ),
inference(resolution,[status(thm)],[p151,c0]) ).
cnf(f52,hypothesis,
value(in(a1,a),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ina1_0) ).
fof(f52_nnf,plain,
value(in(a1,a),n0),
inference(nnf_transformation,[status(thm)],[f52]) ).
cnf(c52,plain,
value(in(a1,a),n0),
inference(cnf_transformation,[status(esa)],[f52_nnf]) ).
cnf(p220,plain,
value(in(n1,v(n1,a)),n0),
inference(resolution,[status(thm)],[p156,c52]) ).
cnf(p248,plain,
value(in(n1,h2(v(n1,a))),n0),
inference(resolution,[status(thm)],[p110,p220]) ).
cnf(p280,plain,
value(in(n1,and2(h2(v(n1,a)))),n0),
inference(resolution,[status(thm)],[p230,p248]) ).
cnf(p81,plain,
type(and2(h2(v(n1,a))),and),
inference(resolution,[status(thm)],[p72,c22]) ).
cnf(p90,plain,
( mode(and2(h2(v(n1,a))),abnormal)
| mode(and2(h2(v(n1,a))),ok) ),
inference(resolution,[status(thm)],[p81,c6]) ).
cnf(f59,negated_conjecture,
~ mode(and2(h2(v(n1,a))),abnormal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagnosis_and2h2v1) ).
fof(f59_nnf,plain,
~ mode(and2(h2(v(n1,a))),abnormal),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
~ mode(and2(h2(v(n1,a))),abnormal),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,plain,
~ mode(and2(h2(v(n1,a))),abnormal),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(p193,plain,
mode(and2(h2(v(n1,a))),ok),
inference(resolution,[status(thm)],[p90,c59]) ).
cnf(p194,plain,
( value(out(n1,and2(h2(v(n1,a)))),n0)
| ~ value(in(X0,and2(h2(v(n1,a)))),n0)
| ~ type(and2(h2(v(n1,a))),and) ),
inference(resolution,[status(thm)],[p193,c7]) ).
cnf(p208,plain,
( value(out(n1,and2(h2(v(n1,a)))),n0)
| ~ value(in(X0,and2(h2(v(n1,a)))),n0) ),
inference(resolution,[status(thm)],[p194,p81]) ).
cnf(p282,plain,
value(out(n1,and2(h2(v(n1,a)))),n0),
inference(resolution,[status(thm)],[p280,p208]) ).
cnf(p283,plain,
( equal_value(n0,X0)
| ~ value(out(n1,and2(h2(v(n1,a)))),X0) ),
inference(resolution,[status(thm)],[p282,c2]) ).
cnf(p309,plain,
( equal_value(n0,n1)
| equal_value(n0,n1) ),
inference(resolution,[status(thm)],[p301,p283]) ).
cnf(p311,plain,
equal_value(n0,n1),
inference(factoring,[status(thm)],[p309]) ).
cnf(f3,axiom,
~ equal_value(n0,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_value1) ).
fof(f3_nnf,plain,
~ equal_value(n0,n1),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
~ equal_value(n0,n1),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
~ equal_value(n0,n1),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p312,plain,
$false,
inference(resolution,[status(thm)],[p311,c3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV008-1.001 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.37 % Computer : n005.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Wed Sep 23 16:20:47 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.62/1.19 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.62/1.19 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------