%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP065-1 : TPTP v9.0.0. Bugfixed v2.3.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 : n031.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:55 PM UTC 2025
% Result : Unsatisfiable 17.64s 7.72s
% Output : CNFRefutation 17.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 4
% Syntax : Number of formulae : 97 ( 94 unt; 0 typ; 0 def)
% Number of atoms : 102 ( 99 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 19 ( 14 ~; 5 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 8 ( 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 : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 203 ( 203 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > divide > #nlpp > inverse > c3 > b3 > b2 > b1 > 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(b3,type,
b3: $i ).
tff(a2,type,
a2: $i ).
tff(f_30,axiom,
! [X,Z] : ( inverse(X) = divide(divide(Z,Z),X) ),
file(unknown,unknown) ).
tff(f_27,axiom,
! [X,Y,Z] : ( multiply(X,Y) = divide(X,divide(divide(Z,Z),Y)) ),
file(unknown,unknown) ).
tff(f_24,axiom,
! [X,Y,Z] : ( divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) = Y ),
file(unknown,unknown) ).
tff(f_38,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)) ) ),
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_30]) ).
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_27]) ).
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_2,plain,
! [X_1,Y_2,Z_3] : ( divide(divide(divide(X_1,X_1),divide(X_1,divide(Y_2,divide(divide(divide(X_1,X_1),X_1),Z_3)))),Z_3) = Y_2 ),
inference(cnfTransformation,[status(thm)],[f_24]) ).
tff(c_10,plain,
! [X_1,Y_2,Z_3] : ( divide(inverse(divide(X_1,divide(Y_2,divide(inverse(X_1),Z_3)))),Z_3) = Y_2 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_6,c_2]) ).
tff(c_28,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_46,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_28]) ).
tff(c_11,plain,
! [Z_9,X_10] : ( divide(divide(Z_9,Z_9),X_10) = inverse(X_10) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_22,plain,
! [Z_8,X_10] : ( divide(inverse(divide(Z_8,Z_8)),X_10) = inverse(X_10) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_11]) ).
tff(c_108,plain,
! [X_17,Y_18,Z_19] : ( divide(inverse(divide(X_17,divide(Y_18,divide(inverse(X_17),Z_19)))),Z_19) = Y_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_6,c_2]) ).
tff(c_159,plain,
! [Y_18,Z_8,Z_19] : ( divide(inverse(inverse(divide(Y_18,divide(inverse(divide(Z_8,Z_8)),Z_19)))),Z_19) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_108]) ).
tff(c_207,plain,
! [Y_22,Z_23] : ( divide(inverse(inverse(multiply(Y_22,Z_23))),Z_23) = Y_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_22,c_159]) ).
tff(c_56482,plain,
! [Y_418,Z_419] : ( divide(inverse(inverse(inverse(inverse(Y_418)))),Y_418) = divide(Z_419,Z_419) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_207]) ).
tff(c_227,plain,
! [Y_12,Z_8] : ( divide(inverse(inverse(inverse(inverse(Y_12)))),Y_12) = divide(Z_8,Z_8) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_207]) ).
tff(c_56598,plain,
! [Z_421,Z_420] : ( divide(Z_421,Z_421) = divide(Z_420,Z_420) ),
inference(superposition,[status(thm),theory(equality)],[c_56482,c_227]) ).
tff(c_56716,plain,
! [Z_8,Z_421] : ( inverse(divide(Z_8,Z_8)) = divide(Z_421,Z_421) ),
inference(superposition,[status(thm),theory(equality)],[c_56598,c_6]) ).
tff(c_59888,plain,
! [X_452,Y_453,X_454,Z_455] : ( inverse(divide(X_452,divide(Y_453,divide(inverse(X_452),divide(inverse(X_454),Z_455))))) = divide(inverse(divide(X_454,Y_453)),Z_455) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_108]) ).
tff(c_60101,plain,
! [X_452,Z_8,X_454,Z_455] : ( inverse(divide(X_452,inverse(divide(Z_8,Z_8)))) = divide(inverse(divide(X_454,divide(inverse(X_452),divide(inverse(X_454),Z_455)))),Z_455) ),
inference(superposition,[status(thm),theory(equality)],[c_56716,c_59888]) ).
tff(c_60657,plain,
! [X_458,Z_459] : ( inverse(multiply(X_458,divide(Z_459,Z_459))) = inverse(X_458) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_10,c_60101]) ).
tff(c_167,plain,
! [Y_18,Z_19] : ( divide(inverse(inverse(multiply(Y_18,Z_19))),Z_19) = Y_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_22,c_159]) ).
tff(c_60737,plain,
! [X_458,Z_459] : ( divide(inverse(inverse(X_458)),divide(Z_459,Z_459)) = X_458 ),
inference(superposition,[status(thm),theory(equality)],[c_60657,c_167]) ).
tff(c_60854,plain,
! [X_460,Z_461] : ( divide(inverse(inverse(X_460)),divide(Z_461,Z_461)) = X_460 ),
inference(superposition,[status(thm),theory(equality)],[c_60657,c_167]) ).
tff(c_56486,plain,
! [Z_8,Z_419] : ( divide(Z_8,Z_8) = divide(Z_419,Z_419) ),
inference(superposition,[status(thm),theory(equality)],[c_56482,c_227]) ).
tff(c_60115,plain,
! [X_452,Z_8,X_454,Z_455] : ( inverse(divide(X_452,divide(Z_8,Z_8))) = divide(inverse(divide(X_454,divide(inverse(X_452),divide(inverse(X_454),Z_455)))),Z_455) ),
inference(superposition,[status(thm),theory(equality)],[c_56486,c_59888]) ).
tff(c_60296,plain,
! [X_452,Z_8] : ( inverse(divide(X_452,divide(Z_8,Z_8))) = inverse(X_452) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_60115]) ).
tff(c_61074,plain,
! [X_462] : ( inverse(inverse(inverse(X_462))) = inverse(X_462) ),
inference(superposition,[status(thm),theory(equality)],[c_60854,c_60296]) ).
tff(c_61086,plain,
! [X_462,Z_459] : ( divide(inverse(inverse(X_462)),divide(Z_459,Z_459)) = inverse(inverse(X_462)) ),
inference(superposition,[status(thm),theory(equality)],[c_61074,c_60737]) ).
tff(c_61219,plain,
! [X_462] : ( inverse(inverse(X_462)) = X_462 ),
inference(demodulation,[status(thm),theory(equality)],[c_60737,c_61086]) ).
tff(c_168,plain,
! [Y_20,X_21] : ( divide(multiply(inverse(Y_20),Y_20),X_21) = inverse(X_21) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_6]) ).
tff(c_202,plain,
! [Y_20,Y_5] : ( multiply(multiply(inverse(Y_20),Y_20),Y_5) = inverse(inverse(Y_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_168]) ).
tff(c_155,plain,
! [X_17,Z_19,Z_8] : ( divide(inverse(divide(X_17,inverse(divide(inverse(X_17),Z_19)))),Z_19) = divide(Z_8,Z_8) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_108]) ).
tff(c_1285,plain,
! [X_51,Z_52,Z_53] : ( divide(inverse(multiply(X_51,divide(inverse(X_51),Z_52))),Z_52) = divide(Z_53,Z_53) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_155]) ).
tff(c_166,plain,
! [X_17,Z_19,Z_8] : ( divide(inverse(multiply(X_17,divide(inverse(X_17),Z_19))),Z_19) = divide(Z_8,Z_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_155]) ).
tff(c_1428,plain,
! [Z_55,Z_54] : ( divide(Z_55,Z_55) = divide(Z_54,Z_54) ),
inference(superposition,[status(thm),theory(equality)],[c_1285,c_166]) ).
tff(c_1526,plain,
! [Z_8,Z_55] : ( inverse(divide(Z_8,Z_8)) = divide(Z_55,Z_55) ),
inference(superposition,[status(thm),theory(equality)],[c_1428,c_6]) ).
tff(c_4421,plain,
! [X_88,Y_89,X_90,Z_91] : ( inverse(divide(X_88,divide(Y_89,divide(inverse(X_88),divide(inverse(X_90),Z_91))))) = divide(inverse(divide(X_90,Y_89)),Z_91) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_108]) ).
tff(c_4616,plain,
! [X_88,Z_8,X_90,Z_91] : ( inverse(divide(X_88,inverse(divide(Z_8,Z_8)))) = divide(inverse(divide(X_90,divide(inverse(X_88),divide(inverse(X_90),Z_91)))),Z_91) ),
inference(superposition,[status(thm),theory(equality)],[c_1526,c_4421]) ).
tff(c_5116,plain,
! [X_94,Z_95] : ( inverse(multiply(X_94,divide(Z_95,Z_95))) = inverse(X_94) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_10,c_4616]) ).
tff(c_5193,plain,
! [X_94,Z_95] : ( divide(inverse(inverse(X_94)),divide(Z_95,Z_95)) = X_94 ),
inference(superposition,[status(thm),theory(equality)],[c_5116,c_167]) ).
tff(c_1296,plain,
! [Z_8,Z_53] : ( divide(Z_8,Z_8) = divide(Z_53,Z_53) ),
inference(superposition,[status(thm),theory(equality)],[c_1285,c_166]) ).
tff(c_4638,plain,
! [X_88,Z_8,X_90,Z_91] : ( inverse(divide(X_88,divide(Z_8,Z_8))) = divide(inverse(divide(X_90,divide(inverse(X_88),divide(inverse(X_90),Z_91)))),Z_91) ),
inference(superposition,[status(thm),theory(equality)],[c_1296,c_4421]) ).
tff(c_4791,plain,
! [X_88,Z_8] : ( inverse(divide(X_88,divide(Z_8,Z_8))) = inverse(X_88) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_4638]) ).
tff(c_5304,plain,
! [X_96,Z_97] : ( divide(inverse(inverse(X_96)),divide(Z_97,Z_97)) = X_96 ),
inference(superposition,[status(thm),theory(equality)],[c_5116,c_167]) ).
tff(c_5374,plain,
! [X_88,Z_97,Z_8] : ( divide(inverse(inverse(X_88)),divide(Z_97,Z_97)) = divide(X_88,divide(Z_8,Z_8)) ),
inference(superposition,[status(thm),theory(equality)],[c_4791,c_5304]) ).
tff(c_5940,plain,
! [X_102,Z_103] : ( divide(X_102,divide(Z_103,Z_103)) = X_102 ),
inference(demodulation,[status(thm),theory(equality)],[c_5193,c_5374]) ).
tff(c_7762,plain,
! [X_124,Y_125] : ( divide(X_124,multiply(inverse(Y_125),Y_125)) = X_124 ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_5940]) ).
tff(c_151,plain,
! [X_17,Y_18,Y_5] : ( multiply(inverse(divide(X_17,divide(Y_18,divide(inverse(X_17),inverse(Y_5))))),Y_5) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_108]) ).
tff(c_165,plain,
! [X_17,Y_18,Y_5] : ( multiply(inverse(divide(X_17,divide(Y_18,multiply(inverse(X_17),Y_5)))),Y_5) = Y_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_151]) ).
tff(c_9091,plain,
! [Y_134,X_135] : ( multiply(inverse(divide(Y_134,X_135)),Y_134) = X_135 ),
inference(superposition,[status(thm),theory(equality)],[c_7762,c_165]) ).
tff(c_5494,plain,
! [X_98] : ( inverse(inverse(inverse(X_98))) = inverse(X_98) ),
inference(superposition,[status(thm),theory(equality)],[c_5304,c_4791]) ).
tff(c_5506,plain,
! [X_98,Z_95] : ( divide(inverse(inverse(X_98)),divide(Z_95,Z_95)) = inverse(inverse(X_98)) ),
inference(superposition,[status(thm),theory(equality)],[c_5494,c_5193]) ).
tff(c_5645,plain,
! [X_98] : ( inverse(inverse(X_98)) = X_98 ),
inference(demodulation,[status(thm),theory(equality)],[c_5193,c_5506]) ).
tff(c_5669,plain,
! [Y_18,Z_19] : ( divide(multiply(Y_18,Z_19),Z_19) = Y_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_5645,c_167]) ).
tff(c_9116,plain,
! [Y_134,X_135] : ( inverse(divide(Y_134,X_135)) = divide(X_135,Y_134) ),
inference(superposition,[status(thm),theory(equality)],[c_9091,c_5669]) ).
tff(c_231,plain,
! [Y_22,Y_5] : ( multiply(inverse(inverse(multiply(Y_22,inverse(Y_5)))),Y_5) = Y_22 ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_207]) ).
tff(c_7290,plain,
! [Y_118,Y_119] : ( multiply(multiply(Y_118,inverse(Y_119)),Y_119) = Y_118 ),
inference(demodulation,[status(thm),theory(equality)],[c_5645,c_231]) ).
tff(c_7347,plain,
! [Y_118,X_98] : ( multiply(multiply(Y_118,X_98),inverse(X_98)) = Y_118 ),
inference(superposition,[status(thm),theory(equality)],[c_5645,c_7290]) ).
tff(c_5354,plain,
! [Y_18,Z_97] : ( multiply(Y_18,divide(Z_97,Z_97)) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_5304,c_167]) ).
tff(c_5808,plain,
! [Y_100,Z_101] : ( multiply(Y_100,divide(Z_101,Z_101)) = Y_100 ),
inference(superposition,[status(thm),theory(equality)],[c_5304,c_167]) ).
tff(c_147,plain,
! [X_17,Y_18,Y_5] : ( divide(inverse(divide(X_17,divide(Y_18,multiply(inverse(X_17),Y_5)))),inverse(Y_5)) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_108]) ).
tff(c_5823,plain,
! [X_17,Y_18,Z_101] : ( divide(inverse(divide(X_17,divide(Y_18,inverse(X_17)))),inverse(divide(Z_101,Z_101))) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_5808,c_147]) ).
tff(c_6564,plain,
! [X_110,Y_111] : ( inverse(divide(X_110,multiply(Y_111,X_110))) = Y_111 ),
inference(demodulation,[status(thm),theory(equality)],[c_5354,c_9,c_9,c_5823]) ).
tff(c_11141,plain,
! [X_148,Y_149] : ( divide(X_148,multiply(Y_149,X_148)) = inverse(Y_149) ),
inference(superposition,[status(thm),theory(equality)],[c_6564,c_5645]) ).
tff(c_11206,plain,
! [X_98,Y_118] : ( divide(inverse(X_98),Y_118) = inverse(multiply(Y_118,X_98)) ),
inference(superposition,[status(thm),theory(equality)],[c_7347,c_11141]) ).
tff(c_5672,plain,
! [X_99] : ( inverse(inverse(X_99)) = X_99 ),
inference(demodulation,[status(thm),theory(equality)],[c_5193,c_5506]) ).
tff(c_5741,plain,
! [X_4,X_99] : ( multiply(X_4,inverse(X_99)) = divide(X_4,X_99) ),
inference(superposition,[status(thm),theory(equality)],[c_5672,c_9]) ).
tff(c_1900,plain,
! [X_60,Y_61,Y_62] : ( multiply(inverse(divide(X_60,divide(Y_61,multiply(inverse(X_60),Y_62)))),Y_62) = Y_61 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_151]) ).
tff(c_1913,plain,
! [X_60,Y_61,Y_62] : ( inverse(divide(X_60,divide(Y_61,multiply(inverse(X_60),Y_62)))) = divide(inverse(inverse(Y_61)),Y_62) ),
inference(superposition,[status(thm),theory(equality)],[c_1900,c_167]) ).
tff(c_19323,plain,
! [X_218,Y_219,Y_220] : ( inverse(divide(X_218,divide(Y_219,multiply(inverse(X_218),Y_220)))) = divide(Y_219,Y_220) ),
inference(demodulation,[status(thm),theory(equality)],[c_5645,c_1913]) ).
tff(c_19554,plain,
! [X_218,Y_219,X_99] : ( inverse(divide(X_218,divide(Y_219,divide(inverse(X_218),X_99)))) = divide(Y_219,inverse(X_99)) ),
inference(superposition,[status(thm),theory(equality)],[c_5741,c_19323]) ).
tff(c_47449,plain,
! [Y_363,X_364,X_365] : ( divide(multiply(Y_363,multiply(X_364,X_365)),X_365) = multiply(Y_363,X_364) ),
inference(demodulation,[status(thm),theory(equality)],[c_9116,c_9,c_11206,c_9,c_19554]) ).
tff(c_49,plain,
! [Z_13,X_14] : ( divide(inverse(divide(Z_13,Z_13)),X_14) = inverse(X_14) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_11]) ).
tff(c_60,plain,
! [Z_13,Y_5] : ( multiply(inverse(divide(Z_13,Z_13)),Y_5) = inverse(inverse(Y_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_49,c_9]) ).
tff(c_7004,plain,
! [Z_114,Y_115] : ( multiply(inverse(divide(Z_114,Z_114)),Y_115) = Y_115 ),
inference(demodulation,[status(thm),theory(equality)],[c_5645,c_60]) ).
tff(c_7032,plain,
! [Z_114,Y_18,Y_115] : ( divide(inverse(divide(divide(Z_114,Z_114),divide(Y_18,Y_115))),inverse(Y_115)) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_7004,c_147]) ).
tff(c_7152,plain,
! [Y_18,Y_115] : ( multiply(divide(Y_18,Y_115),Y_115) = Y_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_5645,c_9,c_6,c_7032]) ).
tff(c_47609,plain,
! [Y_363,X_364,X_365] : ( multiply(multiply(Y_363,X_364),X_365) = multiply(Y_363,multiply(X_364,X_365)) ),
inference(superposition,[status(thm),theory(equality)],[c_47449,c_7152]) ).
tff(c_349,plain,
! [X_28,Z_29,Z_30] : ( divide(inverse(multiply(X_28,divide(inverse(X_28),Z_29))),Z_29) = divide(Z_30,Z_30) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_155]) ).
tff(c_478,plain,
! [Z_32,Z_31] : ( divide(Z_32,Z_32) = divide(Z_31,Z_31) ),
inference(superposition,[status(thm),theory(equality)],[c_349,c_166]) ).
tff(c_562,plain,
! [Y_5,Z_32] : ( multiply(inverse(Y_5),Y_5) = divide(Z_32,Z_32) ),
inference(superposition,[status(thm),theory(equality)],[c_478,c_9]) ).
tff(c_647,plain,
! [Y_33,Z_34] : ( multiply(inverse(Y_33),Y_33) = divide(Z_34,Z_34) ),
inference(superposition,[status(thm),theory(equality)],[c_478,c_9]) ).
tff(c_8,plain,
( ( 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_38]) ).
tff(c_234,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_1014,plain,
! [Z_40] : ( multiply(inverse(a1),a1) != divide(Z_40,Z_40) ),
inference(superposition,[status(thm),theory(equality)],[c_647,c_234]) ).
tff(c_1020,plain,
! [Z_40,Z_32] : ( divide(Z_40,Z_40) != divide(Z_32,Z_32) ),
inference(superposition,[status(thm),theory(equality)],[c_562,c_1014]) ).
tff(c_360,plain,
! [Z_8,Z_30] : ( divide(Z_8,Z_8) = divide(Z_30,Z_30) ),
inference(superposition,[status(thm),theory(equality)],[c_349,c_166]) ).
tff(c_1052,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1020,c_360]) ).
tff(c_1053,plain,
( ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_1206,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(splitLeft,[status(thm)],[c_1053]) ).
tff(c_56136,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_47609,c_1206]) ).
tff(c_56137,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(splitRight,[status(thm)],[c_1053]) ).
tff(c_56195,plain,
inverse(inverse(a2)) != a2,
inference(demodulation,[status(thm),theory(equality)],[c_202,c_56137]) ).
tff(c_61248,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_61219,c_56195]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP065-1 : TPTP v9.0.0. Bugfixed v2.3.0.
% 0.07/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.12/0.34 % Computer : n031.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 21:14:37 EDT 2025
% 0.12/0.34 % CPUTime :
% 17.64/7.72 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.70/7.72
% 17.70/7.72 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------