%------------------------------------------------------------------------------
% 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/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 : n003.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:33 PM UTC 2026
% Result : Theorem 8.01s 2.93s
% Output : CNFRefutation 8.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 6
% Syntax : Number of formulae : 23 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 23 ( 22 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 5 ( 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 : 24 ( 24 usr; 2 con; 0-2 aty)
% Number of variables : 31 ( 30 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ y > x > mulNat > fail4 > fail32 > fail3 > fail22 > fail2 > fail12 > fail1 > fail > addNat > #nlpp > s > proj22 > proj2 > proj1S > proj1N > proj12 > proj1 > opt > n > d > z > x2
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(proj2,type,
proj2: $i > $i ).
tff(proj12,type,
proj12: $i > $i ).
tff(proj1S,type,
proj1S: $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(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(proj1N,type,
proj1N: $i > $i ).
tff(proj1,type,
proj1: $i > $i ).
tff(mulNat,type,
mulNat: ( $i * $i ) > $i ).
tff(proj22,type,
proj22: $i > $i ).
tff(z,type,
z: $i ).
tff(y,type,
y: ( $i * $i ) > $i ).
tff(addNat,type,
addNat: ( $i * $i ) > $i ).
tff(fail,type,
fail: ( $i * $i ) > $i ).
tff(x2,type,
x2: $i ).
tff(f_177,axiom,
! [E] : ( opt(x(n(z),E)) = E ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_050) ).
tff(f_147,axiom,
! [Y] : ( d(n(Y)) = n(z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_039) ).
tff(f_149,axiom,
! [F,G] : ( d(x(F,G)) = x(d(F),d(G)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_040) ).
tff(f_190,negated_conjecture,
~ ? [E] : ( opt(d(E)) != opt(d(opt(E))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_054) ).
tff(f_152,axiom,
d(x2) = n(s(z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_042) ).
tff(f_42,axiom,
! [X,X2,X3] : ( n(X) != x(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_008) ).
tff(c_100,plain,
! [E_89] : ( opt(x(n(z),E_89)) = E_89 ),
inference(cnfTransformation,[status(thm)],[f_177]) ).
tff(c_78,plain,
! [Y_73] : ( d(n(Y_73)) = n(z) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_522,plain,
! [F_162,G_163] : ( x(d(F_162),d(G_163)) = d(x(F_162,G_163)) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_4968,plain,
! [G_400,Y_401] : ( x(n(z),d(G_400)) = d(x(n(Y_401),G_400)) ),
inference(superposition,[status(thm),theory(equality)],[c_78,c_522]) ).
tff(c_5137,plain,
! [Y_401,G_400] : ( opt(d(x(n(Y_401),G_400))) = d(G_400) ),
inference(superposition,[status(thm),theory(equality)],[c_4968,c_100]) ).
tff(c_296,plain,
! [E_135] : ( opt(x(n(z),E_135)) = E_135 ),
inference(cnfTransformation,[status(thm)],[f_177]) ).
tff(c_108,plain,
! [E_95] : ( opt(d(opt(E_95))) = opt(d(E_95)) ),
inference(cnfTransformation,[status(thm)],[f_190]) ).
tff(c_305,plain,
! [E_135] : ( opt(d(x(n(z),E_135))) = opt(d(E_135)) ),
inference(superposition,[status(thm),theory(equality)],[c_296,c_108]) ).
tff(c_5200,plain,
! [E_135] : ( opt(d(E_135)) = d(E_135) ),
inference(demodulation,[status(thm),theory(equality)],[c_5137,c_305]) ).
tff(c_5556,plain,
! [E_407] : ( d(opt(E_407)) = d(E_407) ),
inference(demodulation,[status(thm),theory(equality)],[c_5200,c_5200,c_108]) ).
tff(c_5700,plain,
! [E_410] : ( d(x(n(z),E_410)) = d(E_410) ),
inference(superposition,[status(thm),theory(equality)],[c_100,c_5556]) ).
tff(c_84,plain,
n(s(z)) = d(x2),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_16,plain,
! [X2_13,X3_14,X_12] : ( x(X2_13,X3_14) != n(X_12) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_606,plain,
! [X_168,F_169,G_170] : ( n(X_168) != d(x(F_169,G_170)) ),
inference(superposition,[status(thm),theory(equality)],[c_522,c_16]) ).
tff(c_610,plain,
! [F_169,G_170] : ( d(x(F_169,G_170)) != d(x2) ),
inference(superposition,[status(thm),theory(equality)],[c_84,c_606]) ).
tff(c_5771,plain,
! [E_410] : ( d(x2) != d(E_410) ),
inference(superposition,[status(thm),theory(equality)],[c_5700,c_610]) ).
tff(c_5871,plain,
$false,
inference(reflexivity,[status(thm),theory(equality)],[c_5771]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX190+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.15/0.33 % Computer : n003.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 09:54:26 EDT 2026
% 0.15/0.33 % CPUTime :
% 8.01/2.93 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.01/2.94
% 8.01/2.94 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------