%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP413-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 : n029.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:10 PM UTC 2025
% Result : Unsatisfiable 201.38s 80.09s
% Output : CNFRefutation 201.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% 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 : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 17 ( 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 : 170 ( 170 !; 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] : ( multiply(A,inverse(multiply(multiply(multiply(inverse(B),B),inverse(multiply(inverse(multiply(A,inverse(B))),C))),B))) = C ),
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] : ( multiply(A_1,inverse(multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(multiply(A_1,inverse(B_2))),C_3))),B_2))) = C_3 ),
inference(cnfTransformation,[status(thm)],[f_24]) ).
tff(c_5,plain,
! [A_4,B_5,C_6] : ( multiply(A_4,inverse(multiply(multiply(multiply(inverse(B_5),B_5),inverse(multiply(inverse(multiply(A_4,inverse(B_5))),C_6))),B_5))) = C_6 ),
inference(cnfTransformation,[status(thm)],[f_24]) ).
tff(c_28,plain,
! [A_7,B_8,C_9,B_10] : ( multiply(A_7,inverse(multiply(multiply(multiply(inverse(B_8),B_8),inverse(C_9)),B_8))) = inverse(multiply(multiply(multiply(inverse(B_10),B_10),inverse(multiply(inverse(multiply(inverse(multiply(A_7,inverse(B_8))),inverse(B_10))),C_9))),B_10)) ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_185,plain,
! [B_10,A_1,B_2,C_3] : ( inverse(multiply(multiply(multiply(inverse(B_10),B_10),inverse(multiply(inverse(multiply(inverse(multiply(A_1,inverse(B_2))),inverse(B_10))),multiply(inverse(multiply(A_1,inverse(B_2))),C_3)))),B_10)) = C_3 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_28]) ).
tff(c_264,plain,
! [B_14,A_15,B_16,C_17] : ( inverse(multiply(multiply(multiply(inverse(B_14),B_14),inverse(multiply(inverse(multiply(inverse(multiply(A_15,inverse(B_16))),inverse(B_14))),multiply(inverse(multiply(A_15,inverse(B_16))),C_17)))),B_14)) = C_17 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_28]) ).
tff(c_274,plain,
! [B_16,A_15,B_2,C_3,B_10,C_17] : ( inverse(multiply(multiply(multiply(inverse(B_10),B_10),inverse(multiply(inverse(multiply(C_17,inverse(B_10))),multiply(inverse(multiply(multiply(multiply(inverse(inverse(B_2)),inverse(B_2)),inverse(multiply(inverse(multiply(inverse(multiply(A_15,inverse(B_16))),inverse(inverse(B_2)))),multiply(inverse(multiply(A_15,inverse(B_16))),C_17)))),inverse(B_2))),C_3)))),B_10)) = C_3 ),
inference(superposition,[status(thm),theory(equality)],[c_264,c_185]) ).
tff(c_434,plain,
! [B_10,C_17,C_3] : ( inverse(multiply(multiply(multiply(inverse(B_10),B_10),inverse(multiply(inverse(multiply(C_17,inverse(B_10))),multiply(C_17,C_3)))),B_10)) = C_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_185,c_274]) ).
tff(c_461,plain,
! [B_18,C_19,C_20] : ( inverse(multiply(multiply(multiply(inverse(B_18),B_18),inverse(multiply(inverse(multiply(C_19,inverse(B_18))),multiply(C_19,C_20)))),B_18)) = C_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_185,c_274]) ).
tff(c_100,plain,
! [A_7,B_8,C_9] : ( multiply(inverse(multiply(A_7,inverse(B_8))),multiply(A_7,inverse(multiply(multiply(multiply(inverse(B_8),B_8),inverse(C_9)),B_8)))) = C_9 ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_2]) ).
tff(c_601,plain,
! [C_21,B_22,C_23,A_24] : ( multiply(inverse(multiply(C_21,inverse(B_22))),multiply(C_21,C_23)) = multiply(inverse(multiply(A_24,inverse(B_22))),multiply(A_24,C_23)) ),
inference(superposition,[status(thm),theory(equality)],[c_461,c_100]) ).
tff(c_726,plain,
! [A_24,C_23,C_3,B_10,C_21,C_17] : ( multiply(inverse(multiply(C_21,C_3)),multiply(C_21,C_23)) = multiply(inverse(multiply(A_24,inverse(multiply(multiply(multiply(inverse(B_10),B_10),inverse(multiply(inverse(multiply(C_17,inverse(B_10))),multiply(C_17,C_3)))),B_10)))),multiply(A_24,C_23)) ),
inference(superposition,[status(thm),theory(equality)],[c_434,c_601]) ).
tff(c_800,plain,
! [C_25,C_26,C_27,A_28] : ( multiply(inverse(multiply(C_25,C_26)),multiply(C_25,C_27)) = multiply(inverse(multiply(A_28,C_26)),multiply(A_28,C_27)) ),
inference(demodulation,[status(thm),theory(equality)],[c_434,c_726]) ).
tff(c_870,plain,
! [A_7,C_25,A_28,C_27,C_9] : ( multiply(inverse(multiply(A_7,inverse(multiply(C_25,C_27)))),multiply(A_7,inverse(multiply(multiply(multiply(inverse(multiply(A_28,C_27)),multiply(A_28,C_27)),inverse(C_9)),multiply(C_25,C_27))))) = C_9 ),
inference(superposition,[status(thm),theory(equality)],[c_800,c_100]) ).
tff(c_956,plain,
! [C_3,B_10,C_25,C_27,C_17] : ( multiply(inverse(multiply(C_25,B_10)),multiply(C_25,C_27)) = multiply(C_3,multiply(multiply(multiply(inverse(B_10),B_10),inverse(multiply(inverse(multiply(C_17,inverse(B_10))),multiply(C_17,C_3)))),C_27)) ),
inference(superposition,[status(thm),theory(equality)],[c_434,c_800]) ).
tff(c_7930,plain,
! [C_95,A_92,B_94,B_93,B_91] : ( inverse(multiply(multiply(multiply(inverse(B_93),B_93),inverse(multiply(inverse(multiply(inverse(multiply(A_92,inverse(B_91))),inverse(B_93))),multiply(multiply(multiply(inverse(B_94),B_94),inverse(multiply(inverse(multiply(multiply(inverse(B_91),B_91),inverse(B_94))),C_95))),B_94)))),B_93)) = multiply(A_92,inverse(multiply(C_95,B_91))) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_28]) ).
tff(c_8246,plain,
! [A_92,B_93,B_91,C_25,C_27] : ( multiply(A_92,inverse(multiply(multiply(multiply(inverse(B_91),B_91),inverse(multiply(inverse(multiply(A_92,inverse(B_91))),inverse(B_93)))),B_91))) = inverse(multiply(multiply(multiply(inverse(B_93),B_93),inverse(multiply(inverse(multiply(C_25,C_27)),multiply(C_25,C_27)))),B_93)) ),
inference(superposition,[status(thm),theory(equality)],[c_956,c_7930]) ).
tff(c_8661,plain,
! [B_96,C_97,C_98] : ( inverse(multiply(multiply(multiply(inverse(B_96),B_96),inverse(multiply(inverse(multiply(C_97,C_98)),multiply(C_97,C_98)))),B_96)) = inverse(B_96) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8246]) ).
tff(c_9018,plain,
! [A_7,B_96,C_25,A_28,C_27,C_9] : ( inverse(multiply(multiply(multiply(inverse(B_96),B_96),inverse(multiply(inverse(C_9),multiply(inverse(multiply(A_7,inverse(multiply(C_25,C_27)))),multiply(A_7,inverse(multiply(multiply(multiply(inverse(multiply(A_28,C_27)),multiply(A_28,C_27)),inverse(C_9)),multiply(C_25,C_27)))))))),B_96)) = inverse(B_96) ),
inference(superposition,[status(thm),theory(equality)],[c_870,c_8661]) ).
tff(c_9313,plain,
! [B_99,C_100] : ( inverse(multiply(multiply(multiply(inverse(B_99),B_99),inverse(multiply(inverse(C_100),C_100))),B_99)) = inverse(B_99) ),
inference(demodulation,[status(thm),theory(equality)],[c_870,c_9018]) ).
tff(c_11236,plain,
! [A_108,B_109,C_110] : ( multiply(inverse(multiply(A_108,inverse(B_109))),multiply(A_108,inverse(B_109))) = multiply(inverse(C_110),C_110) ),
inference(superposition,[status(thm),theory(equality)],[c_9313,c_100]) ).
tff(c_9568,plain,
! [A_7,B_99,C_100] : ( multiply(inverse(multiply(A_7,inverse(B_99))),multiply(A_7,inverse(B_99))) = multiply(inverse(C_100),C_100) ),
inference(superposition,[status(thm),theory(equality)],[c_9313,c_100]) ).
tff(c_12040,plain,
! [C_112,C_111] : ( multiply(inverse(C_112),C_112) = multiply(inverse(C_111),C_111) ),
inference(superposition,[status(thm),theory(equality)],[c_11236,c_9568]) ).
tff(c_12636,plain,
! [B_2,C_111,C_3] : ( multiply(inverse(inverse(B_2)),inverse(multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(multiply(inverse(C_111),C_111)),C_3))),B_2))) = C_3 ),
inference(superposition,[status(thm),theory(equality)],[c_12040,c_2]) ).
tff(c_11250,plain,
! [C_110,C_100] : ( multiply(inverse(C_110),C_110) = multiply(inverse(C_100),C_100) ),
inference(superposition,[status(thm),theory(equality)],[c_11236,c_9568]) ).
tff(c_9394,plain,
! [A_7,B_99,C_25,A_28,C_27,C_100] : ( multiply(multiply(multiply(inverse(B_99),B_99),inverse(multiply(inverse(C_100),C_100))),B_99) = multiply(inverse(multiply(A_7,inverse(multiply(C_25,C_27)))),multiply(A_7,inverse(multiply(multiply(multiply(inverse(multiply(A_28,C_27)),multiply(A_28,C_27)),inverse(B_99)),multiply(C_25,C_27))))) ),
inference(superposition,[status(thm),theory(equality)],[c_9313,c_870]) ).
tff(c_9786,plain,
! [B_99,C_100] : ( multiply(multiply(multiply(inverse(B_99),B_99),inverse(multiply(inverse(C_100),C_100))),B_99) = B_99 ),
inference(demodulation,[status(thm),theory(equality)],[c_870,c_9394]) ).
tff(c_14583,plain,
! [C_124,C_125,C_126] : ( multiply(multiply(multiply(inverse(C_124),C_124),inverse(multiply(inverse(C_125),C_125))),C_126) = C_126 ),
inference(superposition,[status(thm),theory(equality)],[c_12040,c_9786]) ).
tff(c_15074,plain,
! [C_127,C_128,C_129] : ( multiply(inverse(multiply(C_127,C_128)),multiply(C_127,C_129)) = multiply(inverse(C_128),C_129) ),
inference(superposition,[status(thm),theory(equality)],[c_14583,c_956]) ).
tff(c_16681,plain,
! [C_138,C_139,C_140] : ( multiply(inverse(multiply(inverse(C_138),C_138)),multiply(inverse(C_139),C_140)) = multiply(inverse(C_139),C_140) ),
inference(superposition,[status(thm),theory(equality)],[c_11250,c_15074]) ).
tff(c_16883,plain,
! [C_138,C_3,B_2,C_111] : ( multiply(inverse(multiply(inverse(C_138),C_138)),C_3) = multiply(inverse(inverse(B_2)),inverse(multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(multiply(inverse(C_111),C_111)),C_3))),B_2))) ),
inference(superposition,[status(thm),theory(equality)],[c_12636,c_16681]) ).
tff(c_17046,plain,
! [C_138,C_3] : ( multiply(inverse(multiply(inverse(C_138),C_138)),C_3) = C_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_12636,c_16883]) ).
tff(c_14670,plain,
! [C_25,C_124,C_126] : ( multiply(inverse(multiply(C_25,C_124)),multiply(C_25,C_126)) = multiply(inverse(C_124),C_126) ),
inference(superposition,[status(thm),theory(equality)],[c_14583,c_956]) ).
tff(c_8201,plain,
! [B_94,B_91,C_95,A_92] : ( multiply(multiply(multiply(inverse(B_94),B_94),inverse(multiply(inverse(multiply(multiply(inverse(B_91),B_91),inverse(B_94))),C_95))),B_94) = multiply(inverse(multiply(A_92,inverse(B_91))),multiply(A_92,inverse(multiply(C_95,B_91)))) ),
inference(superposition,[status(thm),theory(equality)],[c_7930,c_2]) ).
tff(c_35063,plain,
! [B_213,B_214,C_215] : ( multiply(multiply(multiply(inverse(B_213),B_213),inverse(multiply(inverse(multiply(multiply(inverse(B_214),B_214),inverse(B_213))),C_215))),B_213) = multiply(inverse(inverse(B_214)),inverse(multiply(C_215,B_214))) ),
inference(demodulation,[status(thm),theory(equality)],[c_14670,c_8201]) ).
tff(c_12632,plain,
! [A_1,C_111,C_112,C_3] : ( multiply(A_1,inverse(multiply(multiply(multiply(inverse(C_111),C_111),inverse(multiply(inverse(multiply(A_1,inverse(C_112))),C_3))),C_112))) = C_3 ),
inference(superposition,[status(thm),theory(equality)],[c_12040,c_2]) ).
tff(c_35715,plain,
! [B_216,C_217] : ( multiply(multiply(inverse(B_216),B_216),inverse(multiply(inverse(inverse(B_216)),inverse(multiply(C_217,B_216))))) = C_217 ),
inference(superposition,[status(thm),theory(equality)],[c_35063,c_12632]) ).
tff(c_96953,plain,
! [C_347,C_348] : ( multiply(multiply(inverse(C_347),C_347),inverse(multiply(inverse(inverse(C_347)),inverse(multiply(inverse(C_348),C_348))))) = inverse(C_347) ),
inference(superposition,[status(thm),theory(equality)],[c_11250,c_35715]) ).
tff(c_97663,plain,
! [C_348,C_100] : ( multiply(multiply(inverse(multiply(inverse(C_348),C_348)),multiply(inverse(C_348),C_348)),inverse(multiply(inverse(C_100),C_100))) = inverse(multiply(inverse(C_348),C_348)) ),
inference(superposition,[status(thm),theory(equality)],[c_11250,c_96953]) ).
tff(c_97803,plain,
! [C_348,C_100] : ( multiply(multiply(inverse(C_348),C_348),inverse(multiply(inverse(C_100),C_100))) = inverse(multiply(inverse(C_348),C_348)) ),
inference(demodulation,[status(thm),theory(equality)],[c_14670,c_97663]) ).
tff(c_5323,plain,
! [C_75,C_74,C_72,C_71,A_73] : ( inverse(multiply(multiply(multiply(inverse(multiply(C_71,C_74)),multiply(C_71,C_74)),inverse(multiply(inverse(multiply(C_72,inverse(multiply(A_73,C_74)))),multiply(C_72,C_75)))),multiply(A_73,C_74))) = C_75 ),
inference(superposition,[status(thm),theory(equality)],[c_800,c_434]) ).
tff(c_5858,plain,
! [C_75,B_2,C_3,A_1,C_71] : ( inverse(multiply(multiply(multiply(inverse(multiply(C_71,B_2)),multiply(C_71,B_2)),inverse(multiply(inverse(C_3),multiply(A_1,C_75)))),multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(multiply(A_1,inverse(B_2))),C_3))),B_2))) = C_75 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_5323]) ).
tff(c_66781,plain,
! [B_2,C_3,A_1,C_75] : ( inverse(multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(C_3),multiply(A_1,C_75)))),multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(multiply(A_1,inverse(B_2))),C_3))),B_2))) = C_75 ),
inference(demodulation,[status(thm),theory(equality)],[c_14670,c_5858]) ).
tff(c_97363,plain,
! [C_75,B_2,C_3,A_1,C_348] : ( multiply(multiply(inverse(multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(C_3),multiply(A_1,C_75)))),multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(multiply(A_1,inverse(B_2))),C_3))),B_2))),multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(C_3),multiply(A_1,C_75)))),multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(multiply(A_1,inverse(B_2))),C_3))),B_2))),inverse(multiply(inverse(C_75),inverse(multiply(inverse(C_348),C_348))))) = inverse(multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(C_3),multiply(A_1,C_75)))),multiply(multiply(multiply(inverse(B_2),B_2),inverse(multiply(inverse(multiply(A_1,inverse(B_2))),C_3))),B_2))) ),
inference(superposition,[status(thm),theory(equality)],[c_66781,c_96953]) ).
tff(c_108325,plain,
! [B_359,C_360,C_361] : ( multiply(multiply(inverse(B_359),B_359),inverse(multiply(inverse(C_360),inverse(multiply(inverse(C_361),C_361))))) = C_360 ),
inference(demodulation,[status(thm),theory(equality)],[c_66781,c_14670,c_14670,c_97363]) ).
tff(c_112520,plain,
! [A_365,C_366,C_367] : ( multiply(A_365,inverse(multiply(multiply(A_365,inverse(C_366)),C_366))) = inverse(multiply(inverse(C_367),C_367)) ),
inference(superposition,[status(thm),theory(equality)],[c_108325,c_12632]) ).
tff(c_114501,plain,
! [C_100,C_367] : ( multiply(inverse(inverse(inverse(multiply(inverse(C_100),C_100)))),inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(C_100),C_100)))),inverse(inverse(multiply(inverse(C_100),C_100))))))) = inverse(multiply(inverse(C_367),C_367)) ),
inference(superposition,[status(thm),theory(equality)],[c_97803,c_112520]) ).
tff(c_115328,plain,
! [C_368,C_369] : ( multiply(inverse(C_368),C_368) = inverse(multiply(inverse(C_369),C_369)) ),
inference(demodulation,[status(thm),theory(equality)],[c_11250,c_11250,c_114501]) ).
tff(c_4,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_12642,plain,
! [C_112] : ( multiply(multiply(inverse(C_112),C_112),a2) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_12040,c_4]) ).
tff(c_117346,plain,
! [C_369] : ( multiply(inverse(multiply(inverse(C_369),C_369)),a2) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_115328,c_12642]) ).
tff(c_118247,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_17046,c_117346]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP413-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 : n029.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:48:19 EDT 2025
% 0.13/0.34 % CPUTime :
% 201.38/80.09 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 201.38/80.10
% 201.38/80.10 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------