%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP317-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n028.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:25:54 PM UTC 2025
% Result : Unsatisfiable 74.62s 59.57s
% Output : CNFRefutation 75.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 51
% Syntax : Number of formulae : 1404 (1238 unt; 0 typ; 0 def)
% Number of atoms : 1986 (1913 equ)
% Maximal formula atoms : 15 ( 1 avg)
% Number of connectives : 1276 ( 694 ~; 582 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 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 : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 667 ( 667 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > 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_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_188,axiom,
( ( inverse(sk_c4) = sk_c3 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_200,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
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_95,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_224,axiom,
( ( multiply(sk_c4,sk_c9) = sk_c3 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_218,axiom,
( ( multiply(sk_c4,sk_c9) = sk_c3 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_269,axiom,
! [X5,X6,X3,X1,X2,X4] :
( ( multiply(sk_c8,sk_c9) != sk_c7 )
| ( multiply(X3,sk_c9) != sk_c8 )
| ( inverse(X3) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( multiply(X4,sk_c8) != sk_c9 )
| ( inverse(X4) != sk_c8 )
| ( inverse(X5) != X6 )
| ( inverse(X6) != sk_c9 )
| ( multiply(X5,sk_c9) != X6 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(X1,sk_c8) != sk_c9 )
| ( inverse(X1) != sk_c8 )
| ( multiply(X2,sk_c9) != sk_c7 )
| ( inverse(X2) != sk_c9 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_212,axiom,
( ( multiply(sk_c4,sk_c9) = sk_c3 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_209,axiom,
( ( multiply(sk_c4,sk_c9) = sk_c3 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c8,sk_c9) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
( ( inverse(sk_c4) = sk_c3 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_179,axiom,
( ( inverse(sk_c4) = sk_c3 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_176,axiom,
( ( inverse(sk_c4) = sk_c3 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_182,axiom,
( ( inverse(sk_c4) = sk_c3 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_173,axiom,
( ( inverse(sk_c4) = sk_c3 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_194,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_191,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c8,sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_206,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_203,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_197,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
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_90,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c4) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_146,plain,
inverse(sk_c4) = sk_c3,
inference(splitLeft,[status(thm)],[c_90]) ).
tff(c_150,plain,
multiply(sk_c3,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_146,c_4]) ).
tff(c_98,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_133,plain,
inverse(sk_c3) = sk_c9,
inference(splitLeft,[status(thm)],[c_98]) ).
tff(c_137,plain,
multiply(sk_c9,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_133,c_4]) ).
tff(c_34107,plain,
! [X_402,Y_403,Z_404] : ( multiply(multiply(X_402,Y_403),Z_404) = multiply(X_402,multiply(Y_403,Z_404)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_34149,plain,
! [Z_404] : ( multiply(sk_c9,multiply(sk_c3,Z_404)) = multiply(identity,Z_404) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_34107]) ).
tff(c_34210,plain,
! [Z_408] : ( multiply(sk_c9,multiply(sk_c3,Z_408)) = Z_408 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34149]) ).
tff(c_34225,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_34210]) ).
tff(c_33655,plain,
! [X_391,Y_392,Z_393] : ( multiply(multiply(X_391,Y_392),Z_393) = multiply(X_391,multiply(Y_392,Z_393)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33700,plain,
! [Z_393] : ( multiply(sk_c9,multiply(sk_c3,Z_393)) = multiply(identity,Z_393) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_33655]) ).
tff(c_33735,plain,
! [Z_395] : ( multiply(sk_c9,multiply(sk_c3,Z_395)) = Z_395 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33700]) ).
tff(c_33747,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_33735]) ).
tff(c_28,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_33623,plain,
multiply(sk_c1,sk_c9) = sk_c8,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_38,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_158,plain,
inverse(sk_c1) = sk_c9,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_162,plain,
multiply(sk_c9,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_158,c_4]) ).
tff(c_33694,plain,
! [Z_393] : ( multiply(sk_c9,multiply(sk_c1,Z_393)) = multiply(identity,Z_393) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_33655]) ).
tff(c_33803,plain,
! [Z_398] : ( multiply(sk_c9,multiply(sk_c1,Z_398)) = Z_398 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33694]) ).
tff(c_33821,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_33623,c_33803]) ).
tff(c_33703,plain,
! [X_2,Z_393] : ( multiply(inverse(X_2),multiply(X_2,Z_393)) = multiply(identity,Z_393) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_33655]) ).
tff(c_33859,plain,
! [X_399,Z_400] : ( multiply(inverse(X_399),multiply(X_399,Z_400)) = Z_400 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33703]) ).
tff(c_33886,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_33821,c_33859]) ).
tff(c_33974,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33886]) ).
tff(c_33992,plain,
multiply(sk_c9,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_33974,c_33821]) ).
tff(c_34009,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_33747,c_33992]) ).
tff(c_46,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_192,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_14,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_198,plain,
multiply(sk_c8,sk_c9) = sk_c7,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_58,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_24969,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_70,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_170,plain,
inverse(sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_70]) ).
tff(c_174,plain,
multiply(sk_c8,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_170,c_4]) ).
tff(c_25024,plain,
! [X_229,Y_230,Z_231] : ( multiply(multiply(X_229,Y_230),Z_231) = multiply(X_229,multiply(Y_230,Z_231)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_25069,plain,
! [Z_231] : ( multiply(sk_c8,multiply(sk_c2,Z_231)) = multiply(identity,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_25024]) ).
tff(c_25178,plain,
! [Z_234] : ( multiply(sk_c8,multiply(sk_c2,Z_234)) = Z_234 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25069]) ).
tff(c_25190,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_24969,c_25178]) ).
tff(c_25194,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_198,c_25190]) ).
tff(c_114,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c4,sk_c9) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_224]) ).
tff(c_24913,plain,
multiply(sk_c4,sk_c9) = sk_c3,
inference(splitLeft,[status(thm)],[c_114]) ).
tff(c_110,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c4,sk_c9) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_218]) ).
tff(c_199,plain,
multiply(sk_c4,sk_c9) = sk_c3,
inference(splitLeft,[status(thm)],[c_110]) ).
tff(c_22598,plain,
! [X_190,Y_191,Z_192] : ( multiply(multiply(X_190,Y_191),Z_192) = multiply(X_190,multiply(Y_191,Z_192)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_22649,plain,
! [Z_192] : ( multiply(sk_c3,multiply(sk_c4,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_150,c_22598]) ).
tff(c_22708,plain,
! [Z_195] : ( multiply(sk_c3,multiply(sk_c4,Z_195)) = Z_195 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22649]) ).
tff(c_22720,plain,
multiply(sk_c3,sk_c3) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_199,c_22708]) ).
tff(c_22652,plain,
! [Z_192] : ( multiply(sk_c9,multiply(sk_c3,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_22598]) ).
tff(c_23136,plain,
! [Z_202] : ( multiply(sk_c9,multiply(sk_c3,Z_202)) = Z_202 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22652]) ).
tff(c_23148,plain,
multiply(sk_c9,sk_c9) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_22720,c_23136]) ).
tff(c_62,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_211,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_21888,plain,
! [X_182,Y_183,Z_184] : ( multiply(multiply(X_182,Y_183),Z_184) = multiply(X_182,multiply(Y_183,Z_184)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_21933,plain,
! [Z_184] : ( multiply(sk_c8,multiply(sk_c2,Z_184)) = multiply(identity,Z_184) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_21888]) ).
tff(c_21962,plain,
! [Z_185] : ( multiply(sk_c8,multiply(sk_c2,Z_185)) = Z_185 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21933]) ).
tff(c_21974,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_211,c_21962]) ).
tff(c_21978,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_198,c_21974]) ).
tff(c_251,plain,
! [X_14,Y_15,Z_16] : ( multiply(multiply(X_14,Y_15),Z_16) = multiply(X_14,multiply(Y_15,Z_16)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_281,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c2,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_251]) ).
tff(c_307,plain,
! [Z_17] : ( multiply(sk_c8,multiply(sk_c2,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_281]) ).
tff(c_319,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_211,c_307]) ).
tff(c_323,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_198,c_319]) ).
tff(c_327,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_323,c_198]) ).
tff(c_293,plain,
! [X_2,Z_16] : ( multiply(inverse(X_2),multiply(X_2,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_251]) ).
tff(c_408,plain,
! [X_19,Z_20] : ( multiply(inverse(X_19),multiply(X_19,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_293]) ).
tff(c_438,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_327,c_408]) ).
tff(c_484,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_438]) ).
tff(c_287,plain,
! [Z_16] : ( multiply(sk_c3,multiply(sk_c4,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_150,c_251]) ).
tff(c_385,plain,
! [Z_18] : ( multiply(sk_c3,multiply(sk_c4,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_287]) ).
tff(c_397,plain,
multiply(sk_c3,sk_c3) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_199,c_385]) ).
tff(c_426,plain,
multiply(inverse(sk_c3),sk_c9) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_397,c_408]) ).
tff(c_481,plain,
multiply(sk_c9,sk_c9) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_133,c_426]) ).
tff(c_617,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_484,c_2,c_484,c_481]) ).
tff(c_462,plain,
multiply(inverse(sk_c3),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_408]) ).
tff(c_487,plain,
multiply(sk_c9,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_133,c_462]) ).
tff(c_582,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_484,c_487]) ).
tff(c_585,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_582,c_146]) ).
tff(c_618,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_617,c_585]) ).
tff(c_305,plain,
! [X_2,Z_16] : ( multiply(inverse(X_2),multiply(X_2,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_293]) ).
tff(c_751,plain,
! [X_23,Z_24] : ( multiply(inverse(inverse(X_23)),Z_24) = multiply(X_23,Z_24) ),
inference(superposition,[status(thm),theory(equality)],[c_305,c_408]) ).
tff(c_474,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_408]) ).
tff(c_758,plain,
! [X_23] : ( multiply(X_23,identity) = X_23 ),
inference(superposition,[status(thm),theory(equality)],[c_751,c_474]) ).
tff(c_328,plain,
multiply(sk_c9,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_323,c_192]) ).
tff(c_30,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_219,plain,
multiply(sk_c1,sk_c9) = sk_c8,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_325,plain,
multiply(sk_c1,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_323,c_219]) ).
tff(c_432,plain,
multiply(inverse(sk_c1),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_325,c_408]) ).
tff(c_483,plain,
sk_c9 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_328,c_158,c_432]) ).
tff(c_504,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_484,c_483]) ).
tff(c_116,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_269]) ).
tff(c_357,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c9 )
| ( inverse(sk_c7) != sk_c7 )
| ( multiply(sk_c7,sk_c7) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c7 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c7 )
| ( multiply(sk_c7,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_323,c_323,c_323,c_323,c_323,c_323,c_323,c_323,c_323,c_116]) ).
tff(c_358,plain,
multiply(sk_c7,sk_c9) != sk_c7,
inference(splitLeft,[status(thm)],[c_357]) ).
tff(c_359,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_327]) ).
tff(c_360,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c7 )
| ( multiply(sk_c7,sk_c7) != sk_c9 )
| ( inverse(sk_c7) != sk_c7 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c7 )
| ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_357]) ).
tff(c_9113,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X3_8) != identity )
| ( identity != X3_8 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_758,c_504,c_484,c_484,c_758,c_504,c_484,c_504,c_758,c_484,c_758,c_484,c_484,c_758,c_504,c_484,c_504,c_758,c_504,c_484,c_484,c_618,c_504,c_504,c_504,c_2,c_504,c_484,c_2,c_484,c_360]) ).
tff(c_9115,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9113]) ).
tff(c_9117,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9115,c_618]) ).
tff(c_9118,plain,
! [X1_9,X5_6,X4_11,X3_8] :
( ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X3_8) != identity )
| ( identity != X3_8 ) ),
inference(splitRight,[status(thm)],[c_9113]) ).
tff(c_21769,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9118]) ).
tff(c_21771,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21769,c_618]) ).
tff(c_21772,plain,
! [X4_11,X5_6,X1_9] :
( ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 ) ),
inference(splitRight,[status(thm)],[c_9118]) ).
tff(c_21782,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_21772]) ).
tff(c_21784,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21782,c_618]) ).
tff(c_21785,plain,
! [X5_6,X4_11] :
( ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(splitRight,[status(thm)],[c_21772]) ).
tff(c_21787,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_21785]) ).
tff(c_21789,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21787,c_618]) ).
tff(c_21792,plain,
! [X5_181] :
( ( inverse(X5_181) != identity )
| ( inverse(X5_181) != X5_181 ) ),
inference(splitRight,[status(thm)],[c_21785]) ).
tff(c_21804,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_618,c_21792]) ).
tff(c_21813,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_618,c_21804]) ).
tff(c_21815,plain,
multiply(sk_c1,sk_c9) != sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_22,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_21831,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_21815,c_22]) ).
tff(c_21835,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21831,c_4]) ).
tff(c_22085,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21978,c_21835]) ).
tff(c_20,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_21881,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_21815,c_20]) ).
tff(c_22081,plain,
multiply(sk_c7,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_21978,c_21881]) ).
tff(c_22173,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22085,c_22081]) ).
tff(c_21814,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_22189,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22173,c_21814]) ).
tff(c_21869,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_21815,c_28]) ).
tff(c_22187,plain,
multiply(sk_c6,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_22173,c_21869]) ).
tff(c_21945,plain,
! [X_2,Z_184] : ( multiply(inverse(X_2),multiply(X_2,Z_184)) = multiply(identity,Z_184) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_21888]) ).
tff(c_21960,plain,
! [X_2,Z_184] : ( multiply(inverse(X_2),multiply(X_2,Z_184)) = Z_184 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21945]) ).
tff(c_22417,plain,
multiply(inverse(sk_c6),sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22187,c_21960]) ).
tff(c_22423,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22189,c_22417]) ).
tff(c_22191,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22173,c_162]) ).
tff(c_22376,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_22191,c_21960]) ).
tff(c_22388,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22376]) ).
tff(c_22087,plain,
multiply(sk_c1,sk_c9) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21978,c_21815]) ).
tff(c_22182,plain,
multiply(sk_c1,identity) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_22173,c_22087]) ).
tff(c_22515,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_22423,c_2,c_22388,c_22182]) ).
tff(c_22517,plain,
multiply(sk_c2,sk_c8) != sk_c9,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_60,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_22573,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_22517,c_60]) ).
tff(c_22516,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_22521,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22516,c_4]) ).
tff(c_22631,plain,
! [Z_192] : ( multiply(sk_c8,multiply(sk_c5,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_22521,c_22598]) ).
tff(c_23173,plain,
! [Z_203] : ( multiply(sk_c8,multiply(sk_c5,Z_203)) = Z_203 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22631]) ).
tff(c_23185,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_22573,c_23173]) ).
tff(c_23189,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_198,c_23185]) ).
tff(c_56,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_22593,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_22517,c_56]) ).
tff(c_22531,plain,
multiply(sk_c1,sk_c9) = sk_c8,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_23295,plain,
! [Z_205] : ( multiply(sk_c1,multiply(sk_c9,Z_205)) = multiply(sk_c8,Z_205) ),
inference(superposition,[status(thm),theory(equality)],[c_22531,c_22598]) ).
tff(c_23328,plain,
multiply(sk_c8,sk_c7) = multiply(sk_c1,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_192,c_23295]) ).
tff(c_23340,plain,
multiply(sk_c1,sk_c8) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_22593,c_23328]) ).
tff(c_23382,plain,
multiply(sk_c1,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_23189,c_23340]) ).
tff(c_22646,plain,
! [Z_192] : ( multiply(sk_c9,multiply(sk_c1,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_22598]) ).
tff(c_22667,plain,
! [Z_192] : ( multiply(sk_c9,multiply(sk_c1,Z_192)) = Z_192 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22646]) ).
tff(c_23386,plain,
multiply(sk_c9,sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_23382,c_22667]) ).
tff(c_23392,plain,
sk_c7 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_23148,c_23386]) ).
tff(c_22548,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_22517,c_58]) ).
tff(c_23348,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_23189,c_22548]) ).
tff(c_23364,plain,
multiply(sk_c7,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23348,c_4]) ).
tff(c_23417,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22720,c_23392,c_23392,c_23364]) ).
tff(c_23418,plain,
multiply(identity,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_23417,c_23417,c_23148]) ).
tff(c_23430,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23418]) ).
tff(c_23438,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23430,c_23392]) ).
tff(c_23355,plain,
multiply(sk_c7,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23189,c_174]) ).
tff(c_23549,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23438,c_23355]) ).
tff(c_23351,plain,
multiply(sk_c2,sk_c7) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_23189,c_22517]) ).
tff(c_23560,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23549,c_23438,c_23417,c_23351]) ).
tff(c_23562,plain,
multiply(sk_c1,sk_c9) != sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_23610,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_23562,c_28]) ).
tff(c_23561,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_23566,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23561,c_4]) ).
tff(c_23631,plain,
! [X_208,Y_209,Z_210] : ( multiply(multiply(X_208,Y_209),Z_210) = multiply(X_208,multiply(Y_209,Z_210)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_23658,plain,
! [Z_210] : ( multiply(sk_c9,multiply(sk_c6,Z_210)) = multiply(identity,Z_210) ),
inference(superposition,[status(thm),theory(equality)],[c_23566,c_23631]) ).
tff(c_24284,plain,
! [Z_222] : ( multiply(sk_c9,multiply(sk_c6,Z_222)) = Z_222 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23658]) ).
tff(c_24299,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_23610,c_24284]) ).
tff(c_24303,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_192,c_24299]) ).
tff(c_24442,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_24303,c_198]) ).
tff(c_24213,plain,
! [Z_221] : ( multiply(sk_c8,multiply(sk_c9,Z_221)) = multiply(sk_c7,Z_221) ),
inference(superposition,[status(thm),theory(equality)],[c_198,c_23631]) ).
tff(c_24240,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c7,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_192,c_24213]) ).
tff(c_24530,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_24442,c_24240]) ).
tff(c_23685,plain,
! [X_2,Z_210] : ( multiply(inverse(X_2),multiply(X_2,Z_210)) = multiply(identity,Z_210) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_23631]) ).
tff(c_24599,plain,
! [X_225,Z_226] : ( multiply(inverse(X_225),multiply(X_225,Z_226)) = Z_226 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23685]) ).
tff(c_24620,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_24530,c_24599]) ).
tff(c_24703,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24620]) ).
tff(c_23576,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_23562,c_22]) ).
tff(c_24683,plain,
multiply(inverse(sk_c8),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_174,c_24599]) ).
tff(c_24717,plain,
multiply(sk_c7,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_23576,c_24683]) ).
tff(c_24882,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24703,c_24717]) ).
tff(c_24635,plain,
multiply(inverse(sk_c8),sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_24442,c_24599]) ).
tff(c_24708,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_24530,c_23576,c_24635]) ).
tff(c_24758,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24703,c_24708]) ).
tff(c_24440,plain,
multiply(sk_c2,sk_c8) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_24303,c_22517]) ).
tff(c_24760,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_24758,c_24758,c_24440]) ).
tff(c_24910,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24882,c_24760]) ).
tff(c_24912,plain,
multiply(sk_c4,sk_c9) != sk_c3,
inference(splitRight,[status(thm)],[c_110]) ).
tff(c_24930,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24913,c_24912]) ).
tff(c_24932,plain,
multiply(sk_c4,sk_c9) != sk_c3,
inference(splitRight,[status(thm)],[c_114]) ).
tff(c_106,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c4,sk_c9) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_212]) ).
tff(c_24981,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_24932,c_106]) ).
tff(c_24985,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24981,c_4]) ).
tff(c_25198,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25194,c_24985]) ).
tff(c_104,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( multiply(sk_c4,sk_c9) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_25005,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_24932,c_104]) ).
tff(c_25196,plain,
multiply(sk_c7,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_25194,c_25005]) ).
tff(c_25296,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25198,c_25196]) ).
tff(c_25308,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25296,c_137]) ).
tff(c_25421,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_25308,c_2]) ).
tff(c_25432,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25421,c_150]) ).
tff(c_25081,plain,
! [X_2,Z_231] : ( multiply(inverse(X_2),multiply(X_2,Z_231)) = multiply(identity,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_25024]) ).
tff(c_25096,plain,
! [X_2,Z_231] : ( multiply(inverse(X_2),multiply(X_2,Z_231)) = Z_231 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25081]) ).
tff(c_25656,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_25432,c_25096]) ).
tff(c_25668,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25656]) ).
tff(c_25304,plain,
multiply(sk_c4,identity) != sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_25296,c_24932]) ).
tff(c_25576,plain,
multiply(sk_c4,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_25421,c_25304]) ).
tff(c_25672,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_25668,c_25576]) ).
tff(c_25677,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25672]) ).
tff(c_25679,plain,
multiply(sk_c2,sk_c8) != sk_c9,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_25678,plain,
inverse(sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_25683,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25678,c_4]) ).
tff(c_26204,plain,
! [X_250,Y_251,Z_252] : ( multiply(multiply(X_250,Y_251),Z_252) = multiply(X_250,multiply(Y_251,Z_252)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_26228,plain,
! [Z_252] : ( multiply(sk_c7,multiply(sk_c8,Z_252)) = multiply(identity,Z_252) ),
inference(superposition,[status(thm),theory(equality)],[c_25683,c_26204]) ).
tff(c_26400,plain,
! [Z_258] : ( multiply(sk_c7,multiply(sk_c8,Z_258)) = Z_258 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26228]) ).
tff(c_26433,plain,
multiply(sk_c7,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_174,c_26400]) ).
tff(c_24911,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_110]) ).
tff(c_24936,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24911,c_4]) ).
tff(c_26427,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_24936,c_26400]) ).
tff(c_26476,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_26433,c_26427]) ).
tff(c_25706,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_25679,c_60]) ).
tff(c_26477,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_26476,c_25706]) ).
tff(c_26481,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25679,c_26477]) ).
tff(c_26483,plain,
multiply(sk_c8,sk_c9) != sk_c7,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_18,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_27627,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_26483,c_18]) ).
tff(c_16,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_28344,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_26483,c_16]) ).
tff(c_28369,plain,
! [X_296,Y_297,Z_298] : ( multiply(multiply(X_296,Y_297),Z_298) = multiply(X_296,multiply(Y_297,Z_298)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_28420,plain,
! [X_2,Z_298] : ( multiply(inverse(X_2),multiply(X_2,Z_298)) = multiply(identity,Z_298) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_28369]) ).
tff(c_28499,plain,
! [X_301,Z_302] : ( multiply(inverse(X_301),multiply(X_301,Z_302)) = Z_302 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28420]) ).
tff(c_28538,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_28344,c_28499]) ).
tff(c_28602,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_192,c_27627,c_28538]) ).
tff(c_26503,plain,
multiply(sk_c1,sk_c9) = sk_c8,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_27075,plain,
! [X_270,Y_271,Z_272] : ( multiply(multiply(X_270,Y_271),Z_272) = multiply(X_270,multiply(Y_271,Z_272)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_27120,plain,
! [Z_272] : ( multiply(sk_c9,multiply(sk_c1,Z_272)) = multiply(identity,Z_272) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_27075]) ).
tff(c_27159,plain,
! [Z_274] : ( multiply(sk_c9,multiply(sk_c1,Z_274)) = Z_274 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27120]) ).
tff(c_27171,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_26503,c_27159]) ).
tff(c_27129,plain,
! [X_2,Z_272] : ( multiply(inverse(X_2),multiply(X_2,Z_272)) = multiply(identity,Z_272) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_27075]) ).
tff(c_27244,plain,
! [X_277,Z_278] : ( multiply(inverse(X_277),multiply(X_277,Z_278)) = Z_278 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27129]) ).
tff(c_27277,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_27171,c_27244]) ).
tff(c_27358,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_27277]) ).
tff(c_26517,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_26483,c_18]) ).
tff(c_27053,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_26483,c_16]) ).
tff(c_27292,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_27053,c_27244]) ).
tff(c_27361,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_192,c_26517,c_27292]) ).
tff(c_26521,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_26517,c_4]) ).
tff(c_27382,plain,
multiply(sk_c8,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27361,c_26521]) ).
tff(c_27532,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27358,c_27382]) ).
tff(c_27383,plain,
inverse(sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27361,c_26517]) ).
tff(c_27448,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27358,c_27383]) ).
tff(c_27533,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27532,c_27448]) ).
tff(c_26577,plain,
! [X_260,Y_261,Z_262] : ( multiply(multiply(X_260,Y_261),Z_262) = multiply(X_260,multiply(Y_261,Z_262)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_26625,plain,
! [Z_262] : ( multiply(sk_c9,multiply(sk_c1,Z_262)) = multiply(identity,Z_262) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_26577]) ).
tff(c_26677,plain,
! [Z_264] : ( multiply(sk_c9,multiply(sk_c1,Z_264)) = Z_264 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26625]) ).
tff(c_26689,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_26503,c_26677]) ).
tff(c_26634,plain,
! [X_2,Z_262] : ( multiply(inverse(X_2),multiply(X_2,Z_262)) = multiply(identity,Z_262) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_26577]) ).
tff(c_26716,plain,
! [X_266,Z_267] : ( multiply(inverse(X_266),multiply(X_266,Z_267)) = Z_267 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26634]) ).
tff(c_26737,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_26689,c_26716]) ).
tff(c_26822,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26737]) ).
tff(c_26531,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_26622,plain,
! [Z_262] : ( multiply(sk_c8,multiply(sk_c2,Z_262)) = multiply(identity,Z_262) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_26577]) ).
tff(c_26651,plain,
! [Z_263] : ( multiply(sk_c8,multiply(sk_c2,Z_263)) = Z_263 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26622]) ).
tff(c_26663,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_26531,c_26651]) ).
tff(c_26669,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_26663,c_26483]) ).
tff(c_26863,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_26822,c_26669]) ).
tff(c_26870,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26822,c_170]) ).
tff(c_26968,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_26870,c_4]) ).
tff(c_26649,plain,
! [X_2,Z_262] : ( multiply(inverse(X_2),multiply(X_2,Z_262)) = Z_262 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26634]) ).
tff(c_26998,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_26968,c_26649]) ).
tff(c_27010,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26998]) ).
tff(c_27014,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27010,c_26870]) ).
tff(c_10,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_26537,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_26483,c_10]) ).
tff(c_26866,plain,
inverse(identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_26822,c_26537]) ).
tff(c_27024,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27014,c_26866]) ).
tff(c_27026,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26863,c_27024]) ).
tff(c_27027,plain,
inverse(sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_27399,plain,
inverse(identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_27358,c_27027]) ).
tff(c_27538,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27533,c_27399]) ).
tff(c_27386,plain,
multiply(sk_c8,sk_c8) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_27361,c_26483]) ).
tff(c_27606,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_27538,c_27358,c_2,c_27358,c_27386]) ).
tff(c_27608,plain,
multiply(sk_c1,sk_c9) != sk_c8,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_28621,plain,
multiply(sk_c1,sk_c8) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28602,c_27608]) ).
tff(c_27607,plain,
inverse(sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_26482,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_26487,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_26482,c_4]) ).
tff(c_28559,plain,
multiply(inverse(sk_c8),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_26487,c_28499]) ).
tff(c_28605,plain,
multiply(sk_c7,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_27607,c_28559]) ).
tff(c_28624,plain,
multiply(sk_c8,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28602,c_162]) ).
tff(c_28435,plain,
! [X_2,Z_298] : ( multiply(inverse(X_2),multiply(X_2,Z_298)) = Z_298 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28420]) ).
tff(c_28688,plain,
multiply(inverse(sk_c8),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_28624,c_28435]) ).
tff(c_28694,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_28605,c_27607,c_28688]) ).
tff(c_27684,plain,
! [X_282,Y_283,Z_284] : ( multiply(multiply(X_282,Y_283),Z_284) = multiply(X_282,multiply(Y_283,Z_284)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_27735,plain,
! [Z_284] : ( multiply(sk_c9,multiply(sk_c3,Z_284)) = multiply(identity,Z_284) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_27684]) ).
tff(c_27779,plain,
! [Z_286] : ( multiply(sk_c9,multiply(sk_c3,Z_286)) = Z_286 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27735]) ).
tff(c_27791,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_27779]) ).
tff(c_27612,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27607,c_4]) ).
tff(c_27837,plain,
! [Z_289] : ( multiply(sk_c9,multiply(sk_c7,Z_289)) = multiply(sk_c8,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_192,c_27684]) ).
tff(c_27849,plain,
multiply(sk_c9,identity) = multiply(sk_c8,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_27612,c_27837]) ).
tff(c_27853,plain,
multiply(sk_c8,sk_c8) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27791,c_27849]) ).
tff(c_27662,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_26483,c_16]) ).
tff(c_27631,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27627,c_4]) ).
tff(c_27711,plain,
! [Z_284] : ( multiply(sk_c9,multiply(sk_c6,Z_284)) = multiply(identity,Z_284) ),
inference(superposition,[status(thm),theory(equality)],[c_27631,c_27684]) ).
tff(c_27878,plain,
! [Z_290] : ( multiply(sk_c9,multiply(sk_c6,Z_290)) = Z_290 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27711]) ).
tff(c_27890,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_27662,c_27878]) ).
tff(c_27894,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_192,c_27890]) ).
tff(c_27650,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_27726,plain,
! [Z_284] : ( multiply(sk_c8,multiply(sk_c2,Z_284)) = multiply(identity,Z_284) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_27684]) ).
tff(c_27755,plain,
! [Z_285] : ( multiply(sk_c8,multiply(sk_c2,Z_285)) = Z_285 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27726]) ).
tff(c_27767,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_27650,c_27755]) ).
tff(c_27902,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27894,c_27767]) ).
tff(c_27916,plain,
sk_c8 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27853,c_27902]) ).
tff(c_27993,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_27916,c_27607]) ).
tff(c_27998,plain,
sk_c7 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_146,c_27993]) ).
tff(c_27738,plain,
! [X_2,Z_284] : ( multiply(inverse(X_2),multiply(X_2,Z_284)) = multiply(identity,Z_284) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_27684]) ).
tff(c_27921,plain,
! [X_291,Z_292] : ( multiply(inverse(X_291),multiply(X_291,Z_292)) = Z_292 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27738]) ).
tff(c_27963,plain,
multiply(inverse(sk_c8),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_174,c_27921]) ).
tff(c_27985,plain,
multiply(sk_c7,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_27607,c_27963]) ).
tff(c_28130,plain,
multiply(sk_c3,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_27998,c_27985]) ).
tff(c_27915,plain,
inverse(sk_c3) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27894,c_133]) ).
tff(c_28070,plain,
inverse(sk_c3) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27916,c_27915]) ).
tff(c_28077,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28070,c_4]) ).
tff(c_27753,plain,
! [X_2,Z_284] : ( multiply(inverse(X_2),multiply(X_2,Z_284)) = Z_284 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27738]) ).
tff(c_28149,plain,
multiply(inverse(sk_c4),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_28077,c_27753]) ).
tff(c_28158,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28130,c_146,c_28149]) ).
tff(c_28167,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28158,c_27998]) ).
tff(c_27657,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_27608,c_20]) ).
tff(c_27905,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27894,c_27657]) ).
tff(c_28222,plain,
multiply(sk_c4,sk_c2) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_28167,c_27916,c_27916,c_27905]) ).
tff(c_28229,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_28222,c_27753]) ).
tff(c_28236,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_28229]) ).
tff(c_27771,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_27767,c_26483]) ).
tff(c_27990,plain,
sk_c7 != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27916,c_27771]) ).
tff(c_28043,plain,
sk_c4 != sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_27998,c_27990]) ).
tff(c_28166,plain,
sk_c4 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28158,c_28043]) ).
tff(c_28243,plain,
sk_c4 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_28236,c_28166]) ).
tff(c_28170,plain,
inverse(sk_c4) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28158,c_146]) ).
tff(c_28241,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28236,c_28170]) ).
tff(c_27908,plain,
inverse(sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_27894,c_27627]) ).
tff(c_28048,plain,
inverse(sk_c6) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27916,c_27908]) ).
tff(c_28055,plain,
multiply(sk_c4,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28048,c_4]) ).
tff(c_28316,plain,
multiply(inverse(sk_c4),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_28055,c_27753]) ).
tff(c_28322,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28241,c_28316]) ).
tff(c_28242,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28236,c_28167]) ).
tff(c_27904,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_27894,c_27662]) ).
tff(c_28333,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28322,c_28242,c_27916,c_27904]) ).
tff(c_28334,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28243,c_28333]) ).
tff(c_28335,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_28617,plain,
multiply(sk_c5,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28602,c_28335]) ).
tff(c_28814,plain,
multiply(sk_c1,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28694,c_28617]) ).
tff(c_28815,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28621,c_28814]) ).
tff(c_28816,plain,
inverse(sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_32908,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_32956,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_32908]) ).
tff(c_33097,plain,
! [X_386,Z_387] : ( multiply(inverse(X_386),multiply(X_386,Z_387)) = Z_387 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32956]) ).
tff(c_33172,plain,
multiply(inverse(sk_c8),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_174,c_33097]) ).
tff(c_33213,plain,
multiply(sk_c7,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28816,c_33172]) ).
tff(c_28817,plain,
multiply(sk_c9,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_44,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_31838,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_28817,c_44]) ).
tff(c_33148,plain,
multiply(inverse(sk_c8),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_31838,c_33097]) ).
tff(c_33210,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28816,c_33148]) ).
tff(c_32971,plain,
! [X_2,Z_380] : ( multiply(inverse(X_2),multiply(X_2,Z_380)) = Z_380 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32956]) ).
tff(c_33307,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_33210,c_32971]) ).
tff(c_33313,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33307]) ).
tff(c_12,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_31832,plain,
multiply(sk_c8,sk_c9) = sk_c7,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_31200,plain,
! [X_345,Y_346,Z_347] : ( multiply(multiply(X_345,Y_346),Z_347) = multiply(X_345,multiply(Y_346,Z_347)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_31245,plain,
! [Z_347] : ( multiply(sk_c9,multiply(sk_c3,Z_347)) = multiply(identity,Z_347) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_31200]) ).
tff(c_31316,plain,
! [Z_351] : ( multiply(sk_c9,multiply(sk_c3,Z_351)) = Z_351 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31245]) ).
tff(c_31334,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_31316]) ).
tff(c_54,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_30581,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_28817,c_54]) ).
tff(c_52,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_30612,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_28817,c_52]) ).
tff(c_31248,plain,
! [X_2,Z_347] : ( multiply(inverse(X_2),multiply(X_2,Z_347)) = multiply(identity,Z_347) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_31200]) ).
tff(c_31378,plain,
! [X_353,Z_354] : ( multiply(inverse(X_353),multiply(X_353,Z_354)) = Z_354 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31248]) ).
tff(c_31429,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_30612,c_31378]) ).
tff(c_31489,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_30581,c_31429]) ).
tff(c_31263,plain,
! [X_2,Z_347] : ( multiply(inverse(X_2),multiply(X_2,Z_347)) = Z_347 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31248]) ).
tff(c_31503,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_31489,c_31263]) ).
tff(c_31509,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_31503]) ).
tff(c_31511,plain,
multiply(sk_c9,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_31509,c_31489]) ).
tff(c_31518,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_31334,c_31511]) ).
tff(c_28852,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_28817,c_54]) ).
tff(c_28904,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_28817,c_52]) ).
tff(c_28917,plain,
! [X_304,Y_305,Z_306] : ( multiply(multiply(X_304,Y_305),Z_306) = multiply(X_304,multiply(Y_305,Z_306)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_28974,plain,
! [X_2,Z_306] : ( multiply(inverse(X_2),multiply(X_2,Z_306)) = multiply(identity,Z_306) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_28917]) ).
tff(c_29081,plain,
! [X_308,Z_309] : ( multiply(inverse(X_308),multiply(X_308,Z_309)) = Z_309 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28974]) ).
tff(c_29111,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_28904,c_29081]) ).
tff(c_29148,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_28852,c_29111]) ).
tff(c_28989,plain,
! [X_2,Z_306] : ( multiply(inverse(X_2),multiply(X_2,Z_306)) = Z_306 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28974]) ).
tff(c_29176,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_29148,c_28989]) ).
tff(c_29182,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_29176]) ).
tff(c_28836,plain,
multiply(sk_c8,sk_c9) = sk_c7,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_28841,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_28962,plain,
! [Z_306] : ( multiply(sk_c8,multiply(sk_c2,Z_306)) = multiply(identity,Z_306) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_28917]) ).
tff(c_28991,plain,
! [Z_307] : ( multiply(sk_c8,multiply(sk_c2,Z_307)) = Z_307 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28962]) ).
tff(c_29003,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_28841,c_28991]) ).
tff(c_29007,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28836,c_29003]) ).
tff(c_29020,plain,
inverse(sk_c2) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_29007,c_170]) ).
tff(c_29200,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29182,c_29020]) ).
tff(c_29129,plain,
multiply(inverse(sk_c3),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_29081]) ).
tff(c_29150,plain,
multiply(sk_c9,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_133,c_29129]) ).
tff(c_29197,plain,
multiply(sk_c9,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_29182,c_29148]) ).
tff(c_29203,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_29150,c_29197]) ).
tff(c_29014,plain,
multiply(sk_c2,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_29007,c_28841]) ).
tff(c_29326,plain,
multiply(sk_c2,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_29203,c_29182,c_29014]) ).
tff(c_29330,plain,
multiply(inverse(sk_c2),sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_29326,c_28989]) ).
tff(c_29336,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29200,c_29330]) ).
tff(c_29345,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29336,c_29203]) ).
tff(c_29017,plain,
multiply(sk_c9,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_29007,c_28817]) ).
tff(c_29463,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29345,c_29182,c_29182,c_29017]) ).
tff(c_29465,plain,
multiply(sk_c2,sk_c8) != sk_c9,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_66,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_29481,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_29465,c_66]) ).
tff(c_29510,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_28817,c_52]) ).
tff(c_29978,plain,
! [X_322,Y_323,Z_324] : ( multiply(multiply(X_322,Y_323),Z_324) = multiply(X_322,multiply(Y_323,Z_324)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_30029,plain,
! [X_2,Z_324] : ( multiply(inverse(X_2),multiply(X_2,Z_324)) = multiply(identity,Z_324) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_29978]) ).
tff(c_30127,plain,
! [X_329,Z_330] : ( multiply(inverse(X_329),multiply(X_329,Z_330)) = Z_330 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30029]) ).
tff(c_30172,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_29510,c_30127]) ).
tff(c_30235,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_29481,c_30172]) ).
tff(c_30044,plain,
! [X_2,Z_324] : ( multiply(inverse(X_2),multiply(X_2,Z_324)) = Z_324 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30029]) ).
tff(c_30338,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_30235,c_30044]) ).
tff(c_30344,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_30338]) ).
tff(c_30187,plain,
multiply(inverse(sk_c8),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_28836,c_30127]) ).
tff(c_30237,plain,
multiply(sk_c7,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_28816,c_30187]) ).
tff(c_30390,plain,
multiply(identity,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_30344,c_30344,c_30237]) ).
tff(c_30397,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30390]) ).
tff(c_30026,plain,
! [Z_324] : ( multiply(sk_c9,multiply(sk_c3,Z_324)) = multiply(identity,Z_324) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_29978]) ).
tff(c_30061,plain,
! [Z_326] : ( multiply(sk_c9,multiply(sk_c3,Z_326)) = Z_326 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30026]) ).
tff(c_30073,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_30061]) ).
tff(c_30389,plain,
multiply(sk_c9,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_30344,c_30235]) ).
tff(c_30396,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_30073,c_30389]) ).
tff(c_30419,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_30397,c_30396]) ).
tff(c_30412,plain,
inverse(sk_c1) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_30396,c_158]) ).
tff(c_30459,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_30419,c_30412]) ).
tff(c_30466,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_30459,c_4]) ).
tff(c_30539,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_30466,c_30044]) ).
tff(c_30551,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_30539]) ).
tff(c_29464,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_29515,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_29465,c_60]) ).
tff(c_30169,plain,
multiply(inverse(sk_c5),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_29515,c_30127]) ).
tff(c_30234,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28836,c_29464,c_30169]) ).
tff(c_29521,plain,
multiply(sk_c1,sk_c9) = sk_c8,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_29543,plain,
! [X_312,Y_313,Z_314] : ( multiply(multiply(X_312,Y_313),Z_314) = multiply(X_312,multiply(Y_313,Z_314)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_29588,plain,
! [Z_314] : ( multiply(sk_c9,multiply(sk_c1,Z_314)) = multiply(identity,Z_314) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_29543]) ).
tff(c_29627,plain,
! [Z_316] : ( multiply(sk_c9,multiply(sk_c1,Z_316)) = Z_316 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29588]) ).
tff(c_29639,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_29521,c_29627]) ).
tff(c_29597,plain,
! [X_2,Z_314] : ( multiply(inverse(X_2),multiply(X_2,Z_314)) = multiply(identity,Z_314) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_29543]) ).
tff(c_29786,plain,
! [X_320,Z_321] : ( multiply(inverse(X_320),multiply(X_320,Z_321)) = Z_321 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29597]) ).
tff(c_29828,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_29639,c_29786]) ).
tff(c_29896,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_29828]) ).
tff(c_29594,plain,
! [Z_314] : ( multiply(sk_c9,multiply(sk_c3,Z_314)) = multiply(identity,Z_314) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_29543]) ).
tff(c_29675,plain,
! [Z_318] : ( multiply(sk_c9,multiply(sk_c3,Z_318)) = Z_318 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29594]) ).
tff(c_29693,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_29675]) ).
tff(c_28821,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28816,c_4]) ).
tff(c_29712,plain,
! [Z_319] : ( multiply(sk_c8,multiply(sk_c9,Z_319)) = multiply(sk_c7,Z_319) ),
inference(superposition,[status(thm),theory(equality)],[c_28836,c_29543]) ).
tff(c_29733,plain,
multiply(sk_c8,sk_c9) = multiply(sk_c7,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_29639,c_29712]) ).
tff(c_29749,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28821,c_28836,c_29733]) ).
tff(c_29755,plain,
multiply(sk_c9,identity) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_29749,c_28817]) ).
tff(c_29758,plain,
sk_c8 != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_29693,c_29755]) ).
tff(c_29910,plain,
sk_c4 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_29896,c_29758]) ).
tff(c_29756,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29749,c_28816]) ).
tff(c_29753,plain,
multiply(sk_c8,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29749,c_28836]) ).
tff(c_29804,plain,
multiply(inverse(sk_c8),identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_29753,c_29786]) ).
tff(c_29892,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29756,c_29804]) ).
tff(c_29911,plain,
multiply(sk_c9,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_29896,c_29639]) ).
tff(c_29920,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_29693,c_29911]) ).
tff(c_29953,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29892,c_29920]) ).
tff(c_29955,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_29910,c_29953]) ).
tff(c_29957,plain,
multiply(sk_c1,sk_c9) != sk_c8,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_30246,plain,
multiply(sk_c1,sk_c9) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_30234,c_29957]) ).
tff(c_30565,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30551,c_30397,c_30344,c_30246]) ).
tff(c_30566,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_30618,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_30646,plain,
! [X_333,Y_334,Z_335] : ( multiply(multiply(X_333,Y_334),Z_335) = multiply(X_333,multiply(Y_334,Z_335)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_30685,plain,
! [Z_335] : ( multiply(sk_c8,multiply(sk_c2,Z_335)) = multiply(identity,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_30646]) ).
tff(c_30714,plain,
! [Z_336] : ( multiply(sk_c8,multiply(sk_c2,Z_336)) = Z_336 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30685]) ).
tff(c_30726,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_30618,c_30714]) ).
tff(c_30697,plain,
! [X_2,Z_335] : ( multiply(inverse(X_2),multiply(X_2,Z_335)) = multiply(identity,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_30646]) ).
tff(c_30850,plain,
! [X_341,Z_342] : ( multiply(inverse(X_341),multiply(X_341,Z_342)) = Z_342 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30697]) ).
tff(c_30889,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_30726,c_30850]) ).
tff(c_30965,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28821,c_28816,c_30889]) ).
tff(c_30907,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_30612,c_30850]) ).
tff(c_30970,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_30581,c_30907]) ).
tff(c_31133,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_30965,c_2,c_30965,c_30970]) ).
tff(c_30567,plain,
multiply(sk_c8,sk_c9) != sk_c7,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_30732,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_30726,c_30567]) ).
tff(c_31135,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_31133,c_30732]) ).
tff(c_28829,plain,
multiply(sk_c4,sk_c9) = sk_c3,
inference(splitLeft,[status(thm)],[c_110]) ).
tff(c_30691,plain,
! [Z_335] : ( multiply(sk_c3,multiply(sk_c4,Z_335)) = multiply(identity,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_150,c_30646]) ).
tff(c_30740,plain,
! [Z_337] : ( multiply(sk_c3,multiply(sk_c4,Z_337)) = Z_337 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30691]) ).
tff(c_30752,plain,
multiply(sk_c3,sk_c3) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_28829,c_30740]) ).
tff(c_30694,plain,
! [Z_335] : ( multiply(sk_c9,multiply(sk_c3,Z_335)) = multiply(identity,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_30646]) ).
tff(c_30804,plain,
! [Z_340] : ( multiply(sk_c9,multiply(sk_c3,Z_340)) = Z_340 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30694]) ).
tff(c_30819,plain,
multiply(sk_c9,sk_c9) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_30752,c_30804]) ).
tff(c_30979,plain,
multiply(identity,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_30965,c_30965,c_30819]) ).
tff(c_30998,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30979]) ).
tff(c_30825,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_30804]) ).
tff(c_30980,plain,
multiply(identity,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_30965,c_30825]) ).
tff(c_30999,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30980]) ).
tff(c_31008,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_30999,c_146]) ).
tff(c_31064,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_30998,c_31008]) ).
tff(c_30931,plain,
multiply(inverse(sk_c8),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_174,c_30850]) ).
tff(c_30973,plain,
multiply(sk_c7,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28816,c_30931]) ).
tff(c_31134,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_31133,c_30973]) ).
tff(c_31138,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31134]) ).
tff(c_31146,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_31138,c_170]) ).
tff(c_31148,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31064,c_31146]) ).
tff(c_31171,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31135,c_31148]) ).
tff(c_31173,plain,
multiply(sk_c2,sk_c8) != sk_c9,
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_31180,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_31173,c_60]) ).
tff(c_31423,plain,
multiply(inverse(sk_c5),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_31180,c_31378]) ).
tff(c_31487,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_30566,c_31423]) ).
tff(c_31694,plain,
multiply(sk_c8,sk_c4) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_31518,c_31487]) ).
tff(c_31698,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_31694,c_31263]) ).
tff(c_31704,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_31698]) ).
tff(c_31573,plain,
inverse(sk_c3) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_31518,c_133]) ).
tff(c_31643,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_31573,c_4]) ).
tff(c_31773,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31704,c_31643]) ).
tff(c_31716,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_31704,c_146]) ).
tff(c_30571,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_30566,c_4]) ).
tff(c_31438,plain,
multiply(inverse(sk_c8),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_30571,c_31378]) ).
tff(c_31490,plain,
multiply(sk_c7,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_28816,c_31438]) ).
tff(c_31647,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31509,c_31490]) ).
tff(c_31649,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_31647,c_30566]) ).
tff(c_31754,plain,
sk_c8 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_31716,c_31649]) ).
tff(c_31499,plain,
sk_c9 != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_31489,c_28817]) ).
tff(c_31559,plain,
sk_c8 != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_31518,c_31499]) ).
tff(c_31712,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_31704,c_31559]) ).
tff(c_31766,plain,
sk_c3 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_31754,c_31712]) ).
tff(c_31782,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_31773,c_31766]) ).
tff(c_31783,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_110]) ).
tff(c_31843,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_31874,plain,
! [X_358,Y_359,Z_360] : ( multiply(multiply(X_358,Y_359),Z_360) = multiply(X_358,multiply(Y_359,Z_360)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_31916,plain,
! [Z_360] : ( multiply(sk_c8,multiply(sk_c2,Z_360)) = multiply(identity,Z_360) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_31874]) ).
tff(c_31945,plain,
! [Z_361] : ( multiply(sk_c8,multiply(sk_c2,Z_361)) = Z_361 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31916]) ).
tff(c_31957,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_31843,c_31945]) ).
tff(c_31961,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_31832,c_31957]) ).
tff(c_31967,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_31961,c_31832]) ).
tff(c_31928,plain,
! [X_2,Z_360] : ( multiply(inverse(X_2),multiply(X_2,Z_360)) = multiply(identity,Z_360) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_31874]) ).
tff(c_32144,plain,
! [X_364,Z_365] : ( multiply(inverse(X_364),multiply(X_364,Z_365)) = Z_365 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31928]) ).
tff(c_32171,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_31967,c_32144]) ).
tff(c_32226,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_32171]) ).
tff(c_31971,plain,
multiply(sk_c9,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_31961,c_28817]) ).
tff(c_32388,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32226,c_31971]) ).
tff(c_32389,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_33145,plain,
multiply(inverse(sk_c5),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_32389,c_33097]) ).
tff(c_33209,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_31832,c_31783,c_33145]) ).
tff(c_33225,plain,
multiply(sk_c7,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_33209,c_31838]) ).
tff(c_33433,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33313,c_33225]) ).
tff(c_32929,plain,
! [Z_380] : ( multiply(sk_c8,multiply(sk_c7,Z_380)) = multiply(sk_c9,Z_380) ),
inference(superposition,[status(thm),theory(equality)],[c_31838,c_32908]) ).
tff(c_33328,plain,
! [Z_380] : ( multiply(sk_c7,multiply(sk_c7,Z_380)) = Z_380 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33313,c_33209,c_32929]) ).
tff(c_33437,plain,
multiply(sk_c7,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33433,c_33328]) ).
tff(c_33446,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_33213,c_33437]) ).
tff(c_31784,plain,
multiply(sk_c4,sk_c9) != sk_c3,
inference(splitRight,[status(thm)],[c_110]) ).
tff(c_31798,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_31784,c_114]) ).
tff(c_32395,plain,
multiply(sk_c1,sk_c9) = sk_c8,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_32420,plain,
! [X_367,Y_368,Z_369] : ( multiply(multiply(X_367,Y_368),Z_369) = multiply(X_367,multiply(Y_368,Z_369)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_32462,plain,
! [Z_369] : ( multiply(sk_c9,multiply(sk_c1,Z_369)) = multiply(identity,Z_369) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_32420]) ).
tff(c_32527,plain,
! [Z_372] : ( multiply(sk_c9,multiply(sk_c1,Z_372)) = Z_372 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32462]) ).
tff(c_32539,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_32395,c_32527]) ).
tff(c_32471,plain,
! [X_2,Z_369] : ( multiply(inverse(X_2),multiply(X_2,Z_369)) = multiply(identity,Z_369) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_32420]) ).
tff(c_32566,plain,
! [X_374,Z_375] : ( multiply(inverse(X_374),multiply(X_374,Z_375)) = Z_375 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32471]) ).
tff(c_32587,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_32539,c_32566]) ).
tff(c_32670,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_32587]) ).
tff(c_32611,plain,
multiply(inverse(sk_c5),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_32389,c_32566]) ).
tff(c_32674,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_31832,c_31783,c_32611]) ).
tff(c_32702,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_32670,c_32674]) ).
tff(c_32695,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_32674,c_28816]) ).
tff(c_32770,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_32702,c_32702,c_32695]) ).
tff(c_32447,plain,
! [Z_369] : ( multiply(sk_c8,multiply(sk_c9,Z_369)) = multiply(sk_c7,Z_369) ),
inference(superposition,[status(thm),theory(equality)],[c_31832,c_32420]) ).
tff(c_32799,plain,
! [Z_369] : ( multiply(sk_c9,Z_369) = Z_369 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32702,c_2,c_32670,c_32447]) ).
tff(c_32468,plain,
! [Z_369] : ( multiply(sk_c9,multiply(sk_c3,Z_369)) = multiply(identity,Z_369) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_32420]) ).
tff(c_32503,plain,
! [Z_371] : ( multiply(sk_c9,multiply(sk_c3,Z_371)) = Z_371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32468]) ).
tff(c_32515,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_32503]) ).
tff(c_32800,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_32799,c_32515]) ).
tff(c_32850,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_32800,c_146]) ).
tff(c_32853,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_32770,c_32850]) ).
tff(c_32861,plain,
inverse(identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_32853,c_133]) ).
tff(c_32864,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_32770,c_32861]) ).
tff(c_32848,plain,
multiply(identity,sk_c9) != sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_32800,c_31784]) ).
tff(c_32852,plain,
sk_c9 != sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32848]) ).
tff(c_32858,plain,
sk_c9 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_32853,c_32852]) ).
tff(c_32882,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_32864,c_32858]) ).
tff(c_32883,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_33142,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_32883,c_33097]) ).
tff(c_33208,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_31798,c_33142]) ).
tff(c_33522,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33446,c_33313,c_2,c_33313,c_33208]) ).
tff(c_33528,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33522,c_33446]) ).
tff(c_32390,plain,
multiply(sk_c2,sk_c8) != sk_c9,
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_33223,plain,
multiply(sk_c2,sk_c7) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_33209,c_32390]) ).
tff(c_33616,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_33528,c_2,c_33522,c_33313,c_33223]) ).
tff(c_33618,plain,
multiply(sk_c8,sk_c9) != sk_c7,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_8,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( multiply(sk_c8,sk_c9) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_33635,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_33618,c_8]) ).
tff(c_33995,plain,
multiply(identity,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_33974,c_33635]) ).
tff(c_34011,plain,
sk_c9 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33995]) ).
tff(c_34032,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34009,c_34011]) ).
tff(c_33997,plain,
multiply(identity,sk_c9) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33974,c_33618]) ).
tff(c_34012,plain,
sk_c9 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33997]) ).
tff(c_34074,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34032,c_34009,c_34012]) ).
tff(c_34075,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_31802,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_31798,c_4]) ).
tff(c_34131,plain,
! [Z_404] : ( multiply(sk_c9,multiply(sk_c6,Z_404)) = multiply(identity,Z_404) ),
inference(superposition,[status(thm),theory(equality)],[c_31802,c_34107]) ).
tff(c_34237,plain,
! [Z_409] : ( multiply(sk_c9,multiply(sk_c6,Z_409)) = Z_409 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34131]) ).
tff(c_34249,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_34075,c_34237]) ).
tff(c_34152,plain,
! [X_2,Z_404] : ( multiply(inverse(X_2),multiply(X_2,Z_404)) = multiply(identity,Z_404) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34107]) ).
tff(c_34261,plain,
! [X_410,Z_411] : ( multiply(inverse(X_410),multiply(X_410,Z_411)) = Z_411 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34152]) ).
tff(c_34279,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34249,c_34261]) ).
tff(c_34361,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_34279]) ).
tff(c_34375,plain,
multiply(sk_c9,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_34361,c_34249]) ).
tff(c_34381,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34225,c_34375]) ).
tff(c_33617,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_34309,plain,
multiply(inverse(sk_c5),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_33617,c_34261]) ).
tff(c_34366,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_31783,c_34309]) ).
tff(c_34498,plain,
multiply(sk_c8,sk_c4) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_34381,c_34366]) ).
tff(c_34167,plain,
! [X_2,Z_404] : ( multiply(inverse(X_2),multiply(X_2,Z_404)) = Z_404 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34152]) ).
tff(c_34502,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_34498,c_34167]) ).
tff(c_34508,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_34502]) ).
tff(c_34253,plain,
sk_c9 != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_34249,c_28817]) ).
tff(c_34386,plain,
sk_c8 != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34381,c_34253]) ).
tff(c_34515,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_34508,c_34386]) ).
tff(c_34519,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_34508,c_146]) ).
tff(c_34394,plain,
inverse(sk_c6) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34381,c_31798]) ).
tff(c_34466,plain,
multiply(sk_c4,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34394,c_4]) ).
tff(c_34526,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34508,c_34466]) ).
tff(c_34512,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34508,c_34394]) ).
tff(c_34567,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34519,c_34526,c_34512]) ).
tff(c_34399,plain,
inverse(sk_c3) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34381,c_133]) ).
tff(c_34514,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34508,c_34399]) ).
tff(c_34568,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34567,c_34514]) ).
tff(c_34330,plain,
multiply(inverse(sk_c8),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_174,c_34261]) ).
tff(c_34369,plain,
multiply(sk_c7,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28816,c_34330]) ).
tff(c_34622,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34361,c_34369]) ).
tff(c_34625,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_34622,c_170]) ).
tff(c_34627,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34568,c_34625]) ).
tff(c_34629,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34515,c_34627]) ).
tff(c_34630,plain,
inverse(sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_34635,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34630,c_4]) ).
tff(c_34631,plain,
inverse(sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_76,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_34690,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_34631,c_76]) ).
tff(c_78,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_34656,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_34631,c_78]) ).
tff(c_34660,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34656,c_4]) ).
tff(c_34726,plain,
! [X_415,Y_416,Z_417] : ( multiply(multiply(X_415,Y_416),Z_417) = multiply(X_415,multiply(Y_416,Z_417)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_34750,plain,
! [Z_417] : ( multiply(sk_c9,multiply(sk_c6,Z_417)) = multiply(identity,Z_417) ),
inference(superposition,[status(thm),theory(equality)],[c_34660,c_34726]) ).
tff(c_35283,plain,
! [Z_427] : ( multiply(sk_c9,multiply(sk_c6,Z_427)) = Z_427 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34750]) ).
tff(c_35295,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_34690,c_35283]) ).
tff(c_34768,plain,
! [X_2,Z_417] : ( multiply(inverse(X_2),multiply(X_2,Z_417)) = multiply(identity,Z_417) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34726]) ).
tff(c_35430,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_34768]) ).
tff(c_35460,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_35295,c_35430]) ).
tff(c_35516,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_35460]) ).
tff(c_34765,plain,
! [Z_417] : ( multiply(sk_c9,multiply(sk_c3,Z_417)) = multiply(identity,Z_417) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_34726]) ).
tff(c_34810,plain,
! [Z_420] : ( multiply(sk_c9,multiply(sk_c3,Z_420)) = Z_420 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34765]) ).
tff(c_34825,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_34810]) ).
tff(c_34840,plain,
! [Z_421] : ( multiply(sk_c9,multiply(sk_c6,Z_421)) = Z_421 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34750]) ).
tff(c_34852,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_34690,c_34840]) ).
tff(c_34879,plain,
! [X_423,Z_424] : ( multiply(inverse(X_423),multiply(X_423,Z_424)) = Z_424 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34768]) ).
tff(c_34900,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34852,c_34879]) ).
tff(c_34974,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_34900]) ).
tff(c_34986,plain,
multiply(sk_c9,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_34974,c_34852]) ).
tff(c_34992,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34825,c_34986]) ).
tff(c_68,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_34706,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_34631,c_68]) ).
tff(c_34921,plain,
multiply(inverse(sk_c8),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34706,c_34879]) ).
tff(c_34976,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34630,c_34921]) ).
tff(c_35140,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34992,c_34974,c_2,c_34974,c_34976]) ).
tff(c_35146,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35140,c_34992]) ).
tff(c_34991,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34974,c_34630]) ).
tff(c_35018,plain,
multiply(identity,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34991,c_4]) ).
tff(c_34782,plain,
! [X_2,Z_417] : ( multiply(inverse(X_2),multiply(X_2,Z_417)) = Z_417 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34768]) ).
tff(c_35025,plain,
multiply(inverse(identity),identity) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_35018,c_34782]) ).
tff(c_35037,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_35025]) ).
tff(c_34830,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34706,c_34630,c_116]) ).
tff(c_34831,plain,
multiply(sk_c8,sk_c9) != sk_c7,
inference(splitLeft,[status(thm)],[c_34830]) ).
tff(c_34987,plain,
multiply(sk_c8,sk_c9) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_34974,c_34831]) ).
tff(c_35265,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_35146,c_2,c_35037,c_34987]) ).
tff(c_35267,plain,
multiply(sk_c8,sk_c9) = sk_c7,
inference(splitRight,[status(thm)],[c_34830]) ).
tff(c_72,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_34682,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_34631,c_72]) ).
tff(c_35337,plain,
! [Z_429] : ( multiply(sk_c5,multiply(sk_c8,Z_429)) = multiply(sk_c9,Z_429) ),
inference(superposition,[status(thm),theory(equality)],[c_34682,c_34726]) ).
tff(c_35352,plain,
multiply(sk_c9,sk_c7) = multiply(sk_c5,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_34706,c_35337]) ).
tff(c_35359,plain,
multiply(sk_c5,sk_c9) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_35295,c_35352]) ).
tff(c_74,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_34643,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_34631,c_74]) ).
tff(c_34647,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34643,c_4]) ).
tff(c_34753,plain,
! [Z_417] : ( multiply(sk_c8,multiply(sk_c5,Z_417)) = multiply(identity,Z_417) ),
inference(superposition,[status(thm),theory(equality)],[c_34647,c_34726]) ).
tff(c_35382,plain,
! [Z_430] : ( multiply(sk_c8,multiply(sk_c5,Z_430)) = Z_430 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34753]) ).
tff(c_35400,plain,
multiply(sk_c8,sk_c9) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_35359,c_35382]) ).
tff(c_35410,plain,
sk_c9 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35267,c_35400]) ).
tff(c_35538,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35516,c_35410]) ).
tff(c_35406,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_34682,c_35382]) ).
tff(c_35411,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35267,c_35406]) ).
tff(c_35266,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_34830]) ).
tff(c_35306,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( sk_c9 != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35295,c_35266]) ).
tff(c_35307,plain,
sk_c9 != sk_c8,
inference(splitLeft,[status(thm)],[c_35306]) ).
tff(c_35415,plain,
sk_c9 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35411,c_35307]) ).
tff(c_35524,plain,
sk_c9 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_35516,c_35415]) ).
tff(c_35612,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_35538,c_35524]) ).
tff(c_35614,plain,
sk_c9 = sk_c8,
inference(splitRight,[status(thm)],[c_35306]) ).
tff(c_35615,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_35614,c_35614,c_35295]) ).
tff(c_35800,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_35615,c_34782]) ).
tff(c_35809,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34635,c_34630,c_35800]) ).
tff(c_35697,plain,
! [X_435,Z_436] : ( multiply(inverse(X_435),multiply(X_435,Z_436)) = Z_436 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34768]) ).
tff(c_35739,plain,
multiply(inverse(sk_c8),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_34647,c_35697]) ).
tff(c_35768,plain,
multiply(sk_c7,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_34630,c_35739]) ).
tff(c_35830,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_35809,c_35768]) ).
tff(c_35834,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35830]) ).
tff(c_35625,plain,
inverse(sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_35614,c_34656]) ).
tff(c_35655,plain,
multiply(sk_c8,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_35625,c_4]) ).
tff(c_35815,plain,
multiply(inverse(sk_c8),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_35655,c_34782]) ).
tff(c_35824,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_35768,c_34630,c_35815]) ).
tff(c_35862,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35834,c_35824]) ).
tff(c_35617,plain,
multiply(sk_c8,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_35614,c_34825]) ).
tff(c_35828,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_35809,c_35615]) ).
tff(c_35833,plain,
sk_c8 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_35617,c_35828]) ).
tff(c_35846,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_35833,c_35614]) ).
tff(c_34744,plain,
! [Z_417] : ( multiply(sk_c6,multiply(sk_c9,Z_417)) = multiply(sk_c7,Z_417) ),
inference(superposition,[status(thm),theory(equality)],[c_34690,c_34726]) ).
tff(c_35867,plain,
! [Z_417] : ( multiply(sk_c4,Z_417) = Z_417 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35862,c_35846,c_2,c_35809,c_34744]) ).
tff(c_35621,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_35614,c_34706]) ).
tff(c_35939,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35867,c_35833,c_35833,c_35809,c_35621]) ).
tff(c_35832,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35809,c_34630]) ).
tff(c_35916,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_146,c_35833,c_35832]) ).
tff(c_35918,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35916,c_146]) ).
tff(c_35940,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35939,c_35918]) ).
tff(c_36046,plain,
! [X_439,Z_440] : ( multiply(inverse(inverse(X_439)),Z_440) = multiply(X_439,Z_440) ),
inference(superposition,[status(thm),theory(equality)],[c_35697,c_34782]) ).
tff(c_35757,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_35697]) ).
tff(c_36053,plain,
! [X_439] : ( multiply(X_439,identity) = X_439 ),
inference(superposition,[status(thm),theory(equality)],[c_36046,c_35757]) ).
tff(c_35945,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35939,c_35833]) ).
tff(c_35944,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35939,c_35846]) ).
tff(c_35613,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_35306]) ).
tff(c_43030,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != identity )
| ( identity != X2_10 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X3_8) != identity )
| ( identity != X3_8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_36053,c_35945,c_35944,c_35944,c_36053,c_35945,c_35944,c_35945,c_36053,c_35944,c_36053,c_35944,c_35944,c_36053,c_35945,c_35944,c_35945,c_36053,c_35944,c_35809,c_35944,c_35613]) ).
tff(c_43032,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_43030]) ).
tff(c_43034,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43032,c_35940]) ).
tff(c_43035,plain,
! [X4_11,X5_6,X1_9,X2_10] :
( ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(splitRight,[status(thm)],[c_43030]) ).
tff(c_202231,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_43035]) ).
tff(c_202233,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_202231,c_35940]) ).
tff(c_202234,plain,
! [X1_9,X5_6,X4_11] :
( ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(splitRight,[status(thm)],[c_43035]) ).
tff(c_202236,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_202234]) ).
tff(c_202238,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_202236,c_35940]) ).
tff(c_202239,plain,
! [X5_6,X1_9] :
( ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 ) ),
inference(splitRight,[status(thm)],[c_202234]) ).
tff(c_202242,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_202239]) ).
tff(c_202244,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_202242,c_35940]) ).
tff(c_202246,plain,
! [X5_952] :
( ( inverse(X5_952) != identity )
| ( inverse(X5_952) != X5_952 ) ),
inference(splitRight,[status(thm)],[c_202239]) ).
tff(c_202264,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_35940,c_202246]) ).
tff(c_202276,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_35940,c_202264]) ).
tff(c_202278,plain,
inverse(sk_c1) != sk_c9,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_34,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_360660,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_202278,c_34]) ).
tff(c_360664,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_360660,c_4]) ).
tff(c_202302,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_202278,c_34]) ).
tff(c_202306,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_202302,c_4]) ).
tff(c_202277,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_202282,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_202277,c_4]) ).
tff(c_202385,plain,
! [X_953,Y_954,Z_955] : ( multiply(multiply(X_953,Y_954),Z_955) = multiply(X_953,multiply(Y_954,Z_955)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_202424,plain,
! [Z_955] : ( multiply(sk_c9,multiply(sk_c3,Z_955)) = multiply(identity,Z_955) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_202385]) ).
tff(c_202469,plain,
! [Z_958] : ( multiply(sk_c9,multiply(sk_c3,Z_958)) = Z_958 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202424]) ).
tff(c_202484,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_202469]) ).
tff(c_202412,plain,
! [Z_955] : ( multiply(sk_c7,multiply(sk_c8,Z_955)) = multiply(identity,Z_955) ),
inference(superposition,[status(thm),theory(equality)],[c_202306,c_202385]) ).
tff(c_203027,plain,
! [Z_968] : ( multiply(sk_c7,multiply(sk_c8,Z_968)) = Z_968 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202412]) ).
tff(c_203048,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_202282,c_203027]) ).
tff(c_32,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_202342,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_202278,c_32]) ).
tff(c_202406,plain,
! [Z_955] : ( multiply(sk_c8,multiply(sk_c7,Z_955)) = multiply(sk_c9,Z_955) ),
inference(superposition,[status(thm),theory(equality)],[c_202342,c_202385]) ).
tff(c_203091,plain,
multiply(sk_c9,identity) = multiply(sk_c8,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_203048,c_202406]) ).
tff(c_203097,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_202282,c_202484,c_203091]) ).
tff(c_203103,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_203097,c_146]) ).
tff(c_40,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_202353,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_202278,c_40]) ).
tff(c_42,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_202317,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_202278,c_42]) ).
tff(c_202321,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_202317,c_4]) ).
tff(c_202409,plain,
! [Z_955] : ( multiply(sk_c9,multiply(sk_c6,Z_955)) = multiply(identity,Z_955) ),
inference(superposition,[status(thm),theory(equality)],[c_202321,c_202385]) ).
tff(c_203002,plain,
! [Z_967] : ( multiply(sk_c9,multiply(sk_c6,Z_967)) = Z_967 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202409]) ).
tff(c_203014,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_202353,c_203002]) ).
tff(c_202427,plain,
! [X_2,Z_955] : ( multiply(inverse(X_2),multiply(X_2,Z_955)) = multiply(identity,Z_955) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_202385]) ).
tff(c_203138,plain,
! [X_970,Z_971] : ( multiply(inverse(X_970),multiply(X_970,Z_971)) = Z_971 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202427]) ).
tff(c_203171,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_203014,c_203138]) ).
tff(c_203229,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_203171]) ).
tff(c_202286,plain,
inverse(sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_78]) ).
tff(c_202290,plain,
multiply(sk_c8,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_202286,c_4]) ).
tff(c_203051,plain,
multiply(sk_c7,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_202290,c_203027]) ).
tff(c_203045,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_202342,c_203027]) ).
tff(c_203165,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_203045,c_203138]) ).
tff(c_203228,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_203165]) ).
tff(c_203241,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_203228,c_203045]) ).
tff(c_203255,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_203051,c_203241]) ).
tff(c_203269,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203229,c_203255]) ).
tff(c_203273,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_203269,c_202286]) ).
tff(c_203275,plain,
sk_c8 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_203103,c_203273]) ).
tff(c_202620,plain,
! [X_963,Z_964] : ( multiply(inverse(X_963),multiply(X_963,Z_964)) = Z_964 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202427]) ).
tff(c_202662,plain,
multiply(inverse(sk_c8),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_202290,c_202620]) ).
tff(c_202688,plain,
multiply(sk_c7,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_202302,c_202662]) ).
tff(c_36,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_202364,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_202278,c_36]) ).
tff(c_202415,plain,
! [Z_955] : ( multiply(sk_c8,multiply(sk_c5,Z_955)) = multiply(identity,Z_955) ),
inference(superposition,[status(thm),theory(equality)],[c_202282,c_202385]) ).
tff(c_202538,plain,
! [Z_961] : ( multiply(sk_c8,multiply(sk_c5,Z_961)) = Z_961 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202415]) ).
tff(c_202550,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_202364,c_202538]) ).
tff(c_202562,plain,
! [Z_962] : ( multiply(sk_c7,multiply(sk_c8,Z_962)) = Z_962 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202412]) ).
tff(c_202577,plain,
multiply(sk_c7,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_202550,c_202562]) ).
tff(c_202599,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_202306,c_202577]) ).
tff(c_202589,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_202342,c_202562]) ).
tff(c_202900,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_202688,c_202599,c_202589]) ).
tff(c_202610,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_202599,c_202317]) ).
tff(c_202755,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_202610,c_4]) ).
tff(c_202441,plain,
! [X_2,Z_955] : ( multiply(inverse(X_2),multiply(X_2,Z_955)) = Z_955 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202427]) ).
tff(c_202821,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_202755,c_202441]) ).
tff(c_202833,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_202821]) ).
tff(c_202607,plain,
multiply(sk_c6,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_202599,c_202353]) ).
tff(c_202959,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_202900,c_2,c_202833,c_202607]) ).
tff(c_202905,plain,
inverse(sk_c8) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_202900,c_202302]) ).
tff(c_202918,plain,
multiply(sk_c2,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_202905,c_4]) ).
tff(c_202985,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202959,c_202918]) ).
tff(c_202497,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_202342,c_202302,c_116]) ).
tff(c_202498,plain,
multiply(sk_c8,sk_c9) != sk_c7,
inference(splitLeft,[status(thm)],[c_202497]) ).
tff(c_202554,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_202550,c_202498]) ).
tff(c_202903,plain,
sk_c8 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_202900,c_202554]) ).
tff(c_202963,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_202959,c_202903]) ).
tff(c_202992,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_202985,c_202963]) ).
tff(c_202993,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_202497]) ).
tff(c_203025,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( sk_c9 != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_203014,c_202993]) ).
tff(c_203026,plain,
sk_c9 != sk_c8,
inference(splitLeft,[status(thm)],[c_203025]) ).
tff(c_203242,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_203228,c_203026]) ).
tff(c_203300,plain,
sk_c3 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_203275,c_203242]) ).
tff(c_203250,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203228,c_202317]) ).
tff(c_203307,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_203250,c_4]) ).
tff(c_203345,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_203307,c_202441]) ).
tff(c_203357,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_203345]) ).
tff(c_203361,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203357,c_203250]) ).
tff(c_203369,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203361,c_203103]) ).
tff(c_203371,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_203300,c_203369]) ).
tff(c_203373,plain,
sk_c9 = sk_c8,
inference(splitRight,[status(thm)],[c_203025]) ).
tff(c_203374,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_203373,c_203373,c_203014]) ).
tff(c_203520,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_203374,c_202441]) ).
tff(c_203526,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_202306,c_202302,c_203520]) ).
tff(c_203531,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203526,c_202302]) ).
tff(c_203377,plain,
multiply(sk_c8,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_203373,c_202484]) ).
tff(c_203633,plain,
multiply(inverse(sk_c8),sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_203377,c_202441]) ).
tff(c_203639,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_203531,c_203633]) ).
tff(c_203386,plain,
inverse(sk_c3) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_203373,c_133]) ).
tff(c_203460,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_203386,c_4]) ).
tff(c_203564,plain,
multiply(inverse(sk_c8),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_203460,c_202441]) ).
tff(c_203570,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_203531,c_203564]) ).
tff(c_203577,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203570,c_146]) ).
tff(c_203643,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203639,c_203577]) ).
tff(c_203391,plain,
! [X_973,Z_974] : ( multiply(inverse(X_973),multiply(X_973,Z_974)) = Z_974 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_202427]) ).
tff(c_203783,plain,
! [X_977,Z_978] : ( multiply(inverse(inverse(X_977)),Z_978) = multiply(X_977,Z_978) ),
inference(superposition,[status(thm),theory(equality)],[c_202441,c_203391]) ).
tff(c_203442,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_203391]) ).
tff(c_203790,plain,
! [X_977] : ( multiply(X_977,identity) = X_977 ),
inference(superposition,[status(thm),theory(equality)],[c_203783,c_203442]) ).
tff(c_203427,plain,
multiply(inverse(sk_c8),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_202290,c_203391]) ).
tff(c_203451,plain,
multiply(sk_c7,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_202302,c_203427]) ).
tff(c_203529,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_203526,c_203451]) ).
tff(c_203532,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_203529]) ).
tff(c_203541,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_203532,c_202286]) ).
tff(c_203663,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203643,c_203541]) ).
tff(c_203682,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_203663,c_203373]) ).
tff(c_203372,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_203025]) ).
tff(c_210461,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != identity )
| ( identity != X2_10 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X3_8) != identity )
| ( identity != X3_8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_203790,c_203682,c_203663,c_203682,c_203790,c_203682,c_203663,c_203663,c_203790,c_203682,c_203790,c_203682,c_203682,c_203790,c_203682,c_203663,c_203663,c_203790,c_203682,c_203526,c_203682,c_203372]) ).
tff(c_210463,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_210461]) ).
tff(c_210465,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_210463,c_203643]) ).
tff(c_210466,plain,
! [X4_11,X5_6,X1_9,X2_10] :
( ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(splitRight,[status(thm)],[c_210461]) ).
tff(c_357669,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_210466]) ).
tff(c_357671,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_357669,c_203643]) ).
tff(c_357672,plain,
! [X1_9,X5_6,X4_11] :
( ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(splitRight,[status(thm)],[c_210466]) ).
tff(c_357674,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_357672]) ).
tff(c_357676,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_357674,c_203643]) ).
tff(c_357677,plain,
! [X5_6,X1_9] :
( ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 ) ),
inference(splitRight,[status(thm)],[c_357672]) ).
tff(c_360616,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_357677]) ).
tff(c_360618,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360616,c_203643]) ).
tff(c_360620,plain,
! [X5_1473] :
( ( inverse(X5_1473) != identity )
| ( inverse(X5_1473) != X5_1473 ) ),
inference(splitRight,[status(thm)],[c_357677]) ).
tff(c_360638,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_203643,c_360620]) ).
tff(c_360650,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_203643,c_360638]) ).
tff(c_360651,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_78]) ).
tff(c_360652,plain,
inverse(sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_78]) ).
tff(c_360701,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_360652,c_76]) ).
tff(c_360746,plain,
! [X_1474,Y_1475,Z_1476] : ( multiply(multiply(X_1474,Y_1475),Z_1476) = multiply(X_1474,multiply(Y_1475,Z_1476)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_360785,plain,
! [X_2,Z_1476] : ( multiply(inverse(X_2),multiply(X_2,Z_1476)) = multiply(identity,Z_1476) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_360746]) ).
tff(c_361276,plain,
! [X_1486,Z_1487] : ( multiply(inverse(X_1486),multiply(X_1486,Z_1487)) = Z_1487 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360785]) ).
tff(c_361315,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_360701,c_361276]) ).
tff(c_361345,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_360651,c_361315]) ).
tff(c_360798,plain,
! [X_2,Z_1476] : ( multiply(inverse(X_2),multiply(X_2,Z_1476)) = Z_1476 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360785]) ).
tff(c_361352,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_361345,c_360798]) ).
tff(c_361358,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_361352]) ).
tff(c_360693,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_202278,c_32]) ).
tff(c_360770,plain,
! [Z_1476] : ( multiply(sk_c7,multiply(sk_c8,Z_1476)) = multiply(identity,Z_1476) ),
inference(superposition,[status(thm),theory(equality)],[c_360664,c_360746]) ).
tff(c_360843,plain,
! [Z_1479] : ( multiply(sk_c7,multiply(sk_c8,Z_1479)) = Z_1479 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360770]) ).
tff(c_360855,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_360693,c_360843]) ).
tff(c_360869,plain,
! [X_1480,Z_1481] : ( multiply(inverse(X_1480),multiply(X_1480,Z_1481)) = Z_1481 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360785]) ).
tff(c_360887,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_360855,c_360869]) ).
tff(c_360951,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_360887]) ).
tff(c_360969,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_360951,c_360651]) ).
tff(c_360992,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_360969,c_4]) ).
tff(c_360999,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_360992,c_360798]) ).
tff(c_361011,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_360999]) ).
tff(c_361015,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_361011,c_360969]) ).
tff(c_360908,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_360701,c_360869]) ).
tff(c_360954,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_360651,c_360908]) ).
tff(c_361093,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_360951,c_2,c_360951,c_360954]) ).
tff(c_360920,plain,
multiply(inverse(sk_c8),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_202282,c_360869]) ).
tff(c_360956,plain,
multiply(sk_c7,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_360660,c_360920]) ).
tff(c_361126,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_361093,c_360956]) ).
tff(c_361128,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_361126,c_202277]) ).
tff(c_361129,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_361015,c_361128]) ).
tff(c_360814,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_360693,c_360660,c_116]) ).
tff(c_360815,plain,
multiply(sk_c8,sk_c9) != sk_c7,
inference(splitLeft,[status(thm)],[c_360814]) ).
tff(c_360964,plain,
multiply(sk_c8,identity) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_360951,c_360815]) ).
tff(c_361160,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_361129,c_361093,c_360964]) ).
tff(c_361162,plain,
multiply(sk_c8,sk_c9) = sk_c7,
inference(splitRight,[status(thm)],[c_360814]) ).
tff(c_360712,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_360652,c_72]) ).
tff(c_360776,plain,
! [Z_1476] : ( multiply(sk_c8,multiply(sk_c5,Z_1476)) = multiply(identity,Z_1476) ),
inference(superposition,[status(thm),theory(equality)],[c_202282,c_360746]) ).
tff(c_361198,plain,
! [Z_1484] : ( multiply(sk_c8,multiply(sk_c5,Z_1484)) = Z_1484 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360776]) ).
tff(c_361210,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_360712,c_361198]) ).
tff(c_361214,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_361162,c_361210]) ).
tff(c_361245,plain,
multiply(sk_c7,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_361214,c_360693]) ).
tff(c_361361,plain,
multiply(identity,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_361358,c_361358,c_361245]) ).
tff(c_361368,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_361361]) ).
tff(c_361161,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_360814]) ).
tff(c_361189,plain,
multiply(sk_c9,sk_c7) != sk_c8,
inference(splitLeft,[status(thm)],[c_361161]) ).
tff(c_361242,plain,
multiply(sk_c9,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_361214,c_361189]) ).
tff(c_361504,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_361368,c_361358,c_361358,c_361242]) ).
tff(c_361506,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(splitRight,[status(thm)],[c_361161]) ).
tff(c_360656,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_360651,c_4]) ).
tff(c_360773,plain,
! [Z_1476] : ( multiply(sk_c9,multiply(sk_c6,Z_1476)) = multiply(identity,Z_1476) ),
inference(superposition,[status(thm),theory(equality)],[c_360656,c_360746]) ).
tff(c_361522,plain,
! [Z_1488] : ( multiply(sk_c9,multiply(sk_c6,Z_1488)) = Z_1488 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360773]) ).
tff(c_361534,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_360701,c_361522]) ).
tff(c_361538,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_361506,c_361534]) ).
tff(c_361541,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_361538,c_361506]) ).
tff(c_362396,plain,
! [X_1504,Z_1505] : ( multiply(inverse(X_1504),multiply(X_1504,Z_1505)) = Z_1505 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360785]) ).
tff(c_362420,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_361541,c_362396]) ).
tff(c_362468,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_360664,c_360660,c_362420]) ).
tff(c_362478,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_362468,c_360660]) ).
tff(c_360782,plain,
! [Z_1476] : ( multiply(sk_c9,multiply(sk_c3,Z_1476)) = multiply(identity,Z_1476) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_360746]) ).
tff(c_361170,plain,
! [Z_1483] : ( multiply(sk_c9,multiply(sk_c3,Z_1483)) = Z_1483 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360782]) ).
tff(c_361185,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_150,c_361170]) ).
tff(c_361540,plain,
multiply(sk_c8,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_361538,c_361185]) ).
tff(c_362517,plain,
multiply(inverse(sk_c8),sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_361540,c_360798]) ).
tff(c_362523,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_362478,c_362517]) ).
tff(c_362529,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_362523,c_146]) ).
tff(c_362444,plain,
multiply(inverse(sk_c8),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_202282,c_362396]) ).
tff(c_362472,plain,
multiply(sk_c7,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_360660,c_362444]) ).
tff(c_362493,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_362468,c_362472]) ).
tff(c_362496,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_362493,c_202277]) ).
tff(c_362535,plain,
sk_c8 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_362529,c_362496]) ).
tff(c_362547,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_362535,c_362478]) ).
tff(c_361551,plain,
inverse(sk_c3) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_361538,c_133]) ).
tff(c_362552,plain,
inverse(sk_c3) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_362535,c_361551]) ).
tff(c_362603,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_362547,c_362552]) ).
tff(c_362620,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_362603,c_362529]) ).
tff(c_362718,plain,
! [X_1508,Z_1509] : ( multiply(inverse(inverse(X_1508)),Z_1509) = multiply(X_1508,Z_1509) ),
inference(superposition,[status(thm),theory(equality)],[c_362396,c_360798]) ).
tff(c_362459,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_362396]) ).
tff(c_362725,plain,
! [X_1508] : ( multiply(X_1508,identity) = X_1508 ),
inference(superposition,[status(thm),theory(equality)],[c_362718,c_362459]) ).
tff(c_362619,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_362603,c_362535]) ).
tff(c_361610,plain,
! [X_1489,Z_1490] : ( multiply(inverse(X_1489),multiply(X_1489,Z_1490)) = Z_1490 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_360785]) ).
tff(c_361951,plain,
! [X_1494,Z_1495] : ( multiply(inverse(inverse(X_1494)),Z_1495) = multiply(X_1494,Z_1495) ),
inference(superposition,[status(thm),theory(equality)],[c_360798,c_361610]) ).
tff(c_361673,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_361610]) ).
tff(c_361958,plain,
! [X_1494] : ( multiply(X_1494,identity) = X_1494 ),
inference(superposition,[status(thm),theory(equality)],[c_361951,c_361673]) ).
tff(c_361634,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_361541,c_361610]) ).
tff(c_361682,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_360664,c_360660,c_361634]) ).
tff(c_361692,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_361682,c_360660]) ).
tff(c_361731,plain,
multiply(inverse(sk_c8),sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_361540,c_360798]) ).
tff(c_361737,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_361692,c_361731]) ).
tff(c_361743,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_361737,c_146]) ).
tff(c_361658,plain,
multiply(inverse(sk_c8),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_202282,c_361610]) ).
tff(c_361686,plain,
multiply(sk_c7,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_360660,c_361658]) ).
tff(c_361707,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_361682,c_361686]) ).
tff(c_361710,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_361707,c_202277]) ).
tff(c_361749,plain,
sk_c8 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_361743,c_361710]) ).
tff(c_361761,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_361749,c_361692]) ).
tff(c_361766,plain,
inverse(sk_c3) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_361749,c_361551]) ).
tff(c_361817,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_361761,c_361766]) ).
tff(c_361833,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_361817,c_361749]) ).
tff(c_361505,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_361161]) ).
tff(c_361556,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c8 )
| ( multiply(X2_10,sk_c8) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c8 )
| ( inverse(multiply(X5_6,sk_c8)) != sk_c8 )
| ( multiply(X5_6,sk_c8) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(X3_8,sk_c8) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_361538,c_361538,c_361538,c_361538,c_361538,c_361538,c_361538,c_361538,c_361538,c_361505]) ).
tff(c_361557,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(X3_8,sk_c8) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_361556]) ).
tff(c_362340,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_361958,c_361833,c_361833,c_361833,c_361557]) ).
tff(c_361834,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_361817,c_361743]) ).
tff(c_362342,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362340,c_361834]) ).
tff(c_362343,plain,
! [X4_11,X5_6,X1_9,X2_10] :
( ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c8 )
| ( inverse(multiply(X5_6,sk_c8)) != sk_c8 )
| ( multiply(X5_6,sk_c8) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c8 )
| ( inverse(X2_10) != sk_c8 )
| ( multiply(X2_10,sk_c8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_361556]) ).
tff(c_371169,plain,
! [X4_11,X5_6,X1_9,X2_10] :
( ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_362725,c_362619,c_362468,c_362619,c_362725,c_362619,c_362619,c_362619,c_362725,c_362619,c_362725,c_362619,c_362619,c_362725,c_362619,c_362619,c_362619,c_362343]) ).
tff(c_371171,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_371169]) ).
tff(c_371173,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_371171,c_362620]) ).
tff(c_371174,plain,
! [X1_9,X5_6,X4_11] :
( ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(splitRight,[status(thm)],[c_371169]) ).
tff(c_381086,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_371174]) ).
tff(c_381088,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_381086,c_362620]) ).
tff(c_381089,plain,
! [X5_6,X1_9] :
( ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 ) ),
inference(splitRight,[status(thm)],[c_371174]) ).
tff(c_381091,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_381089]) ).
tff(c_381093,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_381091,c_362620]) ).
tff(c_381096,plain,
! [X5_1656] :
( ( inverse(X5_1656) != identity )
| ( inverse(X5_1656) != X5_1656 ) ),
inference(splitRight,[status(thm)],[c_381089]) ).
tff(c_381108,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_362620,c_381096]) ).
tff(c_381117,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_362620,c_381108]) ).
tff(c_381118,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_381119,plain,
inverse(sk_c4) != sk_c3,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_88,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( inverse(sk_c4) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_410489,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_381119,c_88]) ).
tff(c_410533,plain,
! [X_1862,Y_1863,Z_1864] : ( multiply(multiply(X_1862,Y_1863),Z_1864) = multiply(X_1862,multiply(Y_1863,Z_1864)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_410572,plain,
! [X_2,Z_1864] : ( multiply(inverse(X_2),multiply(X_2,Z_1864)) = multiply(identity,Z_1864) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_410533]) ).
tff(c_410951,plain,
! [X_1873,Z_1874] : ( multiply(inverse(X_1873),multiply(X_1873,Z_1874)) = Z_1874 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_410572]) ).
tff(c_410981,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_410489,c_410951]) ).
tff(c_411010,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_381118,c_410981]) ).
tff(c_410585,plain,
! [X_2,Z_1864] : ( multiply(inverse(X_2),multiply(X_2,Z_1864)) = Z_1864 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_410572]) ).
tff(c_411014,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_411010,c_410585]) ).
tff(c_411020,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_411014]) ).
tff(c_381123,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_381118,c_4]) ).
tff(c_410566,plain,
! [Z_1864] : ( multiply(sk_c9,multiply(sk_c6,Z_1864)) = multiply(identity,Z_1864) ),
inference(superposition,[status(thm),theory(equality)],[c_381123,c_410533]) ).
tff(c_410613,plain,
! [Z_1866] : ( multiply(sk_c9,multiply(sk_c6,Z_1866)) = Z_1866 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_410566]) ).
tff(c_410625,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_410489,c_410613]) ).
tff(c_410662,plain,
! [X_1869,Z_1870] : ( multiply(inverse(X_1869),multiply(X_1869,Z_1870)) = Z_1870 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_410572]) ).
tff(c_410686,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_410625,c_410662]) ).
tff(c_410747,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_410686]) ).
tff(c_84,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( inverse(sk_c4) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_410478,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_381119,c_84]) ).
tff(c_82,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c4) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_381159,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_381119,c_82]) ).
tff(c_381163,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_381159,c_4]) ).
tff(c_381213,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_381119,c_84]) ).
tff(c_86,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c4) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_381172,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_381119,c_86]) ).
tff(c_381176,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_381172,c_4]) ).
tff(c_381238,plain,
! [X_1657,Y_1658,Z_1659] : ( multiply(multiply(X_1657,Y_1658),Z_1659) = multiply(X_1657,multiply(Y_1658,Z_1659)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_381262,plain,
! [Z_1659] : ( multiply(sk_c8,multiply(sk_c5,Z_1659)) = multiply(identity,Z_1659) ),
inference(superposition,[status(thm),theory(equality)],[c_381176,c_381238]) ).
tff(c_381296,plain,
! [Z_1660] : ( multiply(sk_c8,multiply(sk_c5,Z_1660)) = Z_1660 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_381262]) ).
tff(c_381308,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_381213,c_381296]) ).
tff(c_381265,plain,
! [Z_1659] : ( multiply(sk_c7,multiply(sk_c8,Z_1659)) = multiply(identity,Z_1659) ),
inference(superposition,[status(thm),theory(equality)],[c_381163,c_381238]) ).
tff(c_381335,plain,
! [Z_1662] : ( multiply(sk_c7,multiply(sk_c8,Z_1662)) = Z_1662 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_381265]) ).
tff(c_381347,plain,
multiply(sk_c7,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_381308,c_381335]) ).
tff(c_381363,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381163,c_381347]) ).
tff(c_381372,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381363,c_381118]) ).
tff(c_381190,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_381119,c_88]) ).
tff(c_381259,plain,
! [Z_1659] : ( multiply(sk_c6,multiply(sk_c9,Z_1659)) = multiply(sk_c7,Z_1659) ),
inference(superposition,[status(thm),theory(equality)],[c_381190,c_381238]) ).
tff(c_381379,plain,
! [Z_1659] : ( multiply(sk_c7,Z_1659) = multiply(sk_c6,Z_1659) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_381363,c_381259]) ).
tff(c_80,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( inverse(sk_c4) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_381197,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_381119,c_80]) ).
tff(c_381353,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_381197,c_381335]) ).
tff(c_381440,plain,
multiply(sk_c6,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_381379,c_381363,c_381353]) ).
tff(c_381280,plain,
! [X_2,Z_1659] : ( multiply(inverse(X_2),multiply(X_2,Z_1659)) = multiply(identity,Z_1659) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_381238]) ).
tff(c_381449,plain,
! [X_1664,Z_1665] : ( multiply(inverse(X_1664),multiply(X_1664,Z_1665)) = Z_1665 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_381280]) ).
tff(c_381467,plain,
multiply(inverse(sk_c6),sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_381440,c_381449]) ).
tff(c_381519,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_381372,c_381467]) ).
tff(c_381132,plain,
inverse(sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_70]) ).
tff(c_381136,plain,
multiply(sk_c8,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_381132,c_4]) ).
tff(c_381506,plain,
multiply(inverse(sk_c8),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_381136,c_381449]) ).
tff(c_381524,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_381440,c_381379,c_381159,c_381506]) ).
tff(c_381569,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381519,c_381524]) ).
tff(c_381494,plain,
multiply(inverse(sk_c8),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_381176,c_381449]) ).
tff(c_381521,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_381440,c_381379,c_381159,c_381494]) ).
tff(c_381536,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_381524,c_381521]) ).
tff(c_381333,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_381308,c_381197,c_381159,c_116]) ).
tff(c_381334,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_381333]) ).
tff(c_381529,plain,
sk_c8 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_381521,c_381334]) ).
tff(c_381559,plain,
sk_c8 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_381536,c_381529]) ).
tff(c_381574,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_381569,c_381559]) ).
tff(c_381408,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_381372,c_4]) ).
tff(c_381294,plain,
! [X_2,Z_1659] : ( multiply(inverse(X_2),multiply(X_2,Z_1659)) = Z_1659 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_381280]) ).
tff(c_381615,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_381408,c_381294]) ).
tff(c_381627,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_381615]) ).
tff(c_381632,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381627,c_381372]) ).
tff(c_381577,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_381569,c_381132]) ).
tff(c_381665,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381632,c_381577]) ).
tff(c_381667,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_381574,c_381665]) ).
tff(c_381669,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_381333]) ).
tff(c_381670,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_381669,c_381669,c_381308]) ).
tff(c_381740,plain,
! [X_1668,Z_1669] : ( multiply(inverse(X_1668),multiply(X_1668,Z_1669)) = Z_1669 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_381280]) ).
tff(c_381761,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_381670,c_381740]) ).
tff(c_381811,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_381761]) ).
tff(c_381782,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_381190,c_381740]) ).
tff(c_381813,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_381118,c_381782]) ).
tff(c_381872,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381811,c_2,c_381811,c_381813]) ).
tff(c_381677,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_381669,c_381159]) ).
tff(c_381876,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381872,c_381872,c_381677]) ).
tff(c_382091,plain,
! [X_1672,Z_1673] : ( multiply(inverse(inverse(X_1672)),Z_1673) = multiply(X_1672,Z_1673) ),
inference(superposition,[status(thm),theory(equality)],[c_381294,c_381740]) ).
tff(c_381803,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_381740]) ).
tff(c_382098,plain,
! [X_1672] : ( multiply(X_1672,identity) = X_1672 ),
inference(superposition,[status(thm),theory(equality)],[c_382091,c_381803]) ).
tff(c_381878,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381872,c_381669]) ).
tff(c_381668,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_381333]) ).
tff(c_388989,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X3_8) != identity )
| ( identity != X3_8 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_382098,c_381872,c_381811,c_381811,c_382098,c_381878,c_381811,c_381878,c_382098,c_381811,c_382098,c_381811,c_381811,c_382098,c_381878,c_381811,c_381878,c_382098,c_381878,c_381811,c_381811,c_381878,c_381872,c_2,c_381811,c_381668]) ).
tff(c_388991,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_388989]) ).
tff(c_388993,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_388991,c_381876]) ).
tff(c_388994,plain,
! [X1_9,X5_6,X4_11,X3_8] :
( ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X3_8) != identity )
| ( identity != X3_8 ) ),
inference(splitRight,[status(thm)],[c_388989]) ).
tff(c_408217,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_388994]) ).
tff(c_408219,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_408217,c_381876]) ).
tff(c_408220,plain,
! [X4_11,X5_6,X1_9] :
( ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 ) ),
inference(splitRight,[status(thm)],[c_388994]) ).
tff(c_409350,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_408220]) ).
tff(c_409352,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_409350,c_381876]) ).
tff(c_409353,plain,
! [X5_6,X4_11] :
( ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(splitRight,[status(thm)],[c_408220]) ).
tff(c_409355,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_409353]) ).
tff(c_409357,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_409355,c_381876]) ).
tff(c_410409,plain,
! [X5_1861] :
( ( inverse(X5_1861) != identity )
| ( inverse(X5_1861) != X5_1861 ) ),
inference(splitRight,[status(thm)],[c_409353]) ).
tff(c_410421,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_381876,c_410409]) ).
tff(c_410430,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_381876,c_410421]) ).
tff(c_410432,plain,
inverse(sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_410462,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_410432,c_74]) ).
tff(c_410466,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_410462,c_4]) ).
tff(c_410557,plain,
! [Z_1864] : ( multiply(sk_c8,multiply(sk_c5,Z_1864)) = multiply(identity,Z_1864) ),
inference(superposition,[status(thm),theory(equality)],[c_410466,c_410533]) ).
tff(c_410587,plain,
! [Z_1865] : ( multiply(sk_c8,multiply(sk_c5,Z_1865)) = Z_1865 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_410557]) ).
tff(c_410599,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_410478,c_410587]) ).
tff(c_410497,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_381119,c_80]) ).
tff(c_410431,plain,
inverse(sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_410611,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_410599,c_410497,c_410431,c_116]) ).
tff(c_410612,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_410611]) ).
tff(c_410759,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_410747,c_410612]) ).
tff(c_410710,plain,
multiply(inverse(sk_c8),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_410466,c_410662]) ).
tff(c_410753,plain,
multiply(sk_c7,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_410431,c_410710]) ).
tff(c_410878,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_410747,c_410753]) ).
tff(c_410881,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_410878,c_410462]) ).
tff(c_410894,plain,
multiply(sk_c8,identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_410881,c_4]) ).
tff(c_410692,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_410599,c_410662]) ).
tff(c_410748,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_410692]) ).
tff(c_410771,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_410748,c_410599]) ).
tff(c_410911,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_410894,c_410771]) ).
tff(c_410913,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_410759,c_410911]) ).
tff(c_410915,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_410611]) ).
tff(c_410924,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_410915,c_410431]) ).
tff(c_411024,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_411020,c_411020,c_410924]) ).
tff(c_411309,plain,
! [X_1878,Z_1879] : ( multiply(inverse(inverse(X_1878)),Z_1879) = multiply(X_1878,Z_1879) ),
inference(superposition,[status(thm),theory(equality)],[c_410951,c_410585]) ).
tff(c_411002,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_410951]) ).
tff(c_411316,plain,
! [X_1878] : ( multiply(X_1878,identity) = X_1878 ),
inference(superposition,[status(thm),theory(equality)],[c_411309,c_411002]) ).
tff(c_410921,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_410915,c_410462]) ).
tff(c_411026,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_411020,c_410921]) ).
tff(c_410919,plain,
multiply(sk_c5,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_410915,c_410478]) ).
tff(c_411126,plain,
multiply(sk_c5,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_411020,c_410919]) ).
tff(c_411130,plain,
multiply(inverse(sk_c5),sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_411126,c_410585]) ).
tff(c_411136,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_411026,c_411130]) ).
tff(c_411027,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_411020,c_410915]) ).
tff(c_410914,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_410611]) ).
tff(c_418560,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X3_8) != identity )
| ( identity != X3_8 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_411316,c_411136,c_411020,c_411136,c_411316,c_411136,c_411027,c_411027,c_411316,c_411136,c_411316,c_411136,c_411136,c_411316,c_411136,c_411027,c_411027,c_411316,c_411136,c_411027,c_411136,c_2,c_411136,c_411027,c_411020,c_410914]) ).
tff(c_418562,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_418560]) ).
tff(c_418564,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_418562,c_411024]) ).
tff(c_418565,plain,
! [X1_9,X5_6,X4_11,X3_8] :
( ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X3_8) != identity )
| ( identity != X3_8 ) ),
inference(splitRight,[status(thm)],[c_418560]) ).
tff(c_432796,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_418565]) ).
tff(c_432798,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_432796,c_411024]) ).
tff(c_432799,plain,
! [X4_11,X5_6,X1_9] :
( ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 ) ),
inference(splitRight,[status(thm)],[c_418565]) ).
tff(c_432809,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_432799]) ).
tff(c_432811,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_432809,c_411024]) ).
tff(c_432812,plain,
! [X5_6,X4_11] :
( ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(splitRight,[status(thm)],[c_432799]) ).
tff(c_432814,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_432812]) ).
tff(c_432816,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_432814,c_411024]) ).
tff(c_432819,plain,
! [X5_2040] :
( ( inverse(X5_2040) != identity )
| ( inverse(X5_2040) != X5_2040 ) ),
inference(splitRight,[status(thm)],[c_432812]) ).
tff(c_432831,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_411024,c_432819]) ).
tff(c_432840,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_411024,c_432831]) ).
tff(c_432842,plain,
inverse(sk_c3) != sk_c9,
inference(splitRight,[status(thm)],[c_98]) ).
tff(c_94,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_432890,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_432842,c_94]) ).
tff(c_432894,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_432890,c_4]) ).
tff(c_92,plain,
( ( multiply(sk_c8,sk_c7) = sk_c9 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_432950,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_432842,c_92]) ).
tff(c_432974,plain,
! [X_2041,Y_2042,Z_2043] : ( multiply(multiply(X_2041,Y_2042),Z_2043) = multiply(X_2041,multiply(Y_2042,Z_2043)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_433001,plain,
! [Z_2043] : ( multiply(sk_c7,multiply(sk_c8,Z_2043)) = multiply(identity,Z_2043) ),
inference(superposition,[status(thm),theory(equality)],[c_432894,c_432974]) ).
tff(c_433032,plain,
! [Z_2044] : ( multiply(sk_c7,multiply(sk_c8,Z_2044)) = Z_2044 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433001]) ).
tff(c_433044,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_432950,c_433032]) ).
tff(c_433016,plain,
! [X_2,Z_2043] : ( multiply(inverse(X_2),multiply(X_2,Z_2043)) = multiply(identity,Z_2043) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_432974]) ).
tff(c_433558,plain,
! [X_2052,Z_2053] : ( multiply(inverse(X_2052),multiply(X_2052,Z_2053)) = Z_2053 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433016]) ).
tff(c_433594,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_433044,c_433558]) ).
tff(c_433631,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_433594]) ).
tff(c_102,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_206]) ).
tff(c_432874,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_432842,c_102]) ).
tff(c_433640,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_433631,c_432874]) ).
tff(c_433682,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_433640,c_4]) ).
tff(c_433030,plain,
! [X_2,Z_2043] : ( multiply(inverse(X_2),multiply(X_2,Z_2043)) = Z_2043 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433016]) ).
tff(c_433757,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_433682,c_433030]) ).
tff(c_433769,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_433757]) ).
tff(c_432866,plain,
inverse(sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_78]) ).
tff(c_432870,plain,
multiply(sk_c8,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_432866,c_4]) ).
tff(c_433047,plain,
multiply(sk_c7,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_432870,c_433032]) ).
tff(c_433635,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_433631,c_433044]) ).
tff(c_433644,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_433047,c_433635]) ).
tff(c_100,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_203]) ).
tff(c_432934,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_432842,c_100]) ).
tff(c_433636,plain,
multiply(sk_c6,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_433631,c_432934]) ).
tff(c_433793,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433769,c_433644,c_433636]) ).
tff(c_433799,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_433793,c_433644]) ).
tff(c_433117,plain,
! [X_2046,Z_2047] : ( multiply(inverse(X_2046),multiply(X_2046,Z_2047)) = Z_2047 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433016]) ).
tff(c_433144,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_433044,c_433117]) ).
tff(c_433198,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_433144]) ).
tff(c_433212,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_433198,c_432874]) ).
tff(c_433233,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_433212,c_4]) ).
tff(c_433240,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_433233,c_433030]) ).
tff(c_433252,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_433240]) ).
tff(c_433256,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_433252,c_433212]) ).
tff(c_433206,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_433198,c_433044]) ).
tff(c_433214,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_433047,c_433206]) ).
tff(c_433156,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_432934,c_433117]) ).
tff(c_433200,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_432874,c_433156]) ).
tff(c_433326,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_433214,c_433198,c_2,c_433198,c_433200]) ).
tff(c_433333,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_433326,c_432866]) ).
tff(c_433335,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_433256,c_433333]) ).
tff(c_433329,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_433326,c_433214]) ).
tff(c_433070,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_432950,c_432890,c_116]) ).
tff(c_433071,plain,
multiply(sk_c8,sk_c9) != sk_c7,
inference(splitLeft,[status(thm)],[c_433070]) ).
tff(c_433205,plain,
multiply(sk_c8,identity) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_433198,c_433071]) ).
tff(c_433393,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433335,c_433329,c_433205]) ).
tff(c_433395,plain,
multiply(sk_c8,sk_c9) = sk_c7,
inference(splitRight,[status(thm)],[c_433070]) ).
tff(c_432841,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_98]) ).
tff(c_432846,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_432841,c_4]) ).
tff(c_433050,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_432846,c_433032]) ).
tff(c_433431,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_433047,c_433050]) ).
tff(c_96,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_432942,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_432842,c_96]) ).
tff(c_433441,plain,
multiply(sk_c2,sk_c8) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_433431,c_432942]) ).
tff(c_433013,plain,
! [Z_2043] : ( multiply(sk_c8,multiply(sk_c5,Z_2043)) = multiply(identity,Z_2043) ),
inference(superposition,[status(thm),theory(equality)],[c_432846,c_432974]) ).
tff(c_433029,plain,
! [Z_2043] : ( multiply(sk_c8,multiply(sk_c5,Z_2043)) = Z_2043 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433013]) ).
tff(c_433499,plain,
! [Z_2051] : ( multiply(sk_c8,multiply(sk_c2,Z_2051)) = Z_2051 ),
inference(demodulation,[status(thm),theory(equality)],[c_433431,c_433029]) ).
tff(c_433514,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_433441,c_433499]) ).
tff(c_433518,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_433395,c_433514]) ).
tff(c_433396,plain,
! [Z_2049] : ( multiply(sk_c5,multiply(sk_c8,Z_2049)) = multiply(sk_c9,Z_2049) ),
inference(superposition,[status(thm),theory(equality)],[c_432942,c_432974]) ).
tff(c_433408,plain,
multiply(sk_c9,sk_c7) = multiply(sk_c5,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_432950,c_433396]) ).
tff(c_433465,plain,
multiply(sk_c9,sk_c7) = multiply(sk_c2,sk_c9),
inference(demodulation,[status(thm),theory(equality)],[c_433431,c_433408]) ).
tff(c_433394,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_433070]) ).
tff(c_433464,plain,
multiply(sk_c9,sk_c7) != sk_c8,
inference(splitLeft,[status(thm)],[c_433394]) ).
tff(c_433466,plain,
multiply(sk_c2,sk_c9) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_433465,c_433464]) ).
tff(c_433520,plain,
multiply(sk_c2,sk_c9) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_433518,c_433466]) ).
tff(c_433879,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_433799,c_2,c_433793,c_433631,c_433520]) ).
tff(c_433881,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(splitRight,[status(thm)],[c_433394]) ).
tff(c_432878,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_432874,c_4]) ).
tff(c_433007,plain,
! [Z_2043] : ( multiply(sk_c9,multiply(sk_c6,Z_2043)) = multiply(identity,Z_2043) ),
inference(superposition,[status(thm),theory(equality)],[c_432878,c_432974]) ).
tff(c_434030,plain,
! [Z_2059] : ( multiply(sk_c9,multiply(sk_c6,Z_2059)) = Z_2059 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433007]) ).
tff(c_434042,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_432934,c_434030]) ).
tff(c_434046,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_433881,c_434042]) ).
tff(c_434053,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_434046,c_433044]) ).
tff(c_434062,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_432894,c_434053]) ).
tff(c_434067,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_434062,c_433047]) ).
tff(c_434071,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_434067]) ).
tff(c_434078,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_434071,c_432866]) ).
tff(c_434895,plain,
multiply(sk_c8,identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_434078,c_4]) ).
tff(c_434054,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_434046,c_432950]) ).
tff(c_434928,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_434895,c_434062,c_434054]) ).
tff(c_434934,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_434928,c_434078]) ).
tff(c_434941,plain,
! [X_2076,Z_2077] : ( multiply(inverse(X_2076),multiply(X_2076,Z_2077)) = Z_2077 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433016]) ).
tff(c_435105,plain,
! [X_2080,Z_2081] : ( multiply(inverse(inverse(X_2080)),Z_2081) = multiply(X_2080,Z_2081) ),
inference(superposition,[status(thm),theory(equality)],[c_433030,c_434941]) ).
tff(c_434968,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_434941]) ).
tff(c_435112,plain,
! [X_2080] : ( multiply(X_2080,identity) = X_2080 ),
inference(superposition,[status(thm),theory(equality)],[c_435105,c_434968]) ).
tff(c_434148,plain,
! [X_2060,Z_2061] : ( multiply(inverse(X_2060),multiply(X_2060,Z_2061)) = Z_2061 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433016]) ).
tff(c_434331,plain,
! [X_2065,Z_2066] : ( multiply(inverse(inverse(X_2065)),Z_2066) = multiply(X_2065,Z_2066) ),
inference(superposition,[status(thm),theory(equality)],[c_433030,c_434148]) ).
tff(c_434175,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_434148]) ).
tff(c_434338,plain,
! [X_2065] : ( multiply(X_2065,identity) = X_2065 ),
inference(superposition,[status(thm),theory(equality)],[c_434331,c_434175]) ).
tff(c_434092,plain,
multiply(sk_c8,identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_434078,c_4]) ).
tff(c_434134,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_434092,c_434062,c_434054]) ).
tff(c_433899,plain,
! [Z_2056] : ( multiply(sk_c9,multiply(sk_c6,Z_2056)) = Z_2056 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433007]) ).
tff(c_433911,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_432934,c_433899]) ).
tff(c_433915,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_433881,c_433911]) ).
tff(c_433922,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_433915,c_433044]) ).
tff(c_433931,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_432894,c_433922]) ).
tff(c_433954,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_433931,c_433047]) ).
tff(c_433959,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_433954]) ).
tff(c_433966,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_433959,c_432866]) ).
tff(c_433880,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_433394]) ).
tff(c_433889,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_433880]) ).
tff(c_433983,plain,
! [X3_2058] :
( ( inverse(X3_2058) != sk_c8 )
| ( multiply(X3_2058,sk_c8) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_433915,c_433915,c_433889]) ).
tff(c_433996,plain,
inverse(identity) != sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_2,c_433983]) ).
tff(c_434019,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_433966,c_433996]) ).
tff(c_434020,plain,
! [X4_11,X5_6,X1_9,X2_10] :
( ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_433880]) ).
tff(c_434083,plain,
! [X4_11,X5_6,X1_9,X2_10] :
( ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c8 )
| ( inverse(multiply(X5_6,sk_c8)) != sk_c8 )
| ( multiply(X5_6,sk_c8) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c8 )
| ( inverse(X2_10) != sk_c8 )
| ( multiply(X2_10,sk_c8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_434062,c_434046,c_434046,c_434046,c_434046,c_434046,c_434046,c_434046,c_434020]) ).
tff(c_434084,plain,
! [X2_10] :
( ( inverse(X2_10) != sk_c8 )
| ( multiply(X2_10,sk_c8) != identity ) ),
inference(splitLeft,[status(thm)],[c_434083]) ).
tff(c_434884,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_434338,c_434134,c_434134,c_434084]) ).
tff(c_434141,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_434134,c_434078]) ).
tff(c_434886,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_434884,c_434141]) ).
tff(c_434887,plain,
! [X1_9,X5_6,X4_11] :
( ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c8 )
| ( inverse(multiply(X5_6,sk_c8)) != sk_c8 )
| ( multiply(X5_6,sk_c8) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_434083]) ).
tff(c_443016,plain,
! [X1_9,X5_6,X4_11] :
( ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_435112,c_434928,c_434928,c_434928,c_435112,c_434928,c_435112,c_434928,c_434928,c_435112,c_434928,c_434928,c_434928,c_434887]) ).
tff(c_443018,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_443016]) ).
tff(c_443020,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_443018,c_434934]) ).
tff(c_443021,plain,
! [X5_6,X1_9] :
( ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 ) ),
inference(splitRight,[status(thm)],[c_443016]) ).
tff(c_443465,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_443021]) ).
tff(c_443467,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_443465,c_434934]) ).
tff(c_443469,plain,
! [X5_2159] :
( ( inverse(X5_2159) != identity )
| ( inverse(X5_2159) != X5_2159 ) ),
inference(splitRight,[status(thm)],[c_443021]) ).
tff(c_443483,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_434934,c_443469]) ).
tff(c_443495,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_434934,c_443483]) ).
tff(c_443496,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_78]) ).
tff(c_443551,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_432842,c_100]) ).
tff(c_443600,plain,
! [X_2160,Y_2161,Z_2162] : ( multiply(multiply(X_2160,Y_2161),Z_2162) = multiply(X_2160,multiply(Y_2161,Z_2162)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_443639,plain,
! [X_2,Z_2162] : ( multiply(inverse(X_2),multiply(X_2,Z_2162)) = multiply(identity,Z_2162) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_443600]) ).
tff(c_444165,plain,
! [X_2172,Z_2173] : ( multiply(inverse(X_2172),multiply(X_2172,Z_2173)) = Z_2173 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_443639]) ).
tff(c_444201,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_443551,c_444165]) ).
tff(c_444232,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_443496,c_444201]) ).
tff(c_443652,plain,
! [X_2,Z_2162] : ( multiply(inverse(X_2),multiply(X_2,Z_2162)) = Z_2162 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_443639]) ).
tff(c_444236,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_444232,c_443652]) ).
tff(c_444242,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_444236]) ).
tff(c_443525,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_432842,c_94]) ).
tff(c_443529,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_443525,c_4]) ).
tff(c_443497,plain,
inverse(sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_78]) ).
tff(c_443557,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_443497,c_72]) ).
tff(c_443636,plain,
! [Z_2162] : ( multiply(sk_c8,multiply(sk_c5,Z_2162)) = multiply(identity,Z_2162) ),
inference(superposition,[status(thm),theory(equality)],[c_432846,c_443600]) ).
tff(c_443688,plain,
! [Z_2164] : ( multiply(sk_c8,multiply(sk_c5,Z_2164)) = Z_2164 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_443636]) ).
tff(c_443703,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_443557,c_443688]) ).
tff(c_443624,plain,
! [Z_2162] : ( multiply(sk_c7,multiply(sk_c8,Z_2162)) = multiply(identity,Z_2162) ),
inference(superposition,[status(thm),theory(equality)],[c_443529,c_443600]) ).
tff(c_443647,plain,
! [Z_2162] : ( multiply(sk_c7,multiply(sk_c8,Z_2162)) = Z_2162 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_443624]) ).
tff(c_443714,plain,
multiply(sk_c7,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_443703,c_443647]) ).
tff(c_443720,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_443529,c_443714]) ).
tff(c_443750,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_443720,c_443496]) ).
tff(c_443654,plain,
! [Z_2163] : ( multiply(sk_c7,multiply(sk_c8,Z_2163)) = Z_2163 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_443624]) ).
tff(c_443669,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_432846,c_443654]) ).
tff(c_443576,plain,
multiply(sk_c8,sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_443497,c_68]) ).
tff(c_443666,plain,
multiply(sk_c7,sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_443576,c_443654]) ).
tff(c_443743,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_443720,c_443666]) ).
tff(c_443753,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_443669,c_443743]) ).
tff(c_443746,plain,
multiply(sk_c6,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_443720,c_443551]) ).
tff(c_443872,plain,
multiply(sk_c6,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_443753,c_443746]) ).
tff(c_443876,plain,
multiply(inverse(sk_c6),sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_443872,c_443652]) ).
tff(c_443882,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_443750,c_443876]) ).
tff(c_443708,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_443576,c_443525,c_116]) ).
tff(c_443709,plain,
multiply(sk_c8,sk_c9) != sk_c7,
inference(splitLeft,[status(thm)],[c_443708]) ).
tff(c_443710,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_443703,c_443709]) ).
tff(c_443758,plain,
sk_c8 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_443753,c_443710]) ).
tff(c_443889,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_443882,c_443758]) ).
tff(c_443745,plain,
multiply(sk_c5,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_443720,c_443557]) ).
tff(c_443945,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_443882,c_443745]) ).
tff(c_443946,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_443889,c_443945]) ).
tff(c_443948,plain,
multiply(sk_c8,sk_c9) = sk_c7,
inference(splitRight,[status(thm)],[c_443708]) ).
tff(c_443989,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_443948,c_443703]) ).
tff(c_444000,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_443989,c_432841]) ).
tff(c_444016,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_444000,c_4]) ).
tff(c_444268,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_444242,c_444016]) ).
tff(c_444246,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_444242,c_444000]) ).
tff(c_444288,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_444268,c_444246]) ).
tff(c_444445,plain,
! [X_2176,Z_2177] : ( multiply(inverse(inverse(X_2176)),Z_2177) = multiply(X_2176,Z_2177) ),
inference(superposition,[status(thm),theory(equality)],[c_444165,c_443652]) ).
tff(c_444222,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_444165]) ).
tff(c_444452,plain,
! [X_2176] : ( multiply(X_2176,identity) = X_2176 ),
inference(superposition,[status(thm),theory(equality)],[c_444445,c_444222]) ).
tff(c_443994,plain,
multiply(sk_c7,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_443989,c_443576]) ).
tff(c_444245,plain,
multiply(identity,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_444242,c_444242,c_443994]) ).
tff(c_444253,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_444245]) ).
tff(c_443997,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_443989,c_443525]) ).
tff(c_444009,plain,
multiply(sk_c7,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_443997,c_4]) ).
tff(c_444038,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_444009,c_443994]) ).
tff(c_443947,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c8 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X1_9,sk_c8) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_443708]) ).
tff(c_444020,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( multiply(sk_c9,sk_c7) != sk_c7 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c7 )
| ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X1_9) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c9 )
| ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_443989,c_443989,c_443989,c_443989,c_443989,c_443989,c_443947]) ).
tff(c_444021,plain,
multiply(sk_c9,sk_c7) != sk_c7,
inference(splitLeft,[status(thm)],[c_444020]) ).
tff(c_444155,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_444038,c_444021]) ).
tff(c_444156,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c9 )
| ( multiply(X2_10,sk_c9) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c9 )
| ( inverse(multiply(X5_6,sk_c9)) != sk_c9 )
| ( multiply(X5_6,sk_c9) != inverse(X5_6) )
| ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c9 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_444020]) ).
tff(c_452031,plain,
! [X5_6,X2_10,X3_8,X1_9,X4_11] :
( ( inverse(X2_10) != identity )
| ( identity != X2_10 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X3_8) != identity )
| ( identity != X3_8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_444452,c_444253,c_444242,c_444253,c_444452,c_444253,c_444242,c_444242,c_444452,c_444253,c_444452,c_444253,c_444253,c_444452,c_444253,c_444242,c_444242,c_444452,c_444253,c_444242,c_444253,c_444156]) ).
tff(c_452033,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_452031]) ).
tff(c_452035,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_452033,c_444288]) ).
tff(c_452036,plain,
! [X4_11,X5_6,X1_9,X2_10] :
( ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(splitRight,[status(thm)],[c_452031]) ).
tff(c_452857,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_452036]) ).
tff(c_452859,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_452857,c_444288]) ).
tff(c_452860,plain,
! [X1_9,X5_6,X4_11] :
( ( inverse(X1_9) != identity )
| ( identity != X1_9 )
| ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(splitRight,[status(thm)],[c_452036]) ).
tff(c_454634,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_452860]) ).
tff(c_454636,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_454634,c_444288]) ).
tff(c_454637,plain,
! [X5_6,X1_9] :
( ( inverse(X5_6) != identity )
| ( inverse(X5_6) != X5_6 )
| ( inverse(X1_9) != identity )
| ( identity != X1_9 ) ),
inference(splitRight,[status(thm)],[c_452860]) ).
tff(c_454639,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_454637]) ).
tff(c_454641,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_454639,c_444288]) ).
tff(c_455080,plain,
! [X5_2269] :
( ( inverse(X5_2269) != identity )
| ( inverse(X5_2269) != X5_2269 ) ),
inference(splitRight,[status(thm)],[c_454637]) ).
tff(c_455094,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_444288,c_455080]) ).
tff(c_455106,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_444288,c_455094]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP317-1 : TPTP v9.0.0. Released v2.5.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.33 % Computer : n028.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Mon Apr 7 21:42:19 EDT 2025
% 0.14/0.34 % CPUTime :
% 74.62/59.57 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 75.13/59.78
% 75.13/59.78 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------