%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX190-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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/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:34 PM UTC 2026
% Result : Unsatisfiable 47.54s 30.96s
% Output : CNFRefutation 47.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 16
% Syntax : Number of formulae : 54 ( 54 unt; 0 typ; 0 def)
% Number of atoms : 54 ( 53 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 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 : 25 ( 25 usr; 4 con; 0-3 aty)
% Number of variables : 64 ( 64 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ aux > y > x > mulNat > fail4 > fail32 > fail3 > fail22 > fail2 > fail12 > fail1 > fail > eq3 > eq2 > eq > addNat > #nlpp > s > prop4 > opt > n > d > z > x2 > btrue > bfalse
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(eq,type,
eq: ( $i * $i ) > $i ).
tff(eq3,type,
eq3: ( $i * $i ) > $i ).
tff(prop4,type,
prop4: $i > $i ).
tff(s,type,
s: $i > $i ).
tff(fail4,type,
fail4: ( $i * $i ) > $i ).
tff(fail22,type,
fail22: ( $i * $i ) > $i ).
tff(fail1,type,
fail1: ( $i * $i ) > $i ).
tff(aux,type,
aux: ( $i * $i * $i ) > $i ).
tff(fail32,type,
fail32: ( $i * $i ) > $i ).
tff(fail12,type,
fail12: ( $i * $i ) > $i ).
tff(n,type,
n: $i > $i ).
tff(d,type,
d: $i > $i ).
tff(fail3,type,
fail3: ( $i * $i ) > $i ).
tff(fail2,type,
fail2: ( $i * $i ) > $i ).
tff(x,type,
x: ( $i * $i ) > $i ).
tff(opt,type,
opt: $i > $i ).
tff(mulNat,type,
mulNat: ( $i * $i ) > $i ).
tff(z,type,
z: $i ).
tff(y,type,
y: ( $i * $i ) > $i ).
tff(bfalse,type,
bfalse: $i ).
tff(eq2,type,
eq2: ( $i * $i ) > $i ).
tff(btrue,type,
btrue: $i ).
tff(addNat,type,
addNat: ( $i * $i ) > $i ).
tff(fail,type,
fail: ( $i * $i ) > $i ).
tff(x2,type,
x2: $i ).
tff(f_207,axiom,
! [X] : ( eq3(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_47,axiom,
! [E] : ( fail1(x2,E) = fail2(x2,E) ),
file(unknown,unknown) ).
tff(f_191,axiom,
! [X] : ( eq2(x2,n(X)) = bfalse ),
file(unknown,unknown) ).
tff(f_33,axiom,
! [Y,E] : ( fail2(Y,E) = aux(Y,E,eq2(Y,E)) ),
file(unknown,unknown) ).
tff(f_144,axiom,
! [X] : ( opt(n(X)) = n(X) ),
file(unknown,unknown) ).
tff(f_145,axiom,
opt(x2) = x2,
file(unknown,unknown) ).
tff(f_31,axiom,
! [E] : ( aux(x2,E,bfalse) = x(opt(x2),opt(E)) ),
file(unknown,unknown) ).
tff(f_114,axiom,
d(x2) = n(s(z)),
file(unknown,unknown) ).
tff(f_111,axiom,
! [F,G] : ( d(x(F,G)) = x(d(F),d(G)) ),
file(unknown,unknown) ).
tff(f_179,axiom,
! [X,Y,Z] : ( eq2(x(X,Y),n(Z)) = bfalse ),
file(unknown,unknown) ).
tff(f_51,axiom,
! [Y] : ( fail(Y,n(z)) = Y ),
file(unknown,unknown) ).
tff(f_109,axiom,
! [Y] : ( d(n(Y)) = n(z) ),
file(unknown,unknown) ).
tff(f_124,axiom,
! [X4,E] : ( opt(x(n(s(X4)),E)) = fail(n(s(X4)),E) ),
file(unknown,unknown) ).
tff(f_126,axiom,
! [E] : ( opt(x(n(z),E)) = E ),
file(unknown,unknown) ).
tff(f_147,axiom,
! [X] : ( prop4(X) = eq2(opt(d(X)),opt(d(opt(X)))) ),
file(unknown,unknown) ).
tff(f_210,axiom,
! [X] : ( eq3(prop4(X),bfalse) != btrue ),
file(unknown,unknown) ).
tff(c_178,plain,
! [X_177] : ( eq3(X_177,X_177) = btrue ),
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_26,plain,
! [E_29] : ( fail2(x2,E_29) = fail1(x2,E_29) ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_162,plain,
! [X_166] : ( eq2(x2,n(X_166)) = bfalse ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_1140,plain,
! [Y_281,E_282] : ( aux(Y_281,E_282,eq2(Y_281,E_282)) = fail2(Y_281,E_282) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_1254,plain,
! [X_166] : ( aux(x2,n(X_166),bfalse) = fail2(x2,n(X_166)) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_1140]) ).
tff(c_1271,plain,
! [X_166] : ( aux(x2,n(X_166),bfalse) = fail1(x2,n(X_166)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_1254]) ).
tff(c_124,plain,
! [X_121] : ( opt(n(X_121)) = n(X_121) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_126,plain,
opt(x2) = x2,
inference(cnfTransformation,[status(thm)],[f_145]) ).
tff(c_10,plain,
! [E_11] : ( x(opt(x2),opt(E_11)) = aux(x2,E_11,bfalse) ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_878,plain,
! [E_259] : ( x(x2,opt(E_259)) = aux(x2,E_259,bfalse) ),
inference(demodulation,[status(thm),theory(equality)],[c_126,c_10]) ).
tff(c_919,plain,
! [X_121] : ( aux(x2,n(X_121),bfalse) = x(x2,n(X_121)) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_878]) ).
tff(c_7936,plain,
! [X_632] : ( x(x2,n(X_632)) = fail1(x2,n(X_632)) ),
inference(demodulation,[status(thm),theory(equality)],[c_1271,c_919]) ).
tff(c_94,plain,
n(s(z)) = d(x2),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_1344,plain,
! [F_286,G_287] : ( x(d(F_286),d(G_287)) = d(x(F_286,G_287)) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_150,plain,
! [X_148,Y_149,Z_150] : ( eq2(x(X_148,Y_149),n(Z_150)) = bfalse ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_1865,plain,
! [F_329,G_330,Z_331] : ( eq2(d(x(F_329,G_330)),n(Z_331)) = bfalse ),
inference(superposition,[status(thm),theory(equality)],[c_1344,c_150]) ).
tff(c_1878,plain,
! [F_329,G_330] : ( eq2(d(x(F_329,G_330)),d(x2)) = bfalse ),
inference(superposition,[status(thm),theory(equality)],[c_94,c_1865]) ).
tff(c_8006,plain,
! [X_632] : ( eq2(d(fail1(x2,n(X_632))),d(x2)) = bfalse ),
inference(superposition,[status(thm),theory(equality)],[c_7936,c_1878]) ).
tff(c_7935,plain,
! [X_121] : ( x(x2,n(X_121)) = fail1(x2,n(X_121)) ),
inference(demodulation,[status(thm),theory(equality)],[c_1271,c_919]) ).
tff(c_30,plain,
! [Y_32] : ( fail(Y_32,n(z)) = Y_32 ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_88,plain,
! [Y_90] : ( d(n(Y_90)) = n(z) ),
inference(cnfTransformation,[status(thm)],[f_109]) ).
tff(c_16888,plain,
! [F_1005,Y_1006] : ( x(d(F_1005),n(z)) = d(x(F_1005,n(Y_1006))) ),
inference(superposition,[status(thm),theory(equality)],[c_88,c_1344]) ).
tff(c_3306,plain,
! [X4_421,E_422] : ( opt(x(n(s(X4_421)),E_422)) = fail(n(s(X4_421)),E_422) ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_3343,plain,
! [E_422] : ( fail(n(s(z)),E_422) = opt(x(d(x2),E_422)) ),
inference(superposition,[status(thm),theory(equality)],[c_94,c_3306]) ).
tff(c_3350,plain,
! [E_422] : ( opt(x(d(x2),E_422)) = fail(d(x2),E_422) ),
inference(demodulation,[status(thm),theory(equality)],[c_94,c_3343]) ).
tff(c_16990,plain,
! [Y_1006] : ( opt(d(x(x2,n(Y_1006)))) = fail(d(x2),n(z)) ),
inference(superposition,[status(thm),theory(equality)],[c_16888,c_3350]) ).
tff(c_17188,plain,
! [Y_1006] : ( opt(d(fail1(x2,n(Y_1006)))) = d(x2) ),
inference(demodulation,[status(thm),theory(equality)],[c_7935,c_30,c_16990]) ).
tff(c_15040,plain,
! [G_941,Y_942] : ( x(n(z),d(G_941)) = d(x(n(Y_942),G_941)) ),
inference(superposition,[status(thm),theory(equality)],[c_88,c_1344]) ).
tff(c_106,plain,
! [E_103] : ( opt(x(n(z),E_103)) = E_103 ),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_15276,plain,
! [Y_942,G_941] : ( opt(d(x(n(Y_942),G_941))) = d(G_941) ),
inference(superposition,[status(thm),theory(equality)],[c_15040,c_106]) ).
tff(c_1741,plain,
! [X_321] : ( eq2(opt(d(X_321)),opt(d(opt(X_321)))) = prop4(X_321) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_1774,plain,
! [E_103] : ( eq2(opt(d(x(n(z),E_103))),opt(d(E_103))) = prop4(x(n(z),E_103)) ),
inference(superposition,[status(thm),theory(equality)],[c_106,c_1741]) ).
tff(c_64127,plain,
! [E_1918] : ( eq2(d(E_1918),opt(d(E_1918))) = prop4(x(n(z),E_1918)) ),
inference(demodulation,[status(thm),theory(equality)],[c_15276,c_1774]) ).
tff(c_64154,plain,
! [Y_1006] : ( eq2(d(fail1(x2,n(Y_1006))),d(x2)) = prop4(x(n(z),fail1(x2,n(Y_1006)))) ),
inference(superposition,[status(thm),theory(equality)],[c_17188,c_64127]) ).
tff(c_64298,plain,
! [Y_1921] : ( prop4(x(n(z),fail1(x2,n(Y_1921)))) = bfalse ),
inference(demodulation,[status(thm),theory(equality)],[c_8006,c_64154]) ).
tff(c_180,plain,
! [X_178] : ( eq3(prop4(X_178),bfalse) != btrue ),
inference(cnfTransformation,[status(thm)],[f_210]) ).
tff(c_64305,plain,
eq3(bfalse,bfalse) != btrue,
inference(superposition,[status(thm),theory(equality)],[c_64298,c_180]) ).
tff(c_64319,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_178,c_64305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SWX190-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.17/0.35 % Computer : n022.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Tue May 5 09:57:20 EDT 2026
% 0.17/0.35 % CPUTime :
% 47.54/30.96 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 47.54/30.96
% 47.54/30.96 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------