%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP366-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 : n010.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:03 PM UTC 2025
% Result : Unsatisfiable 21.42s 9.55s
% Output : CNFRefutation 21.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 49
% Syntax : Number of formulae : 825 ( 690 unt; 0 typ; 0 def)
% Number of atoms : 1131 (1095 equ)
% Maximal formula atoms : 16 ( 1 avg)
% Number of connectives : 629 ( 323 ~; 306 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 2 avg)
% Maximal term depth : 4 ( 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 : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 379 ( 379 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > 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_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_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
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_209,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( inverse(sk_c6) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_236,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( inverse(sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( inverse(sk_c5) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_290,axiom,
! [X5,X6,X3,X7,X1,X2,X4] :
( ( multiply(sk_c8,sk_c10) != sk_c9 )
| ( multiply(sk_c10,X4) != sk_c9 )
| ( multiply(X5,sk_c10) != X4 )
| ( inverse(X5) != sk_c10 )
| ( multiply(X6,sk_c8) != sk_c10 )
| ( inverse(X6) != sk_c8 )
| ( multiply(sk_c9,sk_c10) != sk_c8 )
| ( multiply(X1,sk_c10) != sk_c9 )
| ( inverse(X1) != sk_c10 )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( inverse(X2) != sk_c9 )
| ( multiply(X2,sk_c8) != sk_c9 )
| ( inverse(X3) != X7 )
| ( inverse(X7) != sk_c10 )
| ( multiply(X3,sk_c10) != X7 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( inverse(sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( inverse(sk_c5) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_191,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_194,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( inverse(sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( inverse(sk_c5) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_200,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( inverse(sk_c5) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_197,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_206,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_212,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_173,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c5) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_182,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_176,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_179,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c6) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_239,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c6) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_215,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_224,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_218,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_221,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_227,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_242,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_81335,plain,
! [X_771,Y_772,Z_773] : ( multiply(multiply(X_771,Y_772),Z_773) = multiply(X_771,multiply(Y_772,Z_773)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_81383,plain,
! [X_2,Z_773] : ( multiply(inverse(X_2),multiply(X_2,Z_773)) = multiply(identity,Z_773) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_81335]) ).
tff(c_81397,plain,
! [X_2,Z_773] : ( multiply(inverse(X_2),multiply(X_2,Z_773)) = Z_773 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81383]) ).
tff(c_83075,plain,
! [X_803,Z_804] : ( multiply(inverse(X_803),multiply(X_803,Z_804)) = Z_804 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81383]) ).
tff(c_83321,plain,
! [X_808,Z_809] : ( multiply(inverse(inverse(X_808)),Z_809) = multiply(X_808,Z_809) ),
inference(superposition,[status(thm),theory(equality)],[c_81397,c_83075]) ).
tff(c_83096,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_83075]) ).
tff(c_83328,plain,
! [X_808] : ( multiply(X_808,identity) = X_808 ),
inference(superposition,[status(thm),theory(equality)],[c_83321,c_83096]) ).
tff(c_46924,plain,
! [X_512,Y_513,Z_514] : ( multiply(multiply(X_512,Y_513),Z_514) = multiply(X_512,multiply(Y_513,Z_514)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_46972,plain,
! [X_2,Z_514] : ( multiply(inverse(X_2),multiply(X_2,Z_514)) = multiply(identity,Z_514) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_46924]) ).
tff(c_46986,plain,
! [X_2,Z_514] : ( multiply(inverse(X_2),multiply(X_2,Z_514)) = Z_514 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46972]) ).
tff(c_49920,plain,
! [X_567,Z_568] : ( multiply(inverse(X_567),multiply(X_567,Z_568)) = Z_568 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46972]) ).
tff(c_50227,plain,
! [X_571,Z_572] : ( multiply(inverse(inverse(X_571)),Z_572) = multiply(X_571,Z_572) ),
inference(superposition,[status(thm),theory(equality)],[c_46986,c_49920]) ).
tff(c_49980,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_49920]) ).
tff(c_50234,plain,
! [X_571] : ( multiply(X_571,identity) = X_571 ),
inference(superposition,[status(thm),theory(equality)],[c_50227,c_49980]) ).
tff(c_104,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_177,plain,
multiply(sk_c3,sk_c8) = sk_c10,
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_122,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_236]) ).
tff(c_145,plain,
inverse(sk_c3) = sk_c8,
inference(splitLeft,[status(thm)],[c_122]) ).
tff(c_149,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_145,c_4]) ).
tff(c_39970,plain,
! [X_394,Y_395,Z_396] : ( multiply(multiply(X_394,Y_395),Z_396) = multiply(X_394,multiply(Y_395,Z_396)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_40021,plain,
! [Z_396] : ( multiply(sk_c8,multiply(sk_c3,Z_396)) = multiply(identity,Z_396) ),
inference(superposition,[status(thm),theory(equality)],[c_149,c_39970]) ).
tff(c_40054,plain,
! [Z_398] : ( multiply(sk_c8,multiply(sk_c3,Z_398)) = Z_398 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40021]) ).
tff(c_40066,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_40054]) ).
tff(c_28380,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_28437,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_28380]) ).
tff(c_28452,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_28437]) ).
tff(c_30956,plain,
! [X_287,Z_288] : ( multiply(inverse(X_287),multiply(X_287,Z_288)) = Z_288 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28437]) ).
tff(c_31441,plain,
! [X_292,Z_293] : ( multiply(inverse(inverse(X_292)),Z_293) = multiply(X_292,Z_293) ),
inference(superposition,[status(thm),theory(equality)],[c_28452,c_30956]) ).
tff(c_31055,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_30956]) ).
tff(c_31448,plain,
! [X_292] : ( multiply(X_292,identity) = X_292 ),
inference(superposition,[status(thm),theory(equality)],[c_31441,c_31055]) ).
tff(c_28434,plain,
! [Z_241] : ( multiply(sk_c8,multiply(sk_c3,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_149,c_28380]) ).
tff(c_28692,plain,
! [Z_247] : ( multiply(sk_c8,multiply(sk_c3,Z_247)) = Z_247 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28434]) ).
tff(c_28704,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_28692]) ).
tff(c_14,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_185,plain,
multiply(sk_c8,sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_28708,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28704,c_185]) ).
tff(c_26597,plain,
! [X_209,Y_210,Z_211] : ( multiply(multiply(X_209,Y_210),Z_211) = multiply(X_209,multiply(Y_210,Z_211)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_26654,plain,
! [Z_211] : ( multiply(sk_c8,multiply(sk_c3,Z_211)) = multiply(identity,Z_211) ),
inference(superposition,[status(thm),theory(equality)],[c_149,c_26597]) ).
tff(c_26961,plain,
! [Z_218] : ( multiply(sk_c8,multiply(sk_c3,Z_218)) = Z_218 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26654]) ).
tff(c_26973,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_26961]) ).
tff(c_26977,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_26973,c_185]) ).
tff(c_58,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_191,plain,
multiply(sk_c1,sk_c10) = sk_c2,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_74,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_157,plain,
inverse(sk_c1) = sk_c10,
inference(splitLeft,[status(thm)],[c_74]) ).
tff(c_161,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_157,c_4]) ).
tff(c_26651,plain,
! [Z_211] : ( multiply(sk_c10,multiply(sk_c1,Z_211)) = multiply(identity,Z_211) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_26597]) ).
tff(c_26674,plain,
! [Z_212] : ( multiply(sk_c10,multiply(sk_c1,Z_212)) = Z_212 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26651]) ).
tff(c_26686,plain,
multiply(sk_c10,sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_191,c_26674]) ).
tff(c_243,plain,
! [X_15,Y_16,Z_17] : ( multiply(multiply(X_15,Y_16),Z_17) = multiply(X_15,multiply(Y_16,Z_17)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_270,plain,
! [Z_17] : ( multiply(sk_c10,multiply(sk_c1,Z_17)) = multiply(identity,Z_17) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_243]) ).
tff(c_288,plain,
! [Z_18] : ( multiply(sk_c10,multiply(sk_c1,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_270]) ).
tff(c_300,plain,
multiply(sk_c10,sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_191,c_288]) ).
tff(c_32,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_200,plain,
multiply(sk_c10,sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_304,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_300,c_200]) ).
tff(c_312,plain,
multiply(sk_c8,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_304,c_185]) ).
tff(c_276,plain,
! [X_2,Z_17] : ( multiply(inverse(X_2),multiply(X_2,Z_17)) = multiply(identity,Z_17) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_243]) ).
tff(c_430,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_276]) ).
tff(c_463,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_430]) ).
tff(c_487,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_312,c_145,c_463]) ).
tff(c_273,plain,
! [Z_17] : ( multiply(sk_c8,multiply(sk_c3,Z_17)) = multiply(identity,Z_17) ),
inference(superposition,[status(thm),theory(equality)],[c_149,c_243]) ).
tff(c_327,plain,
! [Z_19] : ( multiply(sk_c8,multiply(sk_c3,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_273]) ).
tff(c_339,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_327]) ).
tff(c_343,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_312,c_339]) ).
tff(c_346,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_343,c_312]) ).
tff(c_128,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( inverse(sk_c9) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_290]) ).
tff(c_325,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) )
| ( multiply(X2_11,sk_c8) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c10 )
| ( inverse(sk_c10) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_312,c_304,c_304,c_304,c_304,c_304,c_304,c_304,c_304,c_128]) ).
tff(c_326,plain,
multiply(sk_c10,sk_c10) != sk_c8,
inference(splitLeft,[status(thm)],[c_325]) ).
tff(c_345,plain,
multiply(sk_c10,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_343,c_326]) ).
tff(c_427,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_346,c_345]) ).
tff(c_429,plain,
multiply(sk_c10,sk_c10) = sk_c8,
inference(splitRight,[status(thm)],[c_325]) ).
tff(c_535,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_487,c_429]) ).
tff(c_286,plain,
! [X_2,Z_17] : ( multiply(inverse(X_2),multiply(X_2,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_276]) ).
tff(c_539,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_535,c_286]) ).
tff(c_545,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_539]) ).
tff(c_491,plain,
multiply(sk_c10,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_487,c_149]) ).
tff(c_590,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_545,c_491]) ).
tff(c_492,plain,
inverse(sk_c3) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_487,c_145]) ).
tff(c_550,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_545,c_492]) ).
tff(c_591,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_590,c_550]) ).
tff(c_725,plain,
! [X_25,Z_26] : ( multiply(inverse(inverse(X_25)),Z_26) = multiply(X_25,Z_26) ),
inference(superposition,[status(thm),theory(equality)],[c_286,c_430]) ).
tff(c_478,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_430]) ).
tff(c_736,plain,
! [X_25] : ( multiply(X_25,identity) = X_25 ),
inference(superposition,[status(thm),theory(equality)],[c_725,c_478]) ).
tff(c_551,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_545,c_487]) ).
tff(c_428,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(sk_c10) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c10 )
| ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c10 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c10 )
| ( multiply(X2_11,sk_c8) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) ) ),
inference(splitRight,[status(thm)],[c_325]) ).
tff(c_7367,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( identity != X2_11 )
| ( inverse(X2_11) != identity )
| ( inverse(X3_8) != identity )
| ( inverse(X3_8) != X3_8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_736,c_545,c_736,c_545,c_545,c_545,c_736,c_551,c_545,c_736,c_545,c_545,c_545,c_736,c_551,c_545,c_551,c_736,c_545,c_545,c_2,c_545,c_545,c_551,c_545,c_2,c_545,c_591,c_551,c_545,c_428]) ).
tff(c_7369,plain,
! [X3_107] :
( ( inverse(X3_107) != identity )
| ( inverse(X3_107) != X3_107 ) ),
inference(splitLeft,[status(thm)],[c_7367]) ).
tff(c_7377,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_591,c_7369]) ).
tff(c_7384,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_591,c_7377]) ).
tff(c_7385,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( identity != X2_11 )
| ( inverse(X2_11) != identity )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(splitRight,[status(thm)],[c_7367]) ).
tff(c_23272,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_7385]) ).
tff(c_23274,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23272,c_591]) ).
tff(c_23275,plain,
! [X6_7,X1_10,X2_11] :
( ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( identity != X2_11 )
| ( inverse(X2_11) != identity ) ),
inference(splitRight,[status(thm)],[c_7385]) ).
tff(c_25195,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_23275]) ).
tff(c_25197,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25195,c_591]) ).
tff(c_25198,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(splitRight,[status(thm)],[c_23275]) ).
tff(c_25200,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25198]) ).
tff(c_25202,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25200,c_591]) ).
tff(c_26479,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_25198]) ).
tff(c_26481,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26479,c_591]) ).
tff(c_26483,plain,
multiply(sk_c10,sk_c2) != sk_c9,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_26690,plain,
sk_c9 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_26686,c_26483]) ).
tff(c_26985,plain,
sk_c8 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_26977,c_26690]) ).
tff(c_36,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_26577,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_26483,c_36]) ).
tff(c_26987,plain,
multiply(sk_c10,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_26977,c_26577]) ).
tff(c_26482,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_30,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_26559,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_26483,c_30]) ).
tff(c_26989,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_26977,c_26559]) ).
tff(c_26657,plain,
! [X_2,Z_211] : ( multiply(inverse(X_2),multiply(X_2,Z_211)) = multiply(identity,Z_211) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_26597]) ).
tff(c_27131,plain,
! [X_221,Z_222] : ( multiply(inverse(X_221),multiply(X_221,Z_222)) = Z_222 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26657]) ).
tff(c_27167,plain,
multiply(inverse(sk_c4),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_26989,c_27131]) ).
tff(c_27249,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_26987,c_26482,c_27167]) ).
tff(c_27251,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26985,c_27249]) ).
tff(c_27253,plain,
multiply(sk_c1,sk_c10) != sk_c2,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_54,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_28311,plain,
inverse(sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_27253,c_54]) ).
tff(c_28315,plain,
multiply(sk_c8,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28311,c_4]) ).
tff(c_28720,plain,
multiply(sk_c8,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28708,c_28315]) ).
tff(c_28721,plain,
inverse(sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28708,c_28311]) ).
tff(c_31007,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_28704,c_30956]) ).
tff(c_31070,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28720,c_28721,c_31007]) ).
tff(c_27252,plain,
inverse(sk_c5) = sk_c9,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_28724,plain,
inverse(sk_c5) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28708,c_27252]) ).
tff(c_27376,plain,
! [X_223,Y_224,Z_225] : ( multiply(multiply(X_223,Y_224),Z_225) = multiply(X_223,multiply(Y_224,Z_225)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_27433,plain,
! [Z_225] : ( multiply(sk_c8,multiply(sk_c3,Z_225)) = multiply(identity,Z_225) ),
inference(superposition,[status(thm),theory(equality)],[c_149,c_27376]) ).
tff(c_27599,plain,
! [Z_229] : ( multiply(sk_c8,multiply(sk_c3,Z_229)) = Z_229 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27433]) ).
tff(c_27611,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_27599]) ).
tff(c_27615,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27611,c_185]) ).
tff(c_27287,plain,
inverse(sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_27253,c_54]) ).
tff(c_27721,plain,
inverse(sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27615,c_27287]) ).
tff(c_27733,plain,
multiply(sk_c8,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27721,c_4]) ).
tff(c_50,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_27343,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_27253,c_50]) ).
tff(c_27718,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27615,c_27343]) ).
tff(c_52,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_27303,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_27253,c_52]) ).
tff(c_27307,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27303,c_4]) ).
tff(c_27409,plain,
! [Z_225] : ( multiply(sk_c10,multiply(sk_c4,Z_225)) = multiply(identity,Z_225) ),
inference(superposition,[status(thm),theory(equality)],[c_27307,c_27376]) ).
tff(c_27857,plain,
! [Z_233] : ( multiply(sk_c10,multiply(sk_c4,Z_233)) = Z_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27409]) ).
tff(c_27872,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_27718,c_27857]) ).
tff(c_27424,plain,
! [Z_225] : ( multiply(sk_c8,multiply(sk_c10,Z_225)) = multiply(sk_c9,Z_225) ),
inference(superposition,[status(thm),theory(equality)],[c_185,c_27376]) ).
tff(c_27808,plain,
! [Z_225] : ( multiply(sk_c8,multiply(sk_c10,Z_225)) = multiply(sk_c8,Z_225) ),
inference(demodulation,[status(thm),theory(equality)],[c_27615,c_27424]) ).
tff(c_27880,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c8,sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_27872,c_27808]) ).
tff(c_27886,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27733,c_27611,c_27880]) ).
tff(c_56,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_27362,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_27253,c_56]) ).
tff(c_27717,plain,
multiply(sk_c10,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27615,c_27362]) ).
tff(c_27876,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_27872,c_27717]) ).
tff(c_27986,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27886,c_27876]) ).
tff(c_27265,plain,
multiply(sk_c10,sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_27722,plain,
multiply(sk_c10,sk_c2) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27615,c_27265]) ).
tff(c_27893,plain,
multiply(sk_c10,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_27876,c_27722]) ).
tff(c_28246,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27986,c_2,c_27986,c_27893]) ).
tff(c_28002,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27986,c_157]) ).
tff(c_28118,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28002,c_4]) ).
tff(c_27436,plain,
! [X_2,Z_225] : ( multiply(inverse(X_2),multiply(X_2,Z_225)) = multiply(identity,Z_225) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_27376]) ).
tff(c_27451,plain,
! [X_2,Z_225] : ( multiply(inverse(X_2),multiply(X_2,Z_225)) = Z_225 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27436]) ).
tff(c_28214,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_28118,c_27451]) ).
tff(c_28226,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_28214]) ).
tff(c_28000,plain,
multiply(sk_c1,identity) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_27986,c_27253]) ).
tff(c_28261,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28246,c_2,c_28226,c_28000]) ).
tff(c_28263,plain,
multiply(sk_c10,sk_c2) != sk_c9,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_40,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_28364,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_28263,c_40]) ).
tff(c_28716,plain,
multiply(sk_c5,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28708,c_28364]) ).
tff(c_30992,plain,
multiply(inverse(sk_c5),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_28716,c_30956]) ).
tff(c_31067,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28720,c_28724,c_30992]) ).
tff(c_28859,plain,
! [X_250,Z_251] : ( multiply(inverse(X_250),multiply(X_250,Z_251)) = Z_251 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28437]) ).
tff(c_28910,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_28704,c_28859]) ).
tff(c_28973,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_28910]) ).
tff(c_28345,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_28263,c_30]) ).
tff(c_28717,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28708,c_28345]) ).
tff(c_28262,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_28268,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28262,c_4]) ).
tff(c_28419,plain,
! [Z_241] : ( multiply(sk_c10,multiply(sk_c4,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_28268,c_28380]) ).
tff(c_28835,plain,
! [Z_249] : ( multiply(sk_c10,multiply(sk_c4,Z_249)) = Z_249 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28419]) ).
tff(c_28847,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_28717,c_28835]) ).
tff(c_28340,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_28263,c_36]) ).
tff(c_28718,plain,
multiply(sk_c10,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28708,c_28340]) ).
tff(c_28851,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_28847,c_28718]) ).
tff(c_29008,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28973,c_28851]) ).
tff(c_29013,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29008,c_29008,c_28721]) ).
tff(c_29319,plain,
! [X_255,Z_256] : ( multiply(inverse(inverse(X_255)),Z_256) = multiply(X_255,Z_256) ),
inference(superposition,[status(thm),theory(equality)],[c_28452,c_28859]) ).
tff(c_28958,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_28859]) ).
tff(c_29326,plain,
! [X_255] : ( multiply(X_255,identity) = X_255 ),
inference(superposition,[status(thm),theory(equality)],[c_29319,c_28958]) ).
tff(c_28431,plain,
! [Z_241] : ( multiply(sk_c10,multiply(sk_c1,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_28380]) ).
tff(c_28450,plain,
! [Z_241] : ( multiply(sk_c10,multiply(sk_c1,Z_241)) = Z_241 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28431]) ).
tff(c_28470,plain,
! [Z_243] : ( multiply(sk_c8,multiply(sk_c3,Z_243)) = Z_243 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28434]) ).
tff(c_28482,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_28470]) ).
tff(c_28486,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28482,c_185]) ).
tff(c_48,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_28335,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_27253,c_48]) ).
tff(c_28468,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_185,c_28335,c_28311,c_28340,c_128]) ).
tff(c_28469,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_28468]) ).
tff(c_28523,plain,
! [X5_244] :
( ( inverse(X5_244) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_244,sk_c10)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28486,c_28469]) ).
tff(c_28530,plain,
( ( inverse(sk_c1) != sk_c10 )
| ( sk_c8 != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_28450,c_28523]) ).
tff(c_28548,plain,
sk_c8 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_157,c_28530]) ).
tff(c_28496,plain,
multiply(sk_c10,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28486,c_28340]) ).
tff(c_28495,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28486,c_28345]) ).
tff(c_28594,plain,
! [X_245,Z_246] : ( multiply(inverse(X_245),multiply(X_245,Z_246)) = Z_246 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28437]) ).
tff(c_28615,plain,
multiply(inverse(sk_c4),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_28495,c_28594]) ).
tff(c_28688,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_28496,c_28262,c_28615]) ).
tff(c_28690,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28548,c_28688]) ).
tff(c_28691,plain,
! [X6_7,X1_10,X2_11,X3_8] :
( ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 )
| ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) ) ),
inference(splitRight,[status(thm)],[c_28468]) ).
tff(c_28784,plain,
! [X6_7,X1_10,X2_11,X3_8] :
( ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28708,c_28708,c_28708,c_28691]) ).
tff(c_28785,plain,
! [X3_8] :
( ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) ) ),
inference(splitLeft,[status(thm)],[c_28784]) ).
tff(c_30869,plain,
! [X3_285] :
( ( inverse(X3_285) != identity )
| ( inverse(X3_285) != X3_285 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29326,c_28973,c_29326,c_28973,c_28973,c_28785]) ).
tff(c_30875,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_29013,c_30869]) ).
tff(c_30881,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_29013,c_30875]) ).
tff(c_30882,plain,
! [X2_11,X1_10,X6_7] :
( ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_28784]) ).
tff(c_38929,plain,
! [X2_11,X1_10,X6_7] :
( ( identity != X2_11 )
| ( inverse(X2_11) != identity )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_31448,c_31070,c_31067,c_31067,c_31448,c_31070,c_31067,c_31070,c_31067,c_31448,c_31067,c_31067,c_30882]) ).
tff(c_38931,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_38929]) ).
tff(c_30932,plain,
! [Z_286] : ( multiply(sk_c10,multiply(sk_c4,Z_286)) = Z_286 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28419]) ).
tff(c_30944,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_28717,c_30932]) ).
tff(c_30948,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_30944,c_28718]) ).
tff(c_31086,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_30948,c_30948,c_28721]) ).
tff(c_31179,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31070,c_31070,c_31086]) ).
tff(c_38933,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38931,c_31179]) ).
tff(c_38934,plain,
! [X1_10,X2_11] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( identity != X2_11 )
| ( inverse(X2_11) != identity ) ),
inference(splitRight,[status(thm)],[c_38929]) ).
tff(c_38936,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_38934]) ).
tff(c_38938,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38936,c_31179]) ).
tff(c_38941,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_38934]) ).
tff(c_38943,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38941,c_31179]) ).
tff(c_38945,plain,
multiply(sk_c8,sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_40072,plain,
sk_c9 != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_40066,c_38945]) ).
tff(c_40024,plain,
! [X_2,Z_396] : ( multiply(inverse(X_2),multiply(X_2,Z_396)) = multiply(identity,Z_396) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39970]) ).
tff(c_40120,plain,
! [X_401,Z_402] : ( multiply(inverse(X_401),multiply(X_401,Z_402)) = Z_402 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40024]) ).
tff(c_40147,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_40066,c_40120]) ).
tff(c_40227,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40147]) ).
tff(c_39572,plain,
! [X_386,Y_387,Z_388] : ( multiply(multiply(X_386,Y_387),Z_388) = multiply(X_386,multiply(Y_387,Z_388)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_39626,plain,
! [Z_388] : ( multiply(sk_c8,multiply(sk_c3,Z_388)) = multiply(identity,Z_388) ),
inference(superposition,[status(thm),theory(equality)],[c_149,c_39572]) ).
tff(c_39672,plain,
! [Z_390] : ( multiply(sk_c8,multiply(sk_c3,Z_390)) = Z_390 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39626]) ).
tff(c_39684,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_39672]) ).
tff(c_39688,plain,
sk_c9 != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_39684,c_38945]) ).
tff(c_39629,plain,
! [X_2,Z_388] : ( multiply(inverse(X_2),multiply(X_2,Z_388)) = multiply(identity,Z_388) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39572]) ).
tff(c_39712,plain,
! [X_392,Z_393] : ( multiply(inverse(X_392),multiply(X_392,Z_393)) = Z_393 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39629]) ).
tff(c_39733,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_39684,c_39712]) ).
tff(c_39818,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39733]) ).
tff(c_38958,plain,
multiply(sk_c1,sk_c10) = sk_c2,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_39074,plain,
! [X_378,Y_379,Z_380] : ( multiply(multiply(X_378,Y_379),Z_380) = multiply(X_378,multiply(Y_379,Z_380)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_39128,plain,
! [Z_380] : ( multiply(sk_c10,multiply(sk_c1,Z_380)) = multiply(identity,Z_380) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_39074]) ).
tff(c_39151,plain,
! [Z_381] : ( multiply(sk_c10,multiply(sk_c1,Z_381)) = Z_381 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39128]) ).
tff(c_39163,plain,
multiply(sk_c10,sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_38958,c_39151]) ).
tff(c_38,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_38975,plain,
multiply(sk_c10,sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_39167,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_39163,c_38975]) ).
tff(c_38944,plain,
inverse(sk_c9) = sk_c8,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_38949,plain,
multiply(sk_c8,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38944,c_4]) ).
tff(c_39181,plain,
multiply(sk_c8,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39167,c_38949]) ).
tff(c_39182,plain,
multiply(sk_c8,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_39167,c_38945]) ).
tff(c_39338,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_39181,c_39182]) ).
tff(c_39134,plain,
! [X_2,Z_380] : ( multiply(inverse(X_2),multiply(X_2,Z_380)) = multiply(identity,Z_380) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39074]) ).
tff(c_39347,plain,
! [X_384,Z_385] : ( multiply(inverse(X_384),multiply(X_384,Z_385)) = Z_385 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39134]) ).
tff(c_39407,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_177,c_39347]) ).
tff(c_39436,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39181,c_145,c_39407]) ).
tff(c_39183,plain,
inverse(sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_39167,c_38944]) ).
tff(c_39334,plain,
multiply(sk_c8,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39183,c_4]) ).
tff(c_39464,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39436,c_39334]) ).
tff(c_39465,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_39338,c_39464]) ).
tff(c_39467,plain,
multiply(sk_c10,sk_c2) != sk_c9,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_39528,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_39467,c_36]) ).
tff(c_39839,plain,
multiply(identity,sk_c8) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_39818,c_39528]) ).
tff(c_39848,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39839]) ).
tff(c_39850,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_39688,c_39848]) ).
tff(c_39852,plain,
multiply(sk_c1,sk_c10) != sk_c2,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_39940,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_39852,c_56]) ).
tff(c_40244,plain,
multiply(identity,sk_c8) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_40227,c_39940]) ).
tff(c_40256,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40244]) ).
tff(c_40258,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_40072,c_40256]) ).
tff(c_40260,plain,
multiply(sk_c3,sk_c8) != sk_c10,
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_92,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_44813,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_40260,c_92]) ).
tff(c_40324,plain,
multiply(sk_c1,sk_c10) = sk_c2,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_40397,plain,
! [X_403,Y_404,Z_405] : ( multiply(multiply(X_403,Y_404),Z_405) = multiply(X_403,multiply(Y_404,Z_405)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_40451,plain,
! [Z_405] : ( multiply(sk_c10,multiply(sk_c1,Z_405)) = multiply(identity,Z_405) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_40397]) ).
tff(c_40474,plain,
! [Z_406] : ( multiply(sk_c10,multiply(sk_c1,Z_406)) = Z_406 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40451]) ).
tff(c_40486,plain,
multiply(sk_c10,sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_40324,c_40474]) ).
tff(c_40317,plain,
multiply(sk_c10,sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_40490,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40486,c_40317]) ).
tff(c_94,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_40290,plain,
inverse(sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_40260,c_94]) ).
tff(c_40583,plain,
inverse(sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_40490,c_40290]) ).
tff(c_40599,plain,
multiply(sk_c8,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40583,c_4]) ).
tff(c_18,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_40285,plain,
multiply(sk_c8,sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_40584,plain,
multiply(sk_c8,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40490,c_40285]) ).
tff(c_40618,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40599,c_40584]) ).
tff(c_98,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_40342,plain,
inverse(sk_c5) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_40260,c_98]) ).
tff(c_40581,plain,
inverse(sk_c5) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40490,c_40342]) ).
tff(c_40592,plain,
multiply(sk_c10,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40581,c_4]) ).
tff(c_40680,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40618,c_40592]) ).
tff(c_40622,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40618,c_40581]) ).
tff(c_40681,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40680,c_40622]) ).
tff(c_40621,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_40618,c_40583]) ).
tff(c_40686,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40681,c_40621]) ).
tff(c_40695,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40686,c_149]) ).
tff(c_40457,plain,
! [X_2,Z_405] : ( multiply(inverse(X_2),multiply(X_2,Z_405)) = multiply(identity,Z_405) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_40397]) ).
tff(c_40472,plain,
! [X_2,Z_405] : ( multiply(inverse(X_2),multiply(X_2,Z_405)) = Z_405 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40457]) ).
tff(c_40919,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_40695,c_40472]) ).
tff(c_40931,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40919]) ).
tff(c_40631,plain,
multiply(sk_c3,sk_c8) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_40618,c_40260]) ).
tff(c_40792,plain,
multiply(sk_c3,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_40686,c_40631]) ).
tff(c_40935,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_40931,c_40792]) ).
tff(c_40940,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40935]) ).
tff(c_40942,plain,
multiply(sk_c1,sk_c10) != sk_c2,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_40991,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_40942,c_50]) ).
tff(c_40303,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_40260,c_92]) ).
tff(c_40307,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40303,c_4]) ).
tff(c_41019,plain,
! [X_411,Y_412,Z_413] : ( multiply(multiply(X_411,Y_412),Z_413) = multiply(X_411,multiply(Y_412,Z_413)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_41055,plain,
! [Z_413] : ( multiply(sk_c10,multiply(sk_c4,Z_413)) = multiply(identity,Z_413) ),
inference(superposition,[status(thm),theory(equality)],[c_40307,c_41019]) ).
tff(c_41755,plain,
! [Z_429] : ( multiply(sk_c10,multiply(sk_c4,Z_429)) = Z_429 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41055]) ).
tff(c_41767,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_40991,c_41755]) ).
tff(c_41076,plain,
! [X_2,Z_413] : ( multiply(inverse(X_2),multiply(X_2,Z_413)) = multiply(identity,Z_413) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_41019]) ).
tff(c_41950,plain,
! [X_431,Z_432] : ( multiply(inverse(X_431),multiply(X_431,Z_432)) = Z_432 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41076]) ).
tff(c_42001,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_41767,c_41950]) ).
tff(c_42085,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42001]) ).
tff(c_40941,plain,
inverse(sk_c5) = sk_c9,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_40946,plain,
multiply(sk_c9,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40941,c_4]) ).
tff(c_40294,plain,
multiply(sk_c8,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40290,c_4]) ).
tff(c_41058,plain,
! [Z_413] : ( multiply(sk_c8,multiply(sk_c9,Z_413)) = multiply(identity,Z_413) ),
inference(superposition,[status(thm),theory(equality)],[c_40294,c_41019]) ).
tff(c_41549,plain,
! [Z_425] : ( multiply(sk_c8,multiply(sk_c9,Z_425)) = Z_425 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41058]) ).
tff(c_41564,plain,
multiply(sk_c8,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_40946,c_41549]) ).
tff(c_96,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_40997,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_40260,c_96]) ).
tff(c_41778,plain,
! [Z_430] : ( multiply(sk_c8,multiply(sk_c10,Z_430)) = multiply(sk_c9,Z_430) ),
inference(superposition,[status(thm),theory(equality)],[c_40285,c_41019]) ).
tff(c_41811,plain,
multiply(sk_c9,sk_c8) = multiply(sk_c8,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_40997,c_41778]) ).
tff(c_41830,plain,
multiply(sk_c9,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40294,c_41811]) ).
tff(c_41086,plain,
! [Z_413] : ( multiply(sk_c8,multiply(sk_c9,Z_413)) = Z_413 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41058]) ).
tff(c_41838,plain,
multiply(sk_c8,identity) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_41830,c_41086]) ).
tff(c_41844,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41564,c_41838]) ).
tff(c_41849,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41844,c_41564]) ).
tff(c_41857,plain,
inverse(sk_c9) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41844,c_40290]) ).
tff(c_41814,plain,
multiply(sk_c9,sk_c2) = multiply(sk_c8,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_40317,c_41778]) ).
tff(c_41831,plain,
multiply(sk_c9,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40294,c_41814]) ).
tff(c_41992,plain,
multiply(inverse(sk_c9),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_41831,c_41950]) ).
tff(c_42084,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_41849,c_41857,c_41992]) ).
tff(c_42105,plain,
inverse(sk_c9) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_42084,c_41857]) ).
tff(c_42256,plain,
inverse(identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_42085,c_42105]) ).
tff(c_40259,plain,
inverse(sk_c6) = sk_c10,
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_40264,plain,
multiply(sk_c10,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40259,c_4]) ).
tff(c_66,plain,
( ( multiply(sk_c7,sk_c10) = sk_c6 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_41008,plain,
multiply(sk_c7,sk_c10) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_40942,c_66]) ).
tff(c_102,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_206]) ).
tff(c_40268,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_40260,c_102]) ).
tff(c_40272,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40268,c_4]) ).
tff(c_41064,plain,
! [Z_413] : ( multiply(sk_c6,multiply(sk_c7,Z_413)) = multiply(identity,Z_413) ),
inference(superposition,[status(thm),theory(equality)],[c_40272,c_41019]) ).
tff(c_41119,plain,
! [Z_416] : ( multiply(sk_c6,multiply(sk_c7,Z_416)) = Z_416 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41064]) ).
tff(c_41131,plain,
multiply(sk_c6,sk_c6) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_41008,c_41119]) ).
tff(c_41067,plain,
! [Z_413] : ( multiply(sk_c10,multiply(sk_c6,Z_413)) = multiply(identity,Z_413) ),
inference(superposition,[status(thm),theory(equality)],[c_40264,c_41019]) ).
tff(c_41512,plain,
! [Z_424] : ( multiply(sk_c10,multiply(sk_c6,Z_424)) = Z_424 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41067]) ).
tff(c_41524,plain,
multiply(sk_c10,sk_c10) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_41131,c_41512]) ).
tff(c_40982,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_40942,c_48]) ).
tff(c_41561,plain,
multiply(sk_c8,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_40982,c_41549]) ).
tff(c_41850,plain,
multiply(sk_c5,sk_c5) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_41844,c_41844,c_41561]) ).
tff(c_41817,plain,
multiply(sk_c9,sk_c4) = multiply(sk_c8,identity),
inference(superposition,[status(thm),theory(equality)],[c_40307,c_41778]) ).
tff(c_41832,plain,
multiply(sk_c9,sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41564,c_41817]) ).
tff(c_41986,plain,
multiply(inverse(sk_c9),sk_c5) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_41832,c_41950]) ).
tff(c_42082,plain,
sk_c4 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_41850,c_41857,c_41986]) ).
tff(c_42120,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_42082,c_40991]) ).
tff(c_42123,plain,
sk_c9 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41524,c_42120]) ).
tff(c_42146,plain,
multiply(sk_c10,sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42123,c_41767]) ).
tff(c_42149,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40264,c_42146]) ).
tff(c_42122,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42082,c_40303]) ).
tff(c_42293,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42256,c_42149,c_42149,c_42122]) ).
tff(c_41861,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41844,c_145]) ).
tff(c_42104,plain,
inverse(sk_c3) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_42084,c_41861]) ).
tff(c_42277,plain,
multiply(sk_c2,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42104,c_4]) ).
tff(c_42344,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42293,c_42277]) ).
tff(c_42299,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42293,c_42084]) ).
tff(c_41859,plain,
multiply(sk_c3,sk_c5) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_41844,c_40260]) ).
tff(c_42368,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42344,c_42299,c_42149,c_41859]) ).
tff(c_42369,plain,
inverse(sk_c5) = sk_c9,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_42375,plain,
multiply(sk_c9,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42369,c_4]) ).
tff(c_43857,plain,
! [X_463,Y_464,Z_465] : ( multiply(multiply(X_463,Y_464),Z_465) = multiply(X_463,multiply(Y_464,Z_465)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_43893,plain,
! [Z_465] : ( multiply(sk_c8,multiply(sk_c9,Z_465)) = multiply(identity,Z_465) ),
inference(superposition,[status(thm),theory(equality)],[c_40294,c_43857]) ).
tff(c_43954,plain,
! [Z_468] : ( multiply(sk_c8,multiply(sk_c9,Z_468)) = Z_468 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43893]) ).
tff(c_43969,plain,
multiply(sk_c8,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_42375,c_43954]) ).
tff(c_42370,plain,
multiply(sk_c10,sk_c2) != sk_c9,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_46,plain,
( ( multiply(sk_c7,sk_c10) = sk_c6 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_42423,plain,
multiply(sk_c7,sk_c10) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_42370,c_46]) ).
tff(c_42456,plain,
! [X_436,Y_437,Z_438] : ( multiply(multiply(X_436,Y_437),Z_438) = multiply(X_436,multiply(Y_437,Z_438)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_42504,plain,
! [Z_438] : ( multiply(sk_c10,multiply(sk_c6,Z_438)) = multiply(identity,Z_438) ),
inference(superposition,[status(thm),theory(equality)],[c_40264,c_42456]) ).
tff(c_43280,plain,
! [Z_457] : ( multiply(sk_c10,multiply(sk_c6,Z_457)) = Z_457 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42504]) ).
tff(c_43304,plain,
multiply(sk_c10,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40272,c_43280]) ).
tff(c_42417,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_42370,c_36]) ).
tff(c_43218,plain,
! [Z_456] : ( multiply(sk_c8,multiply(sk_c10,Z_456)) = multiply(sk_c9,Z_456) ),
inference(superposition,[status(thm),theory(equality)],[c_40285,c_42456]) ).
tff(c_43242,plain,
multiply(sk_c9,sk_c8) = multiply(sk_c8,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_42417,c_43218]) ).
tff(c_43257,plain,
multiply(sk_c9,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40294,c_43242]) ).
tff(c_42407,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_42370,c_30]) ).
tff(c_43492,plain,
! [Z_460] : ( multiply(sk_c4,multiply(sk_c10,Z_460)) = multiply(sk_c9,Z_460) ),
inference(superposition,[status(thm),theory(equality)],[c_42407,c_42456]) ).
tff(c_43528,plain,
multiply(sk_c9,sk_c8) = multiply(sk_c4,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_42417,c_43492]) ).
tff(c_43544,plain,
multiply(sk_c4,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43257,c_43528]) ).
tff(c_42492,plain,
! [Z_438] : ( multiply(sk_c10,multiply(sk_c4,Z_438)) = multiply(identity,Z_438) ),
inference(superposition,[status(thm),theory(equality)],[c_40307,c_42456]) ).
tff(c_42522,plain,
! [Z_438] : ( multiply(sk_c10,multiply(sk_c4,Z_438)) = Z_438 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42492]) ).
tff(c_43548,plain,
multiply(sk_c10,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_43544,c_42522]) ).
tff(c_43554,plain,
sk_c9 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43304,c_43548]) ).
tff(c_28,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_42432,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_42370,c_28]) ).
tff(c_43567,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_43554,c_42432]) ).
tff(c_43575,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42423,c_43567]) ).
tff(c_43568,plain,
multiply(sk_c10,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43554,c_42417]) ).
tff(c_43628,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40264,c_43575,c_43568]) ).
tff(c_42412,plain,
multiply(sk_c1,sk_c10) = sk_c2,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_42507,plain,
! [Z_438] : ( multiply(sk_c10,multiply(sk_c1,Z_438)) = multiply(identity,Z_438) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_42456]) ).
tff(c_42530,plain,
! [Z_439] : ( multiply(sk_c10,multiply(sk_c1,Z_439)) = Z_439 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42507]) ).
tff(c_42542,plain,
multiply(sk_c10,sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_42412,c_42530]) ).
tff(c_42910,plain,
sk_c9 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42542,c_42370]) ).
tff(c_43565,plain,
sk_c7 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_43554,c_42910]) ).
tff(c_43632,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_43628,c_43565]) ).
tff(c_43571,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43554,c_42369]) ).
tff(c_43631,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43628,c_43571]) ).
tff(c_43636,plain,
multiply(identity,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_43628,c_42423]) ).
tff(c_43640,plain,
sk_c6 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43636]) ).
tff(c_43650,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_43640,c_43575]) ).
tff(c_42446,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_42370,c_40]) ).
tff(c_43566,plain,
multiply(sk_c5,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43554,c_42446]) ).
tff(c_43798,plain,
multiply(sk_c5,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43650,c_43628,c_43566]) ).
tff(c_42513,plain,
! [X_2,Z_438] : ( multiply(inverse(X_2),multiply(X_2,Z_438)) = multiply(identity,Z_438) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42456]) ).
tff(c_42528,plain,
! [X_2,Z_438] : ( multiply(inverse(X_2),multiply(X_2,Z_438)) = Z_438 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42513]) ).
tff(c_43802,plain,
multiply(inverse(sk_c5),identity) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_43798,c_42528]) ).
tff(c_43808,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43631,c_43802]) ).
tff(c_43810,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43632,c_43808]) ).
tff(c_43812,plain,
multiply(sk_c1,sk_c10) != sk_c2,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_43837,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_43812,c_56]) ).
tff(c_44247,plain,
! [Z_474] : ( multiply(sk_c8,multiply(sk_c10,Z_474)) = multiply(sk_c9,Z_474) ),
inference(superposition,[status(thm),theory(equality)],[c_40285,c_43857]) ).
tff(c_44262,plain,
multiply(sk_c9,sk_c8) = multiply(sk_c8,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_43837,c_44247]) ).
tff(c_44275,plain,
multiply(sk_c9,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40294,c_44262]) ).
tff(c_43921,plain,
! [Z_465] : ( multiply(sk_c8,multiply(sk_c9,Z_465)) = Z_465 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43893]) ).
tff(c_44282,plain,
multiply(sk_c8,identity) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_44275,c_43921]) ).
tff(c_44288,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_43969,c_44282]) ).
tff(c_43824,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_42370,c_40]) ).
tff(c_44298,plain,
multiply(sk_c5,sk_c5) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_44288,c_43824]) ).
tff(c_44301,plain,
inverse(sk_c9) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_44288,c_40290]) ).
tff(c_44271,plain,
multiply(sk_c9,sk_c1) = multiply(sk_c8,identity),
inference(superposition,[status(thm),theory(equality)],[c_161,c_44247]) ).
tff(c_44278,plain,
multiply(sk_c9,sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_43969,c_44271]) ).
tff(c_43911,plain,
! [X_2,Z_465] : ( multiply(inverse(X_2),multiply(X_2,Z_465)) = multiply(identity,Z_465) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_43857]) ).
tff(c_44386,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_43911]) ).
tff(c_44422,plain,
multiply(inverse(sk_c9),sk_c5) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_44278,c_44386]) ).
tff(c_44488,plain,
sk_c9 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_44298,c_44301,c_44422]) ).
tff(c_44443,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_42407,c_44386]) ).
tff(c_44491,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40303,c_44443]) ).
tff(c_44640,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_161,c_44488,c_44491]) ).
tff(c_44265,plain,
multiply(sk_c9,sk_c4) = multiply(sk_c8,identity),
inference(superposition,[status(thm),theory(equality)],[c_40307,c_44247]) ).
tff(c_44276,plain,
multiply(sk_c9,sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_43969,c_44265]) ).
tff(c_44407,plain,
multiply(inverse(sk_c9),sk_c5) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_44276,c_44386]) ).
tff(c_44484,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_44298,c_44301,c_44407]) ).
tff(c_44501,plain,
inverse(sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_44484,c_44301]) ).
tff(c_44506,plain,
sk_c5 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40303,c_44501]) ).
tff(c_44305,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_44288,c_145]) ).
tff(c_44552,plain,
inverse(sk_c3) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_44506,c_44305]) ).
tff(c_44579,plain,
multiply(sk_c10,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_44552,c_4]) ).
tff(c_44776,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44640,c_44579]) ).
tff(c_44303,plain,
multiply(sk_c3,sk_c5) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_44288,c_40260]) ).
tff(c_44551,plain,
multiply(sk_c3,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_44506,c_44303]) ).
tff(c_44797,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44776,c_44640,c_44640,c_44551]) ).
tff(c_44799,plain,
multiply(sk_c8,sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_10,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_46080,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_44799,c_10]) ).
tff(c_46115,plain,
! [X_498,Y_499,Z_500] : ( multiply(multiply(X_498,Y_499),Z_500) = multiply(X_498,multiply(Y_499,Z_500)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_46169,plain,
! [X_2,Z_500] : ( multiply(inverse(X_2),multiply(X_2,Z_500)) = multiply(identity,Z_500) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_46115]) ).
tff(c_46304,plain,
! [X_507,Z_508] : ( multiply(inverse(X_507),multiply(X_507,Z_508)) = Z_508 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46169]) ).
tff(c_46358,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_46080,c_46304]) ).
tff(c_46421,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_44813,c_46358]) ).
tff(c_46184,plain,
! [X_2,Z_500] : ( multiply(inverse(X_2),multiply(X_2,Z_500)) = Z_500 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46169]) ).
tff(c_46434,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_46421,c_46184]) ).
tff(c_46440,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_46434]) ).
tff(c_8,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_46092,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_44799,c_8]) ).
tff(c_46445,plain,
multiply(identity,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_46440,c_46092]) ).
tff(c_46457,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46445]) ).
tff(c_44798,plain,
inverse(sk_c5) = sk_c9,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_106,plain,
( ( multiply(sk_c7,sk_c10) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_212]) ).
tff(c_44867,plain,
multiply(sk_c7,sk_c10) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_40260,c_106]) ).
tff(c_44916,plain,
! [X_479,Y_480,Z_481] : ( multiply(multiply(X_479,Y_480),Z_481) = multiply(X_479,multiply(Y_480,Z_481)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_44973,plain,
! [X_2,Z_481] : ( multiply(inverse(X_2),multiply(X_2,Z_481)) = multiply(identity,Z_481) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_44916]) ).
tff(c_45050,plain,
! [X_483,Z_484] : ( multiply(inverse(X_483),multiply(X_483,Z_484)) = Z_484 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44973]) ).
tff(c_45086,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_44867,c_45050]) ).
tff(c_45132,plain,
multiply(sk_c6,sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40268,c_45086]) ).
tff(c_44988,plain,
! [X_2,Z_481] : ( multiply(inverse(X_2),multiply(X_2,Z_481)) = Z_481 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44973]) ).
tff(c_45148,plain,
multiply(inverse(sk_c6),sk_c10) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45132,c_44988]) ).
tff(c_45154,plain,
multiply(sk_c10,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40259,c_45148]) ).
tff(c_44837,plain,
multiply(sk_c1,sk_c10) = sk_c2,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_44967,plain,
! [Z_481] : ( multiply(sk_c10,multiply(sk_c1,Z_481)) = multiply(identity,Z_481) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_44916]) ).
tff(c_44990,plain,
! [Z_482] : ( multiply(sk_c10,multiply(sk_c1,Z_482)) = Z_482 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44967]) ).
tff(c_45002,plain,
multiply(sk_c10,sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_44837,c_44990]) ).
tff(c_44872,plain,
multiply(sk_c10,sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_45008,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45002,c_44872]) ).
tff(c_44888,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_44799,c_10]) ).
tff(c_45018,plain,
multiply(sk_c4,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45008,c_44888]) ).
tff(c_45195,plain,
multiply(inverse(sk_c4),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_45018,c_44988]) ).
tff(c_45201,plain,
sk_c6 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45154,c_44813,c_45195]) ).
tff(c_45209,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45201,c_40259]) ).
tff(c_44846,plain,
inverse(sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_40260,c_94]) ).
tff(c_45021,plain,
inverse(sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_45008,c_44846]) ).
tff(c_45262,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45209,c_45021]) ).
tff(c_45032,plain,
multiply(sk_c8,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_45021,c_4]) ).
tff(c_45291,plain,
multiply(sk_c10,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_45262,c_45032]) ).
tff(c_16,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_44881,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_44799,c_16]) ).
tff(c_45019,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45008,c_44881]) ).
tff(c_45314,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_45291,c_45262,c_45019]) ).
tff(c_45318,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_45314,c_45262]) ).
tff(c_45023,plain,
multiply(sk_c8,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45008,c_44799]) ).
tff(c_45470,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45318,c_45314,c_45314,c_45023]) ).
tff(c_45472,plain,
multiply(sk_c10,sk_c2) != sk_c9,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_45508,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_45472,c_30]) ).
tff(c_45529,plain,
! [X_486,Y_487,Z_488] : ( multiply(multiply(X_486,Y_487),Z_488) = multiply(X_486,multiply(Y_487,Z_488)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_45583,plain,
! [X_2,Z_488] : ( multiply(inverse(X_2),multiply(X_2,Z_488)) = multiply(identity,Z_488) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_45529]) ).
tff(c_45723,plain,
! [X_494,Z_495] : ( multiply(inverse(X_494),multiply(X_494,Z_495)) = Z_495 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45583]) ).
tff(c_45768,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_45508,c_45723]) ).
tff(c_45840,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_44813,c_45768]) ).
tff(c_45598,plain,
! [X_2,Z_488] : ( multiply(inverse(X_2),multiply(X_2,Z_488)) = Z_488 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45583]) ).
tff(c_45934,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_45840,c_45598]) ).
tff(c_45940,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_45934]) ).
tff(c_45473,plain,
multiply(sk_c10,sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_45483,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_45473,c_45472]) ).
tff(c_45484,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_44803,plain,
multiply(sk_c9,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_44798,c_4]) ).
tff(c_45568,plain,
! [Z_488] : ( multiply(sk_c9,multiply(sk_c5,Z_488)) = multiply(identity,Z_488) ),
inference(superposition,[status(thm),theory(equality)],[c_44803,c_45529]) ).
tff(c_45681,plain,
! [Z_492] : ( multiply(sk_c9,multiply(sk_c5,Z_492)) = Z_492 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45568]) ).
tff(c_45693,plain,
multiply(sk_c9,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_45484,c_45681]) ).
tff(c_45943,plain,
multiply(identity,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_45940,c_45940,c_45693]) ).
tff(c_45955,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45943]) ).
tff(c_45471,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_45949,plain,
multiply(identity,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_45940,c_45471]) ).
tff(c_45956,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45949]) ).
tff(c_46011,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_45955,c_45956]) ).
tff(c_45577,plain,
! [Z_488] : ( multiply(sk_c10,multiply(sk_c1,Z_488)) = multiply(identity,Z_488) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_45529]) ).
tff(c_45602,plain,
! [Z_489] : ( multiply(sk_c10,multiply(sk_c1,Z_489)) = Z_489 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45577]) ).
tff(c_45614,plain,
multiply(sk_c10,sk_c2) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_44837,c_45602]) ).
tff(c_45618,plain,
sk_c9 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45614,c_45472]) ).
tff(c_45945,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_45940,c_45618]) ).
tff(c_46031,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_46011,c_45945]) ).
tff(c_46033,plain,
multiply(sk_c1,sk_c10) != sk_c2,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_60,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_46075,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_46033,c_60]) ).
tff(c_46361,plain,
multiply(inverse(sk_c5),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_46075,c_46304]) ).
tff(c_46422,plain,
multiply(sk_c9,sk_c9) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_44798,c_46361]) ).
tff(c_46555,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_46457,c_46440,c_2,c_46440,c_46422]) ).
tff(c_46559,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_46555,c_46457]) ).
tff(c_46453,plain,
multiply(sk_c8,sk_c10) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_46440,c_44799]) ).
tff(c_46788,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46559,c_46555,c_46453]) ).
tff(c_46790,plain,
inverse(sk_c1) != sk_c10,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_70,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_46877,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_46790,c_70]) ).
tff(c_80,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_46857,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_46790,c_80]) ).
tff(c_78,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_46841,plain,
inverse(sk_c5) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_46790,c_78]) ).
tff(c_46845,plain,
multiply(sk_c9,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_46841,c_4]) ).
tff(c_46954,plain,
! [Z_514] : ( multiply(sk_c9,multiply(sk_c5,Z_514)) = multiply(identity,Z_514) ),
inference(superposition,[status(thm),theory(equality)],[c_46845,c_46924]) ).
tff(c_46988,plain,
! [Z_515] : ( multiply(sk_c9,multiply(sk_c5,Z_515)) = Z_515 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46954]) ).
tff(c_47000,plain,
multiply(sk_c9,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_46857,c_46988]) ).
tff(c_72,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_46815,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_46790,c_72]) ).
tff(c_46819,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_46815,c_4]) ).
tff(c_46960,plain,
! [Z_514] : ( multiply(sk_c10,multiply(sk_c4,Z_514)) = multiply(identity,Z_514) ),
inference(superposition,[status(thm),theory(equality)],[c_46819,c_46924]) ).
tff(c_47011,plain,
! [Z_516] : ( multiply(sk_c10,multiply(sk_c4,Z_516)) = Z_516 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46960]) ).
tff(c_47023,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_46877,c_47011]) ).
tff(c_47412,plain,
! [Z_526] : ( multiply(sk_c4,multiply(sk_c10,Z_526)) = multiply(sk_c9,Z_526) ),
inference(superposition,[status(thm),theory(equality)],[c_46877,c_46924]) ).
tff(c_47427,plain,
multiply(sk_c9,sk_c9) = multiply(sk_c4,sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_47023,c_47412]) ).
tff(c_47443,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_46877,c_47000,c_47427]) ).
tff(c_46789,plain,
inverse(sk_c9) = sk_c8,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_46794,plain,
multiply(sk_c8,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_46789,c_4]) ).
tff(c_47455,plain,
multiply(sk_c8,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47443,c_46794]) ).
tff(c_47447,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_47443,c_47443,c_47000]) ).
tff(c_49864,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47455,c_47447]) ).
tff(c_49886,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49864,c_47443]) ).
tff(c_47151,plain,
! [X_521,Z_522] : ( multiply(inverse(X_521),multiply(X_521,Z_522)) = Z_522 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46972]) ).
tff(c_47181,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_47023,c_47151]) ).
tff(c_47232,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_47181]) ).
tff(c_86,plain,
( ( multiply(sk_c7,sk_c10) = sk_c6 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_46869,plain,
multiply(sk_c7,sk_c10) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_46790,c_86]) ).
tff(c_82,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_46829,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_46790,c_82]) ).
tff(c_46833,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_46829,c_4]) ).
tff(c_84,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_46802,plain,
inverse(sk_c6) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_46790,c_84]) ).
tff(c_46806,plain,
multiply(sk_c10,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_46802,c_4]) ).
tff(c_46963,plain,
! [Z_514] : ( multiply(sk_c10,multiply(sk_c6,Z_514)) = multiply(identity,Z_514) ),
inference(superposition,[status(thm),theory(equality)],[c_46806,c_46924]) ).
tff(c_47104,plain,
! [Z_520] : ( multiply(sk_c10,multiply(sk_c6,Z_520)) = Z_520 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46963]) ).
tff(c_47122,plain,
multiply(sk_c10,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_46833,c_47104]) ).
tff(c_76,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_46899,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_46790,c_76]) ).
tff(c_47060,plain,
! [Z_518] : ( multiply(sk_c10,multiply(sk_c8,Z_518)) = multiply(sk_c9,Z_518) ),
inference(superposition,[status(thm),theory(equality)],[c_46899,c_46924]) ).
tff(c_47072,plain,
multiply(sk_c9,sk_c9) = multiply(sk_c10,identity),
inference(superposition,[status(thm),theory(equality)],[c_46794,c_47060]) ).
tff(c_47079,plain,
multiply(sk_c10,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_47000,c_47072]) ).
tff(c_47126,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_47122,c_47079]) ).
tff(c_68,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_46891,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_46790,c_68]) ).
tff(c_47035,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_46891,c_46789,c_46899,c_128]) ).
tff(c_47036,plain,
multiply(sk_c8,sk_c10) != sk_c9,
inference(splitLeft,[status(thm)],[c_47035]) ).
tff(c_47137,plain,
multiply(sk_c7,sk_c10) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_47126,c_47036]) ).
tff(c_47146,plain,
sk_c9 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_46869,c_47137]) ).
tff(c_47240,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_47232,c_47146]) ).
tff(c_47138,plain,
multiply(sk_c9,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_47126,c_47000]) ).
tff(c_47319,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47232,c_2,c_47232,c_47138]) ).
tff(c_47322,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47319,c_47126]) ).
tff(c_46942,plain,
! [Z_514] : ( multiply(sk_c9,multiply(sk_c10,Z_514)) = multiply(sk_c8,Z_514) ),
inference(superposition,[status(thm),theory(equality)],[c_46891,c_46924]) ).
tff(c_47339,plain,
! [Z_524] : ( multiply(sk_c10,Z_524) = Z_524 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47322,c_2,c_47232,c_46942]) ).
tff(c_47360,plain,
sk_c6 = identity,
inference(superposition,[status(thm),theory(equality)],[c_47339,c_46806]) ).
tff(c_47379,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_47240,c_47360]) ).
tff(c_47381,plain,
multiply(sk_c8,sk_c10) = sk_c9,
inference(splitRight,[status(thm)],[c_47035]) ).
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_47385,plain,
! [Z_5] : ( multiply(sk_c8,multiply(sk_c10,Z_5)) = multiply(sk_c9,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_47381,c_6]) ).
tff(c_50071,plain,
! [Z_569] : ( multiply(sk_c10,Z_569) = Z_569 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49886,c_2,c_49864,c_47385]) ).
tff(c_50089,plain,
sk_c6 = identity,
inference(superposition,[status(thm),theory(equality)],[c_50071,c_46806]) ).
tff(c_46957,plain,
! [Z_514] : ( multiply(sk_c6,multiply(sk_c7,Z_514)) = multiply(identity,Z_514) ),
inference(superposition,[status(thm),theory(equality)],[c_46833,c_46924]) ).
tff(c_47389,plain,
! [Z_525] : ( multiply(sk_c6,multiply(sk_c7,Z_525)) = Z_525 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46957]) ).
tff(c_47401,plain,
multiply(sk_c6,sk_c6) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_46869,c_47389]) ).
tff(c_50118,plain,
multiply(identity,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_50089,c_50089,c_47401]) ).
tff(c_50121,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50118]) ).
tff(c_47491,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47455,c_47447]) ).
tff(c_47456,plain,
inverse(sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_47443,c_46789]) ).
tff(c_47502,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47491,c_47491,c_47456]) ).
tff(c_47560,plain,
! [X_527,Z_528] : ( multiply(inverse(X_527),multiply(X_527,Z_528)) = Z_528 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46972]) ).
tff(c_47827,plain,
! [X_530,Z_531] : ( multiply(inverse(inverse(X_530)),Z_531) = multiply(X_530,Z_531) ),
inference(superposition,[status(thm),theory(equality)],[c_46986,c_47560]) ).
tff(c_47596,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_47560]) ).
tff(c_47834,plain,
! [X_530] : ( multiply(X_530,identity) = X_530 ),
inference(superposition,[status(thm),theory(equality)],[c_47827,c_47596]) ).
tff(c_47446,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_47443,c_47023]) ).
tff(c_47501,plain,
multiply(sk_c10,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_47491,c_47446]) ).
tff(c_47449,plain,
multiply(sk_c10,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_47443,c_46899]) ).
tff(c_47545,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47501,c_47491,c_47491,c_47449]) ).
tff(c_47380,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 )
| ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) ) ),
inference(splitRight,[status(thm)],[c_47035]) ).
tff(c_47489,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_47443,c_47443,c_47443,c_47443,c_47380]) ).
tff(c_47490,plain,
! [X3_8] :
( ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) ) ),
inference(splitLeft,[status(thm)],[c_47489]) ).
tff(c_49847,plain,
! [X3_566] :
( ( inverse(X3_566) != identity )
| ( inverse(X3_566) != X3_566 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_47834,c_47545,c_47834,c_47545,c_47545,c_47490]) ).
tff(c_49855,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_47502,c_49847]) ).
tff(c_49862,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_47502,c_49855]) ).
tff(c_49863,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_47489]) ).
tff(c_71736,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( identity != X2_11 )
| ( inverse(X2_11) != identity )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_50234,c_50121,c_2,c_50121,c_49864,c_50121,c_50234,c_50121,c_49864,c_49864,c_50234,c_50121,c_49864,c_50121,c_49864,c_50234,c_49864,c_49864,c_49863]) ).
tff(c_71738,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_71736]) ).
tff(c_49884,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49864,c_49864,c_47456]) ).
tff(c_71740,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_71738,c_49884]) ).
tff(c_71741,plain,
! [X6_7,X1_10,X2_11] :
( ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( identity != X2_11 )
| ( inverse(X2_11) != identity ) ),
inference(splitRight,[status(thm)],[c_71736]) ).
tff(c_81176,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_71741]) ).
tff(c_81178,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_81176,c_49884]) ).
tff(c_81179,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(splitRight,[status(thm)],[c_71741]) ).
tff(c_81181,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_81179]) ).
tff(c_81183,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_81181,c_49884]) ).
tff(c_81185,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_81179]) ).
tff(c_81187,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_81185,c_49884]) ).
tff(c_81189,plain,
inverse(sk_c3) != sk_c8,
inference(splitRight,[status(thm)],[c_122]) ).
tff(c_124,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_81213,plain,
inverse(sk_c6) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_81189,c_124]) ).
tff(c_81217,plain,
multiply(sk_c10,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_81213,c_4]) ).
tff(c_108,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_215]) ).
tff(c_81278,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_81189,c_108]) ).
tff(c_114,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_224]) ).
tff(c_81227,plain,
inverse(sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_81189,c_114]) ).
tff(c_81231,plain,
multiply(sk_c8,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_81227,c_4]) ).
tff(c_81371,plain,
! [Z_773] : ( multiply(sk_c8,multiply(sk_c9,Z_773)) = multiply(identity,Z_773) ),
inference(superposition,[status(thm),theory(equality)],[c_81231,c_81335]) ).
tff(c_81921,plain,
! [Z_782] : ( multiply(sk_c8,multiply(sk_c9,Z_782)) = Z_782 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81371]) ).
tff(c_81933,plain,
multiply(sk_c8,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_81278,c_81921]) ).
tff(c_110,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_218]) ).
tff(c_81290,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_81189,c_110]) ).
tff(c_112,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_221]) ).
tff(c_81201,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_81189,c_112]) ).
tff(c_81205,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_81201,c_4]) ).
tff(c_81377,plain,
! [Z_773] : ( multiply(sk_c10,multiply(sk_c4,Z_773)) = multiply(identity,Z_773) ),
inference(superposition,[status(thm),theory(equality)],[c_81205,c_81335]) ).
tff(c_81402,plain,
! [Z_774] : ( multiply(sk_c10,multiply(sk_c4,Z_774)) = Z_774 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81377]) ).
tff(c_81414,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_81290,c_81402]) ).
tff(c_81510,plain,
! [X_777,Z_778] : ( multiply(inverse(X_777),multiply(X_777,Z_778)) = Z_778 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81383]) ).
tff(c_81546,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_81414,c_81510]) ).
tff(c_81619,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_81546]) ).
tff(c_81633,plain,
multiply(identity,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_81619,c_81278]) ).
tff(c_81639,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81633]) ).
tff(c_81564,plain,
multiply(inverse(sk_c9),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_81278,c_81510]) ).
tff(c_81623,plain,
multiply(sk_c8,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81227,c_81564]) ).
tff(c_81709,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81639,c_81639,c_81623]) ).
tff(c_81713,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_81709,c_81397]) ).
tff(c_81722,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_81713]) ).
tff(c_81728,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81722,c_81639]) ).
tff(c_116,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_81271,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_81189,c_116]) ).
tff(c_81400,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_81278,c_81227,c_81271,c_128]) ).
tff(c_81401,plain,
multiply(sk_c8,sk_c10) != sk_c9,
inference(splitLeft,[status(thm)],[c_81400]) ).
tff(c_81630,plain,
multiply(sk_c8,sk_c10) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_81619,c_81401]) ).
tff(c_81911,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81728,c_81722,c_81630]) ).
tff(c_81913,plain,
multiply(sk_c8,sk_c10) = sk_c9,
inference(splitRight,[status(thm)],[c_81400]) ).
tff(c_81955,plain,
! [Z_783] : ( multiply(sk_c10,multiply(sk_c8,Z_783)) = multiply(sk_c9,Z_783) ),
inference(superposition,[status(thm),theory(equality)],[c_81271,c_81335]) ).
tff(c_81976,plain,
multiply(sk_c9,sk_c10) = multiply(sk_c10,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_81913,c_81955]) ).
tff(c_81983,plain,
multiply(sk_c10,sk_c9) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_81278,c_81976]) ).
tff(c_81188,plain,
inverse(sk_c7) = sk_c6,
inference(splitRight,[status(thm)],[c_122]) ).
tff(c_81193,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_81188,c_4]) ).
tff(c_81374,plain,
! [Z_773] : ( multiply(sk_c10,multiply(sk_c6,Z_773)) = multiply(identity,Z_773) ),
inference(superposition,[status(thm),theory(equality)],[c_81217,c_81335]) ).
tff(c_81991,plain,
! [Z_784] : ( multiply(sk_c10,multiply(sk_c6,Z_784)) = Z_784 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81374]) ).
tff(c_82003,plain,
multiply(sk_c10,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_81193,c_81991]) ).
tff(c_81979,plain,
multiply(sk_c9,sk_c9) = multiply(sk_c10,identity),
inference(superposition,[status(thm),theory(equality)],[c_81231,c_81955]) ).
tff(c_82015,plain,
multiply(sk_c9,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_82003,c_81979]) ).
tff(c_81393,plain,
! [Z_773] : ( multiply(sk_c8,multiply(sk_c9,Z_773)) = Z_773 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81371]) ).
tff(c_82019,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_82015,c_81393]) ).
tff(c_81362,plain,
! [Z_773] : ( multiply(sk_c10,multiply(sk_c8,Z_773)) = multiply(sk_c9,Z_773) ),
inference(superposition,[status(thm),theory(equality)],[c_81271,c_81335]) ).
tff(c_82029,plain,
multiply(sk_c9,sk_c7) = multiply(sk_c10,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_82019,c_81362]) ).
tff(c_82035,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_81983,c_82029]) ).
tff(c_82143,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_82035,c_81393]) ).
tff(c_82149,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81933,c_82143]) ).
tff(c_126,plain,
( ( multiply(sk_c7,sk_c10) = sk_c6 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_242]) ).
tff(c_81310,plain,
multiply(sk_c7,sk_c10) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_81189,c_126]) ).
tff(c_82155,plain,
multiply(sk_c10,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82149,c_81310]) ).
tff(c_82385,plain,
! [Z_789] : ( multiply(sk_c10,multiply(sk_c4,Z_789)) = Z_789 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81377]) ).
tff(c_82397,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_81290,c_82385]) ).
tff(c_82401,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_82397,c_81983]) ).
tff(c_82564,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_82401,c_81271]) ).
tff(c_82570,plain,
sk_c9 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82155,c_82564]) ).
tff(c_82582,plain,
multiply(sk_c10,sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_82570,c_82397]) ).
tff(c_82585,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81217,c_82582]) ).
tff(c_83057,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82585,c_82585,c_82155]) ).
tff(c_83069,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_83057]) ).
tff(c_82661,plain,
! [X_793,Z_794] : ( multiply(inverse(X_793),multiply(X_793,Z_794)) = Z_794 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81383]) ).
tff(c_82788,plain,
! [X_796,Z_797] : ( multiply(inverse(inverse(X_796)),Z_797) = multiply(X_796,Z_797) ),
inference(superposition,[status(thm),theory(equality)],[c_82661,c_81397]) ).
tff(c_82685,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_82661]) ).
tff(c_82795,plain,
! [X_796] : ( multiply(X_796,identity) = X_796 ),
inference(superposition,[status(thm),theory(equality)],[c_82788,c_82685]) ).
tff(c_82417,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_82401,c_81271]) ).
tff(c_82423,plain,
sk_c9 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82155,c_82417]) ).
tff(c_82435,plain,
multiply(sk_c10,sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_82423,c_82397]) ).
tff(c_82438,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81217,c_82435]) ).
tff(c_82498,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82438,c_82438,c_82155]) ).
tff(c_82511,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_82498]) ).
tff(c_82495,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_82438,c_82401]) ).
tff(c_82211,plain,
! [Z_786] : ( multiply(sk_c10,multiply(sk_c4,Z_786)) = Z_786 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_81377]) ).
tff(c_82223,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_81290,c_82211]) ).
tff(c_82227,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_82223,c_81983]) ).
tff(c_82242,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_82227,c_81271]) ).
tff(c_82248,plain,
sk_c9 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82155,c_82242]) ).
tff(c_82305,plain,
multiply(sk_c10,sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_82248,c_82223]) ).
tff(c_82310,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_81217,c_82305]) ).
tff(c_82325,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82310,c_82310,c_82155]) ).
tff(c_82338,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_82325]) ).
tff(c_82041,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_82035,c_81393]) ).
tff(c_82047,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_81933,c_82041]) ).
tff(c_82053,plain,
multiply(sk_c10,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82047,c_81310]) ).
tff(c_82055,plain,
inverse(sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82047,c_81188]) ).
tff(c_81912,plain,
! [X5_6,X3_8,X1_10,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 )
| ( inverse(multiply(X3_8,sk_c10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != inverse(X3_8) ) ),
inference(splitRight,[status(thm)],[c_81400]) ).
tff(c_82108,plain,
! [X3_785] :
( ( inverse(multiply(X3_785,sk_c10)) != sk_c10 )
| ( multiply(X3_785,sk_c10) != inverse(X3_785) ) ),
inference(splitLeft,[status(thm)],[c_81912]) ).
tff(c_82111,plain,
( ( inverse(sk_c6) != sk_c10 )
| ( multiply(sk_c10,sk_c10) != inverse(sk_c10) ) ),
inference(superposition,[status(thm),theory(equality)],[c_82053,c_82108]) ).
tff(c_82138,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_82053,c_82055,c_81213,c_82111]) ).
tff(c_82139,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_81912]) ).
tff(c_82210,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c10 )
| ( multiply(sk_c10,multiply(X5_6,sk_c10)) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_82139]) ).
tff(c_82348,plain,
! [X5_788] :
( ( inverse(X5_788) != identity )
| ( multiply(X5_788,identity) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_82310,c_2,c_82310,c_82248,c_82310,c_82210]) ).
tff(c_82360,plain,
( ( inverse(identity) != identity )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_82348]) ).
tff(c_82376,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_82338,c_82360]) ).
tff(c_82370,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_82338,c_82248]) ).
tff(c_82244,plain,
inverse(sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_82227,c_81227]) ).
tff(c_82382,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_82370,c_82310,c_82244]) ).
tff(c_82383,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_82376,c_82382]) ).
tff(c_82384,plain,
! [X6_7,X1_10,X2_11] :
( ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_82139]) ).
tff(c_82409,plain,
! [X2_11] :
( ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X2_11) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_82384]) ).
tff(c_82525,plain,
! [X2_791] :
( ( multiply(X2_791,identity) != sk_c6 )
| ( inverse(X2_791) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_82423,c_82495,c_82423,c_82409]) ).
tff(c_82537,plain,
( ( sk_c6 != identity )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_82525]) ).
tff(c_82553,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_82511,c_82511,c_82537]) ).
tff(c_82539,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_82511,c_82423]) ).
tff(c_82419,plain,
inverse(sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_82401,c_81227]) ).
tff(c_82554,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_82539,c_82438,c_82419]) ).
tff(c_82555,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_82553,c_82554]) ).
tff(c_82556,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_82384]) ).
tff(c_82591,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c6 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_82401,c_82401,c_82570,c_82556]) ).
tff(c_82592,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_82591]) ).
tff(c_83049,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_82795,c_82585,c_82585,c_82585,c_82592]) ).
tff(c_82597,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_82585,c_82585,c_82155]) ).
tff(c_82609,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_82597]) ).
tff(c_82634,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_82609,c_82570]) ).
tff(c_82566,plain,
inverse(sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_82401,c_81227]) ).
tff(c_82652,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_82634,c_82585,c_82566]) ).
tff(c_83051,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_83049,c_82652]) ).
tff(c_83052,plain,
! [X1_10] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_82591]) ).
tff(c_83701,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_83328,c_83069,c_82585,c_82585,c_83052]) ).
tff(c_83111,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_83069,c_82570]) ).
tff(c_83160,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_83111,c_82585,c_82566]) ).
tff(c_83703,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_83701,c_83160]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP366-1 : TPTP v9.0.0. Released v2.5.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.35 % Computer : n010.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Mon Apr 7 21:44:02 EDT 2025
% 0.14/0.35 % CPUTime :
% 21.42/9.55 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.76/9.64
% 21.76/9.64 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------