%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP002-3 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n023.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:42 PM UTC 2025
% Result : Unsatisfiable 12.63s 4.94s
% Output : CNFRefutation 12.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 6
% Syntax : Number of formulae : 72 ( 72 unt; 0 typ; 0 def)
% Number of atoms : 72 ( 71 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 7 ( 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 : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 133 ( 133 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > commutator > #nlpp > inverse > identity > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(commutator,type,
commutator: ( $i * $i ) > $i ).
tff(b,type,
b: $i ).
tff(identity,type,
identity: $i ).
tff(f_64,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_68,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_71,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_78,axiom,
! [X] : ( multiply(X,multiply(X,X)) = identity ),
file(unknown,unknown) ).
tff(f_76,axiom,
! [X,Y] : ( commutator(X,Y) = multiply(X,multiply(Y,multiply(inverse(X),inverse(Y)))) ),
file(unknown,unknown) ).
tff(f_80,axiom,
commutator(commutator(a,b),b) != identity,
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_51,plain,
! [X_12,Y_13,Z_14] : ( multiply(multiply(X_12,Y_13),Z_14) = multiply(X_12,multiply(Y_13,Z_14)) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_81,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_51]) ).
tff(c_92,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81]) ).
tff(c_10,plain,
! [X_8] : ( multiply(X_8,multiply(X_8,X_8)) = identity ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_74,plain,
! [X_8,Z_14] : ( multiply(X_8,multiply(multiply(X_8,X_8),Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_51]) ).
tff(c_379,plain,
! [X_23,Z_24] : ( multiply(X_23,multiply(X_23,multiply(X_23,Z_24))) = Z_24 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_2,c_74]) ).
tff(c_471,plain,
! [X_25] : ( multiply(X_25,identity) = X_25 ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_379]) ).
tff(c_135,plain,
! [X_17,Z_18] : ( multiply(inverse(X_17),multiply(X_17,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81]) ).
tff(c_174,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_135]) ).
tff(c_480,plain,
! [X_2] : ( inverse(inverse(X_2)) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_471,c_174]) ).
tff(c_441,plain,
! [X_8] : ( multiply(X_8,identity) = X_8 ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_379]) ).
tff(c_535,plain,
! [X_26] : ( inverse(inverse(X_26)) = X_26 ),
inference(superposition,[status(thm),theory(equality)],[c_471,c_174]) ).
tff(c_572,plain,
! [X_27] : ( multiply(X_27,inverse(X_27)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_535,c_4]) ).
tff(c_90,plain,
! [X_8,Z_14] : ( multiply(X_8,multiply(X_8,multiply(X_8,Z_14))) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_2,c_74]) ).
tff(c_577,plain,
! [X_27] : ( multiply(X_27,multiply(X_27,identity)) = inverse(X_27) ),
inference(superposition,[status(thm),theory(equality)],[c_572,c_90]) ).
tff(c_613,plain,
! [X_27] : ( multiply(X_27,X_27) = inverse(X_27) ),
inference(demodulation,[status(thm),theory(equality)],[c_441,c_577]) ).
tff(c_1162,plain,
! [X_37,Y_38] : ( multiply(X_37,multiply(Y_38,inverse(multiply(X_37,Y_38)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_572]) ).
tff(c_1189,plain,
! [Y_38,X_37] : ( multiply(Y_38,inverse(multiply(X_37,Y_38))) = multiply(X_37,multiply(X_37,identity)) ),
inference(superposition,[status(thm),theory(equality)],[c_1162,c_90]) ).
tff(c_1327,plain,
! [Y_39,X_40] : ( multiply(Y_39,inverse(multiply(X_40,Y_39))) = inverse(X_40) ),
inference(demodulation,[status(thm),theory(equality)],[c_613,c_441,c_1189]) ).
tff(c_1402,plain,
! [X_2,Z_14] : ( multiply(multiply(X_2,Z_14),inverse(Z_14)) = inverse(inverse(X_2)) ),
inference(superposition,[status(thm),theory(equality)],[c_92,c_1327]) ).
tff(c_1434,plain,
! [X_2,Z_14] : ( multiply(multiply(X_2,Z_14),inverse(Z_14)) = X_2 ),
inference(demodulation,[status(thm),theory(equality)],[c_480,c_1402]) ).
tff(c_8,plain,
! [X_6,Y_7] : ( multiply(X_6,multiply(Y_7,multiply(inverse(X_6),inverse(Y_7)))) = commutator(X_6,Y_7) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_1354,plain,
! [X_6,X_40] : ( multiply(X_6,multiply(multiply(X_40,inverse(X_6)),inverse(X_40))) = commutator(X_6,multiply(X_40,inverse(X_6))) ),
inference(superposition,[status(thm),theory(equality)],[c_1327,c_8]) ).
tff(c_2879,plain,
! [X_60,X_61] : ( commutator(X_60,multiply(X_61,inverse(X_60))) = commutator(X_60,X_61) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6,c_1354]) ).
tff(c_2912,plain,
! [Z_14,X_2] : ( commutator(Z_14,multiply(X_2,Z_14)) = commutator(Z_14,X_2) ),
inference(superposition,[status(thm),theory(equality)],[c_1434,c_2879]) ).
tff(c_1438,plain,
! [X_41,Z_42] : ( multiply(multiply(X_41,Z_42),inverse(Z_42)) = X_41 ),
inference(demodulation,[status(thm),theory(equality)],[c_480,c_1402]) ).
tff(c_1492,plain,
! [X_41,X_2] : ( multiply(multiply(X_41,inverse(X_2)),X_2) = X_41 ),
inference(superposition,[status(thm),theory(equality)],[c_480,c_1438]) ).
tff(c_1298,plain,
! [Y_38,X_37] : ( multiply(Y_38,inverse(multiply(X_37,Y_38))) = inverse(X_37) ),
inference(demodulation,[status(thm),theory(equality)],[c_613,c_441,c_1189]) ).
tff(c_94,plain,
! [X_15,Y_16] : ( multiply(X_15,multiply(Y_16,multiply(inverse(X_15),inverse(Y_16)))) = commutator(X_15,Y_16) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_100,plain,
! [X_15,Y_16,Z_5] : ( multiply(X_15,multiply(multiply(Y_16,multiply(inverse(X_15),inverse(Y_16))),Z_5)) = multiply(commutator(X_15,Y_16),Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_94,c_6]) ).
tff(c_4012,plain,
! [X_72,Y_73,Z_74] : ( multiply(X_72,multiply(Y_73,multiply(inverse(X_72),multiply(inverse(Y_73),Z_74)))) = multiply(commutator(X_72,Y_73),Z_74) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_6,c_100]) ).
tff(c_4294,plain,
! [X_72,X_2] : ( multiply(commutator(X_72,X_2),X_2) = multiply(X_72,multiply(X_2,multiply(inverse(X_72),identity))) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4012]) ).
tff(c_8697,plain,
! [X_104,X_105] : ( multiply(commutator(X_104,X_105),X_105) = multiply(X_104,multiply(X_105,inverse(X_104))) ),
inference(demodulation,[status(thm),theory(equality)],[c_441,c_4294]) ).
tff(c_1350,plain,
! [Y_39,X_40] : ( multiply(inverse(Y_39),inverse(X_40)) = inverse(multiply(X_40,Y_39)) ),
inference(superposition,[status(thm),theory(equality)],[c_1327,c_92]) ).
tff(c_119,plain,
! [X_3,Y_4,Y_16] : ( multiply(X_3,multiply(Y_4,multiply(Y_16,multiply(inverse(multiply(X_3,Y_4)),inverse(Y_16))))) = commutator(multiply(X_3,Y_4),Y_16) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_94]) ).
tff(c_6945,plain,
! [X_3,Y_4,Y_16] : ( multiply(X_3,multiply(Y_4,multiply(Y_16,inverse(multiply(Y_16,multiply(X_3,Y_4)))))) = commutator(multiply(X_3,Y_4),Y_16) ),
inference(demodulation,[status(thm),theory(equality)],[c_1350,c_119]) ).
tff(c_8750,plain,
! [X_105,X_104] : ( multiply(X_105,multiply(inverse(X_104),multiply(X_104,inverse(multiply(commutator(X_104,X_105),X_105))))) = commutator(multiply(X_105,inverse(X_104)),X_104) ),
inference(superposition,[status(thm),theory(equality)],[c_8697,c_6945]) ).
tff(c_10220,plain,
! [X_115,X_116] : ( commutator(multiply(X_115,inverse(X_116)),X_116) = inverse(commutator(X_116,X_115)) ),
inference(demodulation,[status(thm),theory(equality)],[c_1298,c_92,c_8750]) ).
tff(c_10271,plain,
! [X_116,X_41] : ( inverse(commutator(X_116,multiply(X_41,inverse(inverse(X_116))))) = commutator(X_41,X_116) ),
inference(superposition,[status(thm),theory(equality)],[c_1492,c_10220]) ).
tff(c_10317,plain,
! [X_116,X_41] : ( inverse(commutator(X_116,X_41)) = commutator(X_41,X_116) ),
inference(demodulation,[status(thm),theory(equality)],[c_2912,c_480,c_10271]) ).
tff(c_115,plain,
! [X_15,X_3,Y_4] : ( multiply(X_15,multiply(X_3,multiply(Y_4,multiply(inverse(X_15),inverse(multiply(X_3,Y_4)))))) = commutator(X_15,multiply(X_3,Y_4)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_94]) ).
tff(c_5543,plain,
! [X_15,X_3,Y_4] : ( multiply(X_15,multiply(X_3,multiply(Y_4,inverse(multiply(X_3,multiply(Y_4,X_15)))))) = commutator(X_15,multiply(X_3,Y_4)) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_1350,c_115]) ).
tff(c_8793,plain,
! [X_104,X_105] : ( multiply(inverse(X_104),multiply(X_104,multiply(X_105,inverse(multiply(commutator(X_104,X_105),X_105))))) = commutator(inverse(X_104),multiply(X_104,X_105)) ),
inference(superposition,[status(thm),theory(equality)],[c_8697,c_5543]) ).
tff(c_9077,plain,
! [X_104,X_105] : ( commutator(inverse(X_104),multiply(X_104,X_105)) = inverse(commutator(X_104,X_105)) ),
inference(demodulation,[status(thm),theory(equality)],[c_92,c_1298,c_8793]) ).
tff(c_11604,plain,
! [X_129,X_130] : ( commutator(inverse(X_129),multiply(X_129,X_130)) = commutator(X_130,X_129) ),
inference(demodulation,[status(thm),theory(equality)],[c_10317,c_9077]) ).
tff(c_11772,plain,
! [X_2,Z_14] : ( commutator(multiply(X_2,Z_14),inverse(X_2)) = commutator(inverse(inverse(X_2)),Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_92,c_11604]) ).
tff(c_11819,plain,
! [X_2,Z_14] : ( commutator(multiply(X_2,Z_14),inverse(X_2)) = commutator(X_2,Z_14) ),
inference(demodulation,[status(thm),theory(equality)],[c_480,c_11772]) ).
tff(c_10329,plain,
! [X_117,X_118] : ( inverse(commutator(X_117,X_118)) = commutator(X_118,X_117) ),
inference(demodulation,[status(thm),theory(equality)],[c_2912,c_480,c_10271]) ).
tff(c_10437,plain,
! [X_118,X_117] : ( multiply(commutator(X_118,X_117),commutator(X_117,X_118)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_10329,c_4]) ).
tff(c_2092,plain,
! [X_6,Y_7] : ( multiply(X_6,multiply(Y_7,inverse(multiply(Y_7,X_6)))) = commutator(X_6,Y_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_1350,c_8]) ).
tff(c_547,plain,
! [X_26,Z_14] : ( multiply(X_26,multiply(inverse(X_26),Z_14)) = Z_14 ),
inference(superposition,[status(thm),theory(equality)],[c_535,c_92]) ).
tff(c_1344,plain,
! [X_40,X_26] : ( inverse(multiply(X_40,inverse(X_26))) = multiply(X_26,inverse(X_40)) ),
inference(superposition,[status(thm),theory(equality)],[c_1327,c_547]) ).
tff(c_4365,plain,
! [X_72,X_2] : ( multiply(commutator(X_72,X_2),X_2) = multiply(X_72,multiply(X_2,inverse(X_72))) ),
inference(demodulation,[status(thm),theory(equality)],[c_441,c_4294]) ).
tff(c_391,plain,
! [X_23,Z_24] : ( multiply(inverse(X_23),Z_24) = multiply(X_23,multiply(X_23,Z_24)) ),
inference(superposition,[status(thm),theory(equality)],[c_379,c_92]) ).
tff(c_25855,plain,
! [Y_196,X_197] : ( multiply(inverse(Y_196),inverse(multiply(X_197,Y_196))) = multiply(Y_196,inverse(X_197)) ),
inference(superposition,[status(thm),theory(equality)],[c_1327,c_391]) ).
tff(c_26213,plain,
! [X_2,X_72] : ( multiply(inverse(multiply(X_2,inverse(X_72))),inverse(multiply(commutator(X_72,X_2),X_2))) = multiply(multiply(X_2,inverse(X_72)),inverse(X_72)) ),
inference(superposition,[status(thm),theory(equality)],[c_4365,c_25855]) ).
tff(c_27759,plain,
! [X_201,X_202] : ( multiply(X_201,multiply(X_202,commutator(X_202,X_201))) = multiply(X_202,X_201) ),
inference(demodulation,[status(thm),theory(equality)],[c_10317,c_1344,c_613,c_6,c_1350,c_6,c_1344,c_480,c_613,c_6,c_26213]) ).
tff(c_27975,plain,
! [X_202,X_201] : ( multiply(commutator(X_202,X_201),multiply(X_201,multiply(X_202,inverse(multiply(X_202,X_201))))) = commutator(commutator(X_202,X_201),multiply(X_201,X_202)) ),
inference(superposition,[status(thm),theory(equality)],[c_27759,c_5543]) ).
tff(c_28275,plain,
! [X_203,X_204] : ( commutator(commutator(X_203,X_204),multiply(X_204,X_203)) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_10437,c_2092,c_27975]) ).
tff(c_28426,plain,
! [X_2,Z_14] : ( commutator(commutator(X_2,Z_14),multiply(inverse(X_2),multiply(X_2,Z_14))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_11819,c_28275]) ).
tff(c_28600,plain,
! [X_2,Z_14] : ( commutator(commutator(X_2,Z_14),Z_14) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_92,c_28426]) ).
tff(c_12,plain,
commutator(commutator(a,b),b) != identity,
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_28633,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28600,c_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.11 % Problem : GRP002-3 : TPTP v9.0.0. Released v1.0.0.
% 0.02/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.11/0.31 % Computer : n023.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Mon Apr 7 21:09:24 EDT 2025
% 0.11/0.31 % CPUTime :
% 12.63/4.94 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.63/4.95
% 12.63/4.95 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------