%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP442-1 : TPTP v9.0.0. Released v2.6.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 : n032.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:26:14 PM UTC 2025
% Result : Unsatisfiable 283.41s 155.46s
% Output : CNFRefutation 283.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 2
% Syntax : Number of formulae : 81 ( 81 unt; 0 typ; 0 def)
% Number of atoms : 81 ( 80 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 13 ( 3 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 : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 270 ( 270 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > b1 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a1,type,
a1: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b1,type,
b1: $i ).
tff(f_23,axiom,
! [A,B,C,D] : ( inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))) = D ),
file(unknown,unknown) ).
tff(f_25,axiom,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file(unknown,unknown) ).
tff(c_2,plain,
! [A_1,B_2,C_3,D_4] : ( inverse(multiply(A_1,multiply(B_2,multiply(multiply(C_3,inverse(C_3)),inverse(multiply(D_4,multiply(A_1,B_2))))))) = D_4 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_5,plain,
! [A_5,B_6,C_7,D_8] : ( inverse(multiply(A_5,multiply(B_6,multiply(multiply(C_7,inverse(C_7)),inverse(multiply(D_8,multiply(A_5,B_6))))))) = D_8 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_11,plain,
! [B_6,C_7,D_8,C_3,A_5] : ( inverse(multiply(B_6,multiply(multiply(multiply(C_7,inverse(C_7)),inverse(multiply(D_8,multiply(A_5,B_6)))),multiply(multiply(C_3,inverse(C_3)),D_8)))) = A_5 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_26,plain,
! [D_9,C_11,B_10,A_12,C_13] : ( inverse(multiply(B_10,multiply(multiply(multiply(C_11,inverse(C_11)),inverse(multiply(D_9,multiply(A_12,B_10)))),multiply(multiply(C_13,inverse(C_13)),D_9)))) = A_12 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_50,plain,
! [B_6,C_7,D_8,C_11,C_3,A_5,C_13] : ( multiply(multiply(C_7,inverse(C_7)),inverse(multiply(D_8,multiply(A_5,B_6)))) = inverse(multiply(multiply(multiply(C_3,inverse(C_3)),D_8),multiply(multiply(multiply(C_11,inverse(C_11)),A_5),multiply(multiply(C_13,inverse(C_13)),B_6)))) ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_26]) ).
tff(c_224,plain,
! [C_30,C_33,D_27,B_29,A_32,C_31,C_28] : ( multiply(multiply(C_30,inverse(C_30)),inverse(multiply(D_27,multiply(A_32,B_29)))) = inverse(multiply(multiply(multiply(C_33,inverse(C_33)),D_27),multiply(multiply(multiply(C_31,inverse(C_31)),A_32),multiply(multiply(C_28,inverse(C_28)),B_29)))) ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_26]) ).
tff(c_446,plain,
! [D_36,D_39,C_37,A_34,C_38,C_35] : ( multiply(multiply(C_35,inverse(C_35)),inverse(multiply(D_39,multiply(A_34,inverse(multiply(D_36,multiply(multiply(multiply(C_37,inverse(C_37)),D_39),multiply(multiply(C_38,inverse(C_38)),A_34)))))))) = D_36 ),
inference(superposition,[status(thm),theory(equality)],[c_224,c_2]) ).
tff(c_527,plain,
! [B_6,C_7,D_8,C_3,A_5,C_35] : ( multiply(multiply(C_35,inverse(C_35)),inverse(multiply(A_5,multiply(B_6,multiply(multiply(C_7,inverse(C_7)),inverse(multiply(D_8,multiply(A_5,B_6)))))))) = multiply(multiply(C_3,inverse(C_3)),D_8) ),
inference(superposition,[status(thm),theory(equality)],[c_50,c_446]) ).
tff(c_592,plain,
! [C_42,D_41,C_40] : ( multiply(multiply(C_42,inverse(C_42)),D_41) = multiply(multiply(C_40,inverse(C_40)),D_41) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_527]) ).
tff(c_12272,plain,
! [D_130,C_132,A_133,C_129,C_131] : ( inverse(multiply(A_133,multiply(multiply(C_131,inverse(C_131)),multiply(multiply(C_132,inverse(C_132)),inverse(multiply(D_130,multiply(A_133,multiply(C_129,inverse(C_129))))))))) = D_130 ),
inference(superposition,[status(thm),theory(equality)],[c_592,c_2]) ).
tff(c_506,plain,
! [D_36,D_39,C_37,A_34,C_38] : ( inverse(multiply(A_34,multiply(inverse(multiply(D_36,multiply(multiply(multiply(C_37,inverse(C_37)),D_39),multiply(multiply(C_38,inverse(C_38)),A_34)))),D_36))) = D_39 ),
inference(superposition,[status(thm),theory(equality)],[c_446,c_2]) ).
tff(c_14208,plain,
! [D_138,A_139,C_140,C_141] : ( inverse(multiply(inverse(multiply(D_138,multiply(A_139,multiply(C_140,inverse(C_140))))),multiply(D_138,A_139))) = inverse(multiply(C_141,inverse(C_141))) ),
inference(superposition,[status(thm),theory(equality)],[c_12272,c_506]) ).
tff(c_44,plain,
! [D_9,C_11,C_3,B_10,A_12,C_13] : ( inverse(multiply(multiply(multiply(C_11,inverse(C_11)),inverse(multiply(D_9,multiply(A_12,B_10)))),multiply(multiply(multiply(C_13,inverse(C_13)),D_9),multiply(multiply(C_3,inverse(C_3)),A_12)))) = B_10 ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_2]) ).
tff(c_291,plain,
! [C_30,A_32,B_29,B_10] : ( multiply(multiply(C_30,inverse(C_30)),inverse(multiply(inverse(multiply(A_32,multiply(B_29,B_10))),multiply(A_32,B_29)))) = B_10 ),
inference(superposition,[status(thm),theory(equality)],[c_224,c_44]) ).
tff(c_15849,plain,
! [C_144,C_145,C_146] : ( multiply(multiply(C_144,inverse(C_144)),inverse(multiply(C_145,inverse(C_145)))) = multiply(C_146,inverse(C_146)) ),
inference(superposition,[status(thm),theory(equality)],[c_14208,c_291]) ).
tff(c_14566,plain,
! [C_30,C_141,C_140] : ( multiply(multiply(C_30,inverse(C_30)),inverse(multiply(C_141,inverse(C_141)))) = multiply(C_140,inverse(C_140)) ),
inference(superposition,[status(thm),theory(equality)],[c_14208,c_291]) ).
tff(c_16969,plain,
! [C_148,C_147] : ( multiply(C_148,inverse(C_148)) = multiply(C_147,inverse(C_147)) ),
inference(superposition,[status(thm),theory(equality)],[c_15849,c_14566]) ).
tff(c_17890,plain,
! [C_147,B_2,C_3,A_1,D_4] : ( multiply(multiply(A_1,multiply(B_2,multiply(multiply(C_3,inverse(C_3)),inverse(multiply(D_4,multiply(A_1,B_2)))))),D_4) = multiply(C_147,inverse(C_147)) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_16969]) ).
tff(c_15866,plain,
! [C_146,C_140] : ( multiply(C_146,inverse(C_146)) = multiply(C_140,inverse(C_140)) ),
inference(superposition,[status(thm),theory(equality)],[c_15849,c_14566]) ).
tff(c_591,plain,
! [C_35,D_8,C_3] : ( multiply(multiply(C_35,inverse(C_35)),D_8) = multiply(multiply(C_3,inverse(C_3)),D_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_527]) ).
tff(c_1117,plain,
! [C_43,A_44,B_45,B_46] : ( multiply(multiply(C_43,inverse(C_43)),inverse(multiply(inverse(multiply(A_44,multiply(B_45,B_46))),multiply(A_44,B_45)))) = B_46 ),
inference(superposition,[status(thm),theory(equality)],[c_224,c_44]) ).
tff(c_1206,plain,
! [C_3,A_44,B_46,B_45,C_35] : ( multiply(multiply(multiply(C_35,inverse(C_35)),inverse(multiply(C_3,inverse(C_3)))),inverse(multiply(inverse(multiply(A_44,multiply(B_45,B_46))),multiply(A_44,B_45)))) = B_46 ),
inference(superposition,[status(thm),theory(equality)],[c_591,c_1117]) ).
tff(c_17956,plain,
! [C_149,C_150,D_151,C_152] : ( inverse(multiply(C_149,multiply(inverse(C_149),multiply(multiply(C_150,inverse(C_150)),inverse(multiply(D_151,multiply(C_152,inverse(C_152)))))))) = D_151 ),
inference(superposition,[status(thm),theory(equality)],[c_16969,c_2]) ).
tff(c_19782,plain,
! [C_156,B_157,A_158] : ( inverse(multiply(C_156,multiply(inverse(C_156),B_157))) = inverse(multiply(A_158,multiply(inverse(A_158),B_157))) ),
inference(superposition,[status(thm),theory(equality)],[c_1206,c_17956]) ).
tff(c_28566,plain,
! [C_198,C_199,A_200] : ( inverse(multiply(C_198,multiply(C_199,inverse(C_199)))) = inverse(multiply(A_200,multiply(inverse(A_200),inverse(inverse(C_198))))) ),
inference(superposition,[status(thm),theory(equality)],[c_15866,c_19782]) ).
tff(c_29412,plain,
! [C_147,A_200,B_2,C_199,C_3,A_1] : ( inverse(multiply(C_147,inverse(C_147))) = inverse(multiply(A_200,multiply(inverse(A_200),inverse(inverse(multiply(A_1,multiply(B_2,multiply(multiply(C_3,inverse(C_3)),inverse(multiply(multiply(C_199,inverse(C_199)),multiply(A_1,B_2))))))))))) ),
inference(superposition,[status(thm),theory(equality)],[c_17890,c_28566]) ).
tff(c_31584,plain,
! [C_210,A_211,C_212] : ( inverse(multiply(C_210,inverse(C_210))) = inverse(multiply(A_211,multiply(inverse(A_211),inverse(multiply(C_212,inverse(C_212)))))) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29412]) ).
tff(c_43580,plain,
! [A_245,C_246,C_247,C_248] : ( inverse(multiply(inverse(A_245),multiply(inverse(multiply(C_246,inverse(C_246))),multiply(multiply(C_247,inverse(C_247)),inverse(multiply(C_248,inverse(C_248))))))) = A_245 ),
inference(superposition,[status(thm),theory(equality)],[c_31584,c_2]) ).
tff(c_2001,plain,
! [C_51,C_52,D_53,A_55,D_54] : ( multiply(multiply(C_51,inverse(C_51)),inverse(multiply(D_54,multiply(inverse(multiply(D_53,multiply(A_55,multiply(multiply(C_52,inverse(C_52)),D_54)))),D_53)))) = A_55 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_446]) ).
tff(c_2083,plain,
! [D_53,A_55,C_52,D_54] : ( inverse(multiply(inverse(multiply(D_53,multiply(A_55,multiply(multiply(C_52,inverse(C_52)),D_54)))),multiply(D_53,A_55))) = D_54 ),
inference(superposition,[status(thm),theory(equality)],[c_2001,c_2]) ).
tff(c_12435,plain,
! [D_130,A_133,C_131,C_129] : ( inverse(multiply(D_130,multiply(A_133,multiply(C_131,inverse(C_131))))) = inverse(multiply(D_130,multiply(A_133,multiply(C_129,inverse(C_129))))) ),
inference(superposition,[status(thm),theory(equality)],[c_12272,c_2083]) ).
tff(c_45002,plain,
! [A_249,C_250,C_251] : ( inverse(multiply(inverse(A_249),multiply(inverse(multiply(C_250,inverse(C_250))),multiply(C_251,inverse(C_251))))) = A_249 ),
inference(superposition,[status(thm),theory(equality)],[c_43580,c_12435]) ).
tff(c_81969,plain,
! [C_351,C_352,C_353,B_354] : ( multiply(multiply(C_351,inverse(C_351)),multiply(inverse(multiply(C_352,inverse(C_352))),multiply(multiply(C_353,inverse(C_353)),B_354))) = B_354 ),
inference(superposition,[status(thm),theory(equality)],[c_45002,c_291]) ).
tff(c_17654,plain,
! [C_147,C_3,D_4,C_148] : ( inverse(multiply(C_147,multiply(inverse(C_147),multiply(multiply(C_3,inverse(C_3)),inverse(multiply(D_4,multiply(C_148,inverse(C_148)))))))) = D_4 ),
inference(superposition,[status(thm),theory(equality)],[c_16969,c_2]) ).
tff(c_86030,plain,
! [D_366,C_367] : ( inverse(inverse(multiply(D_366,multiply(C_367,inverse(C_367))))) = D_366 ),
inference(superposition,[status(thm),theory(equality)],[c_81969,c_17654]) ).
tff(c_82253,plain,
! [D_4,C_148] : ( inverse(inverse(multiply(D_4,multiply(C_148,inverse(C_148))))) = D_4 ),
inference(superposition,[status(thm),theory(equality)],[c_81969,c_17654]) ).
tff(c_340847,plain,
! [D_755,D_756,C_757] : ( inverse(inverse(multiply(D_755,multiply(inverse(multiply(D_756,multiply(C_757,inverse(C_757)))),D_756)))) = D_755 ),
inference(superposition,[status(thm),theory(equality)],[c_86030,c_82253]) ).
tff(c_29370,plain,
! [C_199,C_3,A_200,C_198] : ( inverse(multiply(C_199,multiply(inverse(C_199),multiply(multiply(C_3,inverse(C_3)),inverse(multiply(A_200,multiply(inverse(A_200),inverse(inverse(C_198))))))))) = C_198 ),
inference(superposition,[status(thm),theory(equality)],[c_28566,c_2]) ).
tff(c_82154,plain,
! [A_200,C_198] : ( inverse(inverse(multiply(A_200,multiply(inverse(A_200),inverse(inverse(C_198)))))) = C_198 ),
inference(superposition,[status(thm),theory(equality)],[c_81969,c_29370]) ).
tff(c_346752,plain,
! [C_762,C_763] : ( multiply(inverse(inverse(C_762)),multiply(C_763,inverse(C_763))) = C_762 ),
inference(superposition,[status(thm),theory(equality)],[c_340847,c_82154]) ).
tff(c_18499,plain,
! [C_149,B_46,A_44] : ( inverse(multiply(C_149,multiply(inverse(C_149),B_46))) = inverse(multiply(A_44,multiply(inverse(A_44),B_46))) ),
inference(superposition,[status(thm),theory(equality)],[c_1206,c_17956]) ).
tff(c_39362,plain,
! [A_229,C_230,C_231,C_232] : ( inverse(multiply(inverse(A_229),multiply(inverse(inverse(C_230)),multiply(multiply(C_231,inverse(C_231)),inverse(multiply(C_230,multiply(C_232,inverse(C_232)))))))) = A_229 ),
inference(superposition,[status(thm),theory(equality)],[c_28566,c_2]) ).
tff(c_40720,plain,
! [A_233,A_234,B_235] : ( inverse(multiply(inverse(A_233),multiply(inverse(inverse(inverse(multiply(A_234,multiply(inverse(A_234),B_235))))),B_235))) = A_233 ),
inference(superposition,[status(thm),theory(equality)],[c_1206,c_39362]) ).
tff(c_41443,plain,
! [A_233,A_234,C_146] : ( inverse(multiply(inverse(A_233),multiply(inverse(inverse(inverse(multiply(A_234,multiply(C_146,inverse(C_146)))))),inverse(inverse(A_234))))) = A_233 ),
inference(superposition,[status(thm),theory(equality)],[c_15866,c_40720]) ).
tff(c_91385,plain,
! [A_375,A_376] : ( inverse(multiply(inverse(A_375),multiply(inverse(A_376),inverse(inverse(A_376))))) = A_375 ),
inference(demodulation,[status(thm),theory(equality)],[c_82253,c_41443]) ).
tff(c_92623,plain,
! [A_44,A_375] : ( inverse(multiply(A_44,multiply(inverse(A_44),inverse(inverse(inverse(A_375)))))) = A_375 ),
inference(superposition,[status(thm),theory(equality)],[c_18499,c_91385]) ).
tff(c_86029,plain,
! [A_233,A_234] : ( inverse(multiply(inverse(A_233),multiply(inverse(A_234),inverse(inverse(A_234))))) = A_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_82253,c_41443]) ).
tff(c_91391,plain,
! [A_233,A_375,A_376] : ( inverse(multiply(inverse(A_233),multiply(A_375,inverse(inverse(multiply(inverse(A_375),multiply(inverse(A_376),inverse(inverse(A_376))))))))) = A_233 ),
inference(superposition,[status(thm),theory(equality)],[c_91385,c_86029]) ).
tff(c_92931,plain,
! [A_233,A_375] : ( inverse(multiply(inverse(A_233),multiply(A_375,inverse(A_375)))) = A_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_82253,c_91391]) ).
tff(c_93028,plain,
! [A_377,A_378] : ( inverse(multiply(inverse(A_377),multiply(A_378,inverse(A_378)))) = A_377 ),
inference(demodulation,[status(thm),theory(equality)],[c_82253,c_91391]) ).
tff(c_141792,plain,
! [C_488,A_489,B_490] : ( multiply(multiply(C_488,inverse(C_488)),multiply(A_489,multiply(inverse(A_489),B_490))) = B_490 ),
inference(superposition,[status(thm),theory(equality)],[c_93028,c_291]) ).
tff(c_47977,plain,
! [C_262,C_263,C_264,A_265] : ( inverse(multiply(inverse(multiply(C_262,inverse(C_262))),multiply(multiply(C_263,inverse(C_263)),multiply(multiply(C_264,inverse(C_264)),A_265)))) = inverse(A_265) ),
inference(superposition,[status(thm),theory(equality)],[c_45002,c_2]) ).
tff(c_49308,plain,
! [D_4,C_262,C_263] : ( inverse(inverse(multiply(D_4,multiply(inverse(multiply(C_262,inverse(C_262))),multiply(C_263,inverse(C_263)))))) = D_4 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_47977]) ).
tff(c_170197,plain,
! [C_532,C_533] : ( multiply(C_532,inverse(C_532)) = inverse(inverse(inverse(inverse(inverse(multiply(C_533,inverse(C_533))))))) ),
inference(superposition,[status(thm),theory(equality)],[c_141792,c_49308]) ).
tff(c_29945,plain,
! [C_147,A_200,C_199] : ( inverse(multiply(C_147,inverse(C_147))) = inverse(multiply(A_200,multiply(inverse(A_200),inverse(multiply(C_199,inverse(C_199)))))) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29412]) ).
tff(c_171338,plain,
! [C_147,A_200,C_533,C_532] : ( inverse(multiply(C_147,inverse(C_147))) = inverse(multiply(A_200,multiply(inverse(A_200),inverse(multiply(inverse(inverse(inverse(inverse(multiply(C_533,inverse(C_533)))))),multiply(C_532,inverse(C_532))))))) ),
inference(superposition,[status(thm),theory(equality)],[c_170197,c_29945]) ).
tff(c_172951,plain,
! [C_534,C_535] : ( multiply(C_534,inverse(C_534)) = inverse(multiply(C_535,inverse(C_535))) ),
inference(demodulation,[status(thm),theory(equality)],[c_92623,c_92931,c_171338]) ).
tff(c_46075,plain,
! [C_250,C_251,C_52,D_54] : ( multiply(inverse(multiply(C_250,inverse(C_250))),multiply(multiply(C_251,inverse(C_251)),multiply(multiply(C_52,inverse(C_52)),D_54))) = D_54 ),
inference(superposition,[status(thm),theory(equality)],[c_2083,c_45002]) ).
tff(c_1020,plain,
! [C_42,C_3,A_1,D_4,C_40] : ( inverse(multiply(A_1,multiply(multiply(C_40,inverse(C_40)),multiply(multiply(C_3,inverse(C_3)),inverse(multiply(D_4,multiply(A_1,multiply(C_42,inverse(C_42))))))))) = D_4 ),
inference(superposition,[status(thm),theory(equality)],[c_592,c_2]) ).
tff(c_82272,plain,
! [C_353,C_3,C_351,C_352,C_40] : ( multiply(C_351,inverse(C_351)) = inverse(multiply(inverse(multiply(C_352,inverse(C_352))),multiply(multiply(C_40,inverse(C_40)),multiply(multiply(C_3,inverse(C_3)),inverse(inverse(multiply(C_353,inverse(C_353)))))))) ),
inference(superposition,[status(thm),theory(equality)],[c_81969,c_1020]) ).
tff(c_83495,plain,
! [C_351,C_353] : ( multiply(C_351,inverse(C_351)) = inverse(inverse(inverse(multiply(C_353,inverse(C_353))))) ),
inference(demodulation,[status(thm),theory(equality)],[c_46075,c_82272]) ).
tff(c_92197,plain,
! [A_375,C_353] : ( inverse(multiply(inverse(A_375),inverse(inverse(inverse(multiply(C_353,inverse(C_353))))))) = A_375 ),
inference(superposition,[status(thm),theory(equality)],[c_83495,c_91385]) ).
tff(c_173161,plain,
! [A_375,C_535,C_534] : ( inverse(multiply(inverse(A_375),inverse(inverse(inverse(multiply(multiply(C_535,inverse(C_535)),multiply(C_534,inverse(C_534)))))))) = A_375 ),
inference(superposition,[status(thm),theory(equality)],[c_172951,c_92197]) ).
tff(c_175716,plain,
! [A_375,C_535] : ( inverse(multiply(inverse(A_375),inverse(multiply(C_535,inverse(C_535))))) = A_375 ),
inference(demodulation,[status(thm),theory(equality)],[c_82253,c_173161]) ).
tff(c_55919,plain,
! [A_286,B_287,C_288,A_289] : ( inverse(multiply(inverse(inverse(inverse(multiply(A_286,multiply(inverse(A_286),B_287))))),multiply(B_287,multiply(multiply(C_288,inverse(C_288)),A_289)))) = inverse(A_289) ),
inference(superposition,[status(thm),theory(equality)],[c_40720,c_2]) ).
tff(c_43835,plain,
! [A_245,C_246,C_129] : ( inverse(multiply(inverse(A_245),multiply(inverse(multiply(C_246,inverse(C_246))),multiply(C_129,inverse(C_129))))) = A_245 ),
inference(superposition,[status(thm),theory(equality)],[c_43580,c_12435]) ).
tff(c_56005,plain,
! [C_288,A_286,C_246] : ( inverse(inverse(multiply(C_288,inverse(C_288)))) = inverse(inverse(multiply(A_286,multiply(inverse(A_286),inverse(multiply(C_246,inverse(C_246))))))) ),
inference(superposition,[status(thm),theory(equality)],[c_55919,c_43835]) ).
tff(c_170938,plain,
! [C_288,A_286,C_533,C_532] : ( inverse(inverse(multiply(C_288,inverse(C_288)))) = inverse(inverse(multiply(A_286,multiply(inverse(A_286),inverse(multiply(inverse(inverse(inverse(inverse(multiply(C_533,inverse(C_533)))))),multiply(C_532,inverse(C_532)))))))) ),
inference(superposition,[status(thm),theory(equality)],[c_170197,c_56005]) ).
tff(c_185596,plain,
! [C_550,C_551] : ( inverse(multiply(C_550,inverse(C_550))) = inverse(inverse(multiply(C_551,inverse(C_551)))) ),
inference(demodulation,[status(thm),theory(equality)],[c_82154,c_92931,c_170938]) ).
tff(c_186923,plain,
! [C_30,C_551,C_550,C_140] : ( multiply(multiply(C_30,inverse(C_30)),inverse(multiply(inverse(multiply(C_551,inverse(C_551))),inverse(multiply(C_550,inverse(C_550)))))) = multiply(C_140,inverse(C_140)) ),
inference(superposition,[status(thm),theory(equality)],[c_185596,c_14566]) ).
tff(c_245089,plain,
! [C_632,C_633,C_634] : ( multiply(multiply(C_632,inverse(C_632)),multiply(C_633,inverse(C_633))) = multiply(C_634,inverse(C_634)) ),
inference(demodulation,[status(thm),theory(equality)],[c_175716,c_186923]) ).
tff(c_94317,plain,
! [D_53,C_52,D_54] : ( multiply(D_53,multiply(inverse(D_53),multiply(multiply(C_52,inverse(C_52)),D_54))) = D_54 ),
inference(superposition,[status(thm),theory(equality)],[c_2083,c_93028]) ).
tff(c_245637,plain,
! [D_53,C_634,C_633] : ( multiply(D_53,multiply(inverse(D_53),multiply(C_634,inverse(C_634)))) = multiply(C_633,inverse(C_633)) ),
inference(superposition,[status(thm),theory(equality)],[c_245089,c_94317]) ).
tff(c_348795,plain,
! [C_764,C_765] : ( multiply(inverse(C_764),C_764) = multiply(C_765,inverse(C_765)) ),
inference(superposition,[status(thm),theory(equality)],[c_346752,c_245637]) ).
tff(c_346821,plain,
! [C_762,C_633] : ( multiply(inverse(C_762),C_762) = multiply(C_633,inverse(C_633)) ),
inference(superposition,[status(thm),theory(equality)],[c_346752,c_245637]) ).
tff(c_362256,plain,
! [C_809,C_808] : ( multiply(inverse(C_809),C_809) = multiply(inverse(C_808),C_808) ),
inference(superposition,[status(thm),theory(equality)],[c_348795,c_346821]) ).
tff(c_4,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_362492,plain,
! [C_808] : ( multiply(inverse(a1),a1) != multiply(inverse(C_808),C_808) ),
inference(superposition,[status(thm),theory(equality)],[c_362256,c_4]) ).
tff(c_363455,plain,
$false,
inference(reflexivity,[status(thm),theory(equality)],[c_362492]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.08 % Problem : GRP442-1 : TPTP v9.0.0. Released v2.6.0.
% 0.05/0.09 % 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.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Mon Apr 7 21:50:01 EDT 2025
% 0.09/0.28 % CPUTime :
% 283.41/155.46 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 283.41/155.47
% 283.41/155.47 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------