%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX199+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 : n027.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:35 PM UTC 2026
% Result : Theorem 10.17s 3.42s
% Output : CNFRefutation 10.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 11
% Syntax : Number of formulae : 88 ( 33 unt; 0 typ; 0 def)
% Number of atoms : 175 ( 84 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 153 ( 66 ~; 82 |; 0 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 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 : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 205 ( 202 !; 3 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ leqNat > merge > cons > #nlpp > tail > s > proj1S > head > z > nil
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(proj1S,type,
proj1S: $i > $i ).
tff(s,type,
s: $i > $i ).
tff(merge,type,
merge: ( $i * $i ) > $i ).
tff(leqNat,type,
leqNat: ( $i * $i ) > $o ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(tail,type,
tail: $i > $i ).
tff(z,type,
z: $i ).
tff(head,type,
head: $i > $i ).
tff(nil,type,
nil: $i ).
tff(f_41,axiom,
! [Z] : ~ leqNat(s(Z),z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_007) ).
tff(f_36,axiom,
! [X] : ( z != s(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
tff(f_38,axiom,
! [Y] : leqNat(z,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
tff(f_26,axiom,
! [X,X2] : ( head(cons(X,X2)) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_001) ).
tff(f_49,axiom,
! [Z,Xs] : ( merge(cons(Z,Xs),nil) = cons(Z,Xs) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_010) ).
tff(f_53,axiom,
! [Z,Xs,Y2,Ys] :
( leqNat(Z,Y2)
=> ( merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_011) ).
tff(f_47,axiom,
! [Y] : ( merge(nil,Y) = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_009) ).
tff(f_66,negated_conjecture,
~ ? [Xs,Ys,Zs] :
~ ( ( merge(Xs,Ys) = merge(Ys,Xs) )
=> ( ( merge(Xs,Zs) = merge(Zs,Xs) )
=> ( merge(Ys,Zs) = merge(Zs,Ys) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_013) ).
tff(f_28,axiom,
! [X,X2] : ( tail(cons(X,X2)) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_002) ).
tff(f_58,axiom,
! [Z,Xs,Y2,Ys] :
( ~ leqNat(Z,Y2)
=> ( merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Y2,merge(cons(Z,Xs),Ys)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
tff(f_45,axiom,
! [Z,M] :
( leqNat(s(Z),s(M))
<=> leqNat(Z,M) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_008) ).
tff(c_14,plain,
! [Z_10] : ~ leqNat(s(Z_10),z),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_10,plain,
! [X_8] : ( s(X_8) != z ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_12,plain,
! [Y_9] : leqNat(z,Y_9),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_2,plain,
! [X_1,X2_2] : ( head(cons(X_1,X2_2)) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_22,plain,
! [Z_14,Xs_15] : ( merge(cons(Z_14,Xs_15),nil) = cons(Z_14,Xs_15) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_273,plain,
! [Z_61,Xs_62,Y2_63,Ys_64] :
( ( merge(cons(Z_61,Xs_62),cons(Y2_63,Ys_64)) = cons(Z_61,merge(Xs_62,cons(Y2_63,Ys_64))) )
| ~ leqNat(Z_61,Y2_63) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_20,plain,
! [Y_13] : ( merge(nil,Y_13) = Y_13 ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_80,plain,
! [Z_43,Xs_44] : ( merge(cons(Z_43,Xs_44),nil) = cons(Z_43,Xs_44) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_28,plain,
! [Zs_26,Ys_25,Xs_24] :
( ( merge(Zs_26,Ys_25) = merge(Ys_25,Zs_26) )
| ( merge(Zs_26,Xs_24) != merge(Xs_24,Zs_26) )
| ( merge(Ys_25,Xs_24) != merge(Xs_24,Ys_25) ) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_85,plain,
! [Z_43,Xs_44,Ys_25] :
( ( merge(cons(Z_43,Xs_44),Ys_25) = merge(Ys_25,cons(Z_43,Xs_44)) )
| ( merge(nil,cons(Z_43,Xs_44)) != cons(Z_43,Xs_44) )
| ( merge(nil,Ys_25) != merge(Ys_25,nil) ) ),
inference(superposition,[status(thm),theory(equality)],[c_80,c_28]) ).
tff(c_93,plain,
! [Z_43,Xs_44,Ys_25] :
( ( merge(cons(Z_43,Xs_44),Ys_25) = merge(Ys_25,cons(Z_43,Xs_44)) )
| ( merge(Ys_25,nil) != Ys_25 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_20,c_85]) ).
tff(c_285,plain,
! [Y2_63,Ys_64,Z_61,Xs_62] :
( ( merge(cons(Y2_63,Ys_64),cons(Z_61,Xs_62)) = cons(Z_61,merge(Xs_62,cons(Y2_63,Ys_64))) )
| ( merge(cons(Z_61,Xs_62),nil) != cons(Z_61,Xs_62) )
| ~ leqNat(Z_61,Y2_63) ),
inference(superposition,[status(thm),theory(equality)],[c_273,c_93]) ).
tff(c_314,plain,
! [Y2_63,Ys_64,Z_61,Xs_62] :
( ( merge(cons(Y2_63,Ys_64),cons(Z_61,Xs_62)) = cons(Z_61,merge(Xs_62,cons(Y2_63,Ys_64))) )
| ~ leqNat(Z_61,Y2_63) ),
inference(demodulation,[status(thm),theory(equality)],[c_22,c_285]) ).
tff(c_4,plain,
! [X_3,X2_4] : ( tail(cons(X_3,X2_4)) = X2_4 ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_26,plain,
! [Z_20,Xs_21,Y2_22,Ys_23] :
( ( merge(cons(Z_20,Xs_21),cons(Y2_22,Ys_23)) = cons(Y2_22,merge(cons(Z_20,Xs_21),Ys_23)) )
| leqNat(Z_20,Y2_22) ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_216,plain,
! [Z_55,Xs_56,Y2_57,Ys_58] :
( ( merge(cons(Z_55,Xs_56),cons(Y2_57,Ys_58)) = cons(Y2_57,merge(cons(Z_55,Xs_56),Ys_58)) )
| leqNat(Z_55,Y2_57) ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_225,plain,
! [Y2_57,Ys_58,Z_55,Xs_56] :
( ( merge(cons(Y2_57,Ys_58),cons(Z_55,Xs_56)) = cons(Y2_57,merge(cons(Z_55,Xs_56),Ys_58)) )
| ( merge(cons(Z_55,Xs_56),nil) != cons(Z_55,Xs_56) )
| leqNat(Z_55,Y2_57) ),
inference(superposition,[status(thm),theory(equality)],[c_216,c_93]) ).
tff(c_322,plain,
! [Y2_65,Ys_66,Z_67,Xs_68] :
( ( merge(cons(Y2_65,Ys_66),cons(Z_67,Xs_68)) = cons(Y2_65,merge(cons(Z_67,Xs_68),Ys_66)) )
| leqNat(Z_67,Y2_65) ),
inference(demodulation,[status(thm),theory(equality)],[c_22,c_225]) ).
tff(c_1649,plain,
! [Z_113,Y2_114,Ys_115,Xs_116] :
( ( cons(Z_113,merge(cons(Y2_114,Ys_115),Xs_116)) = cons(Y2_114,merge(cons(Z_113,Xs_116),Ys_115)) )
| leqNat(Y2_114,Z_113)
| leqNat(Z_113,Y2_114) ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_322]) ).
tff(c_1759,plain,
! [Y2_114,Z_113,Xs_116,Ys_115] :
( ( tail(cons(Y2_114,merge(cons(Z_113,Xs_116),Ys_115))) = merge(cons(Y2_114,Ys_115),Xs_116) )
| leqNat(Y2_114,Z_113)
| leqNat(Z_113,Y2_114) ),
inference(superposition,[status(thm),theory(equality)],[c_1649,c_4]) ).
tff(c_2109,plain,
! [Z_127,Xs_128,Ys_129,Y2_130] :
( ( merge(cons(Z_127,Xs_128),Ys_129) = merge(cons(Y2_130,Ys_129),Xs_128) )
| leqNat(Y2_130,Z_127)
| leqNat(Z_127,Y2_130) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1759]) ).
tff(c_24,plain,
! [Z_16,Xs_17,Y2_18,Ys_19] :
( ( merge(cons(Z_16,Xs_17),cons(Y2_18,Ys_19)) = cons(Z_16,merge(Xs_17,cons(Y2_18,Ys_19))) )
| ~ leqNat(Z_16,Y2_18) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_768,plain,
! [Y2_90,Z_91,Xs_92,Ys_93] :
( ( cons(Y2_90,merge(cons(Z_91,Xs_92),Ys_93)) = cons(Y2_90,merge(Ys_93,cons(Z_91,Xs_92))) )
| ~ leqNat(Y2_90,Z_91)
| leqNat(Z_91,Y2_90) ),
inference(superposition,[status(thm),theory(equality)],[c_322,c_24]) ).
tff(c_921,plain,
! [Y2_90,Z_91,Xs_92,Ys_93] :
( ( tail(cons(Y2_90,merge(cons(Z_91,Xs_92),Ys_93))) = merge(Ys_93,cons(Z_91,Xs_92)) )
| ~ leqNat(Y2_90,Z_91)
| leqNat(Z_91,Y2_90) ),
inference(superposition,[status(thm),theory(equality)],[c_768,c_4]) ).
tff(c_1067,plain,
! [Z_99,Xs_100,Ys_101,Y2_102] :
( ( merge(cons(Z_99,Xs_100),Ys_101) = merge(Ys_101,cons(Z_99,Xs_100)) )
| ~ leqNat(Y2_102,Z_99)
| leqNat(Z_99,Y2_102) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_921]) ).
tff(c_1074,plain,
! [Y_103,Xs_104,Ys_105] :
( ( merge(cons(Y_103,Xs_104),Ys_105) = merge(Ys_105,cons(Y_103,Xs_104)) )
| leqNat(Y_103,z) ),
inference(resolution,[status(thm)],[c_12,c_1067]) ).
tff(c_87,plain,
! [Ys_25,Z_43,Xs_44] :
( ( merge(nil,Ys_25) = merge(Ys_25,nil) )
| ( merge(nil,cons(Z_43,Xs_44)) != cons(Z_43,Xs_44) )
| ( merge(cons(Z_43,Xs_44),Ys_25) != merge(Ys_25,cons(Z_43,Xs_44)) ) ),
inference(superposition,[status(thm),theory(equality)],[c_80,c_28]) ).
tff(c_95,plain,
! [Ys_25,Z_43,Xs_44] :
( ( merge(Ys_25,nil) = Ys_25 )
| ( merge(cons(Z_43,Xs_44),Ys_25) != merge(Ys_25,cons(Z_43,Xs_44)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_20,c_87]) ).
tff(c_1344,plain,
! [Ys_105,Y_103] :
( ( merge(Ys_105,nil) = Ys_105 )
| leqNat(Y_103,z) ),
inference(superposition,[status(thm),theory(equality)],[c_1074,c_95]) ).
tff(c_1370,plain,
! [Y_103] : leqNat(Y_103,z),
inference(splitLeft,[status(thm)],[c_1344]) ).
tff(c_1451,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1370,c_14]) ).
tff(c_1452,plain,
! [Ys_105] : ( merge(Ys_105,nil) = Ys_105 ),
inference(splitRight,[status(thm)],[c_1344]) ).
tff(c_3561,plain,
! [Y2_148,Xs_149,Z_150] :
( ( merge(cons(Y2_148,nil),Xs_149) = cons(Z_150,Xs_149) )
| leqNat(Y2_148,Z_150)
| leqNat(Z_150,Y2_148) ),
inference(superposition,[status(thm),theory(equality)],[c_2109,c_1452]) ).
tff(c_3734,plain,
! [Y2_148,Xs_149,Z_150] :
( ( head(merge(cons(Y2_148,nil),Xs_149)) = Z_150 )
| leqNat(Y2_148,Z_150)
| leqNat(Z_150,Y2_148) ),
inference(superposition,[status(thm),theory(equality)],[c_3561,c_2]) ).
tff(c_4506,plain,
! [Y2_477,Xs_478] :
( ( head(merge(cons(Y2_477,nil),Xs_478)) = Y2_477 )
| leqNat(Y2_477,Y2_477) ),
inference(factorization,[status(thm),theory(equality)],[c_3734]) ).
tff(c_4633,plain,
! [Z_61,Xs_62,Y2_63] :
( ( head(cons(Z_61,merge(Xs_62,cons(Y2_63,nil)))) = Y2_63 )
| leqNat(Y2_63,Y2_63)
| ~ leqNat(Z_61,Y2_63) ),
inference(superposition,[status(thm),theory(equality)],[c_314,c_4506]) ).
tff(c_10731,plain,
! [Z_1121,Y2_1122] :
( ( Z_1121 = Y2_1122 )
| leqNat(Y2_1122,Y2_1122)
| ~ leqNat(Z_1121,Y2_1122) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4633]) ).
tff(c_10816,plain,
! [Y_1147] :
( ( z = Y_1147 )
| leqNat(Y_1147,Y_1147) ),
inference(resolution,[status(thm)],[c_12,c_10731]) ).
tff(c_16,plain,
! [Z_11,M_12] :
( leqNat(Z_11,M_12)
| ~ leqNat(s(Z_11),s(M_12)) ),
inference(cnfTransformation,[status(thm)],[f_45]) ).
tff(c_10822,plain,
! [Z_11] :
( leqNat(Z_11,Z_11)
| ( s(Z_11) = z ) ),
inference(resolution,[status(thm)],[c_10816,c_16]) ).
tff(c_10842,plain,
! [Z_11] : leqNat(Z_11,Z_11),
inference(negUnitSimplification,[status(thm)],[c_10,c_10822]) ).
tff(c_415,plain,
! [Y2_73,Ys_74,Z_75,Xs_76] :
( ( merge(cons(Y2_73,Ys_74),cons(Z_75,Xs_76)) = cons(Z_75,merge(Xs_76,cons(Y2_73,Ys_74))) )
| ~ leqNat(Z_75,Y2_73) ),
inference(demodulation,[status(thm),theory(equality)],[c_22,c_285]) ).
tff(c_11061,plain,
! [Z_1214,Xs_1215,Y2_1216,Ys_1217] :
( ( cons(Z_1214,merge(Xs_1215,cons(Y2_1216,Ys_1217))) = cons(Y2_1216,merge(Ys_1217,cons(Z_1214,Xs_1215))) )
| ~ leqNat(Y2_1216,Z_1214)
| ~ leqNat(Z_1214,Y2_1216) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_415]) ).
tff(c_11171,plain,
! [Y2_1216,Ys_1217,Z_1214,Xs_1215] :
( ( tail(cons(Y2_1216,merge(Ys_1217,cons(Z_1214,Xs_1215)))) = merge(Xs_1215,cons(Y2_1216,Ys_1217)) )
| ~ leqNat(Y2_1216,Z_1214)
| ~ leqNat(Z_1214,Y2_1216) ),
inference(superposition,[status(thm),theory(equality)],[c_11061,c_4]) ).
tff(c_14333,plain,
! [Ys_1298,Z_1299,Xs_1300,Y2_1301] :
( ( merge(Ys_1298,cons(Z_1299,Xs_1300)) = merge(Xs_1300,cons(Y2_1301,Ys_1298)) )
| ~ leqNat(Y2_1301,Z_1299)
| ~ leqNat(Z_1299,Y2_1301) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11171]) ).
tff(c_14363,plain,
! [Ys_1298,Z_11,Xs_1300] :
( ( merge(Ys_1298,cons(Z_11,Xs_1300)) = merge(Xs_1300,cons(Z_11,Ys_1298)) )
| ~ leqNat(Z_11,Z_11) ),
inference(resolution,[status(thm)],[c_10842,c_14333]) ).
tff(c_14543,plain,
! [Ys_1304,Z_1305,Xs_1306] : ( merge(Ys_1304,cons(Z_1305,Xs_1306)) = merge(Xs_1306,cons(Z_1305,Ys_1304)) ),
inference(demodulation,[status(thm),theory(equality)],[c_10842,c_14363]) ).
tff(c_14726,plain,
! [Ys_1307,Z_1308] : ( merge(Ys_1307,cons(Z_1308,nil)) = cons(Z_1308,Ys_1307) ),
inference(superposition,[status(thm),theory(equality)],[c_14543,c_20]) ).
tff(c_73,plain,
! [Zs_40,Ys_41,Xs_42] :
( ( merge(Zs_40,Ys_41) = merge(Ys_41,Zs_40) )
| ( merge(Zs_40,Xs_42) != merge(Xs_42,Zs_40) )
| ( merge(Ys_41,Xs_42) != merge(Xs_42,Ys_41) ) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_77,plain,
! [Ys_41,Y_13] :
( ( merge(Ys_41,Y_13) = merge(Y_13,Ys_41) )
| ( merge(Y_13,nil) != Y_13 )
| ( merge(nil,Ys_41) != merge(Ys_41,nil) ) ),
inference(superposition,[status(thm),theory(equality)],[c_20,c_73]) ).
tff(c_79,plain,
! [Ys_41,Y_13] :
( ( merge(Ys_41,Y_13) = merge(Y_13,Ys_41) )
| ( merge(Y_13,nil) != Y_13 )
| ( merge(Ys_41,nil) != Ys_41 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_77]) ).
tff(c_1458,plain,
! [Ys_41,Y_13] : ( merge(Ys_41,Y_13) = merge(Y_13,Ys_41) ),
inference(demodulation,[status(thm),theory(equality)],[c_1452,c_1452,c_79]) ).
tff(c_14833,plain,
! [Z_1309,Ys_1310] : ( merge(cons(Z_1309,nil),Ys_1310) = cons(Z_1309,Ys_1310) ),
inference(superposition,[status(thm),theory(equality)],[c_14726,c_1458]) ).
tff(c_14629,plain,
! [Ys_1304,Z_1305] : ( merge(Ys_1304,cons(Z_1305,nil)) = cons(Z_1305,Ys_1304) ),
inference(superposition,[status(thm),theory(equality)],[c_14543,c_20]) ).
tff(c_15136,plain,
! [Z_1317,Z_1316] : ( cons(Z_1317,cons(Z_1316,nil)) = cons(Z_1316,cons(Z_1317,nil)) ),
inference(superposition,[status(thm),theory(equality)],[c_14833,c_14629]) ).
tff(c_15225,plain,
! [Z_1318,Z_1319] : ( head(cons(Z_1318,cons(Z_1319,nil))) = Z_1319 ),
inference(superposition,[status(thm),theory(equality)],[c_15136,c_2]) ).
tff(c_15704,plain,
! [Z_1323] : ( z = Z_1323 ),
inference(superposition,[status(thm),theory(equality)],[c_15225,c_2]) ).
tff(c_18,plain,
! [Z_11,M_12] :
( leqNat(s(Z_11),s(M_12))
| ~ leqNat(Z_11,M_12) ),
inference(cnfTransformation,[status(thm)],[f_45]) ).
tff(c_11162,plain,
! [Z_1214,Xs_1215,Y2_1216,Ys_1217] :
( ( head(cons(Z_1214,merge(Xs_1215,cons(Y2_1216,Ys_1217)))) = Y2_1216 )
| ~ leqNat(Y2_1216,Z_1214)
| ~ leqNat(Z_1214,Y2_1216) ),
inference(superposition,[status(thm),theory(equality)],[c_11061,c_2]) ).
tff(c_11286,plain,
! [Z_1218,Y2_1219] :
( ( Z_1218 = Y2_1219 )
| ~ leqNat(Y2_1219,Z_1218)
| ~ leqNat(Z_1218,Y2_1219) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11162]) ).
tff(c_11335,plain,
! [Z_1221,M_1222] :
( ( s(Z_1221) = s(M_1222) )
| ~ leqNat(s(M_1222),s(Z_1221))
| ~ leqNat(Z_1221,M_1222) ),
inference(resolution,[status(thm)],[c_18,c_11286]) ).
tff(c_11360,plain,
! [Z_1223,M_1224] :
( ( s(Z_1223) = s(M_1224) )
| ~ leqNat(M_1224,Z_1223)
| ~ leqNat(Z_1223,M_1224) ),
inference(resolution,[status(thm)],[c_18,c_11335]) ).
tff(c_11407,plain,
! [Z_1226,M_1227] :
( ( s(s(Z_1226)) = s(s(M_1227)) )
| ~ leqNat(s(M_1227),s(Z_1226))
| ~ leqNat(Z_1226,M_1227) ),
inference(resolution,[status(thm)],[c_18,c_11360]) ).
tff(c_11432,plain,
! [Z_1228,M_1229] :
( ( s(s(Z_1228)) = s(s(M_1229)) )
| ~ leqNat(M_1229,Z_1228)
| ~ leqNat(Z_1228,M_1229) ),
inference(resolution,[status(thm)],[c_18,c_11407]) ).
tff(c_11454,plain,
! [Y_1230] :
( ( s(s(z)) = s(s(Y_1230)) )
| ~ leqNat(Y_1230,z) ),
inference(resolution,[status(thm)],[c_12,c_11432]) ).
tff(c_13863,plain,
! [Y_1286,M_1287] :
( leqNat(s(s(Y_1286)),s(M_1287))
| ~ leqNat(s(z),M_1287)
| ~ leqNat(Y_1286,z) ),
inference(superposition,[status(thm),theory(equality)],[c_11454,c_18]) ).
tff(c_13957,plain,
! [Y_1288,M_1289] :
( leqNat(s(Y_1288),M_1289)
| ~ leqNat(s(z),M_1289)
| ~ leqNat(Y_1288,z) ),
inference(resolution,[status(thm)],[c_13863,c_16]) ).
tff(c_14013,plain,
! [Y_1288,M_12] :
( leqNat(s(Y_1288),s(M_12))
| ~ leqNat(Y_1288,z)
| ~ leqNat(z,M_12) ),
inference(resolution,[status(thm)],[c_18,c_13957]) ).
tff(c_14051,plain,
! [Y_1290,M_1291] :
( leqNat(s(Y_1290),s(M_1291))
| ~ leqNat(Y_1290,z) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_14013]) ).
tff(c_11515,plain,
! [M_12,Y_1230] :
( leqNat(s(s(z)),s(M_12))
| ~ leqNat(s(Y_1230),M_12)
| ~ leqNat(Y_1230,z) ),
inference(superposition,[status(thm),theory(equality)],[c_11454,c_18]) ).
tff(c_14123,plain,
! [M_1291,Y_1290] :
( leqNat(s(s(z)),s(s(M_1291)))
| ~ leqNat(Y_1290,z) ),
inference(resolution,[status(thm)],[c_14051,c_11515]) ).
tff(c_14231,plain,
! [Y_1296] : ~ leqNat(Y_1296,z),
inference(splitLeft,[status(thm)],[c_14123]) ).
tff(c_14251,plain,
$false,
inference(resolution,[status(thm)],[c_10842,c_14231]) ).
tff(c_14256,plain,
! [M_1297] : leqNat(s(s(z)),s(s(M_1297))),
inference(splitRight,[status(thm)],[c_14123]) ).
tff(c_14320,plain,
! [M_1297] : leqNat(s(z),s(M_1297)),
inference(resolution,[status(thm)],[c_14256,c_16]) ).
tff(c_15706,plain,
leqNat(s(z),z),
inference(superposition,[status(thm),theory(equality)],[c_15704,c_14320]) ).
tff(c_17299,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_15706]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX199+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % 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.32 % Computer : n027.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 11:12:34 EDT 2026
% 0.15/0.32 % CPUTime :
% 10.17/3.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.17/3.43
% 10.17/3.43 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------