%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP431-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 : n008.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:13 PM UTC 2025
% Result : Unsatisfiable 15.62s 5.96s
% Output : CNFRefutation 15.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 2
% Syntax : Number of formulae : 53 ( 53 unt; 0 typ; 0 def)
% Number of atoms : 53 ( 52 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 10 ( 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 : 185 ( 185 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > b2 > a2
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(b2,type,
b2: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(a2,type,
a2: $i ).
tff(f_24,axiom,
! [A,B,C,D] : ( multiply(A,inverse(multiply(B,multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,B))),A)))) = D ),
file(unknown,unknown) ).
tff(f_26,axiom,
multiply(multiply(inverse(b2),b2),a2) != a2,
file(unknown,unknown) ).
tff(c_2,plain,
! [A_1,B_2,C_3,D_4] : ( multiply(A_1,inverse(multiply(B_2,multiply(multiply(multiply(C_3,inverse(C_3)),inverse(multiply(D_4,B_2))),A_1)))) = D_4 ),
inference(cnfTransformation,[status(thm)],[f_24]) ).
tff(c_5,plain,
! [A_5,B_6,C_7,D_8] : ( multiply(A_5,inverse(multiply(B_6,multiply(multiply(multiply(C_7,inverse(C_7)),inverse(multiply(D_8,B_6))),A_5)))) = D_8 ),
inference(cnfTransformation,[status(thm)],[f_24]) ).
tff(c_213,plain,
! [A_25,D_20,C_21,A_22,B_23,C_24] : ( multiply(A_22,inverse(multiply(inverse(multiply(B_23,multiply(multiply(multiply(C_24,inverse(C_24)),inverse(multiply(D_20,B_23))),A_25))),multiply(multiply(multiply(C_21,inverse(C_21)),inverse(D_20)),A_22)))) = A_25 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_5]) ).
tff(c_10601,plain,
! [A_134,C_132,C_136,C_133,A_137,B_138,D_135] : ( multiply(A_137,inverse(multiply(multiply(multiply(multiply(C_132,inverse(C_132)),inverse(D_135)),multiply(C_136,inverse(C_136))),multiply(A_134,A_137)))) = inverse(multiply(B_138,multiply(multiply(multiply(C_133,inverse(C_133)),inverse(multiply(D_135,B_138))),A_134))) ),
inference(superposition,[status(thm),theory(equality)],[c_213,c_2]) ).
tff(c_12,plain,
! [B_6,C_7,D_8,C_3,A_1] : ( multiply(A_1,inverse(multiply(multiply(multiply(multiply(C_7,inverse(C_7)),inverse(multiply(D_8,B_6))),multiply(C_3,inverse(C_3))),multiply(D_8,A_1)))) = B_6 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_11140,plain,
! [B_138,C_133,A_134,B_6] : ( inverse(multiply(B_138,multiply(multiply(multiply(C_133,inverse(C_133)),inverse(multiply(multiply(A_134,B_6),B_138))),A_134))) = B_6 ),
inference(superposition,[status(thm),theory(equality)],[c_10601,c_12]) ).
tff(c_11924,plain,
! [B_139,C_140,A_141,B_142] : ( inverse(multiply(B_139,multiply(multiply(multiply(C_140,inverse(C_140)),inverse(multiply(multiply(A_141,B_142),B_139))),A_141))) = B_142 ),
inference(superposition,[status(thm),theory(equality)],[c_10601,c_12]) ).
tff(c_36,plain,
! [D_9,C_12,C_11,A_13,B_10] : ( multiply(A_13,inverse(multiply(multiply(multiply(multiply(C_11,inverse(C_11)),inverse(multiply(D_9,B_10))),multiply(C_12,inverse(C_12))),multiply(D_9,A_13)))) = B_10 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_87,plain,
! [D_15,B_14,C_19,C_16,A_18,C_17] : ( multiply(multiply(multiply(C_16,inverse(C_16)),inverse(multiply(D_15,B_14))),multiply(C_19,inverse(C_19))) = multiply(A_18,inverse(multiply(multiply(D_15,multiply(C_17,inverse(C_17))),multiply(B_14,A_18)))) ),
inference(superposition,[status(thm),theory(equality)],[c_36,c_2]) ).
tff(c_481,plain,
! [C_33,B_32,A_34,C_31,D_35] : ( multiply(multiply(C_33,inverse(C_33)),inverse(multiply(B_32,multiply(A_34,inverse(multiply(multiply(D_35,multiply(C_31,inverse(C_31))),multiply(B_32,A_34))))))) = D_35 ),
inference(superposition,[status(thm),theory(equality)],[c_87,c_2]) ).
tff(c_579,plain,
! [C_39,D_37,B_38,C_36] : ( multiply(multiply(C_39,inverse(C_39)),inverse(multiply(D_37,B_38))) = multiply(multiply(C_36,inverse(C_36)),inverse(multiply(D_37,B_38))) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_481]) ).
tff(c_996,plain,
! [C_39,B_2,C_3,A_1,D_4,C_36] : ( multiply(multiply(C_39,inverse(C_39)),inverse(D_4)) = multiply(multiply(C_36,inverse(C_36)),inverse(multiply(A_1,inverse(multiply(B_2,multiply(multiply(multiply(C_3,inverse(C_3)),inverse(multiply(D_4,B_2))),A_1)))))) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_579]) ).
tff(c_1028,plain,
! [C_39,D_4,C_36] : ( multiply(multiply(C_39,inverse(C_39)),inverse(D_4)) = multiply(multiply(C_36,inverse(C_36)),inverse(D_4)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_996]) ).
tff(c_12181,plain,
! [C_39,C_140,A_141,B_142,C_36,B_139] : ( multiply(multiply(C_39,inverse(C_39)),B_142) = multiply(multiply(C_36,inverse(C_36)),inverse(multiply(B_139,multiply(multiply(multiply(C_140,inverse(C_140)),inverse(multiply(multiply(A_141,B_142),B_139))),A_141)))) ),
inference(superposition,[status(thm),theory(equality)],[c_11924,c_1028]) ).
tff(c_12674,plain,
! [C_145,B_144,C_143] : ( multiply(multiply(C_145,inverse(C_145)),B_144) = multiply(multiply(C_143,inverse(C_143)),B_144) ),
inference(demodulation,[status(thm),theory(equality)],[c_11140,c_12181]) ).
tff(c_12720,plain,
! [B_144,B_6,C_145] : ( inverse(multiply(inverse(multiply(B_144,B_6)),multiply(multiply(C_145,inverse(C_145)),B_144))) = B_6 ),
inference(superposition,[status(thm),theory(equality)],[c_12674,c_11140]) ).
tff(c_3339,plain,
! [C_75,C_74,C_76,B_72,C_77,A_73,D_71] : ( multiply(D_71,multiply(C_75,inverse(C_75))) = multiply(A_73,inverse(multiply(multiply(B_72,multiply(C_77,inverse(C_77))),multiply(multiply(multiply(multiply(C_74,inverse(C_74)),inverse(multiply(D_71,B_72))),multiply(C_76,inverse(C_76))),A_73)))) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_36]) ).
tff(c_67,plain,
! [B_6,C_7,D_8,C_12,C_11,C_3,A_13] : ( multiply(D_8,multiply(C_11,inverse(C_11))) = multiply(A_13,inverse(multiply(multiply(B_6,multiply(C_12,inverse(C_12))),multiply(multiply(multiply(multiply(C_7,inverse(C_7)),inverse(multiply(D_8,B_6))),multiply(C_3,inverse(C_3))),A_13)))) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_36]) ).
tff(c_3900,plain,
! [D_78,C_80,C_79] : ( multiply(D_78,multiply(C_80,inverse(C_80))) = multiply(D_78,multiply(C_79,inverse(C_79))) ),
inference(superposition,[status(thm),theory(equality)],[c_3339,c_67]) ).
tff(c_4280,plain,
! [D_78,C_36,C_39,C_80] : ( multiply(D_78,multiply(multiply(C_36,inverse(C_36)),inverse(multiply(C_39,inverse(C_39))))) = multiply(D_78,multiply(C_80,inverse(C_80))) ),
inference(superposition,[status(thm),theory(equality)],[c_1028,c_3900]) ).
tff(c_17074,plain,
! [C_154,B_155,C_156] : ( inverse(multiply(inverse(multiply(inverse(multiply(C_154,inverse(C_154))),B_155)),multiply(C_156,inverse(C_156)))) = B_155 ),
inference(superposition,[status(thm),theory(equality)],[c_4280,c_11924]) ).
tff(c_17762,plain,
! [C_157,B_158,C_159] : ( multiply(multiply(C_157,inverse(C_157)),B_158) = inverse(multiply(inverse(B_158),multiply(C_159,inverse(C_159)))) ),
inference(superposition,[status(thm),theory(equality)],[c_12720,c_17074]) ).
tff(c_12311,plain,
! [C_39,B_142,C_80] : ( inverse(multiply(inverse(multiply(inverse(multiply(C_39,inverse(C_39))),B_142)),multiply(C_80,inverse(C_80)))) = B_142 ),
inference(superposition,[status(thm),theory(equality)],[c_4280,c_11924]) ).
tff(c_17799,plain,
! [C_157,C_39,B_142] : ( multiply(multiply(C_157,inverse(C_157)),multiply(inverse(multiply(C_39,inverse(C_39))),B_142)) = B_142 ),
inference(superposition,[status(thm),theory(equality)],[c_17762,c_12311]) ).
tff(c_22,plain,
! [C_7,B_2,C_3,A_1,D_4,A_5] : ( multiply(A_5,inverse(multiply(inverse(multiply(B_2,multiply(multiply(multiply(C_3,inverse(C_3)),inverse(multiply(D_4,B_2))),A_1))),multiply(multiply(multiply(C_7,inverse(C_7)),inverse(D_4)),A_5)))) = A_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_5]) ).
tff(c_1030,plain,
! [D_40,B_41,C_42,C_43] : ( multiply(inverse(multiply(D_40,B_41)),inverse(multiply(inverse(C_42),multiply(multiply(C_43,inverse(C_43)),inverse(multiply(D_40,B_41)))))) = C_42 ),
inference(superposition,[status(thm),theory(equality)],[c_579,c_2]) ).
tff(c_1148,plain,
! [B_2,C_3,C_7,A_1] : ( multiply(B_2,multiply(multiply(multiply(C_3,inverse(C_3)),inverse(multiply(multiply(C_7,inverse(C_7)),B_2))),A_1)) = A_1 ),
inference(superposition,[status(thm),theory(equality)],[c_22,c_1030]) ).
tff(c_19157,plain,
! [C_160,C_161,B_162] : ( multiply(multiply(C_160,inverse(C_160)),multiply(inverse(multiply(C_161,inverse(C_161))),B_162)) = B_162 ),
inference(superposition,[status(thm),theory(equality)],[c_17762,c_12311]) ).
tff(c_20681,plain,
! [C_166,B_167,B_168] : ( inverse(multiply(inverse(multiply(multiply(inverse(multiply(C_166,inverse(C_166))),B_167),B_168)),B_167)) = B_168 ),
inference(superposition,[status(thm),theory(equality)],[c_19157,c_12720]) ).
tff(c_21371,plain,
! [C_7,C_3,A_1,C_166,B_167] : ( multiply(multiply(multiply(C_3,inverse(C_3)),inverse(multiply(multiply(C_7,inverse(C_7)),multiply(inverse(multiply(C_166,inverse(C_166))),B_167)))),A_1) = inverse(multiply(inverse(A_1),B_167)) ),
inference(superposition,[status(thm),theory(equality)],[c_1148,c_20681]) ).
tff(c_21446,plain,
! [C_3,B_167,A_1] : ( multiply(multiply(multiply(C_3,inverse(C_3)),inverse(B_167)),A_1) = inverse(multiply(inverse(A_1),B_167)) ),
inference(demodulation,[status(thm),theory(equality)],[c_17799,c_21371]) ).
tff(c_22876,plain,
! [A_1,B_2,D_4] : ( multiply(A_1,inverse(multiply(B_2,inverse(multiply(inverse(A_1),multiply(D_4,B_2)))))) = D_4 ),
inference(demodulation,[status(thm),theory(equality)],[c_21446,c_2]) ).
tff(c_23516,plain,
! [A_180,B_181,D_182] : ( multiply(A_180,inverse(multiply(B_181,inverse(multiply(inverse(A_180),multiply(D_182,B_181)))))) = D_182 ),
inference(demodulation,[status(thm),theory(equality)],[c_21446,c_2]) ).
tff(c_4201,plain,
! [C_3,D_4,D_78,C_80] : ( multiply(inverse(multiply(multiply(C_3,inverse(C_3)),inverse(multiply(D_4,D_78)))),inverse(multiply(D_78,multiply(C_80,inverse(C_80))))) = D_4 ),
inference(superposition,[status(thm),theory(equality)],[c_3900,c_2]) ).
tff(c_23588,plain,
! [D_182,C_3,B_181,C_80] : ( multiply(inverse(D_182),inverse(multiply(inverse(multiply(inverse(multiply(C_3,inverse(C_3))),multiply(D_182,B_181))),multiply(C_80,inverse(C_80))))) = B_181 ),
inference(superposition,[status(thm),theory(equality)],[c_23516,c_4201]) ).
tff(c_23856,plain,
! [D_183,B_184] : ( multiply(inverse(D_183),multiply(D_183,B_184)) = B_184 ),
inference(demodulation,[status(thm),theory(equality)],[c_12311,c_23588]) ).
tff(c_23845,plain,
! [D_182,B_181] : ( multiply(inverse(D_182),multiply(D_182,B_181)) = B_181 ),
inference(demodulation,[status(thm),theory(equality)],[c_12311,c_23588]) ).
tff(c_24160,plain,
! [D_185,B_186] : ( multiply(inverse(inverse(D_185)),B_186) = multiply(D_185,B_186) ),
inference(superposition,[status(thm),theory(equality)],[c_23856,c_23845]) ).
tff(c_24173,plain,
! [A_1,B_186,D_185] : ( multiply(A_1,inverse(multiply(B_186,inverse(multiply(inverse(A_1),multiply(D_185,B_186)))))) = inverse(inverse(D_185)) ),
inference(superposition,[status(thm),theory(equality)],[c_24160,c_22876]) ).
tff(c_24592,plain,
! [D_185] : ( inverse(inverse(D_185)) = D_185 ),
inference(demodulation,[status(thm),theory(equality)],[c_22876,c_24173]) ).
tff(c_1985,plain,
! [B_56,C_57,C_58,A_59] : ( multiply(B_56,multiply(multiply(multiply(C_57,inverse(C_57)),inverse(multiply(multiply(C_58,inverse(C_58)),B_56))),A_59)) = A_59 ),
inference(superposition,[status(thm),theory(equality)],[c_22,c_1030]) ).
tff(c_2094,plain,
! [C_58,A_59] : ( multiply(C_58,inverse(C_58)) = multiply(A_59,inverse(A_59)) ),
inference(superposition,[status(thm),theory(equality)],[c_1985,c_2]) ).
tff(c_25632,plain,
! [D_194,B_195] : ( multiply(D_194,multiply(inverse(D_194),B_195)) = B_195 ),
inference(superposition,[status(thm),theory(equality)],[c_23845,c_24160]) ).
tff(c_25977,plain,
! [D_194,C_58] : ( multiply(D_194,multiply(C_58,inverse(C_58))) = inverse(inverse(D_194)) ),
inference(superposition,[status(thm),theory(equality)],[c_2094,c_25632]) ).
tff(c_26049,plain,
! [D_194,C_58] : ( multiply(D_194,multiply(C_58,inverse(C_58))) = D_194 ),
inference(demodulation,[status(thm),theory(equality)],[c_24592,c_25977]) ).
tff(c_17457,plain,
! [C_145,B_144,C_156] : ( multiply(multiply(C_145,inverse(C_145)),B_144) = inverse(multiply(inverse(B_144),multiply(C_156,inverse(C_156)))) ),
inference(superposition,[status(thm),theory(equality)],[c_12720,c_17074]) ).
tff(c_26495,plain,
! [C_145,B_144] : ( multiply(multiply(C_145,inverse(C_145)),B_144) = inverse(inverse(B_144)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26049,c_17457]) ).
tff(c_27283,plain,
! [C_206,B_207] : ( multiply(multiply(C_206,inverse(C_206)),B_207) = B_207 ),
inference(demodulation,[status(thm),theory(equality)],[c_24592,c_26495]) ).
tff(c_27461,plain,
! [D_185,B_207] : ( multiply(multiply(inverse(D_185),D_185),B_207) = B_207 ),
inference(superposition,[status(thm),theory(equality)],[c_24592,c_27283]) ).
tff(c_4,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_27938,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_27461,c_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP431-1 : TPTP v9.0.0. Released v2.6.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.13/0.34 % Computer : n008.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 21:49:32 EDT 2025
% 0.13/0.34 % CPUTime :
% 15.62/5.96 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.62/5.97
% 15.62/5.97 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------