%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : FLD068-4 : TPTP v9.0.0. Bugfixed 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 : 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 : Wed Apr 9 06:10:54 PM UTC 2025
% Result : Unsatisfiable 10.52s 3.59s
% Output : CNFRefutation 10.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 17
% Syntax : Number of formulae : 141 ( 58 unt; 0 typ; 0 def)
% Number of atoms : 294 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 317 ( 164 ~; 153 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 138 ( 138 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ sum > product > less_or_equal > defined > multiply > add > #nlpp > multiplicative_inverse > additive_inverse > u > multiplicative_identity > b > additive_identity > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sum,type,
sum: ( $i * $i * $i ) > $o ).
tff(less_or_equal,type,
less_or_equal: ( $i * $i ) > $o ).
tff(a,type,
a: $i ).
tff(product,type,
product: ( $i * $i * $i ) > $o ).
tff(additive_identity,type,
additive_identity: $i ).
tff(multiplicative_identity,type,
multiplicative_identity: $i ).
tff(u,type,
u: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(additive_inverse,type,
additive_inverse: $i > $i ).
tff(b,type,
b: $i ).
tff(defined,type,
defined: $i > $o ).
tff(multiplicative_inverse,type,
multiplicative_inverse: $i > $i ).
tff(add,type,
add: ( $i * $i ) > $i ).
tff(f_255,axiom,
~ less_or_equal(a,b),
file(unknown,unknown) ).
tff(f_250,axiom,
defined(b),
file(unknown,unknown) ).
tff(f_253,axiom,
less_or_equal(additive_identity,u),
file(unknown,unknown) ).
tff(f_249,axiom,
defined(a),
file(unknown,unknown) ).
tff(f_164,axiom,
! [X] :
( defined(additive_inverse(X))
| ~ defined(X) ),
file(unknown,unknown) ).
tff(f_73,axiom,
! [X] :
( sum(additive_identity,X,X)
| ~ defined(X) ),
file(unknown,unknown) ).
tff(f_252,axiom,
sum(b,additive_inverse(a),u),
file(unknown,unknown) ).
tff(f_233,axiom,
! [U,Z,X,Y,V] :
( less_or_equal(U,V)
| ~ less_or_equal(X,Y)
| ~ sum(X,Z,U)
| ~ sum(Y,Z,V) ),
file(unknown,unknown) ).
tff(f_83,axiom,
! [Y,X,Z] :
( sum(Y,X,Z)
| ~ sum(X,Y,Z) ),
file(unknown,unknown) ).
tff(f_159,axiom,
defined(additive_identity),
file(unknown,unknown) ).
tff(f_222,axiom,
! [X,Y] :
( less_or_equal(X,Y)
| less_or_equal(Y,X)
| ~ defined(X)
| ~ defined(Y) ),
file(unknown,unknown) ).
tff(f_212,axiom,
! [X,Z,Y] :
( less_or_equal(X,Z)
| ~ less_or_equal(X,Y)
| ~ less_or_equal(Y,Z) ),
file(unknown,unknown) ).
tff(f_251,axiom,
defined(u),
file(unknown,unknown) ).
tff(f_68,axiom,
! [W,U,Z,X,Y,V] :
( sum(U,Z,W)
| ~ sum(X,Y,U)
| ~ sum(Y,Z,V)
| ~ sum(X,V,W) ),
file(unknown,unknown) ).
tff(f_78,axiom,
! [X] :
( sum(additive_inverse(X),X,additive_identity)
| ~ defined(X) ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [W,U,Z,X,Y,V] :
( sum(X,V,W)
| ~ sum(X,Y,U)
| ~ sum(Y,Z,V)
| ~ sum(U,Z,W) ),
file(unknown,unknown) ).
tff(f_204,axiom,
! [X,Y] :
( sum(additive_identity,X,Y)
| ~ less_or_equal(X,Y)
| ~ less_or_equal(Y,X) ),
file(unknown,unknown) ).
tff(c_64,plain,
~ less_or_equal(a,b),
inference(cnfTransformation,[status(thm)],[f_255]) ).
tff(c_56,plain,
defined(b),
inference(cnfTransformation,[status(thm)],[f_250]) ).
tff(c_62,plain,
less_or_equal(additive_identity,u),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_54,plain,
defined(a),
inference(cnfTransformation,[status(thm)],[f_249]) ).
tff(c_30,plain,
! [X_51] :
( ~ defined(X_51)
| defined(additive_inverse(X_51)) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_6,plain,
! [X_13] :
( ~ defined(X_13)
| sum(additive_identity,X_13,X_13) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_60,plain,
sum(b,additive_inverse(a),u),
inference(cnfTransformation,[status(thm)],[f_252]) ).
tff(c_226,plain,
! [X_119,V_122,U_118,Y_121,Z_120] :
( ~ sum(Y_121,Z_120,V_122)
| ~ sum(X_119,Z_120,U_118)
| ~ less_or_equal(X_119,Y_121)
| less_or_equal(U_118,V_122) ),
inference(cnfTransformation,[status(thm)],[f_233]) ).
tff(c_257,plain,
! [X_123,U_124] :
( ~ sum(X_123,additive_inverse(a),U_124)
| ~ less_or_equal(X_123,b)
| less_or_equal(U_124,u) ),
inference(resolution,[status(thm)],[c_60,c_226]) ).
tff(c_293,plain,
( ~ less_or_equal(additive_identity,b)
| less_or_equal(additive_inverse(a),u)
| ~ defined(additive_inverse(a)) ),
inference(resolution,[status(thm)],[c_6,c_257]) ).
tff(c_339,plain,
~ defined(additive_inverse(a)),
inference(splitLeft,[status(thm)],[c_293]) ).
tff(c_342,plain,
~ defined(a),
inference(resolution,[status(thm)],[c_30,c_339]) ).
tff(c_346,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_54,c_342]) ).
tff(c_347,plain,
( ~ less_or_equal(additive_identity,b)
| less_or_equal(additive_inverse(a),u) ),
inference(splitRight,[status(thm)],[c_293]) ).
tff(c_380,plain,
~ less_or_equal(additive_identity,b),
inference(splitLeft,[status(thm)],[c_347]) ).
tff(c_79,plain,
! [X_86,Y_87,Z_88] :
( ~ sum(X_86,Y_87,Z_88)
| sum(Y_87,X_86,Z_88) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_88,plain,
sum(additive_inverse(a),b,u),
inference(resolution,[status(thm)],[c_60,c_79]) ).
tff(c_383,plain,
! [X_137,U_138] :
( ~ sum(X_137,b,U_138)
| ~ less_or_equal(X_137,additive_inverse(a))
| less_or_equal(U_138,u) ),
inference(resolution,[status(thm)],[c_88,c_226]) ).
tff(c_400,plain,
( ~ less_or_equal(additive_identity,additive_inverse(a))
| less_or_equal(b,u)
| ~ defined(b) ),
inference(resolution,[status(thm)],[c_6,c_383]) ).
tff(c_415,plain,
( ~ less_or_equal(additive_identity,additive_inverse(a))
| less_or_equal(b,u) ),
inference(demodulation,[status(thm),theory(equality)],[c_56,c_400]) ).
tff(c_416,plain,
~ less_or_equal(additive_identity,additive_inverse(a)),
inference(splitLeft,[status(thm)],[c_415]) ).
tff(c_28,plain,
defined(additive_identity),
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_348,plain,
defined(additive_inverse(a)),
inference(splitRight,[status(thm)],[c_293]) ).
tff(c_46,plain,
! [Y_65,X_64] :
( ~ defined(Y_65)
| ~ defined(X_64)
| less_or_equal(Y_65,X_64)
| less_or_equal(X_64,Y_65) ),
inference(cnfTransformation,[status(thm)],[f_222]) ).
tff(c_452,plain,
! [X_147,X_148,U_149] :
( ~ sum(X_147,X_148,U_149)
| ~ less_or_equal(X_147,additive_identity)
| less_or_equal(U_149,X_148)
| ~ defined(X_148) ),
inference(resolution,[status(thm)],[c_6,c_226]) ).
tff(c_473,plain,
( ~ less_or_equal(additive_inverse(a),additive_identity)
| less_or_equal(u,b)
| ~ defined(b) ),
inference(resolution,[status(thm)],[c_88,c_452]) ).
tff(c_495,plain,
( ~ less_or_equal(additive_inverse(a),additive_identity)
| less_or_equal(u,b) ),
inference(demodulation,[status(thm),theory(equality)],[c_56,c_473]) ).
tff(c_682,plain,
~ less_or_equal(additive_inverse(a),additive_identity),
inference(splitLeft,[status(thm)],[c_495]) ).
tff(c_685,plain,
( ~ defined(additive_inverse(a))
| ~ defined(additive_identity)
| less_or_equal(additive_identity,additive_inverse(a)) ),
inference(resolution,[status(thm)],[c_46,c_682]) ).
tff(c_691,plain,
less_or_equal(additive_identity,additive_inverse(a)),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_348,c_685]) ).
tff(c_693,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_416,c_691]) ).
tff(c_694,plain,
less_or_equal(u,b),
inference(splitRight,[status(thm)],[c_495]) ).
tff(c_44,plain,
! [Y_63,Z_62,X_61] :
( ~ less_or_equal(Y_63,Z_62)
| ~ less_or_equal(X_61,Y_63)
| less_or_equal(X_61,Z_62) ),
inference(cnfTransformation,[status(thm)],[f_212]) ).
tff(c_751,plain,
! [X_179] :
( ~ less_or_equal(X_179,u)
| less_or_equal(X_179,b) ),
inference(resolution,[status(thm)],[c_694,c_44]) ).
tff(c_787,plain,
less_or_equal(additive_identity,b),
inference(resolution,[status(thm)],[c_62,c_751]) ).
tff(c_809,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_380,c_787]) ).
tff(c_810,plain,
less_or_equal(b,u),
inference(splitRight,[status(thm)],[c_415]) ).
tff(c_811,plain,
less_or_equal(additive_identity,additive_inverse(a)),
inference(splitRight,[status(thm)],[c_415]) ).
tff(c_833,plain,
! [X_181] :
( ~ less_or_equal(X_181,additive_identity)
| less_or_equal(X_181,additive_inverse(a)) ),
inference(resolution,[status(thm)],[c_811,c_44]) ).
tff(c_899,plain,
! [X_190,X_191] :
( ~ less_or_equal(X_190,X_191)
| less_or_equal(X_190,additive_inverse(a))
| ~ less_or_equal(X_191,additive_identity) ),
inference(resolution,[status(thm)],[c_833,c_44]) ).
tff(c_926,plain,
( less_or_equal(b,additive_inverse(a))
| ~ less_or_equal(u,additive_identity) ),
inference(resolution,[status(thm)],[c_810,c_899]) ).
tff(c_935,plain,
~ less_or_equal(u,additive_identity),
inference(splitLeft,[status(thm)],[c_926]) ).
tff(c_58,plain,
defined(u),
inference(cnfTransformation,[status(thm)],[f_251]) ).
tff(c_87,plain,
! [X_13] :
( sum(X_13,additive_identity,X_13)
| ~ defined(X_13) ),
inference(resolution,[status(thm)],[c_6,c_79]) ).
tff(c_349,plain,
! [Y_136,W_132,V_134,U_133,X_135,Z_131] :
( ~ sum(X_135,V_134,W_132)
| ~ sum(Y_136,Z_131,V_134)
| ~ sum(X_135,Y_136,U_133)
| sum(U_133,Z_131,W_132) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_1443,plain,
! [Y_227,Z_228,U_229] :
( ~ sum(Y_227,Z_228,additive_inverse(a))
| ~ sum(b,Y_227,U_229)
| sum(U_229,Z_228,u) ),
inference(resolution,[status(thm)],[c_60,c_349]) ).
tff(c_1452,plain,
! [U_229] :
( ~ sum(b,additive_inverse(a),U_229)
| sum(U_229,additive_identity,u)
| ~ defined(additive_inverse(a)) ),
inference(resolution,[status(thm)],[c_87,c_1443]) ).
tff(c_1464,plain,
! [U_230] :
( ~ sum(b,additive_inverse(a),U_230)
| sum(U_230,additive_identity,u) ),
inference(demodulation,[status(thm),theory(equality)],[c_348,c_1452]) ).
tff(c_1482,plain,
sum(u,additive_identity,u),
inference(resolution,[status(thm)],[c_60,c_1464]) ).
tff(c_10,plain,
! [X_16,Y_15,Z_17] :
( ~ sum(X_16,Y_15,Z_17)
| sum(Y_15,X_16,Z_17) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_1504,plain,
sum(additive_identity,u,u),
inference(resolution,[status(thm)],[c_1482,c_10]) ).
tff(c_8,plain,
! [X_14] :
( ~ defined(X_14)
| sum(additive_inverse(X_14),X_14,additive_identity) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_2876,plain,
! [X_267,X_268,U_269] :
( ~ sum(X_267,X_268,U_269)
| ~ less_or_equal(X_267,additive_inverse(X_268))
| less_or_equal(U_269,additive_identity)
| ~ defined(X_268) ),
inference(resolution,[status(thm)],[c_8,c_226]) ).
tff(c_2898,plain,
( ~ less_or_equal(additive_identity,additive_inverse(u))
| less_or_equal(u,additive_identity)
| ~ defined(u) ),
inference(resolution,[status(thm)],[c_1504,c_2876]) ).
tff(c_2959,plain,
( ~ less_or_equal(additive_identity,additive_inverse(u))
| less_or_equal(u,additive_identity) ),
inference(demodulation,[status(thm),theory(equality)],[c_58,c_2898]) ).
tff(c_2960,plain,
~ less_or_equal(additive_identity,additive_inverse(u)),
inference(negUnitSimplification,[status(thm)],[c_935,c_2959]) ).
tff(c_147,plain,
! [Y_65] :
( ~ defined(Y_65)
| less_or_equal(Y_65,Y_65) ),
inference(factorization,[status(thm),theory(equality)],[c_46]) ).
tff(c_948,plain,
! [Y_193,U_195,X_196,Z_192,V_194,W_197] :
( ~ sum(U_195,Z_192,W_197)
| ~ sum(Y_193,Z_192,V_194)
| ~ sum(X_196,Y_193,U_195)
| sum(X_196,V_194,W_197) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_1685,plain,
! [Y_233,V_234,X_235] :
( ~ sum(Y_233,additive_inverse(a),V_234)
| ~ sum(X_235,Y_233,b)
| sum(X_235,V_234,u) ),
inference(resolution,[status(thm)],[c_60,c_948]) ).
tff(c_1722,plain,
! [X_235] :
( ~ sum(X_235,b,b)
| sum(X_235,u,u) ),
inference(resolution,[status(thm)],[c_60,c_1685]) ).
tff(c_2886,plain,
! [X_235] :
( ~ less_or_equal(X_235,additive_inverse(u))
| less_or_equal(u,additive_identity)
| ~ defined(u)
| ~ sum(X_235,b,b) ),
inference(resolution,[status(thm)],[c_1722,c_2876]) ).
tff(c_2937,plain,
! [X_235] :
( ~ less_or_equal(X_235,additive_inverse(u))
| less_or_equal(u,additive_identity)
| ~ sum(X_235,b,b) ),
inference(demodulation,[status(thm),theory(equality)],[c_58,c_2886]) ).
tff(c_3473,plain,
! [X_284] :
( ~ less_or_equal(X_284,additive_inverse(u))
| ~ sum(X_284,b,b) ),
inference(negUnitSimplification,[status(thm)],[c_935,c_2937]) ).
tff(c_3498,plain,
( ~ sum(additive_inverse(u),b,b)
| ~ defined(additive_inverse(u)) ),
inference(resolution,[status(thm)],[c_147,c_3473]) ).
tff(c_3662,plain,
~ defined(additive_inverse(u)),
inference(splitLeft,[status(thm)],[c_3498]) ).
tff(c_3665,plain,
~ defined(u),
inference(resolution,[status(thm)],[c_30,c_3662]) ).
tff(c_3669,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_58,c_3665]) ).
tff(c_3671,plain,
defined(additive_inverse(u)),
inference(splitRight,[status(thm)],[c_3498]) ).
tff(c_1005,plain,
! [X_200,X_201,U_202] :
( ~ sum(X_200,X_201,U_202)
| ~ less_or_equal(X_200,additive_identity)
| less_or_equal(U_202,X_201)
| ~ defined(X_201) ),
inference(resolution,[status(thm)],[c_6,c_226]) ).
tff(c_1035,plain,
( ~ less_or_equal(b,additive_identity)
| less_or_equal(u,additive_inverse(a))
| ~ defined(additive_inverse(a)) ),
inference(resolution,[status(thm)],[c_60,c_1005]) ).
tff(c_1053,plain,
( ~ less_or_equal(b,additive_identity)
| less_or_equal(u,additive_inverse(a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_348,c_1035]) ).
tff(c_1086,plain,
~ less_or_equal(b,additive_identity),
inference(splitLeft,[status(thm)],[c_1053]) ).
tff(c_1089,plain,
( ~ defined(b)
| ~ defined(additive_identity)
| less_or_equal(additive_identity,b) ),
inference(resolution,[status(thm)],[c_46,c_1086]) ).
tff(c_1095,plain,
less_or_equal(additive_identity,b),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_56,c_1089]) ).
tff(c_1097,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_380,c_1095]) ).
tff(c_1099,plain,
less_or_equal(b,additive_identity),
inference(splitRight,[status(thm)],[c_1053]) ).
tff(c_839,plain,
! [X_61,X_181] :
( ~ less_or_equal(X_61,X_181)
| less_or_equal(X_61,additive_inverse(a))
| ~ less_or_equal(X_181,additive_identity) ),
inference(resolution,[status(thm)],[c_833,c_44]) ).
tff(c_1139,plain,
( less_or_equal(b,additive_inverse(a))
| ~ less_or_equal(additive_identity,additive_identity) ),
inference(resolution,[status(thm)],[c_1099,c_839]) ).
tff(c_1200,plain,
~ less_or_equal(additive_identity,additive_identity),
inference(splitLeft,[status(thm)],[c_1139]) ).
tff(c_1278,plain,
~ defined(additive_identity),
inference(resolution,[status(thm)],[c_147,c_1200]) ).
tff(c_1284,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28,c_1278]) ).
tff(c_1286,plain,
less_or_equal(additive_identity,additive_identity),
inference(splitRight,[status(thm)],[c_1139]) ).
tff(c_149,plain,
! [Y_104,X_105] :
( ~ defined(Y_104)
| ~ defined(X_105)
| less_or_equal(Y_104,X_105)
| less_or_equal(X_105,Y_104) ),
inference(cnfTransformation,[status(thm)],[f_222]) ).
tff(c_1934,plain,
! [X_244,X_245,Y_246] :
( ~ less_or_equal(X_244,X_245)
| less_or_equal(X_244,Y_246)
| ~ defined(Y_246)
| ~ defined(X_245)
| less_or_equal(Y_246,X_245) ),
inference(resolution,[status(thm)],[c_149,c_44]) ).
tff(c_1950,plain,
! [Y_246] :
( less_or_equal(additive_identity,Y_246)
| ~ defined(Y_246)
| ~ defined(additive_identity)
| less_or_equal(Y_246,additive_identity) ),
inference(resolution,[status(thm)],[c_1286,c_1934]) ).
tff(c_2002,plain,
! [Y_246] :
( less_or_equal(additive_identity,Y_246)
| ~ defined(Y_246)
| less_or_equal(Y_246,additive_identity) ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_1950]) ).
tff(c_86,plain,
! [X_14] :
( sum(X_14,additive_inverse(X_14),additive_identity)
| ~ defined(X_14) ),
inference(resolution,[status(thm)],[c_8,c_79]) ).
tff(c_3273,plain,
! [Y_274,X_275,V_276,X_277] :
( ~ sum(Y_274,X_275,V_276)
| ~ sum(X_277,Y_274,additive_identity)
| sum(X_277,V_276,X_275)
| ~ defined(X_275) ),
inference(resolution,[status(thm)],[c_6,c_948]) ).
tff(c_3311,plain,
! [X_277] :
( ~ sum(X_277,additive_inverse(a),additive_identity)
| sum(X_277,u,b)
| ~ defined(b) ),
inference(resolution,[status(thm)],[c_88,c_3273]) ).
tff(c_6076,plain,
! [X_330] :
( ~ sum(X_330,additive_inverse(a),additive_identity)
| sum(X_330,u,b) ),
inference(demodulation,[status(thm),theory(equality)],[c_56,c_3311]) ).
tff(c_6084,plain,
( sum(a,u,b)
| ~ defined(a) ),
inference(resolution,[status(thm)],[c_86,c_6076]) ).
tff(c_6094,plain,
sum(a,u,b),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_6084]) ).
tff(c_6159,plain,
sum(u,a,b),
inference(resolution,[status(thm)],[c_6094,c_10]) ).
tff(c_977,plain,
! [Y_193,X_13,V_194,X_196] :
( ~ sum(Y_193,X_13,V_194)
| ~ sum(X_196,Y_193,additive_identity)
| sum(X_196,V_194,X_13)
| ~ defined(X_13) ),
inference(resolution,[status(thm)],[c_6,c_948]) ).
tff(c_6171,plain,
! [X_196] :
( ~ sum(X_196,u,additive_identity)
| sum(X_196,b,a)
| ~ defined(a) ),
inference(resolution,[status(thm)],[c_6159,c_977]) ).
tff(c_7017,plain,
! [X_347] :
( ~ sum(X_347,u,additive_identity)
| sum(X_347,b,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_6171]) ).
tff(c_7025,plain,
( sum(additive_inverse(u),b,a)
| ~ defined(u) ),
inference(resolution,[status(thm)],[c_8,c_7017]) ).
tff(c_7031,plain,
sum(additive_inverse(u),b,a),
inference(demodulation,[status(thm),theory(equality)],[c_58,c_7025]) ).
tff(c_255,plain,
! [X_119,X_13,U_118] :
( ~ sum(X_119,X_13,U_118)
| ~ less_or_equal(X_119,additive_identity)
| less_or_equal(U_118,X_13)
| ~ defined(X_13) ),
inference(resolution,[status(thm)],[c_6,c_226]) ).
tff(c_7063,plain,
( ~ less_or_equal(additive_inverse(u),additive_identity)
| less_or_equal(a,b)
| ~ defined(b) ),
inference(resolution,[status(thm)],[c_7031,c_255]) ).
tff(c_7096,plain,
( ~ less_or_equal(additive_inverse(u),additive_identity)
| less_or_equal(a,b) ),
inference(demodulation,[status(thm),theory(equality)],[c_56,c_7063]) ).
tff(c_7097,plain,
~ less_or_equal(additive_inverse(u),additive_identity),
inference(negUnitSimplification,[status(thm)],[c_64,c_7096]) ).
tff(c_7112,plain,
( less_or_equal(additive_identity,additive_inverse(u))
| ~ defined(additive_inverse(u)) ),
inference(resolution,[status(thm)],[c_2002,c_7097]) ).
tff(c_7128,plain,
less_or_equal(additive_identity,additive_inverse(u)),
inference(demodulation,[status(thm),theory(equality)],[c_3671,c_7112]) ).
tff(c_7130,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2960,c_7128]) ).
tff(c_7132,plain,
less_or_equal(u,additive_identity),
inference(splitRight,[status(thm)],[c_926]) ).
tff(c_7162,plain,
! [X_349] :
( ~ less_or_equal(X_349,u)
| less_or_equal(X_349,additive_identity) ),
inference(resolution,[status(thm)],[c_7132,c_44]) ).
tff(c_7204,plain,
less_or_equal(additive_identity,additive_identity),
inference(resolution,[status(thm)],[c_62,c_7162]) ).
tff(c_42,plain,
! [Y_60,X_59] :
( ~ less_or_equal(Y_60,X_59)
| ~ less_or_equal(X_59,Y_60)
| sum(additive_identity,X_59,Y_60) ),
inference(cnfTransformation,[status(thm)],[f_204]) ).
tff(c_7205,plain,
! [Y_351,Z_350,W_355,U_353,X_354,V_352] :
( ~ sum(U_353,Z_350,W_355)
| ~ sum(Y_351,Z_350,V_352)
| ~ sum(X_354,Y_351,U_353)
| sum(X_354,V_352,W_355) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_9786,plain,
! [Y_435,X_436,V_437,X_438] :
( ~ sum(Y_435,X_436,V_437)
| ~ sum(X_438,Y_435,additive_identity)
| sum(X_438,V_437,X_436)
| ~ defined(X_436) ),
inference(resolution,[status(thm)],[c_6,c_7205]) ).
tff(c_9824,plain,
! [X_438] :
( ~ sum(X_438,additive_inverse(a),additive_identity)
| sum(X_438,u,b)
| ~ defined(b) ),
inference(resolution,[status(thm)],[c_88,c_9786]) ).
tff(c_10673,plain,
! [X_455] :
( ~ sum(X_455,additive_inverse(a),additive_identity)
| sum(X_455,u,b) ),
inference(demodulation,[status(thm),theory(equality)],[c_56,c_9824]) ).
tff(c_10681,plain,
( sum(a,u,b)
| ~ defined(a) ),
inference(resolution,[status(thm)],[c_86,c_10673]) ).
tff(c_10691,plain,
sum(a,u,b),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_10681]) ).
tff(c_10730,plain,
sum(u,a,b),
inference(resolution,[status(thm)],[c_10691,c_10]) ).
tff(c_7234,plain,
! [Y_351,X_13,V_352,X_354] :
( ~ sum(Y_351,X_13,V_352)
| ~ sum(X_354,Y_351,additive_identity)
| sum(X_354,V_352,X_13)
| ~ defined(X_13) ),
inference(resolution,[status(thm)],[c_6,c_7205]) ).
tff(c_10895,plain,
! [X_354] :
( ~ sum(X_354,u,additive_identity)
| sum(X_354,b,a)
| ~ defined(a) ),
inference(resolution,[status(thm)],[c_10730,c_7234]) ).
tff(c_11814,plain,
! [X_471] :
( ~ sum(X_471,u,additive_identity)
| sum(X_471,b,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_10895]) ).
tff(c_11818,plain,
( sum(additive_identity,b,a)
| ~ less_or_equal(additive_identity,u)
| ~ less_or_equal(u,additive_identity) ),
inference(resolution,[status(thm)],[c_42,c_11814]) ).
tff(c_11825,plain,
sum(additive_identity,b,a),
inference(demodulation,[status(thm),theory(equality)],[c_7132,c_62,c_11818]) ).
tff(c_11841,plain,
( ~ less_or_equal(additive_identity,additive_identity)
| less_or_equal(a,b)
| ~ defined(b) ),
inference(resolution,[status(thm)],[c_11825,c_255]) ).
tff(c_11871,plain,
less_or_equal(a,b),
inference(demodulation,[status(thm),theory(equality)],[c_56,c_7204,c_11841]) ).
tff(c_11873,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64,c_11871]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : FLD068-4 : TPTP v9.0.0. Bugfixed v2.1.0.
% 0.03/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.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 18:57:18 EDT 2025
% 0.13/0.34 % CPUTime :
% 10.52/3.59 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.64/3.61
% 10.64/3.61 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------