%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP002-4 : 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 : n022.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 18.91s 7.90s
% Output : CNFRefutation 18.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 8
% Syntax : Number of formulae : 65 ( 65 unt; 0 typ; 0 def)
% Number of atoms : 65 ( 64 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 : 117 ( 117 !; 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_63,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_67,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_70,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_75,axiom,
! [X] : ( multiply(X,identity) = X ),
file(unknown,unknown) ).
tff(f_82,axiom,
! [X] : ( multiply(X,multiply(X,X)) = identity ),
file(unknown,unknown) ).
tff(f_77,axiom,
! [X] : ( multiply(X,inverse(X)) = identity ),
file(unknown,unknown) ).
tff(f_80,axiom,
! [X,Y] : ( commutator(X,Y) = multiply(X,multiply(Y,multiply(inverse(X),inverse(Y)))) ),
file(unknown,unknown) ).
tff(f_84,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_63]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_117,plain,
! [X_16,Y_17,Z_18] : ( multiply(multiply(X_16,Y_17),Z_18) = multiply(X_16,multiply(Y_17,Z_18)) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_155,plain,
! [X_2,Z_18] : ( multiply(inverse(X_2),multiply(X_2,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_117]) ).
tff(c_181,plain,
! [X_2,Z_18] : ( multiply(inverse(X_2),multiply(X_2,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_155]) ).
tff(c_8,plain,
! [X_6] : ( multiply(X_6,identity) = X_6 ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_14,plain,
! [X_10] : ( multiply(X_10,multiply(X_10,X_10)) = identity ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_307,plain,
! [X_25,Z_26] : ( multiply(inverse(X_25),multiply(X_25,Z_26)) = Z_26 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_155]) ).
tff(c_343,plain,
! [X_10] : ( multiply(inverse(X_10),identity) = multiply(X_10,X_10) ),
inference(superposition,[status(thm),theory(equality)],[c_14,c_307]) ).
tff(c_364,plain,
! [X_10] : ( multiply(X_10,X_10) = inverse(X_10) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_343]) ).
tff(c_10,plain,
! [X_7] : ( multiply(X_7,inverse(X_7)) = identity ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_771,plain,
! [X_36,Y_37] : ( multiply(X_36,multiply(Y_37,inverse(multiply(X_36,Y_37)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_117]) ).
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_70]) ).
tff(c_148,plain,
! [X_10,Z_18] : ( multiply(X_10,multiply(multiply(X_10,X_10),Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_14,c_117]) ).
tff(c_179,plain,
! [X_10,Z_18] : ( multiply(X_10,multiply(X_10,multiply(X_10,Z_18))) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_2,c_148]) ).
tff(c_779,plain,
! [Y_37,X_36] : ( multiply(Y_37,inverse(multiply(X_36,Y_37))) = multiply(X_36,multiply(X_36,identity)) ),
inference(superposition,[status(thm),theory(equality)],[c_771,c_179]) ).
tff(c_903,plain,
! [Y_38,X_39] : ( multiply(Y_38,inverse(multiply(X_39,Y_38))) = inverse(X_39) ),
inference(demodulation,[status(thm),theory(equality)],[c_364,c_8,c_779]) ).
tff(c_919,plain,
! [Y_38,X_39] : ( multiply(inverse(Y_38),inverse(X_39)) = inverse(multiply(X_39,Y_38)) ),
inference(superposition,[status(thm),theory(equality)],[c_903,c_181]) ).
tff(c_12,plain,
! [X_8,Y_9] : ( multiply(X_8,multiply(Y_9,multiply(inverse(X_8),inverse(Y_9)))) = commutator(X_8,Y_9) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_2335,plain,
! [X_8,Y_9] : ( multiply(X_8,multiply(Y_9,inverse(multiply(Y_9,X_8)))) = commutator(X_8,Y_9) ),
inference(demodulation,[status(thm),theory(equality)],[c_919,c_12]) ).
tff(c_11195,plain,
! [X_121,Y_122] : ( multiply(X_121,multiply(Y_122,inverse(multiply(Y_122,X_121)))) = commutator(X_121,Y_122) ),
inference(demodulation,[status(thm),theory(equality)],[c_919,c_12]) ).
tff(c_11533,plain,
! [X_2,Z_18] : ( multiply(multiply(X_2,Z_18),multiply(inverse(X_2),inverse(Z_18))) = commutator(multiply(X_2,Z_18),inverse(X_2)) ),
inference(superposition,[status(thm),theory(equality)],[c_181,c_11195]) ).
tff(c_11645,plain,
! [X_2,Z_18] : ( commutator(multiply(X_2,Z_18),inverse(X_2)) = commutator(X_2,Z_18) ),
inference(demodulation,[status(thm),theory(equality)],[c_2335,c_6,c_919,c_11533]) ).
tff(c_418,plain,
! [X_28] : ( multiply(inverse(inverse(X_28)),identity) = X_28 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_307]) ).
tff(c_430,plain,
! [X_28] : ( inverse(inverse(X_28)) = X_28 ),
inference(superposition,[status(thm),theory(equality)],[c_418,c_8]) ).
tff(c_11656,plain,
! [X_123,Z_124] : ( commutator(multiply(X_123,Z_124),inverse(X_123)) = commutator(X_123,Z_124) ),
inference(demodulation,[status(thm),theory(equality)],[c_2335,c_6,c_919,c_11533]) ).
tff(c_11773,plain,
! [X_2,Z_18] : ( commutator(inverse(X_2),multiply(X_2,Z_18)) = commutator(Z_18,inverse(inverse(X_2))) ),
inference(superposition,[status(thm),theory(equality)],[c_181,c_11656]) ).
tff(c_11816,plain,
! [X_2,Z_18] : ( commutator(inverse(X_2),multiply(X_2,Z_18)) = commutator(Z_18,X_2) ),
inference(demodulation,[status(thm),theory(equality)],[c_430,c_11773]) ).
tff(c_874,plain,
! [Y_37,X_36] : ( multiply(Y_37,inverse(multiply(X_36,Y_37))) = inverse(X_36) ),
inference(demodulation,[status(thm),theory(equality)],[c_364,c_8,c_779]) ).
tff(c_186,plain,
! [X_19,Y_20] : ( multiply(X_19,multiply(Y_20,multiply(inverse(X_19),inverse(Y_20)))) = commutator(X_19,Y_20) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_192,plain,
! [X_19,Y_20,Z_5] : ( multiply(X_19,multiply(multiply(Y_20,multiply(inverse(X_19),inverse(Y_20))),Z_5)) = multiply(commutator(X_19,Y_20),Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_186,c_6]) ).
tff(c_3776,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_192]) ).
tff(c_4036,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_3776]) ).
tff(c_13830,plain,
! [X_144,X_145] : ( multiply(commutator(X_144,X_145),X_145) = multiply(X_144,multiply(X_145,inverse(X_144))) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_4036]) ).
tff(c_207,plain,
! [X_19,X_3,Y_4] : ( multiply(X_19,multiply(X_3,multiply(Y_4,multiply(inverse(X_19),inverse(multiply(X_3,Y_4)))))) = commutator(X_19,multiply(X_3,Y_4)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_186]) ).
tff(c_8270,plain,
! [X_19,X_3,Y_4] : ( multiply(X_19,multiply(X_3,multiply(Y_4,inverse(multiply(X_3,multiply(Y_4,X_19)))))) = commutator(X_19,multiply(X_3,Y_4)) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_919,c_207]) ).
tff(c_13962,plain,
! [X_144,X_145] : ( multiply(inverse(X_144),multiply(X_144,multiply(X_145,inverse(multiply(commutator(X_144,X_145),X_145))))) = commutator(inverse(X_144),multiply(X_144,X_145)) ),
inference(superposition,[status(thm),theory(equality)],[c_13830,c_8270]) ).
tff(c_14404,plain,
! [X_146,X_147] : ( inverse(commutator(X_146,X_147)) = commutator(X_147,X_146) ),
inference(demodulation,[status(thm),theory(equality)],[c_11816,c_181,c_874,c_13962]) ).
tff(c_14545,plain,
! [X_147,X_146] : ( multiply(commutator(X_147,X_146),commutator(X_146,X_147)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_14404,c_4]) ).
tff(c_14334,plain,
! [X_144,X_145] : ( inverse(commutator(X_144,X_145)) = commutator(X_145,X_144) ),
inference(demodulation,[status(thm),theory(equality)],[c_11816,c_181,c_874,c_13962]) ).
tff(c_158,plain,
! [X_7,Z_18] : ( multiply(X_7,multiply(inverse(X_7),Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_117]) ).
tff(c_182,plain,
! [X_7,Z_18] : ( multiply(X_7,multiply(inverse(X_7),Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_916,plain,
! [X_39,X_7] : ( inverse(multiply(X_39,inverse(X_7))) = multiply(X_7,inverse(X_39)) ),
inference(superposition,[status(thm),theory(equality)],[c_903,c_182]) ).
tff(c_4115,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_8,c_4036]) ).
tff(c_787,plain,
! [Y_37,X_7] : ( multiply(Y_37,inverse(multiply(inverse(X_7),Y_37))) = multiply(X_7,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_771,c_182]) ).
tff(c_1186,plain,
! [Y_44,X_45] : ( multiply(Y_44,inverse(multiply(inverse(X_45),Y_44))) = X_45 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_787]) ).
tff(c_4125,plain,
! [Y_75,X_76] : ( multiply(Y_75,multiply(Y_75,X_76)) = inverse(multiply(inverse(X_76),Y_75)) ),
inference(superposition,[status(thm),theory(equality)],[c_1186,c_179]) ).
tff(c_4368,plain,
! [Y_38,X_39] : ( multiply(inverse(Y_38),inverse(multiply(X_39,Y_38))) = inverse(multiply(inverse(inverse(X_39)),inverse(Y_38))) ),
inference(superposition,[status(thm),theory(equality)],[c_919,c_4125]) ).
tff(c_30902,plain,
! [Y_208,X_209] : ( multiply(inverse(Y_208),inverse(multiply(X_209,Y_208))) = multiply(Y_208,inverse(X_209)) ),
inference(demodulation,[status(thm),theory(equality)],[c_916,c_430,c_4368]) ).
tff(c_31276,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_4115,c_30902]) ).
tff(c_31597,plain,
! [X_210,X_211] : ( multiply(X_210,multiply(X_211,commutator(X_211,X_210))) = multiply(X_211,X_210) ),
inference(demodulation,[status(thm),theory(equality)],[c_14334,c_916,c_364,c_6,c_919,c_6,c_916,c_430,c_364,c_6,c_31276]) ).
tff(c_31774,plain,
! [X_211,X_210] : ( multiply(commutator(X_211,X_210),multiply(X_210,multiply(X_211,inverse(multiply(X_211,X_210))))) = commutator(commutator(X_211,X_210),multiply(X_210,X_211)) ),
inference(superposition,[status(thm),theory(equality)],[c_31597,c_8270]) ).
tff(c_32488,plain,
! [X_216,X_217] : ( commutator(commutator(X_216,X_217),multiply(X_217,X_216)) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_14545,c_2335,c_31774]) ).
tff(c_32642,plain,
! [X_2,Z_18] : ( commutator(commutator(X_2,Z_18),multiply(inverse(X_2),multiply(X_2,Z_18))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_11645,c_32488]) ).
tff(c_32808,plain,
! [X_2,Z_18] : ( commutator(commutator(X_2,Z_18),Z_18) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_181,c_32642]) ).
tff(c_16,plain,
commutator(commutator(a,b),b) != identity,
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_32844,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_32808,c_16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : GRP002-4 : TPTP v9.0.0. Released v1.0.0.
% 0.00/0.10 % 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.10/0.30 % Computer : n022.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Mon Apr 7 21:09:20 EDT 2025
% 0.10/0.30 % CPUTime :
% 18.91/7.90 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.91/7.91
% 18.91/7.91 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------