%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : HWV008-1.001 : TPTP v9.0.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:46:43 PM UTC 2025
% Result : Unsatisfiable 8.45s 2.97s
% Output : CNFRefutation 8.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 43
% Syntax : Number of formulae : 208 ( 80 unt; 0 typ; 0 def)
% Number of atoms : 408 ( 0 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 431 ( 231 ~; 200 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 15 con; 0-2 aty)
% Number of variables : 113 ( 113 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ value > type > mode > equal_value > connection > v > out > in > #nlpp > or1 > not1 > nbit_adder > h2 > h1 > and2 > and1 > s > or > ok > not > n2 > n1 > n0 > halfadder > fulladder > c > b1 > and > abnormal > a1 > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(or,type,
or: $i ).
tff(a1,type,
a1: $i ).
tff(and,type,
and: $i ).
tff(not,type,
not: $i ).
tff(or1,type,
or1: $i > $i ).
tff(a,type,
a: $i ).
tff(in,type,
in: ( $i * $i ) > $i ).
tff(v,type,
v: ( $i * $i ) > $i ).
tff(connection,type,
connection: ( $i * $i ) > $o ).
tff(s,type,
s: $i ).
tff(halfadder,type,
halfadder: $i ).
tff(h2,type,
h2: $i > $i ).
tff(and2,type,
and2: $i > $i ).
tff(b1,type,
b1: $i ).
tff(equal_value,type,
equal_value: ( $i * $i ) > $o ).
tff(n1,type,
n1: $i ).
tff(nbit_adder,type,
nbit_adder: $i > $i ).
tff(h1,type,
h1: $i > $i ).
tff(n0,type,
n0: $i ).
tff(type,type,
type: ( $i * $i ) > $o ).
tff(fulladder,type,
fulladder: $i ).
tff(value,type,
value: ( $i * $i ) > $o ).
tff(not1,type,
not1: $i > $i ).
tff(and1,type,
and1: $i > $i ).
tff(abnormal,type,
abnormal: $i ).
tff(n2,type,
n2: $i ).
tff(out,type,
out: ( $i * $i ) > $i ).
tff(mode,type,
mode: ( $i * $i ) > $o ).
tff(ok,type,
ok: $i ).
tff(c,type,
c: $i ).
tff(f_456,axiom,
type(a,nbit_adder(n1)),
file(unknown,unknown) ).
tff(f_428,axiom,
! [X] :
( ~ type(X,nbit_adder(n1))
| type(v(n1,X),fulladder) ),
file(unknown,unknown) ).
tff(f_405,axiom,
! [X] :
( ~ type(X,fulladder)
| connection(in(n2,X),in(n1,h1(X))) ),
file(unknown,unknown) ).
tff(f_449,axiom,
! [X] :
( ~ type(X,nbit_adder(n1))
| connection(in(b1,X),in(n2,v(n1,X))) ),
file(unknown,unknown) ).
tff(f_458,axiom,
value(in(b1,a),n0),
file(unknown,unknown) ).
tff(f_51,axiom,
! [P1,P2,V] :
( ~ connection(P1,P2)
| ~ value(P1,V)
| value(P2,V) ),
file(unknown,unknown) ).
tff(f_379,axiom,
! [X] :
( ~ type(X,fulladder)
| type(or1(X),or) ),
file(unknown,unknown) ).
tff(f_71,axiom,
~ equal_value(n1,n0),
file(unknown,unknown) ).
tff(f_464,axiom,
~ mode(or1(v(n1,a)),abnormal),
file(unknown,unknown) ).
tff(f_85,axiom,
! [K,Any] :
( ~ type(K,Any)
| mode(K,ok)
| mode(K,abnormal) ),
file(unknown,unknown) ).
tff(f_420,axiom,
! [X] :
( ~ type(X,fulladder)
| connection(out(c,X),out(n1,or1(X))) ),
file(unknown,unknown) ).
tff(f_439,axiom,
! [X] :
( ~ type(X,nbit_adder(n1))
| connection(out(c,X),out(c,v(n1,X))) ),
file(unknown,unknown) ).
tff(f_461,axiom,
value(out(c,a),n1),
file(unknown,unknown) ).
tff(f_252,axiom,
! [K] :
( ~ mode(K,ok)
| ~ type(K,not)
| ~ value(out(n1,K),n1)
| value(in(n1,K),n0) ),
file(unknown,unknown) ).
tff(f_172,axiom,
! [K] :
( ~ mode(K,ok)
| ~ type(K,or)
| ~ value(in(n1,K),n0)
| ~ value(in(n2,K),n0)
| value(out(n1,K),n0) ),
file(unknown,unknown) ).
tff(f_67,axiom,
! [P,V1,V2] :
( ~ value(P,V1)
| ~ value(P,V2)
| equal_value(V1,V2) ),
file(unknown,unknown) ).
tff(f_390,axiom,
! [X] :
( ~ type(X,fulladder)
| connection(out(c,h1(X)),in(n2,or1(X))) ),
file(unknown,unknown) ).
tff(f_369,axiom,
! [X] :
( ~ type(X,fulladder)
| type(h1(X),halfadder) ),
file(unknown,unknown) ).
tff(f_306,axiom,
! [X] :
( ~ type(X,halfadder)
| connection(in(n2,X),in(n2,or1(X))) ),
file(unknown,unknown) ).
tff(f_410,axiom,
! [X] :
( ~ type(X,fulladder)
| connection(in(c,X),in(n2,h1(X))) ),
file(unknown,unknown) ).
tff(f_454,axiom,
! [X] :
( ~ type(X,nbit_adder(n1))
| connection(in(c,X),in(c,v(n1,X))) ),
file(unknown,unknown) ).
tff(f_459,axiom,
value(in(c,a),n0),
file(unknown,unknown) ).
tff(f_326,axiom,
! [X] :
( ~ type(X,halfadder)
| connection(out(c,X),out(n1,and2(X))) ),
file(unknown,unknown) ).
tff(f_466,axiom,
~ mode(and2(h1(v(n1,a))),abnormal),
file(unknown,unknown) ).
tff(f_285,axiom,
! [X] :
( ~ type(X,halfadder)
| type(and2(X),and) ),
file(unknown,unknown) ).
tff(f_311,axiom,
! [X] :
( ~ type(X,halfadder)
| connection(in(n1,X),in(n1,and2(X))) ),
file(unknown,unknown) ).
tff(f_219,axiom,
! [K] :
( ~ mode(K,ok)
| ~ type(K,not)
| ~ value(in(n1,K),n0)
| value(out(n1,K),n1) ),
file(unknown,unknown) ).
tff(f_135,axiom,
! [K] :
( ~ mode(K,ok)
| ~ type(K,and)
| ~ value(out(n1,K),n1)
| value(in(n1,K),n1) ),
file(unknown,unknown) ).
tff(f_69,axiom,
~ equal_value(n0,n1),
file(unknown,unknown) ).
tff(f_230,axiom,
! [K] :
( ~ mode(K,ok)
| ~ type(K,not)
| ~ value(in(n1,K),n1)
| value(out(n1,K),n0) ),
file(unknown,unknown) ).
tff(f_316,axiom,
! [X] :
( ~ type(X,halfadder)
| connection(in(n2,X),in(n2,and2(X))) ),
file(unknown,unknown) ).
tff(f_97,axiom,
! [K,Any] :
( ~ mode(K,ok)
| ~ type(K,and)
| ~ value(in(Any,K),n0)
| value(out(n1,K),n0) ),
file(unknown,unknown) ).
tff(f_59,axiom,
! [P1,P2,V] :
( ~ connection(P1,P2)
| ~ value(P2,V)
| value(P1,V) ),
file(unknown,unknown) ).
tff(f_395,axiom,
! [X] :
( ~ type(X,fulladder)
| connection(out(c,h2(X)),in(n1,or1(X))) ),
file(unknown,unknown) ).
tff(f_374,axiom,
! [X] :
( ~ type(X,fulladder)
| type(h2(X),halfadder) ),
file(unknown,unknown) ).
tff(f_321,axiom,
! [X] :
( ~ type(X,halfadder)
| connection(out(s,X),out(n1,and1(X))) ),
file(unknown,unknown) ).
tff(f_415,axiom,
! [X] :
( ~ type(X,fulladder)
| connection(out(s,X),out(s,h2(X))) ),
file(unknown,unknown) ).
tff(f_434,axiom,
! [X] :
( ~ type(X,nbit_adder(n1))
| connection(out(n1,X),out(s,v(n1,X))) ),
file(unknown,unknown) ).
tff(f_460,axiom,
value(out(n1,a),n0),
file(unknown,unknown) ).
tff(f_468,axiom,
~ mode(and2(h2(v(n1,a))),abnormal),
file(unknown,unknown) ).
tff(f_400,axiom,
! [X] :
( ~ type(X,fulladder)
| connection(in(n1,X),in(n1,h2(X))) ),
file(unknown,unknown) ).
tff(f_444,axiom,
! [X] :
( ~ type(X,nbit_adder(n1))
| connection(in(a1,X),in(n1,v(n1,X))) ),
file(unknown,unknown) ).
tff(f_457,axiom,
value(in(a1,a),n0),
file(unknown,unknown) ).
tff(c_104,plain,
type(a,nbit_adder(n1)),
inference(cnfTransformation,[status(thm)],[f_456]) ).
tff(c_92,plain,
! [X_53] :
( type(v(n1,X_53),fulladder)
| ~ type(X_53,nbit_adder(n1)) ),
inference(cnfTransformation,[status(thm)],[f_428]) ).
tff(c_84,plain,
! [X_49] :
( connection(in(n2,X_49),in(n1,h1(X_49)))
| ~ type(X_49,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_405]) ).
tff(c_474,plain,
! [X_130] :
( connection(in(b1,X_130),in(n2,v(n1,X_130)))
| ~ type(X_130,nbit_adder(n1)) ),
inference(cnfTransformation,[status(thm)],[f_449]) ).
tff(c_108,plain,
value(in(b1,a),n0),
inference(cnfTransformation,[status(thm)],[f_458]) ).
tff(c_129,plain,
! [P2_67,V_68,P1_69] :
( value(P2_67,V_68)
| ~ value(P1_69,V_68)
| ~ connection(P1_69,P2_67) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_141,plain,
! [P2_67] :
( value(P2_67,n0)
| ~ connection(in(b1,a),P2_67) ),
inference(resolution,[status(thm)],[c_108,c_129]) ).
tff(c_478,plain,
( value(in(n2,v(n1,a)),n0)
| ~ type(a,nbit_adder(n1)) ),
inference(resolution,[status(thm)],[c_474,c_141]) ).
tff(c_481,plain,
value(in(n2,v(n1,a)),n0),
inference(demodulation,[status(thm),theory(equality)],[c_104,c_478]) ).
tff(c_2,plain,
! [P2_2,V_3,P1_1] :
( value(P2_2,V_3)
| ~ value(P1_1,V_3)
| ~ connection(P1_1,P2_2) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_529,plain,
! [P2_138] :
( value(P2_138,n0)
| ~ connection(in(n2,v(n1,a)),P2_138) ),
inference(resolution,[status(thm)],[c_481,c_2]) ).
tff(c_542,plain,
( value(in(n1,h1(v(n1,a))),n0)
| ~ type(v(n1,a),fulladder) ),
inference(resolution,[status(thm)],[c_84,c_529]) ).
tff(c_572,plain,
~ type(v(n1,a),fulladder),
inference(splitLeft,[status(thm)],[c_542]) ).
tff(c_575,plain,
~ type(a,nbit_adder(n1)),
inference(resolution,[status(thm)],[c_92,c_572]) ).
tff(c_579,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_104,c_575]) ).
tff(c_581,plain,
type(v(n1,a),fulladder),
inference(splitRight,[status(thm)],[c_542]) ).
tff(c_74,plain,
! [X_44] :
( type(or1(X_44),or)
| ~ type(X_44,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_379]) ).
tff(c_10,plain,
~ equal_value(n1,n0),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_116,plain,
~ mode(or1(v(n1,a)),abnormal),
inference(cnfTransformation,[status(thm)],[f_464]) ).
tff(c_211,plain,
! [K_87,Any_88] :
( mode(K_87,abnormal)
| mode(K_87,ok)
| ~ type(K_87,Any_88) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_242,plain,
! [X_44] :
( mode(or1(X_44),abnormal)
| mode(or1(X_44),ok)
| ~ type(X_44,fulladder) ),
inference(resolution,[status(thm)],[c_74,c_211]) ).
tff(c_90,plain,
! [X_52] :
( connection(out(c,X_52),out(n1,or1(X_52)))
| ~ type(X_52,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_327,plain,
! [X_118] :
( connection(out(c,X_118),out(c,v(n1,X_118)))
| ~ type(X_118,nbit_adder(n1)) ),
inference(cnfTransformation,[status(thm)],[f_439]) ).
tff(c_114,plain,
value(out(c,a),n1),
inference(cnfTransformation,[status(thm)],[f_461]) ).
tff(c_144,plain,
! [P2_67] :
( value(P2_67,n1)
| ~ connection(out(c,a),P2_67) ),
inference(resolution,[status(thm)],[c_114,c_129]) ).
tff(c_331,plain,
( value(out(c,v(n1,a)),n1)
| ~ type(a,nbit_adder(n1)) ),
inference(resolution,[status(thm)],[c_327,c_144]) ).
tff(c_334,plain,
value(out(c,v(n1,a)),n1),
inference(demodulation,[status(thm),theory(equality)],[c_104,c_331]) ).
tff(c_369,plain,
! [P2_121] :
( value(P2_121,n1)
| ~ connection(out(c,v(n1,a)),P2_121) ),
inference(resolution,[status(thm)],[c_334,c_2]) ).
tff(c_383,plain,
( value(out(n1,or1(v(n1,a))),n1)
| ~ type(v(n1,a),fulladder) ),
inference(resolution,[status(thm)],[c_90,c_369]) ).
tff(c_718,plain,
value(out(n1,or1(v(n1,a))),n1),
inference(demodulation,[status(thm),theory(equality)],[c_581,c_383]) ).
tff(c_747,plain,
! [K_152] :
( value(in(n1,K_152),n0)
| ~ value(out(n1,K_152),n1)
| ~ type(K_152,not)
| ~ mode(K_152,ok) ),
inference(cnfTransformation,[status(thm)],[f_252]) ).
tff(c_754,plain,
( value(in(n1,or1(v(n1,a))),n0)
| ~ type(or1(v(n1,a)),not)
| ~ mode(or1(v(n1,a)),ok) ),
inference(resolution,[status(thm)],[c_718,c_747]) ).
tff(c_1796,plain,
~ mode(or1(v(n1,a)),ok),
inference(splitLeft,[status(thm)],[c_754]) ).
tff(c_1805,plain,
( mode(or1(v(n1,a)),abnormal)
| ~ type(v(n1,a),fulladder) ),
inference(resolution,[status(thm)],[c_242,c_1796]) ).
tff(c_1810,plain,
mode(or1(v(n1,a)),abnormal),
inference(demodulation,[status(thm),theory(equality)],[c_581,c_1805]) ).
tff(c_1812,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_116,c_1810]) ).
tff(c_1814,plain,
mode(or1(v(n1,a)),ok),
inference(splitRight,[status(thm)],[c_754]) ).
tff(c_881,plain,
! [K_162] :
( value(out(n1,K_162),n0)
| ~ value(in(n2,K_162),n0)
| ~ value(in(n1,K_162),n0)
| ~ type(K_162,or)
| ~ mode(K_162,ok) ),
inference(cnfTransformation,[status(thm)],[f_172]) ).
tff(c_6,plain,
! [V1_8,V2_9,P_7] :
( equal_value(V1_8,V2_9)
| ~ value(P_7,V2_9)
| ~ value(P_7,V1_8) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_2001,plain,
! [V1_217,K_218] :
( equal_value(V1_217,n0)
| ~ value(out(n1,K_218),V1_217)
| ~ value(in(n2,K_218),n0)
| ~ value(in(n1,K_218),n0)
| ~ type(K_218,or)
| ~ mode(K_218,ok) ),
inference(resolution,[status(thm)],[c_881,c_6]) ).
tff(c_2013,plain,
( equal_value(n1,n0)
| ~ value(in(n2,or1(v(n1,a))),n0)
| ~ value(in(n1,or1(v(n1,a))),n0)
| ~ type(or1(v(n1,a)),or)
| ~ mode(or1(v(n1,a)),ok) ),
inference(resolution,[status(thm)],[c_718,c_2001]) ).
tff(c_2032,plain,
( equal_value(n1,n0)
| ~ value(in(n2,or1(v(n1,a))),n0)
| ~ value(in(n1,or1(v(n1,a))),n0)
| ~ type(or1(v(n1,a)),or) ),
inference(demodulation,[status(thm),theory(equality)],[c_1814,c_2013]) ).
tff(c_2033,plain,
( ~ value(in(n2,or1(v(n1,a))),n0)
| ~ value(in(n1,or1(v(n1,a))),n0)
| ~ type(or1(v(n1,a)),or) ),
inference(negUnitSimplification,[status(thm)],[c_10,c_2032]) ).
tff(c_2214,plain,
~ type(or1(v(n1,a)),or),
inference(splitLeft,[status(thm)],[c_2033]) ).
tff(c_2217,plain,
~ type(v(n1,a),fulladder),
inference(resolution,[status(thm)],[c_74,c_2214]) ).
tff(c_2224,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_581,c_2217]) ).
tff(c_2225,plain,
( ~ value(in(n1,or1(v(n1,a))),n0)
| ~ value(in(n2,or1(v(n1,a))),n0) ),
inference(splitRight,[status(thm)],[c_2033]) ).
tff(c_2255,plain,
~ value(in(n2,or1(v(n1,a))),n0),
inference(splitLeft,[status(thm)],[c_2225]) ).
tff(c_78,plain,
! [X_46] :
( connection(out(c,h1(X_46)),in(n2,or1(X_46)))
| ~ type(X_46,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_390]) ).
tff(c_70,plain,
! [X_42] :
( type(h1(X_42),halfadder)
| ~ type(X_42,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_369]) ).
tff(c_54,plain,
! [X_34] :
( connection(in(n2,X_34),in(n2,or1(X_34)))
| ~ type(X_34,halfadder) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_86,plain,
! [X_50] :
( connection(in(c,X_50),in(n2,h1(X_50)))
| ~ type(X_50,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_410]) ).
tff(c_441,plain,
! [X_127] :
( connection(in(c,X_127),in(c,v(n1,X_127)))
| ~ type(X_127,nbit_adder(n1)) ),
inference(cnfTransformation,[status(thm)],[f_454]) ).
tff(c_110,plain,
value(in(c,a),n0),
inference(cnfTransformation,[status(thm)],[f_459]) ).
tff(c_140,plain,
! [P2_67] :
( value(P2_67,n0)
| ~ connection(in(c,a),P2_67) ),
inference(resolution,[status(thm)],[c_110,c_129]) ).
tff(c_445,plain,
( value(in(c,v(n1,a)),n0)
| ~ type(a,nbit_adder(n1)) ),
inference(resolution,[status(thm)],[c_441,c_140]) ).
tff(c_448,plain,
value(in(c,v(n1,a)),n0),
inference(demodulation,[status(thm),theory(equality)],[c_104,c_445]) ).
tff(c_518,plain,
! [P2_137] :
( value(P2_137,n0)
| ~ connection(in(c,v(n1,a)),P2_137) ),
inference(resolution,[status(thm)],[c_448,c_2]) ).
tff(c_528,plain,
( value(in(n2,h1(v(n1,a))),n0)
| ~ type(v(n1,a),fulladder) ),
inference(resolution,[status(thm)],[c_86,c_518]) ).
tff(c_838,plain,
value(in(n2,h1(v(n1,a))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_581,c_528]) ).
tff(c_865,plain,
! [P2_161] :
( value(P2_161,n0)
| ~ connection(in(n2,h1(v(n1,a))),P2_161) ),
inference(resolution,[status(thm)],[c_838,c_2]) ).
tff(c_879,plain,
( value(in(n2,or1(h1(v(n1,a)))),n0)
| ~ type(h1(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_54,c_865]) ).
tff(c_1011,plain,
~ type(h1(v(n1,a)),halfadder),
inference(splitLeft,[status(thm)],[c_879]) ).
tff(c_1029,plain,
~ type(v(n1,a),fulladder),
inference(resolution,[status(thm)],[c_70,c_1011]) ).
tff(c_1033,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_581,c_1029]) ).
tff(c_1035,plain,
type(h1(v(n1,a)),halfadder),
inference(splitRight,[status(thm)],[c_879]) ).
tff(c_62,plain,
! [X_38] :
( connection(out(c,X_38),out(n1,and2(X_38)))
| ~ type(X_38,halfadder) ),
inference(cnfTransformation,[status(thm)],[f_326]) ).
tff(c_118,plain,
~ mode(and2(h1(v(n1,a))),abnormal),
inference(cnfTransformation,[status(thm)],[f_466]) ).
tff(c_46,plain,
! [X_30] :
( type(and2(X_30),and)
| ~ type(X_30,halfadder) ),
inference(cnfTransformation,[status(thm)],[f_285]) ).
tff(c_244,plain,
! [X_30] :
( mode(and2(X_30),abnormal)
| mode(and2(X_30),ok)
| ~ type(X_30,halfadder) ),
inference(resolution,[status(thm)],[c_46,c_211]) ).
tff(c_56,plain,
! [X_35] :
( connection(in(n1,X_35),in(n1,and2(X_35)))
| ~ type(X_35,halfadder) ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_580,plain,
value(in(n1,h1(v(n1,a))),n0),
inference(splitRight,[status(thm)],[c_542]) ).
tff(c_615,plain,
! [P2_143] :
( value(P2_143,n0)
| ~ connection(in(n1,h1(v(n1,a))),P2_143) ),
inference(resolution,[status(thm)],[c_580,c_2]) ).
tff(c_629,plain,
( value(in(n1,and2(h1(v(n1,a)))),n0)
| ~ type(h1(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_56,c_615]) ).
tff(c_1479,plain,
value(in(n1,and2(h1(v(n1,a)))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_1035,c_629]) ).
tff(c_36,plain,
! [K_25] :
( value(out(n1,K_25),n1)
| ~ value(in(n1,K_25),n0)
| ~ type(K_25,not)
| ~ mode(K_25,ok) ),
inference(cnfTransformation,[status(thm)],[f_219]) ).
tff(c_775,plain,
! [K_154] :
( value(in(n1,K_154),n1)
| ~ value(out(n1,K_154),n1)
| ~ type(K_154,and)
| ~ mode(K_154,ok) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_1641,plain,
! [K_206] :
( value(in(n1,K_206),n1)
| ~ type(K_206,and)
| ~ value(in(n1,K_206),n0)
| ~ type(K_206,not)
| ~ mode(K_206,ok) ),
inference(resolution,[status(thm)],[c_36,c_775]) ).
tff(c_8,plain,
~ equal_value(n0,n1),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_38,plain,
! [K_26] :
( value(out(n1,K_26),n0)
| ~ value(in(n1,K_26),n1)
| ~ type(K_26,not)
| ~ mode(K_26,ok) ),
inference(cnfTransformation,[status(thm)],[f_230]) ).
tff(c_553,plain,
! [K_140] :
( value(out(n1,K_140),n1)
| ~ value(in(n1,K_140),n0)
| ~ type(K_140,not)
| ~ mode(K_140,ok) ),
inference(cnfTransformation,[status(thm)],[f_219]) ).
tff(c_1357,plain,
! [V1_186,K_187] :
( equal_value(V1_186,n1)
| ~ value(out(n1,K_187),V1_186)
| ~ value(in(n1,K_187),n0)
| ~ type(K_187,not)
| ~ mode(K_187,ok) ),
inference(resolution,[status(thm)],[c_553,c_6]) ).
tff(c_1372,plain,
! [K_26] :
( equal_value(n0,n1)
| ~ value(in(n1,K_26),n0)
| ~ value(in(n1,K_26),n1)
| ~ type(K_26,not)
| ~ mode(K_26,ok) ),
inference(resolution,[status(thm)],[c_38,c_1357]) ).
tff(c_1391,plain,
! [K_26] :
( ~ value(in(n1,K_26),n0)
| ~ value(in(n1,K_26),n1)
| ~ type(K_26,not)
| ~ mode(K_26,ok) ),
inference(negUnitSimplification,[status(thm)],[c_8,c_1372]) ).
tff(c_1729,plain,
! [K_209] :
( ~ type(K_209,and)
| ~ value(in(n1,K_209),n0)
| ~ type(K_209,not)
| ~ mode(K_209,ok) ),
inference(resolution,[status(thm)],[c_1641,c_1391]) ).
tff(c_1751,plain,
( ~ type(and2(h1(v(n1,a))),and)
| ~ type(and2(h1(v(n1,a))),not)
| ~ mode(and2(h1(v(n1,a))),ok) ),
inference(resolution,[status(thm)],[c_1479,c_1729]) ).
tff(c_1975,plain,
~ mode(and2(h1(v(n1,a))),ok),
inference(splitLeft,[status(thm)],[c_1751]) ).
tff(c_1979,plain,
( mode(and2(h1(v(n1,a))),abnormal)
| ~ type(h1(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_244,c_1975]) ).
tff(c_1982,plain,
mode(and2(h1(v(n1,a))),abnormal),
inference(demodulation,[status(thm),theory(equality)],[c_1035,c_1979]) ).
tff(c_1984,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_118,c_1982]) ).
tff(c_1986,plain,
mode(and2(h1(v(n1,a))),ok),
inference(splitRight,[status(thm)],[c_1751]) ).
tff(c_1985,plain,
( ~ type(and2(h1(v(n1,a))),not)
| ~ type(and2(h1(v(n1,a))),and) ),
inference(splitRight,[status(thm)],[c_1751]) ).
tff(c_1991,plain,
~ type(and2(h1(v(n1,a))),and),
inference(splitLeft,[status(thm)],[c_1985]) ).
tff(c_1994,plain,
~ type(h1(v(n1,a)),halfadder),
inference(resolution,[status(thm)],[c_46,c_1991]) ).
tff(c_1998,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1035,c_1994]) ).
tff(c_2000,plain,
type(and2(h1(v(n1,a))),and),
inference(splitRight,[status(thm)],[c_1985]) ).
tff(c_58,plain,
! [X_36] :
( connection(in(n2,X_36),in(n2,and2(X_36)))
| ~ type(X_36,halfadder) ),
inference(cnfTransformation,[status(thm)],[f_316]) ).
tff(c_880,plain,
( value(in(n2,and2(h1(v(n1,a)))),n0)
| ~ type(h1(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_58,c_865]) ).
tff(c_1429,plain,
value(in(n2,and2(h1(v(n1,a)))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_1035,c_880]) ).
tff(c_16,plain,
! [K_13,Any_14] :
( value(out(n1,K_13),n0)
| ~ value(in(Any_14,K_13),n0)
| ~ type(K_13,and)
| ~ mode(K_13,ok) ),
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_1438,plain,
( value(out(n1,and2(h1(v(n1,a)))),n0)
| ~ type(and2(h1(v(n1,a))),and)
| ~ mode(and2(h1(v(n1,a))),ok) ),
inference(resolution,[status(thm)],[c_1429,c_16]) ).
tff(c_2445,plain,
value(out(n1,and2(h1(v(n1,a)))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_1986,c_2000,c_1438]) ).
tff(c_4,plain,
! [P1_4,V_6,P2_5] :
( value(P1_4,V_6)
| ~ value(P2_5,V_6)
| ~ connection(P1_4,P2_5) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_2505,plain,
! [P1_248] :
( value(P1_248,n0)
| ~ connection(P1_248,out(n1,and2(h1(v(n1,a))))) ),
inference(resolution,[status(thm)],[c_2445,c_4]) ).
tff(c_2509,plain,
( value(out(c,h1(v(n1,a))),n0)
| ~ type(h1(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_62,c_2505]) ).
tff(c_2512,plain,
value(out(c,h1(v(n1,a))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_1035,c_2509]) ).
tff(c_2577,plain,
! [P2_251] :
( value(P2_251,n0)
| ~ connection(out(c,h1(v(n1,a))),P2_251) ),
inference(resolution,[status(thm)],[c_2512,c_2]) ).
tff(c_2585,plain,
( value(in(n2,or1(v(n1,a))),n0)
| ~ type(v(n1,a),fulladder) ),
inference(resolution,[status(thm)],[c_78,c_2577]) ).
tff(c_2597,plain,
value(in(n2,or1(v(n1,a))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_581,c_2585]) ).
tff(c_2599,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2255,c_2597]) ).
tff(c_2600,plain,
~ value(in(n1,or1(v(n1,a))),n0),
inference(splitRight,[status(thm)],[c_2225]) ).
tff(c_80,plain,
! [X_47] :
( connection(out(c,h2(X_47)),in(n1,or1(X_47)))
| ~ type(X_47,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_395]) ).
tff(c_72,plain,
! [X_43] :
( type(h2(X_43),halfadder)
| ~ type(X_43,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_60,plain,
! [X_37] :
( connection(out(s,X_37),out(n1,and1(X_37)))
| ~ type(X_37,halfadder) ),
inference(cnfTransformation,[status(thm)],[f_321]) ).
tff(c_88,plain,
! [X_51] :
( connection(out(s,X_51),out(s,h2(X_51)))
| ~ type(X_51,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_415]) ).
tff(c_344,plain,
! [X_119] :
( connection(out(n1,X_119),out(s,v(n1,X_119)))
| ~ type(X_119,nbit_adder(n1)) ),
inference(cnfTransformation,[status(thm)],[f_434]) ).
tff(c_112,plain,
value(out(n1,a),n0),
inference(cnfTransformation,[status(thm)],[f_460]) ).
tff(c_143,plain,
! [P2_67] :
( value(P2_67,n0)
| ~ connection(out(n1,a),P2_67) ),
inference(resolution,[status(thm)],[c_112,c_129]) ).
tff(c_348,plain,
( value(out(s,v(n1,a)),n0)
| ~ type(a,nbit_adder(n1)) ),
inference(resolution,[status(thm)],[c_344,c_143]) ).
tff(c_351,plain,
value(out(s,v(n1,a)),n0),
inference(demodulation,[status(thm),theory(equality)],[c_104,c_348]) ).
tff(c_402,plain,
! [P2_123] :
( value(P2_123,n0)
| ~ connection(out(s,v(n1,a)),P2_123) ),
inference(resolution,[status(thm)],[c_351,c_2]) ).
tff(c_412,plain,
( value(out(s,h2(v(n1,a))),n0)
| ~ type(v(n1,a),fulladder) ),
inference(resolution,[status(thm)],[c_88,c_402]) ).
tff(c_918,plain,
value(out(s,h2(v(n1,a))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_581,c_412]) ).
tff(c_978,plain,
! [P2_166] :
( value(P2_166,n0)
| ~ connection(out(s,h2(v(n1,a))),P2_166) ),
inference(resolution,[status(thm)],[c_918,c_2]) ).
tff(c_987,plain,
( value(out(n1,and1(h2(v(n1,a)))),n0)
| ~ type(h2(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_60,c_978]) ).
tff(c_1107,plain,
~ type(h2(v(n1,a)),halfadder),
inference(splitLeft,[status(thm)],[c_987]) ).
tff(c_1110,plain,
~ type(v(n1,a),fulladder),
inference(resolution,[status(thm)],[c_72,c_1107]) ).
tff(c_1114,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_581,c_1110]) ).
tff(c_1116,plain,
type(h2(v(n1,a)),halfadder),
inference(splitRight,[status(thm)],[c_987]) ).
tff(c_120,plain,
~ mode(and2(h2(v(n1,a))),abnormal),
inference(cnfTransformation,[status(thm)],[f_468]) ).
tff(c_82,plain,
! [X_48] :
( connection(in(n1,X_48),in(n1,h2(X_48)))
| ~ type(X_48,fulladder) ),
inference(cnfTransformation,[status(thm)],[f_400]) ).
tff(c_385,plain,
! [X_122] :
( connection(in(a1,X_122),in(n1,v(n1,X_122)))
| ~ type(X_122,nbit_adder(n1)) ),
inference(cnfTransformation,[status(thm)],[f_444]) ).
tff(c_106,plain,
value(in(a1,a),n0),
inference(cnfTransformation,[status(thm)],[f_457]) ).
tff(c_142,plain,
! [P2_67] :
( value(P2_67,n0)
| ~ connection(in(a1,a),P2_67) ),
inference(resolution,[status(thm)],[c_106,c_129]) ).
tff(c_389,plain,
( value(in(n1,v(n1,a)),n0)
| ~ type(a,nbit_adder(n1)) ),
inference(resolution,[status(thm)],[c_385,c_142]) ).
tff(c_392,plain,
value(in(n1,v(n1,a)),n0),
inference(demodulation,[status(thm),theory(equality)],[c_104,c_389]) ).
tff(c_413,plain,
! [P2_124] :
( value(P2_124,n0)
| ~ connection(in(n1,v(n1,a)),P2_124) ),
inference(resolution,[status(thm)],[c_392,c_2]) ).
tff(c_426,plain,
( value(in(n1,h2(v(n1,a))),n0)
| ~ type(v(n1,a),fulladder) ),
inference(resolution,[status(thm)],[c_82,c_413]) ).
tff(c_785,plain,
value(in(n1,h2(v(n1,a))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_581,c_426]) ).
tff(c_821,plain,
! [P2_158] :
( value(P2_158,n0)
| ~ connection(in(n1,h2(v(n1,a))),P2_158) ),
inference(resolution,[status(thm)],[c_785,c_2]) ).
tff(c_835,plain,
( value(in(n1,and2(h2(v(n1,a)))),n0)
| ~ type(h2(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_56,c_821]) ).
tff(c_1344,plain,
value(in(n1,and2(h2(v(n1,a)))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_1116,c_835]) ).
tff(c_1355,plain,
! [V1_8] :
( equal_value(V1_8,n0)
| ~ value(in(n1,and2(h2(v(n1,a)))),V1_8) ),
inference(resolution,[status(thm)],[c_1344,c_6]) ).
tff(c_1655,plain,
( equal_value(n1,n0)
| ~ type(and2(h2(v(n1,a))),and)
| ~ value(in(n1,and2(h2(v(n1,a)))),n0)
| ~ type(and2(h2(v(n1,a))),not)
| ~ mode(and2(h2(v(n1,a))),ok) ),
inference(resolution,[status(thm)],[c_1641,c_1355]) ).
tff(c_1692,plain,
( equal_value(n1,n0)
| ~ type(and2(h2(v(n1,a))),and)
| ~ type(and2(h2(v(n1,a))),not)
| ~ mode(and2(h2(v(n1,a))),ok) ),
inference(demodulation,[status(thm),theory(equality)],[c_1344,c_1655]) ).
tff(c_1693,plain,
( ~ type(and2(h2(v(n1,a))),and)
| ~ type(and2(h2(v(n1,a))),not)
| ~ mode(and2(h2(v(n1,a))),ok) ),
inference(negUnitSimplification,[status(thm)],[c_10,c_1692]) ).
tff(c_1901,plain,
~ mode(and2(h2(v(n1,a))),ok),
inference(splitLeft,[status(thm)],[c_1693]) ).
tff(c_1904,plain,
( mode(and2(h2(v(n1,a))),abnormal)
| ~ type(h2(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_244,c_1901]) ).
tff(c_1907,plain,
mode(and2(h2(v(n1,a))),abnormal),
inference(demodulation,[status(thm),theory(equality)],[c_1116,c_1904]) ).
tff(c_1909,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_120,c_1907]) ).
tff(c_1911,plain,
mode(and2(h2(v(n1,a))),ok),
inference(splitRight,[status(thm)],[c_1693]) ).
tff(c_1910,plain,
( ~ type(and2(h2(v(n1,a))),not)
| ~ type(and2(h2(v(n1,a))),and) ),
inference(splitRight,[status(thm)],[c_1693]) ).
tff(c_1916,plain,
~ type(and2(h2(v(n1,a))),and),
inference(splitLeft,[status(thm)],[c_1910]) ).
tff(c_1919,plain,
~ type(h2(v(n1,a)),halfadder),
inference(resolution,[status(thm)],[c_46,c_1916]) ).
tff(c_1923,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1116,c_1919]) ).
tff(c_1925,plain,
type(and2(h2(v(n1,a))),and),
inference(splitRight,[status(thm)],[c_1910]) ).
tff(c_1353,plain,
( value(out(n1,and2(h2(v(n1,a)))),n0)
| ~ type(and2(h2(v(n1,a))),and)
| ~ mode(and2(h2(v(n1,a))),ok) ),
inference(resolution,[status(thm)],[c_1344,c_16]) ).
tff(c_3175,plain,
value(out(n1,and2(h2(v(n1,a)))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_1911,c_1925,c_1353]) ).
tff(c_3235,plain,
! [P1_276] :
( value(P1_276,n0)
| ~ connection(P1_276,out(n1,and2(h2(v(n1,a))))) ),
inference(resolution,[status(thm)],[c_3175,c_4]) ).
tff(c_3239,plain,
( value(out(c,h2(v(n1,a))),n0)
| ~ type(h2(v(n1,a)),halfadder) ),
inference(resolution,[status(thm)],[c_62,c_3235]) ).
tff(c_3242,plain,
value(out(c,h2(v(n1,a))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_1116,c_3239]) ).
tff(c_3333,plain,
! [P2_281] :
( value(P2_281,n0)
| ~ connection(out(c,h2(v(n1,a))),P2_281) ),
inference(resolution,[status(thm)],[c_3242,c_2]) ).
tff(c_3341,plain,
( value(in(n1,or1(v(n1,a))),n0)
| ~ type(v(n1,a),fulladder) ),
inference(resolution,[status(thm)],[c_80,c_3333]) ).
tff(c_3353,plain,
value(in(n1,or1(v(n1,a))),n0),
inference(demodulation,[status(thm),theory(equality)],[c_581,c_3341]) ).
tff(c_3355,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2600,c_3353]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : HWV008-1.001 : TPTP v9.0.0. Released v2.1.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.32 % Computer : n017.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Mon Apr 7 22:54:25 EDT 2025
% 0.12/0.32 % CPUTime :
% 8.45/2.97 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.45/2.99
% 8.45/2.99 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------