%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP379-1 : TPTP v9.0.0. Released v2.5.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 : n025.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:06 PM UTC 2025
% Result : Unsatisfiable 19.44s 8.17s
% Output : CNFRefutation 19.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 33
% Syntax : Number of formulae : 510 ( 416 unt; 0 typ; 0 def)
% Number of atoms : 719 ( 699 equ)
% Maximal formula atoms : 15 ( 1 avg)
% Number of connectives : 429 ( 220 ~; 209 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 2 avg)
% Maximal term depth : 5 ( 1 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 : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 280 ( 280 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c11 > sk_c10 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c10,type,
sk_c10: $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c11,type,
sk_c11: $i ).
tff(sk_c9,type,
sk_c9: $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( inverse(sk_c11) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( multiply(sk_c1,sk_c2) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_194,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c11 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_257,axiom,
! [X5,X6,X3,X7,X1,X2,X8,X4] :
( ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( multiply(X3,X4) != sk_c11 )
| ( inverse(X3) != X4 )
| ( multiply(X4,sk_c9) != sk_c11 )
| ( multiply(X1,sk_c11) != sk_c10 )
| ( inverse(X1) != sk_c11 )
| ( multiply(X2,sk_c10) != sk_c9 )
| ( inverse(X2) != sk_c10 )
| ( multiply(X5,X6) != sk_c11 )
| ( inverse(X5) != X6 )
| ( multiply(X6,sk_c10) != sk_c11 )
| ( inverse(X7) != X8 )
| ( inverse(X8) != X6 )
| ( multiply(X7,X6) != X8 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_188,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_191,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c1,sk_c2) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c11) = sk_c10 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c11) = sk_c10 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( inverse(sk_c11) = sk_c10 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c11) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_173,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_182,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_176,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_179,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_69085,plain,
! [X_525,Y_526,Z_527] : ( multiply(multiply(X_525,Y_526),Z_527) = multiply(X_525,multiply(Y_526,Z_527)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_69133,plain,
! [X_2,Z_527] : ( multiply(inverse(X_2),multiply(X_2,Z_527)) = multiply(identity,Z_527) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_69085]) ).
tff(c_83184,plain,
! [X_693,Z_694] : ( multiply(inverse(X_693),multiply(X_693,Z_694)) = Z_694 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69133]) ).
tff(c_69147,plain,
! [X_2,Z_527] : ( multiply(inverse(X_2),multiply(X_2,Z_527)) = Z_527 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69133]) ).
tff(c_83448,plain,
! [X_697,Z_698] : ( multiply(inverse(inverse(X_697)),Z_698) = multiply(X_697,Z_698) ),
inference(superposition,[status(thm),theory(equality)],[c_83184,c_69147]) ).
tff(c_83205,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_83184]) ).
tff(c_83455,plain,
! [X_697] : ( multiply(X_697,identity) = X_697 ),
inference(superposition,[status(thm),theory(equality)],[c_83448,c_83205]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_138,plain,
inverse(sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_142,plain,
multiply(sk_c10,sk_c11) = identity,
inference(superposition,[status(thm),theory(equality)],[c_138,c_4]) ).
tff(c_50,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_157,plain,
multiply(sk_c1,sk_c2) = sk_c11,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_78,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_125,plain,
inverse(sk_c1) = sk_c2,
inference(splitLeft,[status(thm)],[c_78]) ).
tff(c_129,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_125,c_4]) ).
tff(c_65742,plain,
! [X_469,Y_470,Z_471] : ( multiply(multiply(X_469,Y_470),Z_471) = multiply(X_469,multiply(Y_470,Z_471)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_65793,plain,
! [Z_471] : ( multiply(sk_c2,multiply(sk_c1,Z_471)) = multiply(identity,Z_471) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_65742]) ).
tff(c_65837,plain,
! [Z_473] : ( multiply(sk_c2,multiply(sk_c1,Z_473)) = Z_473 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65793]) ).
tff(c_65849,plain,
multiply(sk_c2,sk_c11) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_157,c_65837]) ).
tff(c_65796,plain,
! [X_2,Z_471] : ( multiply(inverse(X_2),multiply(X_2,Z_471)) = multiply(identity,Z_471) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65742]) ).
tff(c_65917,plain,
! [X_475,Z_476] : ( multiply(inverse(X_475),multiply(X_475,Z_476)) = Z_476 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65796]) ).
tff(c_65935,plain,
multiply(inverse(sk_c2),sk_c2) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_65849,c_65917]) ).
tff(c_65984,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_65935]) ).
tff(c_32331,plain,
! [X_239,Y_240,Z_241] : ( multiply(multiply(X_239,Y_240),Z_241) = multiply(X_239,multiply(Y_240,Z_241)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_32385,plain,
! [Z_241] : ( multiply(sk_c2,multiply(sk_c1,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_32331]) ).
tff(c_32429,plain,
! [Z_243] : ( multiply(sk_c2,multiply(sk_c1,Z_243)) = Z_243 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32385]) ).
tff(c_32441,plain,
multiply(sk_c2,sk_c11) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_157,c_32429]) ).
tff(c_32388,plain,
! [X_2,Z_241] : ( multiply(inverse(X_2),multiply(X_2,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_32331]) ).
tff(c_32566,plain,
! [X_249,Z_250] : ( multiply(inverse(X_249),multiply(X_249,Z_250)) = Z_250 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32388]) ).
tff(c_32611,plain,
multiply(inverse(sk_c2),sk_c2) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_32441,c_32566]) ).
tff(c_32699,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_32611]) ).
tff(c_209,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_60]) ).
tff(c_236,plain,
! [Z_18] : ( multiply(sk_c2,multiply(sk_c1,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_209]) ).
tff(c_264,plain,
! [Z_20] : ( multiply(sk_c2,multiply(sk_c1,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_236]) ).
tff(c_276,plain,
multiply(sk_c2,sk_c11) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_157,c_264]) ).
tff(c_239,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_209]) ).
tff(c_287,plain,
! [X_21,Z_22] : ( multiply(inverse(X_21),multiply(X_21,Z_22)) = Z_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_239]) ).
tff(c_305,plain,
multiply(inverse(sk_c2),sk_c2) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_276,c_287]) ).
tff(c_345,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_305]) ).
tff(c_355,plain,
inverse(identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_138]) ).
tff(c_233,plain,
! [Z_18] : ( multiply(sk_c10,multiply(sk_c11,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_209]) ).
tff(c_247,plain,
! [Z_18] : ( multiply(sk_c10,multiply(sk_c11,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_233]) ).
tff(c_350,plain,
! [Z_18] : ( multiply(sk_c10,multiply(identity,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_345,c_247]) ).
tff(c_458,plain,
! [Z_24] : ( multiply(sk_c10,Z_24) = Z_24 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_350]) ).
tff(c_42,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_170,plain,
multiply(sk_c10,sk_c9) = sk_c11,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_351,plain,
multiply(sk_c10,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_170]) ).
tff(c_467,plain,
sk_c9 = identity,
inference(superposition,[status(thm),theory(equality)],[c_458,c_351]) ).
tff(c_94,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_164,plain,
multiply(sk_c2,sk_c9) = sk_c11,
inference(splitLeft,[status(thm)],[c_94]) ).
tff(c_227,plain,
! [Z_18] : ( multiply(sk_c2,multiply(sk_c9,Z_18)) = multiply(sk_c11,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_164,c_209]) ).
tff(c_514,plain,
! [Z_25] : ( multiply(sk_c2,Z_25) = Z_25 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_467,c_2,c_345,c_227]) ).
tff(c_529,plain,
sk_c1 = identity,
inference(superposition,[status(thm),theory(equality)],[c_514,c_129]) ).
tff(c_352,plain,
multiply(sk_c2,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_164]) ).
tff(c_486,plain,
multiply(sk_c2,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_467,c_352]) ).
tff(c_349,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_276]) ).
tff(c_500,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_486,c_349]) ).
tff(c_546,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_500,c_125]) ).
tff(c_576,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_355,c_529,c_546]) ).
tff(c_578,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_355]) ).
tff(c_249,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_239]) ).
tff(c_613,plain,
! [X_27,Z_28] : ( multiply(inverse(inverse(X_27)),Z_28) = multiply(X_27,Z_28) ),
inference(superposition,[status(thm),theory(equality)],[c_249,c_287]) ).
tff(c_338,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_287]) ).
tff(c_620,plain,
! [X_27] : ( multiply(X_27,identity) = X_27 ),
inference(superposition,[status(thm),theory(equality)],[c_613,c_338]) ).
tff(c_634,plain,
! [X_27] : ( multiply(X_27,inverse(X_27)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_613,c_4]) ).
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_60]) ).
tff(c_750,plain,
! [X_31] : ( multiply(X_31,inverse(X_31)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_613,c_4]) ).
tff(c_800,plain,
! [X_32,Y_33] : ( multiply(X_32,multiply(Y_33,inverse(multiply(X_32,Y_33)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_750]) ).
tff(c_808,plain,
! [Y_33,X_32] : ( multiply(Y_33,inverse(multiply(X_32,Y_33))) = multiply(inverse(X_32),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_800,c_249]) ).
tff(c_1979,plain,
! [Y_55,X_56] : ( multiply(Y_55,inverse(multiply(X_56,Y_55))) = inverse(X_56) ),
inference(demodulation,[status(thm),theory(equality)],[c_620,c_808]) ).
tff(c_647,plain,
! [X_27,Z_18] : ( multiply(X_27,multiply(inverse(X_27),Z_18)) = Z_18 ),
inference(superposition,[status(thm),theory(equality)],[c_249,c_613]) ).
tff(c_2009,plain,
! [X_56,X_27] : ( inverse(multiply(X_56,inverse(X_27))) = multiply(X_27,inverse(X_56)) ),
inference(superposition,[status(thm),theory(equality)],[c_1979,c_647]) ).
tff(c_108,plain,
! [X5_6,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c9) != sk_c11 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c11 )
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_257]) ).
tff(c_361,plain,
! [X5_6,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != identity )
| ( multiply(X5_6,inverse(X5_6)) != identity )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != identity )
| ( multiply(X1_10,identity) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c9) != identity )
| ( multiply(X3_8,inverse(X3_8)) != identity )
| ( multiply(sk_c10,sk_c9) != identity )
| ( inverse(identity) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_345,c_345,c_345,c_345,c_345,c_345,c_345,c_345,c_108]) ).
tff(c_362,plain,
inverse(identity) != sk_c10,
inference(splitLeft,[status(thm)],[c_361]) ).
tff(c_363,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_355]) ).
tff(c_364,plain,
! [X5_6,X3_8,X1_10,X7_9,X2_11] :
( ( multiply(sk_c10,sk_c9) != identity )
| ( multiply(inverse(X3_8),sk_c9) != identity )
| ( multiply(X3_8,inverse(X3_8)) != identity )
| ( inverse(X1_10) != identity )
| ( multiply(X1_10,identity) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != identity )
| ( multiply(X5_6,inverse(X5_6)) != identity ) ),
inference(splitRight,[status(thm)],[c_361]) ).
tff(c_28207,plain,
! [X5_6,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(X3_8) != identity )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( multiply(X5_6,inverse(X7_9)) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( inverse(X5_6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_634,c_620,c_576,c_2009,c_620,c_576,c_467,c_576,c_620,c_576,c_634,c_620,c_467,c_2,c_576,c_467,c_364]) ).
tff(c_32084,plain,
! [X5_236,X7_237] :
( ( multiply(X5_236,inverse(X7_237)) != inverse(X5_236) )
| ( multiply(X7_237,inverse(X5_236)) != inverse(X7_237) )
| ( inverse(X5_236) != identity ) ),
inference(splitLeft,[status(thm)],[c_28207]) ).
tff(c_32154,plain,
! [X7_237] :
( ( inverse(identity) != inverse(X7_237) )
| ( multiply(X7_237,inverse(identity)) != inverse(X7_237) )
| ( inverse(identity) != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_32084]) ).
tff(c_32184,plain,
! [X7_238] :
( ( inverse(X7_238) != identity )
| ( inverse(X7_238) != X7_238 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_578,c_620,c_578,c_578,c_32154]) ).
tff(c_32196,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_578,c_32184]) ).
tff(c_32205,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_578,c_32196]) ).
tff(c_32206,plain,
! [X3_8,X1_10,X2_11] :
( ( inverse(X3_8) != identity )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_28207]) ).
tff(c_32208,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_32206]) ).
tff(c_32210,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32208,c_578]) ).
tff(c_32211,plain,
! [X1_10,X3_8] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X3_8) != identity ) ),
inference(splitRight,[status(thm)],[c_32206]) ).
tff(c_32213,plain,
! [X3_8] : ( inverse(X3_8) != identity ),
inference(splitLeft,[status(thm)],[c_32211]) ).
tff(c_32215,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32213,c_578]) ).
tff(c_32217,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_32211]) ).
tff(c_32219,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32217,c_578]) ).
tff(c_32221,plain,
multiply(sk_c10,sk_c9) != sk_c11,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_30,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_32282,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_32221,c_30]) ).
tff(c_28,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_32297,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_32221,c_28]) ).
tff(c_32638,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_32297,c_32566]) ).
tff(c_32703,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_32282,c_32638]) ).
tff(c_32873,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_32699,c_2,c_32699,c_32703]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_32254,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_32221,c_34]) ).
tff(c_32,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_32324,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_32221,c_32]) ).
tff(c_32626,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_32324,c_32566]) ).
tff(c_32700,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_32254,c_32626]) ).
tff(c_32403,plain,
! [X_2,Z_241] : ( multiply(inverse(X_2),multiply(X_2,Z_241)) = Z_241 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32388]) ).
tff(c_32830,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_32700,c_32403]) ).
tff(c_32836,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_32830]) ).
tff(c_32722,plain,
multiply(sk_c10,sk_c9) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_32699,c_32221]) ).
tff(c_33121,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32873,c_32836,c_32722]) ).
tff(c_33123,plain,
multiply(sk_c2,sk_c9) != sk_c11,
inference(splitRight,[status(thm)],[c_94]) ).
tff(c_88,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_65727,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_33123,c_88]) ).
tff(c_90,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c2,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_65677,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_33123,c_90]) ).
tff(c_65681,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_65677,c_4]) ).
tff(c_65772,plain,
! [Z_471] : ( multiply(sk_c11,multiply(sk_c3,Z_471)) = multiply(identity,Z_471) ),
inference(superposition,[status(thm),theory(equality)],[c_65681,c_65742]) ).
tff(c_65862,plain,
! [Z_474] : ( multiply(sk_c11,multiply(sk_c3,Z_474)) = Z_474 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65772]) ).
tff(c_65877,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_65727,c_65862]) ).
tff(c_65790,plain,
! [Z_471] : ( multiply(sk_c10,multiply(sk_c11,Z_471)) = multiply(identity,Z_471) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_65742]) ).
tff(c_65809,plain,
! [Z_471] : ( multiply(sk_c10,multiply(sk_c11,Z_471)) = Z_471 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65790]) ).
tff(c_65884,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_65877,c_65809]) ).
tff(c_65890,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_142,c_65884]) ).
tff(c_33239,plain,
! [X_255,Y_256,Z_257] : ( multiply(multiply(X_255,Y_256),Z_257) = multiply(X_255,multiply(Y_256,Z_257)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33296,plain,
! [X_2,Z_257] : ( multiply(inverse(X_2),multiply(X_2,Z_257)) = multiply(identity,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_33239]) ).
tff(c_64388,plain,
! [X_451,Z_452] : ( multiply(inverse(X_451),multiply(X_451,Z_452)) = Z_452 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33296]) ).
tff(c_33311,plain,
! [X_2,Z_257] : ( multiply(inverse(X_2),multiply(X_2,Z_257)) = Z_257 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33296]) ).
tff(c_64979,plain,
! [X_457,Z_458] : ( multiply(inverse(inverse(X_457)),Z_458) = multiply(X_457,Z_458) ),
inference(superposition,[status(thm),theory(equality)],[c_64388,c_33311]) ).
tff(c_64475,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_64388]) ).
tff(c_64989,plain,
! [X_457] : ( multiply(X_457,identity) = X_457 ),
inference(superposition,[status(thm),theory(equality)],[c_64979,c_64475]) ).
tff(c_92,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_33211,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_33123,c_92]) ).
tff(c_33122,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_94]) ).
tff(c_33127,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33122,c_4]) ).
tff(c_33284,plain,
! [Z_257] : ( multiply(sk_c10,multiply(sk_c4,Z_257)) = multiply(identity,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_33127,c_33239]) ).
tff(c_63077,plain,
! [Z_430] : ( multiply(sk_c10,multiply(sk_c4,Z_430)) = Z_430 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33284]) ).
tff(c_63089,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_33211,c_63077]) ).
tff(c_33136,plain,
multiply(sk_c10,sk_c9) = sk_c11,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_63093,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_63089,c_33136]) ).
tff(c_33293,plain,
! [Z_257] : ( multiply(sk_c2,multiply(sk_c1,Z_257)) = multiply(identity,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_33239]) ).
tff(c_33337,plain,
! [Z_259] : ( multiply(sk_c2,multiply(sk_c1,Z_259)) = Z_259 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33293]) ).
tff(c_33349,plain,
multiply(sk_c2,sk_c11) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_157,c_33337]) ).
tff(c_63115,plain,
multiply(sk_c2,sk_c10) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_63093,c_33349]) ).
tff(c_64415,plain,
multiply(inverse(sk_c2),sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_63115,c_64388]) ).
tff(c_64484,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_64415]) ).
tff(c_33234,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_33123,c_88]) ).
tff(c_63117,plain,
multiply(sk_c3,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_63093,c_33234]) ).
tff(c_33144,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_33123,c_90]) ).
tff(c_33148,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33144,c_4]) ).
tff(c_33290,plain,
! [Z_257] : ( multiply(sk_c10,multiply(sk_c11,Z_257)) = multiply(identity,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_33239]) ).
tff(c_33313,plain,
! [Z_258] : ( multiply(sk_c10,multiply(sk_c11,Z_258)) = Z_258 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33290]) ).
tff(c_33325,plain,
multiply(sk_c10,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_33148,c_33313]) ).
tff(c_63125,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_63093,c_138]) ).
tff(c_64463,plain,
multiply(inverse(sk_c10),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_33127,c_64388]) ).
tff(c_64491,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_33325,c_63125,c_64463]) ).
tff(c_64495,plain,
multiply(sk_c3,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_64491,c_33211]) ).
tff(c_64498,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_63117,c_64495]) ).
tff(c_64525,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64484,c_64498]) ).
tff(c_63219,plain,
! [X_433,Z_434] : ( multiply(inverse(X_433),multiply(X_433,Z_434)) = Z_434 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33296]) ).
tff(c_63682,plain,
! [X_438,Z_439] : ( multiply(inverse(inverse(X_438)),Z_439) = multiply(X_438,Z_439) ),
inference(superposition,[status(thm),theory(equality)],[c_33311,c_63219]) ).
tff(c_63318,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_63219]) ).
tff(c_63692,plain,
! [X_438] : ( multiply(X_438,identity) = X_438 ),
inference(superposition,[status(thm),theory(equality)],[c_63682,c_63318]) ).
tff(c_63258,plain,
multiply(inverse(sk_c2),sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_63115,c_63219]) ).
tff(c_63330,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_63258]) ).
tff(c_33656,plain,
! [Z_264] : ( multiply(sk_c10,multiply(sk_c4,Z_264)) = Z_264 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33284]) ).
tff(c_33668,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_33211,c_33656]) ).
tff(c_33672,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33668,c_33136]) ).
tff(c_33704,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33672,c_138]) ).
tff(c_33719,plain,
multiply(sk_c10,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33704,c_4]) ).
tff(c_33696,plain,
multiply(sk_c3,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33672,c_33234]) ).
tff(c_33832,plain,
! [X_269,Z_270] : ( multiply(inverse(X_269),multiply(X_269,Z_270)) = Z_270 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33296]) ).
tff(c_33919,plain,
multiply(inverse(sk_c10),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_33127,c_33832]) ).
tff(c_33951,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_33325,c_33704,c_33919]) ).
tff(c_33955,plain,
multiply(sk_c3,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_33951,c_33211]) ).
tff(c_33958,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33696,c_33955]) ).
tff(c_33966,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33958,c_33668]) ).
tff(c_33968,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33719,c_33966]) ).
tff(c_34027,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33968,c_33968,c_33704]) ).
tff(c_34285,plain,
! [X_274,Z_275] : ( multiply(inverse(inverse(X_274)),Z_275) = multiply(X_274,Z_275) ),
inference(superposition,[status(thm),theory(equality)],[c_33311,c_33832]) ).
tff(c_33931,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_33832]) ).
tff(c_34292,plain,
! [X_274] : ( multiply(X_274,identity) = X_274 ),
inference(superposition,[status(thm),theory(equality)],[c_34285,c_33931]) ).
tff(c_33700,plain,
inverse(sk_c3) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33672,c_33144]) ).
tff(c_33363,plain,
! [Z_260] : ( multiply(sk_c10,multiply(sk_c4,Z_260)) = Z_260 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33284]) ).
tff(c_33375,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_33211,c_33363]) ).
tff(c_33379,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33375,c_33136]) ).
tff(c_33387,plain,
multiply(sk_c2,sk_c10) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_33379,c_33349]) ).
tff(c_33486,plain,
! [X_262,Z_263] : ( multiply(inverse(X_262),multiply(X_262,Z_263)) = Z_263 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33296]) ).
tff(c_33504,plain,
multiply(inverse(sk_c2),sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_33387,c_33486]) ).
tff(c_33583,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33504]) ).
tff(c_33525,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_33375,c_33486]) ).
tff(c_33587,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33525]) ).
tff(c_33354,plain,
! [X5_6,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c9) != sk_c11 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_138,c_33136,c_108]) ).
tff(c_33355,plain,
! [X3_8] :
( ( multiply(inverse(X3_8),sk_c9) != sk_c11 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_33354]) ).
tff(c_33410,plain,
! [X3_261] :
( ( multiply(inverse(X3_261),sk_c9) != sk_c10 )
| ( multiply(X3_261,inverse(X3_261)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_33379,c_33379,c_33355]) ).
tff(c_33420,plain,
( ( multiply(sk_c10,sk_c9) != sk_c10 )
| ( multiply(sk_c4,inverse(sk_c4)) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_33122,c_33410]) ).
tff(c_33432,plain,
sk_c9 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33211,c_33122,c_33375,c_33420]) ).
tff(c_33607,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_33587,c_33432]) ).
tff(c_33646,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_33583,c_33607]) ).
tff(c_33647,plain,
! [X1_10,X2_11,X7_9,X5_6] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_33354]) ).
tff(c_33648,plain,
! [X7_9,X5_6] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_33647]) ).
tff(c_33738,plain,
! [X7_266,X5_267] :
( ( inverse(multiply(X7_266,inverse(X5_267))) != inverse(X5_267) )
| ( multiply(X7_266,inverse(X5_267)) != inverse(X7_266) )
| ( multiply(inverse(X5_267),sk_c10) != sk_c10 )
| ( multiply(X5_267,inverse(X5_267)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_33672,c_33672,c_33648]) ).
tff(c_33742,plain,
! [X7_266] :
( ( inverse(multiply(X7_266,sk_c10)) != inverse(sk_c3) )
| ( multiply(X7_266,inverse(sk_c3)) != inverse(X7_266) )
| ( multiply(inverse(sk_c3),sk_c10) != sk_c10 )
| ( multiply(sk_c3,inverse(sk_c3)) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_33700,c_33738]) ).
tff(c_33764,plain,
! [X7_266] :
( ( inverse(multiply(X7_266,sk_c10)) != sk_c10 )
| ( multiply(X7_266,sk_c10) != inverse(X7_266) )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_33696,c_33700,c_33700,c_33700,c_33700,c_33742]) ).
tff(c_63036,plain,
! [X7_429] :
( ( inverse(X7_429) != identity )
| ( inverse(X7_429) != X7_429 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33968,c_34292,c_33968,c_34292,c_33968,c_33968,c_33764]) ).
tff(c_63054,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_34027,c_63036]) ).
tff(c_63068,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34027,c_63054]) ).
tff(c_63069,plain,
! [X2_11,X1_10] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_33647]) ).
tff(c_63158,plain,
! [X2_11,X1_10] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_63093,c_63093,c_63069]) ).
tff(c_63159,plain,
! [X1_10] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_63158]) ).
tff(c_64366,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_63692,c_63330,c_63330,c_63330,c_63159]) ).
tff(c_63412,plain,
multiply(identity,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_63330,c_33325]) ).
tff(c_63414,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63412]) ).
tff(c_63121,plain,
inverse(sk_c3) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_63093,c_33144]) ).
tff(c_63410,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63330,c_63121]) ).
tff(c_63538,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63414,c_63410]) ).
tff(c_64368,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64366,c_63538]) ).
tff(c_64369,plain,
! [X2_11] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_63158]) ).
tff(c_65629,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_64989,c_64525,c_64484,c_64484,c_64369]) ).
tff(c_64533,plain,
multiply(identity,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_64484,c_33325]) ).
tff(c_64534,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_64533]) ).
tff(c_64531,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64484,c_63121]) ).
tff(c_64585,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64534,c_64531]) ).
tff(c_65631,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65629,c_64585]) ).
tff(c_65633,plain,
multiply(sk_c10,sk_c9) != sk_c11,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_65898,plain,
multiply(identity,sk_c9) != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_65890,c_65633]) ).
tff(c_65904,plain,
sk_c9 != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65898]) ).
tff(c_65998,plain,
sk_c9 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_65984,c_65904]) ).
tff(c_65899,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_65890,c_33127]) ).
tff(c_65811,plain,
! [X_2,Z_471] : ( multiply(inverse(X_2),multiply(X_2,Z_471)) = Z_471 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65796]) ).
tff(c_66191,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_65899,c_65811]) ).
tff(c_66203,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_66191]) ).
tff(c_65715,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_33123,c_92]) ).
tff(c_65897,plain,
multiply(sk_c4,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_65890,c_65715]) ).
tff(c_66303,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66203,c_65897]) ).
tff(c_66304,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65998,c_66303]) ).
tff(c_66306,plain,
multiply(sk_c1,sk_c2) != sk_c11,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_48,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_67453,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_66306,c_48]) ).
tff(c_66305,plain,
inverse(sk_c3) = sk_c11,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_66310,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_66305,c_4]) ).
tff(c_67479,plain,
! [X_497,Y_498,Z_499] : ( multiply(multiply(X_497,Y_498),Z_499) = multiply(X_497,multiply(Y_498,Z_499)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_67524,plain,
! [Z_499] : ( multiply(sk_c11,multiply(sk_c3,Z_499)) = multiply(identity,Z_499) ),
inference(superposition,[status(thm),theory(equality)],[c_66310,c_67479]) ).
tff(c_67862,plain,
! [Z_507] : ( multiply(sk_c11,multiply(sk_c3,Z_507)) = Z_507 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67524]) ).
tff(c_67877,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_67453,c_67862]) ).
tff(c_67527,plain,
! [Z_499] : ( multiply(sk_c10,multiply(sk_c11,Z_499)) = multiply(identity,Z_499) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_67479]) ).
tff(c_67546,plain,
! [Z_499] : ( multiply(sk_c10,multiply(sk_c11,Z_499)) = Z_499 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67527]) ).
tff(c_67884,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_67877,c_67546]) ).
tff(c_67890,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_142,c_67884]) ).
tff(c_67550,plain,
! [Z_500] : ( multiply(sk_c10,multiply(sk_c11,Z_500)) = Z_500 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67527]) ).
tff(c_67562,plain,
multiply(sk_c10,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_66310,c_67550]) ).
tff(c_67907,plain,
multiply(identity,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_67890,c_67562]) ).
tff(c_67917,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67907]) ).
tff(c_67923,plain,
multiply(sk_c11,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67917,c_66310]) ).
tff(c_67906,plain,
multiply(sk_c11,identity) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_67890,c_67877]) ).
tff(c_67961,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67923,c_67906]) ).
tff(c_67975,plain,
multiply(sk_c1,sk_c2) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_67961,c_66306]) ).
tff(c_67533,plain,
! [X_2,Z_499] : ( multiply(inverse(X_2),multiply(X_2,Z_499)) = multiply(identity,Z_499) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_67479]) ).
tff(c_68008,plain,
! [X_509,Z_510] : ( multiply(inverse(X_509),multiply(X_509,Z_510)) = Z_510 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67533]) ).
tff(c_68065,plain,
multiply(inverse(sk_c2),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_129,c_68008]) ).
tff(c_67548,plain,
! [X_2,Z_499] : ( multiply(inverse(X_2),multiply(X_2,Z_499)) = Z_499 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67533]) ).
tff(c_68270,plain,
! [X_512,Z_513] : ( multiply(inverse(inverse(X_512)),Z_513) = multiply(X_512,Z_513) ),
inference(superposition,[status(thm),theory(equality)],[c_67548,c_68008]) ).
tff(c_68071,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_68008]) ).
tff(c_68325,plain,
! [X_514] : ( multiply(X_514,identity) = X_514 ),
inference(superposition,[status(thm),theory(equality)],[c_68270,c_68071]) ).
tff(c_68370,plain,
inverse(sk_c2) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_68065,c_68325]) ).
tff(c_68415,plain,
multiply(sk_c1,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68370,c_4]) ).
tff(c_68421,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_67975,c_68415]) ).
tff(c_68423,plain,
inverse(sk_c11) != sk_c10,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_24,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_68474,plain,
inverse(sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_68423,c_24]) ).
tff(c_68478,plain,
multiply(sk_c8,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68474,c_4]) ).
tff(c_26,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_68503,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_68423,c_26]) ).
tff(c_16,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_68517,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_68423,c_16]) ).
tff(c_18,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_68461,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_68423,c_18]) ).
tff(c_68465,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68461,c_4]) ).
tff(c_68546,plain,
! [X_515,Y_516,Z_517] : ( multiply(multiply(X_515,Y_516),Z_517) = multiply(X_515,multiply(Y_516,Z_517)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_68579,plain,
! [Z_517] : ( multiply(sk_c8,multiply(sk_c5,Z_517)) = multiply(identity,Z_517) ),
inference(superposition,[status(thm),theory(equality)],[c_68465,c_68546]) ).
tff(c_68647,plain,
! [Z_520] : ( multiply(sk_c8,multiply(sk_c5,Z_520)) = Z_520 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68579]) ).
tff(c_68659,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_68517,c_68647]) ).
tff(c_68567,plain,
! [Z_517] : ( multiply(sk_c7,multiply(sk_c8,Z_517)) = multiply(sk_c6,Z_517) ),
inference(superposition,[status(thm),theory(equality)],[c_68503,c_68546]) ).
tff(c_68697,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c6,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_68659,c_68567]) ).
tff(c_68703,plain,
multiply(sk_c6,sk_c11) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_68503,c_68697]) ).
tff(c_68576,plain,
! [Z_517] : ( multiply(sk_c8,multiply(sk_c6,Z_517)) = multiply(identity,Z_517) ),
inference(superposition,[status(thm),theory(equality)],[c_68478,c_68546]) ).
tff(c_68602,plain,
! [Z_517] : ( multiply(sk_c8,multiply(sk_c6,Z_517)) = Z_517 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68576]) ).
tff(c_68708,plain,
multiply(sk_c8,sk_c6) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_68703,c_68602]) ).
tff(c_68714,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68478,c_68708]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_68448,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_68423,c_10]) ).
tff(c_68722,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68714,c_68448]) ).
tff(c_68745,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68722,c_4]) ).
tff(c_68594,plain,
! [X_2,Z_517] : ( multiply(inverse(X_2),multiply(X_2,Z_517)) = multiply(identity,Z_517) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_68546]) ).
tff(c_68608,plain,
! [X_2,Z_517] : ( multiply(inverse(X_2),multiply(X_2,Z_517)) = Z_517 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68594]) ).
tff(c_68829,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_68745,c_68608]) ).
tff(c_68841,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_68829]) ).
tff(c_68845,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68841,c_68722]) ).
tff(c_68723,plain,
inverse(identity) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_68714,c_68423]) ).
tff(c_68853,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_68845,c_68723]) ).
tff(c_8,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_68497,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_68423,c_8]) ).
tff(c_68719,plain,
multiply(sk_c3,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_68714,c_68497]) ).
tff(c_68946,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68841,c_68719]) ).
tff(c_68947,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_68853,c_68946]) ).
tff(c_68949,plain,
inverse(sk_c1) != sk_c2,
inference(splitRight,[status(thm)],[c_78]) ).
tff(c_72,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_69061,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_68949,c_72]) ).
tff(c_74,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_68998,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_68949,c_74]) ).
tff(c_69002,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68998,c_4]) ).
tff(c_69118,plain,
! [Z_527] : ( multiply(sk_c10,multiply(sk_c4,Z_527)) = multiply(identity,Z_527) ),
inference(superposition,[status(thm),theory(equality)],[c_69002,c_69085]) ).
tff(c_81138,plain,
! [Z_655] : ( multiply(sk_c10,multiply(sk_c4,Z_655)) = Z_655 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69118]) ).
tff(c_81150,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69061,c_81138]) ).
tff(c_68,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_69026,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_68949,c_68]) ).
tff(c_70,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_68961,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_68949,c_70]) ).
tff(c_68965,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68961,c_4]) ).
tff(c_69127,plain,
! [Z_527] : ( multiply(sk_c11,multiply(sk_c3,Z_527)) = multiply(identity,Z_527) ),
inference(superposition,[status(thm),theory(equality)],[c_68965,c_69085]) ).
tff(c_69252,plain,
! [Z_532] : ( multiply(sk_c11,multiply(sk_c3,Z_532)) = Z_532 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69127]) ).
tff(c_69270,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_69026,c_69252]) ).
tff(c_69292,plain,
! [X_533,Z_534] : ( multiply(inverse(X_533),multiply(X_533,Z_534)) = Z_534 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69133]) ).
tff(c_69313,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69270,c_69292]) ).
tff(c_69405,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_69313]) ).
tff(c_69212,plain,
! [Z_530] : ( multiply(sk_c10,multiply(sk_c4,Z_530)) = Z_530 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69118]) ).
tff(c_69224,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69061,c_69212]) ).
tff(c_22,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_68986,plain,
inverse(sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_69203,plain,
! [X5_6,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c9) != sk_c11 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c11 )
| ( multiply(sk_c10,sk_c9) != sk_c11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_68986,c_108]) ).
tff(c_69204,plain,
multiply(sk_c10,sk_c9) != sk_c11,
inference(splitLeft,[status(thm)],[c_69203]) ).
tff(c_69244,plain,
sk_c11 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69224,c_69204]) ).
tff(c_69423,plain,
sk_c11 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_69405,c_69244]) ).
tff(c_68948,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_78]) ).
tff(c_76,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_69032,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_68949,c_76]) ).
tff(c_69355,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69032,c_69292]) ).
tff(c_69413,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_68948,c_69355]) ).
tff(c_69504,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_69413,c_69147]) ).
tff(c_69510,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_69504]) ).
tff(c_69512,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_69423,c_69510]) ).
tff(c_69514,plain,
multiply(sk_c10,sk_c9) = sk_c11,
inference(splitRight,[status(thm)],[c_69203]) ).
tff(c_81154,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81150,c_69514]) ).
tff(c_68990,plain,
multiply(sk_c10,sk_c11) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68986,c_4]) ).
tff(c_81197,plain,
multiply(sk_c10,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81154,c_68990]) ).
tff(c_80,plain,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_69037,plain,
multiply(sk_c8,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_68949,c_80]) ).
tff(c_81194,plain,
multiply(sk_c8,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81154,c_69037]) ).
tff(c_81195,plain,
multiply(sk_c5,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81154,c_69032]) ).
tff(c_68953,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68948,c_4]) ).
tff(c_69130,plain,
! [Z_527] : ( multiply(sk_c8,multiply(sk_c5,Z_527)) = multiply(identity,Z_527) ),
inference(superposition,[status(thm),theory(equality)],[c_68953,c_69085]) ).
tff(c_83125,plain,
! [Z_692] : ( multiply(sk_c8,multiply(sk_c5,Z_692)) = Z_692 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69130]) ).
tff(c_83137,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_81195,c_83125]) ).
tff(c_83141,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81194,c_83137]) ).
tff(c_83143,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_83141,c_81194]) ).
tff(c_83154,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81197,c_83143]) ).
tff(c_83171,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_83154,c_68998]) ).
tff(c_83277,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_83171,c_4]) ).
tff(c_83306,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_83277,c_69147]) ).
tff(c_83318,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_83306]) ).
tff(c_83169,plain,
multiply(sk_c4,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_83154,c_69061]) ).
tff(c_83406,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_83318,c_83169]) ).
tff(c_81319,plain,
! [X_658,Z_659] : ( multiply(inverse(X_658),multiply(X_658,Z_659)) = Z_659 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69133]) ).
tff(c_81583,plain,
! [X_662,Z_663] : ( multiply(inverse(inverse(X_662)),Z_663) = multiply(X_662,Z_663) ),
inference(superposition,[status(thm),theory(equality)],[c_81319,c_69147]) ).
tff(c_81621,plain,
! [X_662] : ( multiply(X_662,inverse(X_662)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_81583]) ).
tff(c_81260,plain,
! [Z_657] : ( multiply(sk_c8,multiply(sk_c5,Z_657)) = Z_657 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69130]) ).
tff(c_81272,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_81195,c_81260]) ).
tff(c_81276,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81194,c_81272]) ).
tff(c_81278,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81276,c_81194]) ).
tff(c_81289,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81197,c_81278]) ).
tff(c_81340,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_81319]) ).
tff(c_81590,plain,
! [X_662] : ( multiply(X_662,identity) = X_662 ),
inference(superposition,[status(thm),theory(equality)],[c_81583,c_81340]) ).
tff(c_81306,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81289,c_68998]) ).
tff(c_81412,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_81306,c_4]) ).
tff(c_81441,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_81412,c_69147]) ).
tff(c_81453,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_81441]) ).
tff(c_81304,plain,
multiply(sk_c4,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_81289,c_69061]) ).
tff(c_81541,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81453,c_81304]) ).
tff(c_69530,plain,
! [Z_536] : ( multiply(sk_c10,multiply(sk_c4,Z_536)) = Z_536 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69118]) ).
tff(c_69542,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69061,c_69530]) ).
tff(c_69546,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69542,c_69514]) ).
tff(c_69589,plain,
multiply(sk_c10,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69546,c_68990]) ).
tff(c_69586,plain,
multiply(sk_c8,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69546,c_69037]) ).
tff(c_69587,plain,
multiply(sk_c5,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69546,c_69032]) ).
tff(c_69730,plain,
! [X_541,Z_542] : ( multiply(inverse(X_541),multiply(X_541,Z_542)) = Z_542 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69133]) ).
tff(c_69769,plain,
multiply(inverse(sk_c5),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69587,c_69730]) ).
tff(c_69845,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69586,c_68948,c_69769]) ).
tff(c_86,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_69055,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_68949,c_86]) ).
tff(c_82,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_69011,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_68949,c_82]) ).
tff(c_69015,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69011,c_4]) ).
tff(c_69115,plain,
! [Z_527] : ( multiply(sk_c6,multiply(sk_c7,Z_527)) = multiply(identity,Z_527) ),
inference(superposition,[status(thm),theory(equality)],[c_69015,c_69085]) ).
tff(c_69149,plain,
! [Z_528] : ( multiply(sk_c6,multiply(sk_c7,Z_528)) = Z_528 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69115]) ).
tff(c_69161,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69055,c_69149]) ).
tff(c_84,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_68973,plain,
inverse(sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_68949,c_84]) ).
tff(c_68977,plain,
multiply(sk_c8,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68973,c_4]) ).
tff(c_69124,plain,
! [Z_527] : ( multiply(sk_c8,multiply(sk_c6,Z_527)) = multiply(identity,Z_527) ),
inference(superposition,[status(thm),theory(equality)],[c_68977,c_69085]) ).
tff(c_69172,plain,
! [Z_529] : ( multiply(sk_c8,multiply(sk_c6,Z_529)) = Z_529 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69124]) ).
tff(c_69184,plain,
multiply(sk_c8,sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_69161,c_69172]) ).
tff(c_69860,plain,
multiply(sk_c10,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_69845,c_69845,c_69184]) ).
tff(c_69871,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69589,c_69860]) ).
tff(c_69588,plain,
multiply(sk_c3,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69546,c_69026]) ).
tff(c_69145,plain,
! [Z_527] : ( multiply(sk_c11,multiply(sk_c3,Z_527)) = Z_527 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69127]) ).
tff(c_69713,plain,
! [Z_540] : ( multiply(sk_c10,multiply(sk_c3,Z_540)) = Z_540 ),
inference(demodulation,[status(thm),theory(equality)],[c_69546,c_69145]) ).
tff(c_69725,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69588,c_69713]) ).
tff(c_69729,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69589,c_69725]) ).
tff(c_69554,plain,
! [Z_537] : ( multiply(sk_c5,multiply(sk_c8,Z_537)) = multiply(sk_c11,Z_537) ),
inference(superposition,[status(thm),theory(equality)],[c_69032,c_69085]) ).
tff(c_69578,plain,
multiply(sk_c5,identity) = multiply(sk_c11,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_68977,c_69554]) ).
tff(c_69693,plain,
multiply(sk_c5,identity) = multiply(sk_c10,sk_c6),
inference(demodulation,[status(thm),theory(equality)],[c_69546,c_69578]) ).
tff(c_69581,plain,
multiply(sk_c5,identity) = multiply(sk_c11,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_68953,c_69554]) ).
tff(c_69702,plain,
multiply(sk_c10,sk_c6) = multiply(sk_c10,sk_c5),
inference(demodulation,[status(thm),theory(equality)],[c_69693,c_69546,c_69581]) ).
tff(c_69884,plain,
multiply(identity,sk_c6) = multiply(identity,sk_c5),
inference(demodulation,[status(thm),theory(equality)],[c_69729,c_69729,c_69702]) ).
tff(c_69896,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_69884]) ).
tff(c_69958,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69871,c_69896]) ).
tff(c_69868,plain,
inverse(sk_c5) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69845,c_68948]) ).
tff(c_69984,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69958,c_69729,c_69868]) ).
tff(c_70083,plain,
! [X_545,Z_546] : ( multiply(inverse(inverse(X_545)),Z_546) = multiply(X_545,Z_546) ),
inference(superposition,[status(thm),theory(equality)],[c_69147,c_69730]) ).
tff(c_69832,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_69730]) ).
tff(c_70090,plain,
! [X_545] : ( multiply(X_545,identity) = X_545 ),
inference(superposition,[status(thm),theory(equality)],[c_70083,c_69832]) ).
tff(c_69592,plain,
inverse(sk_c3) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69546,c_68961]) ).
tff(c_69513,plain,
! [X5_6,X3_8,X1_10,X7_9,X2_11] :
( ( multiply(inverse(X3_8),sk_c9) != sk_c11 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c11 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_69203]) ).
tff(c_69522,plain,
! [X7_9,X5_6] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_69513]) ).
tff(c_69626,plain,
! [X7_538,X5_539] :
( ( inverse(multiply(X7_538,inverse(X5_539))) != inverse(X5_539) )
| ( multiply(X7_538,inverse(X5_539)) != inverse(X7_538) )
| ( multiply(inverse(X5_539),sk_c10) != sk_c10 )
| ( multiply(X5_539,inverse(X5_539)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_69546,c_69546,c_69522]) ).
tff(c_69630,plain,
! [X7_538] :
( ( inverse(multiply(X7_538,sk_c10)) != inverse(sk_c3) )
| ( multiply(X7_538,inverse(sk_c3)) != inverse(X7_538) )
| ( multiply(inverse(sk_c3),sk_c10) != sk_c10 )
| ( multiply(sk_c3,inverse(sk_c3)) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_69592,c_69626]) ).
tff(c_69650,plain,
! [X7_538] :
( ( inverse(multiply(X7_538,sk_c10)) != sk_c10 )
| ( multiply(X7_538,sk_c10) != inverse(X7_538) )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_69588,c_69592,c_69592,c_69592,c_69592,c_69630]) ).
tff(c_81111,plain,
! [X7_654] :
( ( inverse(X7_654) != identity )
| ( inverse(X7_654) != X7_654 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69729,c_70090,c_69729,c_70090,c_69729,c_69729,c_69650]) ).
tff(c_81121,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_69984,c_81111]) ).
tff(c_81129,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_69984,c_81121]) ).
tff(c_81130,plain,
! [X2_11,X1_10,X3_8] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c9) != sk_c11 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_69513]) ).
tff(c_81233,plain,
! [X2_11,X1_10,X3_8] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c9) != sk_c10 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_81154,c_81154,c_81154,c_81154,c_81130]) ).
tff(c_81234,plain,
! [X3_8] :
( ( multiply(inverse(X3_8),sk_c9) != sk_c10 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_81233]) ).
tff(c_83096,plain,
! [X3_8] : ( inverse(X3_8) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_81621,c_81289,c_81590,c_81541,c_81289,c_81234]) ).
tff(c_81280,plain,
multiply(sk_c10,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_81276,c_81276,c_69184]) ).
tff(c_81290,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81197,c_81280]) ).
tff(c_81286,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81276,c_68973]) ).
tff(c_81393,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81290,c_81289,c_81286]) ).
tff(c_83098,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_83096,c_81393]) ).
tff(c_83099,plain,
! [X1_10,X2_11] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_81233]) ).
tff(c_86676,plain,
! [X1_10,X2_11] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_83455,c_83406,c_83154,c_83154,c_83455,c_83154,c_83154,c_83154,c_83099]) ).
tff(c_86678,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_86676]) ).
tff(c_83145,plain,
multiply(sk_c10,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_83141,c_83141,c_69184]) ).
tff(c_83155,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81197,c_83145]) ).
tff(c_83151,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_83141,c_68973]) ).
tff(c_83258,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_83155,c_83154,c_83151]) ).
tff(c_86680,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_86678,c_83258]) ).
tff(c_86682,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_86676]) ).
tff(c_86684,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_86682,c_83258]) ).
tff(c_86686,plain,
inverse(sk_c11) != sk_c10,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_86721,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_86686,c_16]) ).
tff(c_86786,plain,
! [X_749,Y_750,Z_751] : ( multiply(multiply(X_749,Y_750),Z_751) = multiply(X_749,multiply(Y_750,Z_751)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_86828,plain,
! [Z_751] : ( multiply(sk_c8,multiply(sk_c5,Z_751)) = multiply(identity,Z_751) ),
inference(superposition,[status(thm),theory(equality)],[c_68953,c_86786]) ).
tff(c_86894,plain,
! [Z_754] : ( multiply(sk_c8,multiply(sk_c5,Z_754)) = Z_754 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_86828]) ).
tff(c_86906,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_86721,c_86894]) ).
tff(c_86831,plain,
! [X_2,Z_751] : ( multiply(inverse(X_2),multiply(X_2,Z_751)) = multiply(identity,Z_751) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_86786]) ).
tff(c_87012,plain,
! [X_757,Z_758] : ( multiply(inverse(X_757),multiply(X_757,Z_758)) = Z_758 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_86831]) ).
tff(c_87045,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_86906,c_87012]) ).
tff(c_87122,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_87045]) ).
tff(c_86747,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_86686,c_8]) ).
tff(c_87066,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_86747,c_87012]) ).
tff(c_87124,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_68961,c_87066]) ).
tff(c_87269,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_87122,c_2,c_87122,c_87124]) ).
tff(c_87142,plain,
inverse(identity) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_87122,c_86686]) ).
tff(c_87271,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_87269,c_87142]) ).
tff(c_86694,plain,
inverse(sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_86695,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_86686,c_86694]) ).
tff(c_86696,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_86701,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_86696,c_4]) ).
tff(c_87273,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_87269,c_86701]) ).
tff(c_86844,plain,
! [X_2,Z_751] : ( multiply(inverse(X_2),multiply(X_2,Z_751)) = Z_751 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_86831]) ).
tff(c_87307,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_87273,c_86844]) ).
tff(c_87319,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_87307]) ).
tff(c_87274,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_87269,c_86696]) ).
tff(c_87323,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_87319,c_87274]) ).
tff(c_87326,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_87271,c_87323]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP379-1 : TPTP v9.0.0. Released v2.5.0.
% 0.07/0.12 % 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.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 21:44:35 EDT 2025
% 0.12/0.33 % CPUTime :
% 19.44/8.17 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.56/8.24
% 19.56/8.24 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------