%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : HEN007-1 : TPTP v9.0.0. Released v1.0.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 : n002.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:45:54 PM UTC 2025
% Result : Unsatisfiable 80.63s 65.01s
% Output : CNFRefutation 80.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 12
% Syntax : Number of formulae : 66 ( 34 unt; 0 typ; 0 def)
% Number of atoms : 130 ( 16 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 131 ( 67 ~; 64 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% Number of variables : 110 ( 110 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ quotient > less_equal > divide > #nlpp > zero > zQy > zQx > z > y > x > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(less_equal,type,
less_equal: ( $i * $i ) > $o ).
tff(divide,type,
divide: ( $i * $i ) > $i ).
tff(x,type,
x: $i ).
tff(zQx,type,
zQx: $i ).
tff(y,type,
y: $i ).
tff(quotient,type,
quotient: ( $i * $i * $i ) > $o ).
tff(zQy,type,
zQy: $i ).
tff(identity,type,
identity: $i ).
tff(z,type,
z: $i ).
tff(zero,type,
zero: $i ).
tff(f_111,axiom,
~ less_equal(zQy,zQx),
file(unknown,unknown) ).
tff(f_80,axiom,
! [X] : less_equal(zero,X),
file(unknown,unknown) ).
tff(f_109,axiom,
quotient(z,x,zQx),
file(unknown,unknown) ).
tff(f_59,axiom,
! [X,Y,Z] :
( ~ quotient(X,Y,Z)
| less_equal(Z,X) ),
file(unknown,unknown) ).
tff(f_48,axiom,
! [X,Y] :
( ~ less_equal(X,Y)
| quotient(X,Y,zero) ),
file(unknown,unknown) ).
tff(f_95,axiom,
! [X,Y] : quotient(X,Y,divide(X,Y)),
file(unknown,unknown) ).
tff(f_104,axiom,
! [X,Y,Z,W] :
( ~ quotient(X,Y,Z)
| ~ quotient(X,Y,W)
| ( Z = W ) ),
file(unknown,unknown) ).
tff(f_108,axiom,
quotient(z,y,zQy),
file(unknown,unknown) ).
tff(f_77,axiom,
! [V3,V5,Z,V1,X,Y,V2,V4] :
( ~ quotient(X,Y,V1)
| ~ quotient(Y,Z,V2)
| ~ quotient(X,Z,V3)
| ~ quotient(V3,V2,V4)
| ~ quotient(V1,Z,V5)
| less_equal(V4,V5) ),
file(unknown,unknown) ).
tff(f_89,axiom,
! [X,Y] :
( ~ less_equal(X,Y)
| ~ less_equal(Y,X)
| ( X = Y ) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X,Y] :
( ~ quotient(X,Y,zero)
| less_equal(X,Y) ),
file(unknown,unknown) ).
tff(f_107,axiom,
less_equal(x,y),
file(unknown,unknown) ).
tff(c_26,plain,
~ less_equal(zQy,zQx),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_10,plain,
! [X_16] : less_equal(zero,X_16),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_24,plain,
quotient(z,x,zQx),
inference(cnfTransformation,[status(thm)],[f_109]) ).
tff(c_30,plain,
! [Z_30,X_31,Y_32] :
( less_equal(Z_30,X_31)
| ~ quotient(X_31,Y_32,Z_30) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_42,plain,
less_equal(zQx,z),
inference(resolution,[status(thm)],[c_24,c_30]) ).
tff(c_2,plain,
! [X_1,Y_2] :
( quotient(X_1,Y_2,zero)
| ~ less_equal(X_1,Y_2) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_16,plain,
! [X_20,Y_21] : quotient(X_20,Y_21,divide(X_20,Y_21)),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_81,plain,
! [Z_42,W_43,X_44,Y_45] :
( ( Z_42 = W_43 )
| ~ quotient(X_44,Y_45,W_43)
| ~ quotient(X_44,Y_45,Z_42) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_231,plain,
! [X_61,Y_62,Z_63] :
( ( divide(X_61,Y_62) = Z_63 )
| ~ quotient(X_61,Y_62,Z_63) ),
inference(resolution,[status(thm)],[c_16,c_81]) ).
tff(c_256,plain,
! [X_64,Y_65] :
( ( divide(X_64,Y_65) = zero )
| ~ less_equal(X_64,Y_65) ),
inference(resolution,[status(thm)],[c_2,c_231]) ).
tff(c_276,plain,
divide(zQx,z) = zero,
inference(resolution,[status(thm)],[c_42,c_256]) ).
tff(c_288,plain,
quotient(zQx,z,zero),
inference(superposition,[status(thm),theory(equality)],[c_276,c_16]) ).
tff(c_22,plain,
quotient(z,y,zQy),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_107,plain,
! [X_51,V4_49,Y_53,V3_48,V2_47,Z_50,V5_54,V1_52] :
( less_equal(V4_49,V5_54)
| ~ quotient(V1_52,Z_50,V5_54)
| ~ quotient(V3_48,V2_47,V4_49)
| ~ quotient(X_51,Z_50,V3_48)
| ~ quotient(Y_53,Z_50,V2_47)
| ~ quotient(X_51,Y_53,V1_52) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_1381,plain,
! [V2_131,X_128,Y_127,V4_132,Y_133,X_129,V3_130] :
( less_equal(V4_132,zero)
| ~ quotient(V3_130,V2_131,V4_132)
| ~ quotient(X_129,Y_133,V3_130)
| ~ quotient(Y_127,Y_133,V2_131)
| ~ quotient(X_129,Y_127,X_128)
| ~ less_equal(X_128,Y_133) ),
inference(resolution,[status(thm)],[c_2,c_107]) ).
tff(c_2730,plain,
! [Y_227,Y_232,Y_228,X_231,X_229,X_230] :
( less_equal(divide(X_229,Y_227),zero)
| ~ quotient(X_231,Y_228,X_229)
| ~ quotient(Y_232,Y_228,Y_227)
| ~ quotient(X_231,Y_232,X_230)
| ~ less_equal(X_230,Y_228) ),
inference(resolution,[status(thm)],[c_16,c_1381]) ).
tff(c_281426,plain,
! [Y_2499,X_2498,Y_2496,Y_2497,X_2500] :
( less_equal(divide(divide(X_2498,Y_2496),Y_2499),zero)
| ~ quotient(Y_2497,Y_2496,Y_2499)
| ~ quotient(X_2498,Y_2497,X_2500)
| ~ less_equal(X_2500,Y_2496) ),
inference(resolution,[status(thm)],[c_16,c_2730]) ).
tff(c_445881,plain,
! [X_3624,X_3625] :
( less_equal(divide(divide(X_3624,y),zQy),zero)
| ~ quotient(X_3624,z,X_3625)
| ~ less_equal(X_3625,y) ),
inference(resolution,[status(thm)],[c_22,c_281426]) ).
tff(c_445890,plain,
( less_equal(divide(divide(zQx,y),zQy),zero)
| ~ less_equal(zero,y) ),
inference(resolution,[status(thm)],[c_288,c_445881]) ).
tff(c_445911,plain,
less_equal(divide(divide(zQx,y),zQy),zero),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_445890]) ).
tff(c_55,plain,
! [Y_39,X_40] :
( ( Y_39 = X_40 )
| ~ less_equal(Y_39,X_40)
| ~ less_equal(X_40,Y_39) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_72,plain,
! [X_16] :
( ( zero = X_16 )
| ~ less_equal(X_16,zero) ),
inference(resolution,[status(thm)],[c_10,c_55]) ).
tff(c_445937,plain,
divide(divide(zQx,y),zQy) = zero,
inference(resolution,[status(thm)],[c_445911,c_72]) ).
tff(c_446012,plain,
quotient(divide(zQx,y),zQy,zero),
inference(superposition,[status(thm),theory(equality)],[c_445937,c_16]) ).
tff(c_4,plain,
! [X_3,Y_4] :
( less_equal(X_3,Y_4)
| ~ quotient(X_3,Y_4,zero) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_446112,plain,
less_equal(divide(zQx,y),zQy),
inference(resolution,[status(thm)],[c_446012,c_4]) ).
tff(c_12,plain,
! [Y_18,X_17] :
( ( Y_18 = X_17 )
| ~ less_equal(Y_18,X_17)
| ~ less_equal(X_17,Y_18) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_446122,plain,
( ( divide(zQx,y) = zQy )
| ~ less_equal(zQy,divide(zQx,y)) ),
inference(resolution,[status(thm)],[c_446112,c_12]) ).
tff(c_447057,plain,
~ less_equal(zQy,divide(zQx,y)),
inference(splitLeft,[status(thm)],[c_446122]) ).
tff(c_20,plain,
less_equal(x,y),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_918,plain,
! [X_111,V3_114,Y_112,V4_116,X_113,V2_115,Y_110] :
( less_equal(V4_116,divide(X_111,Y_110))
| ~ quotient(V3_114,V2_115,V4_116)
| ~ quotient(X_113,Y_110,V3_114)
| ~ quotient(Y_112,Y_110,V2_115)
| ~ quotient(X_113,Y_112,X_111) ),
inference(resolution,[status(thm)],[c_16,c_107]) ).
tff(c_2612,plain,
! [Y_222,X_221,Y_220,X_218,X_219,Y_217] :
( less_equal(divide(X_218,Y_217),divide(X_219,Y_222))
| ~ quotient(X_221,Y_222,X_218)
| ~ quotient(Y_220,Y_222,Y_217)
| ~ quotient(X_221,Y_220,X_219) ),
inference(resolution,[status(thm)],[c_16,c_918]) ).
tff(c_2678,plain,
! [Y_223,X_224,Y_225] :
( less_equal(divide(zQy,Y_223),divide(X_224,y))
| ~ quotient(Y_225,y,Y_223)
| ~ quotient(z,Y_225,X_224) ),
inference(resolution,[status(thm)],[c_22,c_2612]) ).
tff(c_444321,plain,
! [X_3606,X_3607] :
( less_equal(divide(zQy,zero),divide(X_3606,y))
| ~ quotient(z,X_3607,X_3606)
| ~ less_equal(X_3607,y) ),
inference(resolution,[status(thm)],[c_2,c_2678]) ).
tff(c_444336,plain,
( less_equal(divide(zQy,zero),divide(zQx,y))
| ~ less_equal(x,y) ),
inference(resolution,[status(thm)],[c_24,c_444321]) ).
tff(c_444347,plain,
less_equal(divide(zQy,zero),divide(zQx,y)),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_444336]) ).
tff(c_249,plain,
! [X_1,Y_2] :
( ( divide(X_1,Y_2) = zero )
| ~ less_equal(X_1,Y_2) ),
inference(resolution,[status(thm)],[c_2,c_231]) ).
tff(c_444620,plain,
divide(divide(zQy,zero),divide(zQx,y)) = zero,
inference(resolution,[status(thm)],[c_444347,c_249]) ).
tff(c_281180,plain,
! [Y_2488,Y_2489,X_2486,X_2487,Y_2485] :
( less_equal(divide(divide(X_2486,Y_2485),Y_2489),divide(X_2487,Y_2485))
| ~ quotient(Y_2488,Y_2485,Y_2489)
| ~ quotient(X_2486,Y_2488,X_2487) ),
inference(resolution,[status(thm)],[c_16,c_2612]) ).
tff(c_523947,plain,
! [X_4154,Y_4155,X_4156,X_4157] :
( less_equal(divide(divide(X_4154,Y_4155),zero),divide(X_4156,Y_4155))
| ~ quotient(X_4154,X_4157,X_4156)
| ~ less_equal(X_4157,Y_4155) ),
inference(resolution,[status(thm)],[c_2,c_281180]) ).
tff(c_652278,plain,
! [X_4834,Y_4835,Y_4836] :
( less_equal(divide(divide(X_4834,Y_4835),zero),divide(divide(X_4834,Y_4836),Y_4835))
| ~ less_equal(Y_4836,Y_4835) ),
inference(resolution,[status(thm)],[c_16,c_523947]) ).
tff(c_652893,plain,
( less_equal(divide(divide(zQy,divide(zQx,y)),zero),zero)
| ~ less_equal(zero,divide(zQx,y)) ),
inference(superposition,[status(thm),theory(equality)],[c_444620,c_652278]) ).
tff(c_653237,plain,
less_equal(divide(divide(zQy,divide(zQx,y)),zero),zero),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_652893]) ).
tff(c_655751,plain,
divide(divide(zQy,divide(zQx,y)),zero) = zero,
inference(resolution,[status(thm)],[c_653237,c_72]) ).
tff(c_656032,plain,
quotient(divide(zQy,divide(zQx,y)),zero,zero),
inference(superposition,[status(thm),theory(equality)],[c_655751,c_16]) ).
tff(c_656225,plain,
less_equal(divide(zQy,divide(zQx,y)),zero),
inference(resolution,[status(thm)],[c_656032,c_4]) ).
tff(c_656260,plain,
divide(zQy,divide(zQx,y)) = zero,
inference(resolution,[status(thm)],[c_656225,c_72]) ).
tff(c_656561,plain,
quotient(zQy,divide(zQx,y),zero),
inference(superposition,[status(thm),theory(equality)],[c_656260,c_16]) ).
tff(c_656685,plain,
less_equal(zQy,divide(zQx,y)),
inference(resolution,[status(thm)],[c_656561,c_4]) ).
tff(c_656723,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_447057,c_656685]) ).
tff(c_656724,plain,
divide(zQx,y) = zQy,
inference(splitRight,[status(thm)],[c_446122]) ).
tff(c_40,plain,
! [X_20,Y_21] : less_equal(divide(X_20,Y_21),X_20),
inference(resolution,[status(thm)],[c_16,c_30]) ).
tff(c_656900,plain,
less_equal(zQy,zQx),
inference(superposition,[status(thm),theory(equality)],[c_656724,c_40]) ).
tff(c_656944,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26,c_656900]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HEN007-1 : TPTP v9.0.0. Released v1.0.0.
% 0.03/0.13 % 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.13/0.34 % Computer : n002.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 22:51:31 EDT 2025
% 0.13/0.34 % CPUTime :
% 80.63/65.01 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 80.63/65.03
% 80.63/65.03 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------