%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP090-1 : TPTP v9.0.0. Bugfixed v2.7.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 : n028.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:24:58 PM UTC 2025
% Result : Unsatisfiable 22.07s 8.15s
% Output : CNFRefutation 22.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 4
% Syntax : Number of formulae : 72 ( 68 unt; 0 typ; 0 def)
% Number of atoms : 81 ( 77 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 32 ( 23 ~; 9 |; 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 : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 120 ( 120 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > divide > #nlpp > inverse > c3 > b4 > b3 > b2 > b1 > a4 > a3 > a2 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a1,type,
a1: $i ).
tff(a3,type,
a3: $i ).
tff(c3,type,
c3: $i ).
tff(divide,type,
divide: ( $i * $i ) > $i ).
tff(b2,type,
b2: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b1,type,
b1: $i ).
tff(b4,type,
b4: $i ).
tff(b3,type,
b3: $i ).
tff(a2,type,
a2: $i ).
tff(a4,type,
a4: $i ).
tff(f_32,axiom,
! [X,Z] : ( inverse(X) = divide(divide(Z,Z),X) ),
file(unknown,unknown) ).
tff(f_29,axiom,
! [X,Y,Z] : ( multiply(X,Y) = divide(X,divide(divide(Z,Z),Y)) ),
file(unknown,unknown) ).
tff(f_26,axiom,
! [X,Y,Z] : ( divide(divide(X,divide(Y,Z)),divide(X,Y)) = Z ),
file(unknown,unknown) ).
tff(f_43,axiom,
( ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(a4,b4) != multiply(b4,a4) ) ),
file(unknown,unknown) ).
tff(c_6,plain,
! [Z_8,X_7] : ( divide(divide(Z_8,Z_8),X_7) = inverse(X_7) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_4,plain,
! [X_4,Z_6,Y_5] : ( divide(X_4,divide(divide(Z_6,Z_6),Y_5)) = multiply(X_4,Y_5) ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_9,plain,
! [X_4,Y_5] : ( divide(X_4,inverse(Y_5)) = multiply(X_4,Y_5) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4]) ).
tff(c_107,plain,
! [X_17,Y_18,Z_19] : ( divide(divide(X_17,divide(Y_18,Z_19)),divide(X_17,Y_18)) = Z_19 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_174,plain,
! [Y_20,Z_21] : ( inverse(divide(divide(Y_20,Z_21),Y_20)) = Z_21 ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_6]) ).
tff(c_203,plain,
! [X_7] : ( inverse(inverse(X_7)) = X_7 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_174]) ).
tff(c_27,plain,
! [X_11,Y_12] : ( divide(X_11,inverse(Y_12)) = multiply(X_11,Y_12) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4]) ).
tff(c_45,plain,
! [Z_8,Y_12] : ( multiply(divide(Z_8,Z_8),Y_12) = inverse(inverse(Y_12)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_27]) ).
tff(c_207,plain,
! [Z_8,Y_12] : ( multiply(divide(Z_8,Z_8),Y_12) = Y_12 ),
inference(demodulation,[status(thm),theory(equality)],[c_203,c_45]) ).
tff(c_123,plain,
! [Y_18,Z_19] : ( inverse(divide(divide(Y_18,Z_19),Y_18)) = Z_19 ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_6]) ).
tff(c_158,plain,
! [Y_18,Z_19,Z_8] : ( divide(inverse(divide(Y_18,Z_19)),divide(divide(Z_8,Z_8),Y_18)) = Z_19 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_107]) ).
tff(c_20026,plain,
! [Y_213,Z_214] : ( multiply(inverse(divide(Y_213,Z_214)),Y_213) = Z_214 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_158]) ).
tff(c_20052,plain,
! [Z_215,Y_216] : ( multiply(Z_215,divide(Y_216,Z_215)) = Y_216 ),
inference(superposition,[status(thm),theory(equality)],[c_123,c_20026]) ).
tff(c_20135,plain,
! [Y_219,Z_220] : ( divide(Y_219,divide(Z_220,Z_220)) = Y_219 ),
inference(superposition,[status(thm),theory(equality)],[c_207,c_20052]) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3] : ( divide(divide(X_1,divide(Y_2,Z_3)),divide(X_1,Y_2)) = Z_3 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_20172,plain,
! [Y_219,Z_220,Z_3] : ( divide(divide(Y_219,divide(divide(Z_220,Z_220),Z_3)),Y_219) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_20135,c_2]) ).
tff(c_20485,plain,
! [Y_225,Z_226] : ( divide(multiply(Y_225,Z_226),Y_225) = Z_226 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_20172]) ).
tff(c_20169,plain,
! [Y_219,Z_220] : ( divide(Y_219,divide(Y_219,Z_220)) = Z_220 ),
inference(superposition,[status(thm),theory(equality)],[c_20135,c_2]) ).
tff(c_21294,plain,
! [Y_243,Z_244] : ( divide(multiply(Y_243,Z_244),Z_244) = Y_243 ),
inference(superposition,[status(thm),theory(equality)],[c_20485,c_20169]) ).
tff(c_20035,plain,
! [Z_19,Y_18] : ( multiply(Z_19,divide(Y_18,Z_19)) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_123,c_20026]) ).
tff(c_21314,plain,
! [Z_244,Y_243] : ( multiply(Z_244,Y_243) = multiply(Y_243,Z_244) ),
inference(superposition,[status(thm),theory(equality)],[c_21294,c_20035]) ).
tff(c_20044,plain,
! [X_4,Y_5] : ( multiply(inverse(multiply(X_4,Y_5)),X_4) = inverse(Y_5) ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_20026]) ).
tff(c_34715,plain,
! [Z_378,X_379,Y_380] : ( multiply(inverse(Z_378),divide(X_379,divide(Y_380,Z_378))) = divide(X_379,Y_380) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_20026]) ).
tff(c_35005,plain,
! [X_7,X_379,Y_380] : ( multiply(X_7,divide(X_379,divide(Y_380,inverse(X_7)))) = divide(X_379,Y_380) ),
inference(superposition,[status(thm),theory(equality)],[c_203,c_34715]) ).
tff(c_55066,plain,
! [X_477,X_478,Y_479] : ( multiply(X_477,divide(X_478,multiply(Y_479,X_477))) = divide(X_478,Y_479) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_35005]) ).
tff(c_55343,plain,
! [X_4,X_478,Y_5] : ( multiply(X_4,divide(X_478,inverse(Y_5))) = divide(X_478,inverse(multiply(X_4,Y_5))) ),
inference(superposition,[status(thm),theory(equality)],[c_20044,c_55066]) ).
tff(c_55511,plain,
! [X_478,X_4,Y_5] : ( multiply(X_478,multiply(X_4,Y_5)) = multiply(X_4,multiply(X_478,Y_5)) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_9,c_55343]) ).
tff(c_20230,plain,
! [Y_219,Z_3] : ( divide(multiply(Y_219,Z_3),Y_219) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_20172]) ).
tff(c_20237,plain,
! [Y_221,Z_222] : ( divide(Y_221,divide(Y_221,Z_222)) = Z_222 ),
inference(superposition,[status(thm),theory(equality)],[c_20135,c_2]) ).
tff(c_20781,plain,
! [Y_233,Z_234] : ( multiply(divide(Y_233,Z_234),Z_234) = Y_233 ),
inference(superposition,[status(thm),theory(equality)],[c_20237,c_20035]) ).
tff(c_20801,plain,
! [Z_3,Y_219] : ( multiply(Z_3,Y_219) = multiply(Y_219,Z_3) ),
inference(superposition,[status(thm),theory(equality)],[c_20230,c_20781]) ).
tff(c_20047,plain,
! [X_7,Z_8] : ( multiply(inverse(inverse(X_7)),divide(Z_8,Z_8)) = X_7 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_20026]) ).
tff(c_20085,plain,
! [X_217,Z_218] : ( multiply(X_217,divide(Z_218,Z_218)) = X_217 ),
inference(demodulation,[status(thm),theory(equality)],[c_203,c_20047]) ).
tff(c_20123,plain,
! [X_217,Y_5] : ( multiply(X_217,multiply(inverse(Y_5),Y_5)) = X_217 ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_20085]) ).
tff(c_21288,plain,
! [X_217,Y_5] : ( multiply(X_217,multiply(Y_5,inverse(Y_5))) = X_217 ),
inference(demodulation,[status(thm),theory(equality)],[c_20801,c_20123]) ).
tff(c_20553,plain,
! [Y_227,Z_228] : ( multiply(divide(Y_227,Z_228),Z_228) = Y_227 ),
inference(superposition,[status(thm),theory(equality)],[c_20237,c_20035]) ).
tff(c_20573,plain,
! [Z_3,Y_219] : ( multiply(Z_3,Y_219) = multiply(Y_219,Z_3) ),
inference(superposition,[status(thm),theory(equality)],[c_20230,c_20553]) ).
tff(c_255,plain,
! [Y_25,Z_26] : ( multiply(inverse(divide(Y_25,Z_26)),Y_25) = Z_26 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_158]) ).
tff(c_276,plain,
! [X_7,Z_8] : ( multiply(inverse(inverse(X_7)),divide(Z_8,Z_8)) = X_7 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_255]) ).
tff(c_310,plain,
! [X_29,Z_30] : ( multiply(X_29,divide(Z_30,Z_30)) = X_29 ),
inference(demodulation,[status(thm),theory(equality)],[c_203,c_276]) ).
tff(c_340,plain,
! [Z_8,Z_30] : ( divide(Z_8,Z_8) = divide(Z_30,Z_30) ),
inference(superposition,[status(thm),theory(equality)],[c_207,c_310]) ).
tff(c_208,plain,
! [X_22] : ( inverse(inverse(X_22)) = X_22 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_174]) ).
tff(c_217,plain,
! [X_4,X_22] : ( multiply(X_4,inverse(X_22)) = divide(X_4,X_22) ),
inference(superposition,[status(thm),theory(equality)],[c_208,c_9]) ).
tff(c_281,plain,
! [Z_27,Y_28] : ( multiply(Z_27,divide(Y_28,Z_27)) = Y_28 ),
inference(superposition,[status(thm),theory(equality)],[c_123,c_255]) ).
tff(c_360,plain,
! [Y_31,Z_32] : ( divide(Y_31,divide(Z_32,Z_32)) = Y_31 ),
inference(superposition,[status(thm),theory(equality)],[c_281,c_207]) ).
tff(c_397,plain,
! [Y_31,Z_32,Z_3] : ( divide(divide(Y_31,divide(divide(Z_32,Z_32),Z_3)),Y_31) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_360,c_2]) ).
tff(c_455,plain,
! [Y_31,Z_3] : ( divide(multiply(Y_31,Z_3),Y_31) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_397]) ).
tff(c_617,plain,
! [Y_35,Z_36] : ( divide(Y_35,divide(Y_35,Z_36)) = Z_36 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_360]) ).
tff(c_264,plain,
! [Z_19,Y_18] : ( multiply(Z_19,divide(Y_18,Z_19)) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_123,c_255]) ).
tff(c_775,plain,
! [Y_39,Z_40] : ( multiply(divide(Y_39,Z_40),Z_40) = Y_39 ),
inference(superposition,[status(thm),theory(equality)],[c_617,c_264]) ).
tff(c_795,plain,
! [Z_3,Y_31] : ( multiply(Z_3,Y_31) = multiply(Y_31,Z_3) ),
inference(superposition,[status(thm),theory(equality)],[c_455,c_775]) ).
tff(c_8,plain,
( ( multiply(b4,a4) != multiply(a4,b4) )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_253,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_921,plain,
multiply(b1,inverse(b1)) != multiply(a1,inverse(a1)),
inference(demodulation,[status(thm),theory(equality)],[c_795,c_795,c_253]) ).
tff(c_20014,plain,
divide(b1,b1) != divide(a1,a1),
inference(demodulation,[status(thm),theory(equality)],[c_217,c_217,c_921]) ).
tff(c_20016,plain,
! [Z_8] : ( divide(a1,a1) != divide(Z_8,Z_8) ),
inference(superposition,[status(thm),theory(equality)],[c_340,c_20014]) ).
tff(c_20022,plain,
$false,
inference(reflexivity,[status(thm),theory(equality)],[c_20016]) ).
tff(c_20023,plain,
( ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(b4,a4) != multiply(a4,b4) ) ),
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_20552,plain,
multiply(b4,a4) != multiply(a4,b4),
inference(splitLeft,[status(thm)],[c_20023]) ).
tff(c_20771,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20573,c_20552]) ).
tff(c_20772,plain,
( ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 ) ),
inference(splitRight,[status(thm)],[c_20023]) ).
tff(c_20845,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(splitLeft,[status(thm)],[c_20772]) ).
tff(c_21136,plain,
multiply(a2,multiply(b2,inverse(b2))) != a2,
inference(demodulation,[status(thm),theory(equality)],[c_20801,c_20801,c_20845]) ).
tff(c_21291,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21288,c_21136]) ).
tff(c_21292,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(splitRight,[status(thm)],[c_20772]) ).
tff(c_21595,plain,
multiply(c3,multiply(a3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_21314,c_21292]) ).
tff(c_61136,plain,
multiply(a3,multiply(c3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_55511,c_21595]) ).
tff(c_61139,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21314,c_61136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP090-1 : TPTP v9.0.0. Bugfixed v2.7.0.
% 0.03/0.12 % 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.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 21:17:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 22.07/8.15 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.07/8.16
% 22.07/8.16 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------