%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.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 : n022.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 : Tue May 5 06:56:40 PM UTC 2026
% Result : Unsatisfiable 172.69s 145.04s
% Output : CNFRefutation 172.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 17
% Syntax : Number of formulae : 59 ( 59 unt; 0 typ; 0 def)
% Number of atoms : 59 ( 58 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 10 con; 0-4 aty)
% Number of variables : 90 ( 90 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ aux3 > aux2 > reck > aux > z > y > x2 > x > step > splits > reck2 > rec > prop_same > pair2 > orb > eq2 > eq > cons3 > cons2 > cons > andb > #nlpp > star > splits2 > or2 > notb > eps2 > atom > nil4 > nil3 > nil2 > nil > eps > c > btrue > bfalse > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(eq,type,
eq: ( $i * $i ) > $i ).
tff(prop_same,type,
prop_same: ( $i * $i ) > $i ).
tff(splits2,type,
splits2: $i > $i ).
tff(aux2,type,
aux2: ( $i * $i * $i * $i ) > $i ).
tff(a,type,
a: $i ).
tff(nil4,type,
nil4: $i ).
tff(cons3,type,
cons3: ( $i * $i ) > $i ).
tff(aux,type,
aux: ( $i * $i * $i ) > $i ).
tff(or2,type,
or2: $i > $i ).
tff(star,type,
star: $i > $i ).
tff(atom,type,
atom: $i > $i ).
tff(aux3,type,
aux3: ( $i * $i * $i * $i ) > $i ).
tff(rec,type,
rec: ( $i * $i ) > $i ).
tff(b,type,
b: $i ).
tff(eps,type,
eps: $i ).
tff(step,type,
step: ( $i * $i ) > $i ).
tff(x,type,
x: ( $i * $i ) > $i ).
tff(reck,type,
reck: ( $i * $i * $i ) > $i ).
tff(cons2,type,
cons2: ( $i * $i ) > $i ).
tff(notb,type,
notb: $i > $i ).
tff(eps2,type,
eps2: $i > $i ).
tff(nil3,type,
nil3: $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(z,type,
z: ( $i * $i ) > $i ).
tff(pair2,type,
pair2: ( $i * $i ) > $i ).
tff(x2,type,
x2: ( $i * $i ) > $i ).
tff(y,type,
y: ( $i * $i ) > $i ).
tff(splits,type,
splits: ( $i * $i ) > $i ).
tff(bfalse,type,
bfalse: $i ).
tff(eq2,type,
eq2: ( $i * $i ) > $i ).
tff(andb,type,
andb: ( $i * $i ) > $i ).
tff(nil,type,
nil: $i ).
tff(btrue,type,
btrue: $i ).
tff(nil2,type,
nil2: $i ).
tff(reck2,type,
reck2: ( $i * $i ) > $i ).
tff(orb,type,
orb: ( $i * $i ) > $i ).
tff(c,type,
c: $i ).
tff(f_228,axiom,
! [X] : ( eq2(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_224,axiom,
eq2(btrue,bfalse) = bfalse,
file(unknown,unknown) ).
tff(f_33,axiom,
! [P2,X6,X7] : ( aux3(P2,X6,X7,bfalse) = bfalse ),
file(unknown,unknown) ).
tff(f_160,axiom,
notb(btrue) = bfalse,
file(unknown,unknown) ).
tff(f_172,axiom,
! [Y] : ( eps2(star(Y)) = btrue ),
file(unknown,unknown) ).
tff(f_214,axiom,
! [P2,X6,X7] : ( reck2(star(P2),cons2(X6,X7)) = aux3(P2,X6,X7,notb(eps2(P2))) ),
file(unknown,unknown) ).
tff(f_166,axiom,
eps2(eps) = btrue,
file(unknown,unknown) ).
tff(f_163,axiom,
! [Q] : ( andb(btrue,Q) = Q ),
file(unknown,unknown) ).
tff(f_170,axiom,
! [R,Q2] : ( eps2(y(R,Q2)) = andb(eps2(R),eps2(Q2)) ),
file(unknown,unknown) ).
tff(f_23,axiom,
! [Y,B] : ( aux(Y,B,btrue) = eps ),
file(unknown,unknown) ).
tff(f_226,axiom,
! [X] : ( eq(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_177,axiom,
! [B,Y] : ( step(atom(B),Y) = aux(Y,B,eq(B,Y)) ),
file(unknown,unknown) ).
tff(f_183,axiom,
! [P2,Y] : ( step(star(P2),Y) = y(step(P2,Y),star(P2)) ),
file(unknown,unknown) ).
tff(f_191,axiom,
! [X,Z,Xs] : ( rec(X,cons2(Z,Xs)) = rec(step(X,Z),Xs) ),
file(unknown,unknown) ).
tff(f_189,axiom,
! [X] : ( rec(X,nil2) = eps2(X) ),
file(unknown,unknown) ).
tff(f_216,axiom,
! [X,Y] : ( prop_same(X,Y) = eq2(rec(X,Y),reck2(X,Y)) ),
file(unknown,unknown) ).
tff(f_231,axiom,
! [X,Y] : ( eq2(prop_same(X,Y),bfalse) != btrue ),
file(unknown,unknown) ).
tff(c_224,plain,
! [X_211] : ( eq2(X_211,X_211) = btrue ),
inference(cnfTransformation,[status(thm)],[f_228]) ).
tff(c_220,plain,
eq2(btrue,bfalse) = bfalse,
inference(cnfTransformation,[status(thm)],[f_224]) ).
tff(c_12,plain,
! [P2_14,X6_15,X7_16] : ( aux3(P2_14,X6_15,X7_16,bfalse) = bfalse ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_144,plain,
notb(btrue) = bfalse,
inference(cnfTransformation,[status(thm)],[f_160]) ).
tff(c_158,plain,
! [Y_163] : ( eps2(star(Y_163)) = btrue ),
inference(cnfTransformation,[status(thm)],[f_172]) ).
tff(c_6820,plain,
! [P2_553,X6_554,X7_555] : ( aux3(P2_553,X6_554,X7_555,notb(eps2(P2_553))) = reck2(star(P2_553),cons2(X6_554,X7_555)) ),
inference(cnfTransformation,[status(thm)],[f_214]) ).
tff(c_7027,plain,
! [Y_163,X6_554,X7_555] : ( reck2(star(star(Y_163)),cons2(X6_554,X7_555)) = aux3(star(Y_163),X6_554,X7_555,notb(btrue)) ),
inference(superposition,[status(thm),theory(equality)],[c_158,c_6820]) ).
tff(c_7091,plain,
! [Y_163,X6_554,X7_555] : ( reck2(star(star(Y_163)),cons2(X6_554,X7_555)) = bfalse ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_144,c_7027]) ).
tff(c_152,plain,
eps2(eps) = btrue,
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_148,plain,
! [Q_157] : ( andb(btrue,Q_157) = Q_157 ),
inference(cnfTransformation,[status(thm)],[f_163]) ).
tff(c_704,plain,
! [R_278,Q2_279] : ( andb(eps2(R_278),eps2(Q2_279)) = eps2(y(R_278,Q2_279)) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_713,plain,
! [Y_163,Q2_279] : ( eps2(y(star(Y_163),Q2_279)) = andb(btrue,eps2(Q2_279)) ),
inference(superposition,[status(thm),theory(equality)],[c_158,c_704]) ).
tff(c_737,plain,
! [Y_163,Q2_279] : ( eps2(y(star(Y_163),Q2_279)) = eps2(Q2_279) ),
inference(demodulation,[status(thm),theory(equality)],[c_148,c_713]) ).
tff(c_156,plain,
! [R_161,Q2_162] : ( andb(eps2(R_161),eps2(Q2_162)) = eps2(y(R_161,Q2_162)) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_725,plain,
! [Q2_279] : ( andb(btrue,eps2(Q2_279)) = eps2(y(eps,Q2_279)) ),
inference(superposition,[status(thm),theory(equality)],[c_152,c_704]) ).
tff(c_769,plain,
! [Q2_283] : ( eps2(y(eps,Q2_283)) = eps2(Q2_283) ),
inference(demodulation,[status(thm),theory(equality)],[c_148,c_725]) ).
tff(c_775,plain,
! [Q2_283,Q2_162] : ( andb(eps2(Q2_283),eps2(Q2_162)) = eps2(y(y(eps,Q2_283),Q2_162)) ),
inference(superposition,[status(thm),theory(equality)],[c_769,c_156]) ).
tff(c_783,plain,
! [Q2_283,Q2_162] : ( eps2(y(y(eps,Q2_283),Q2_162)) = eps2(y(Q2_283,Q2_162)) ),
inference(demodulation,[status(thm),theory(equality)],[c_156,c_775]) ).
tff(c_2,plain,
! [Y_1,B_2] : ( aux(Y_1,B_2,btrue) = eps ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_222,plain,
! [X_210] : ( eq(X_210,X_210) = btrue ),
inference(cnfTransformation,[status(thm)],[f_226]) ).
tff(c_2968,plain,
! [Y_385,B_386] : ( aux(Y_385,B_386,eq(B_386,Y_385)) = step(atom(B_386),Y_385) ),
inference(cnfTransformation,[status(thm)],[f_177]) ).
tff(c_2977,plain,
! [X_210] : ( step(atom(X_210),X_210) = aux(X_210,X_210,btrue) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_2968]) ).
tff(c_3005,plain,
! [X_387] : ( step(atom(X_387),X_387) = eps ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2977]) ).
tff(c_170,plain,
! [P2_173,Y_174] : ( y(step(P2_173,Y_174),star(P2_173)) = step(star(P2_173),Y_174) ),
inference(cnfTransformation,[status(thm)],[f_183]) ).
tff(c_3013,plain,
! [X_387] : ( y(eps,star(atom(X_387))) = step(star(atom(X_387)),X_387) ),
inference(superposition,[status(thm),theory(equality)],[c_3005,c_170]) ).
tff(c_2356,plain,
! [P2_350,Y_351] : ( y(step(P2_350,Y_351),star(P2_350)) = step(star(P2_350),Y_351) ),
inference(cnfTransformation,[status(thm)],[f_183]) ).
tff(c_728,plain,
! [R_278] : ( andb(eps2(R_278),btrue) = eps2(y(R_278,eps)) ),
inference(superposition,[status(thm),theory(equality)],[c_152,c_704]) ).
tff(c_716,plain,
! [R_278,Y_163] : ( eps2(y(R_278,star(Y_163))) = andb(eps2(R_278),btrue) ),
inference(superposition,[status(thm),theory(equality)],[c_158,c_704]) ).
tff(c_1979,plain,
! [R_278,Y_163] : ( eps2(y(R_278,star(Y_163))) = eps2(y(R_278,eps)) ),
inference(demodulation,[status(thm),theory(equality)],[c_728,c_716]) ).
tff(c_27552,plain,
! [P2_940,Y_941] : ( eps2(y(step(P2_940,Y_941),eps)) = eps2(step(star(P2_940),Y_941)) ),
inference(superposition,[status(thm),theory(equality)],[c_2356,c_1979]) ).
tff(c_27682,plain,
! [X_387] : ( eps2(y(y(eps,star(atom(X_387))),eps)) = eps2(step(star(star(atom(X_387))),X_387)) ),
inference(superposition,[status(thm),theory(equality)],[c_3013,c_27552]) ).
tff(c_27897,plain,
! [X_387] : ( eps2(step(star(star(atom(X_387))),X_387)) = btrue ),
inference(demodulation,[status(thm),theory(equality)],[c_152,c_737,c_783,c_27682]) ).
tff(c_2841,plain,
! [X_372,Z_373,Xs_374] : ( rec(step(X_372,Z_373),Xs_374) = rec(X_372,cons2(Z_373,Xs_374)) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_176,plain,
! [X_177] : ( rec(X_177,nil2) = eps2(X_177) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_3557,plain,
! [X_408,Z_409] : ( rec(X_408,cons2(Z_409,nil2)) = eps2(step(X_408,Z_409)) ),
inference(superposition,[status(thm),theory(equality)],[c_2841,c_176]) ).
tff(c_204,plain,
! [X_208,Y_209] : ( eq2(rec(X_208,Y_209),reck2(X_208,Y_209)) = prop_same(X_208,Y_209) ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_238845,plain,
! [X_3406,Z_3407] : ( eq2(eps2(step(X_3406,Z_3407)),reck2(X_3406,cons2(Z_3407,nil2))) = prop_same(X_3406,cons2(Z_3407,nil2)) ),
inference(superposition,[status(thm),theory(equality)],[c_3557,c_204]) ).
tff(c_239675,plain,
! [X_387] : ( eq2(btrue,reck2(star(star(atom(X_387))),cons2(X_387,nil2))) = prop_same(star(star(atom(X_387))),cons2(X_387,nil2)) ),
inference(superposition,[status(thm),theory(equality)],[c_27897,c_238845]) ).
tff(c_249990,plain,
! [X_3448] : ( prop_same(star(star(atom(X_3448))),cons2(X_3448,nil2)) = bfalse ),
inference(demodulation,[status(thm),theory(equality)],[c_220,c_7091,c_239675]) ).
tff(c_226,plain,
! [X_212,Y_213] : ( eq2(prop_same(X_212,Y_213),bfalse) != btrue ),
inference(cnfTransformation,[status(thm)],[f_231]) ).
tff(c_249994,plain,
eq2(bfalse,bfalse) != btrue,
inference(superposition,[status(thm),theory(equality)],[c_249990,c_226]) ).
tff(c_250000,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_224,c_249994]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/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.14/0.34 % Computer : n022.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue May 5 13:19:50 EDT 2026
% 0.14/0.34 % CPUTime :
% 172.69/145.04 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 172.69/145.05
% 172.69/145.05 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------