%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP330-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n018.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:57 PM UTC 2025
% Result : Unsatisfiable 25.74s 11.38s
% Output : CNFRefutation 26.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 45
% Syntax : Number of formulae : 712 ( 573 unt; 0 typ; 0 def)
% Number of atoms : 988 ( 956 equ)
% Maximal formula atoms : 15 ( 1 avg)
% Number of connectives : 580 ( 304 ~; 276 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 331 ( 331 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c11 > sk_c10 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c10,type,
sk_c10: $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c11,type,
sk_c11: $i ).
tff(sk_c9,type,
sk_c9: $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( 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_89,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_206,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_257,axiom,
! [X5,X6,X3,X7,X1,X2,X8,X4] :
( ( multiply(sk_c10,sk_c11) != sk_c9 )
| ( multiply(X3,sk_c10) != sk_c11 )
| ( inverse(X3) != sk_c10 )
| ( multiply(X4,sk_c9) != sk_c10 )
| ( inverse(X4) != sk_c9 )
| ( multiply(X1,sk_c11) != sk_c10 )
| ( inverse(X1) != sk_c11 )
| ( multiply(X2,sk_c10) != sk_c9 )
| ( inverse(X2) != sk_c10 )
| ( multiply(X5,X6) != sk_c11 )
| ( inverse(X5) != X6 )
| ( multiply(X6,sk_c10) != sk_c11 )
| ( inverse(X7) != X8 )
| ( inverse(X8) != X6 )
| ( multiply(X7,X6) != X8 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_188,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_203,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_197,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_200,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_212,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_209,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_194,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_191,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_44,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_164,plain,
multiply(sk_c1,sk_c10) = sk_c11,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_58,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_137,plain,
inverse(sk_c1) = sk_c10,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_141,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_137,c_4]) ).
tff(c_62096,plain,
! [X_374,Y_375,Z_376] : ( multiply(multiply(X_374,Y_375),Z_376) = multiply(X_374,multiply(Y_375,Z_376)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_62147,plain,
! [Z_376] : ( multiply(sk_c10,multiply(sk_c1,Z_376)) = multiply(identity,Z_376) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_62096]) ).
tff(c_62296,plain,
! [Z_380] : ( multiply(sk_c10,multiply(sk_c1,Z_380)) = Z_380 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62147]) ).
tff(c_62308,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_164,c_62296]) ).
tff(c_62153,plain,
! [X_2,Z_376] : ( multiply(inverse(X_2),multiply(X_2,Z_376)) = multiply(identity,Z_376) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_62096]) ).
tff(c_62505,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_62153]) ).
tff(c_62562,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_62308,c_62505]) ).
tff(c_62637,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_62562]) ).
tff(c_209,plain,
! [X_16,Y_17,Z_18] : ( multiply(multiply(X_16,Y_17),Z_18) = multiply(X_16,multiply(Y_17,Z_18)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_233,plain,
! [Z_18] : ( multiply(sk_c10,multiply(sk_c1,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_209]) ).
tff(c_251,plain,
! [Z_19] : ( multiply(sk_c10,multiply(sk_c1,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_233]) ).
tff(c_263,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_164,c_251]) ).
tff(c_24,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_157,plain,
multiply(sk_c10,sk_c11) = sk_c9,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_267,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_263,c_157]) ).
tff(c_74,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_170,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_74]) ).
tff(c_275,plain,
multiply(sk_c2,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_267,c_170]) ).
tff(c_102,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_206]) ).
tff(c_125,plain,
inverse(sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_102]) ).
tff(c_129,plain,
multiply(sk_c9,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_125,c_4]) ).
tff(c_236,plain,
! [Z_18] : ( multiply(sk_c9,multiply(sk_c2,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_209]) ).
tff(c_248,plain,
! [Z_18] : ( multiply(sk_c9,multiply(sk_c2,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_236]) ).
tff(c_935,plain,
! [Z_33] : ( multiply(sk_c10,multiply(sk_c2,Z_33)) = Z_33 ),
inference(demodulation,[status(thm),theory(equality)],[c_267,c_248]) ).
tff(c_947,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_275,c_935]) ).
tff(c_239,plain,
! [X_2,Z_18] : ( multiply(inverse(X_2),multiply(X_2,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_209]) ).
tff(c_959,plain,
! [X_34,Z_35] : ( multiply(inverse(X_34),multiply(X_34,Z_35)) = Z_35 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_239]) ).
tff(c_977,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_947,c_959]) ).
tff(c_1017,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_977]) ).
tff(c_277,plain,
inverse(sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_267,c_125]) ).
tff(c_1034,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1017,c_277]) ).
tff(c_1054,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1034,c_4]) ).
tff(c_249,plain,
! [X_2,Z_18] : ( multiply(inverse(X_2),multiply(X_2,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_239]) ).
tff(c_1061,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_1054,c_249]) ).
tff(c_1073,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1061]) ).
tff(c_1077,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1073,c_1034]) ).
tff(c_1184,plain,
! [X_37,Z_38] : ( multiply(inverse(inverse(X_37)),Z_38) = multiply(X_37,Z_38) ),
inference(superposition,[status(thm),theory(equality)],[c_959,c_249]) ).
tff(c_1010,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_959]) ).
tff(c_1191,plain,
! [X_37] : ( multiply(X_37,identity) = X_37 ),
inference(superposition,[status(thm),theory(equality)],[c_1184,c_1010]) ).
tff(c_1205,plain,
! [X_37] : ( multiply(X_37,inverse(X_37)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_1184,c_4]) ).
tff(c_992,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_263,c_959]) ).
tff(c_1020,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_992]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_1447,plain,
! [X_44,Y_45,Z_46] : ( multiply(inverse(multiply(X_44,Y_45)),multiply(X_44,multiply(Y_45,Z_46))) = Z_46 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_959]) ).
tff(c_1526,plain,
! [X_44,X_2] : ( multiply(inverse(multiply(X_44,inverse(X_2))),multiply(X_44,identity)) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1447]) ).
tff(c_1559,plain,
! [X_44,X_2] : ( multiply(inverse(multiply(X_44,inverse(X_2))),X_44) = X_2 ),
inference(demodulation,[status(thm),theory(equality)],[c_1191,c_1526]) ).
tff(c_1227,plain,
! [X_39] : ( multiply(X_39,identity) = X_39 ),
inference(superposition,[status(thm),theory(equality)],[c_1184,c_1010]) ).
tff(c_962,plain,
! [X_34,Z_35] : ( multiply(inverse(inverse(X_34)),Z_35) = multiply(X_34,Z_35) ),
inference(superposition,[status(thm),theory(equality)],[c_959,c_249]) ).
tff(c_1234,plain,
! [X_34] : ( inverse(inverse(X_34)) = multiply(X_34,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_1227,c_962]) ).
tff(c_1279,plain,
! [X_34] : ( inverse(inverse(X_34)) = X_34 ),
inference(demodulation,[status(thm),theory(equality)],[c_1191,c_1234]) ).
tff(c_1565,plain,
! [X_47,X_48] : ( multiply(inverse(multiply(X_47,inverse(X_48))),X_47) = X_48 ),
inference(demodulation,[status(thm),theory(equality)],[c_1191,c_1526]) ).
tff(c_1218,plain,
! [X_37,Z_18] : ( multiply(X_37,multiply(inverse(X_37),Z_18)) = Z_18 ),
inference(superposition,[status(thm),theory(equality)],[c_249,c_1184]) ).
tff(c_1639,plain,
! [X_49,X_50] : ( multiply(multiply(X_49,inverse(X_50)),X_50) = X_49 ),
inference(superposition,[status(thm),theory(equality)],[c_1565,c_1218]) ).
tff(c_1730,plain,
! [X_51,X_52] : ( multiply(multiply(X_51,X_52),inverse(X_52)) = X_51 ),
inference(superposition,[status(thm),theory(equality)],[c_1279,c_1639]) ).
tff(c_1769,plain,
! [X_44,X_2] : ( inverse(multiply(X_44,inverse(X_2))) = multiply(X_2,inverse(X_44)) ),
inference(superposition,[status(thm),theory(equality)],[c_1559,c_1730]) ).
tff(c_391,plain,
! [X_22,Z_23] : ( multiply(inverse(X_22),multiply(X_22,Z_23)) = Z_23 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_239]) ).
tff(c_655,plain,
! [X_26,Z_27] : ( multiply(inverse(inverse(X_26)),Z_27) = multiply(X_26,Z_27) ),
inference(superposition,[status(thm),theory(equality)],[c_391,c_249]) ).
tff(c_454,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_391]) ).
tff(c_662,plain,
! [X_26] : ( multiply(X_26,identity) = X_26 ),
inference(superposition,[status(thm),theory(equality)],[c_655,c_454]) ).
tff(c_309,plain,
! [Z_20] : ( multiply(sk_c10,multiply(sk_c2,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_267,c_248]) ).
tff(c_321,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_275,c_309]) ).
tff(c_415,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_321,c_391]) ).
tff(c_462,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_415]) ).
tff(c_436,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_263,c_391]) ).
tff(c_467,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_436]) ).
tff(c_108,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X3_8) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( multiply(sk_c10,sk_c11) != sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_257]) ).
tff(c_297,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X4_13,sk_c10) != sk_c10 )
| ( inverse(X3_8) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_267,c_263,c_267,c_267,c_267,c_108]) ).
tff(c_298,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_297]) ).
tff(c_921,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_662,c_462,c_467,c_462,c_298]) ).
tff(c_475,plain,
multiply(sk_c1,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_467,c_164]) ).
tff(c_561,plain,
multiply(sk_c1,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_462,c_475]) ).
tff(c_325,plain,
! [Z_21] : ( multiply(sk_c1,multiply(sk_c10,Z_21)) = multiply(sk_c11,Z_21) ),
inference(superposition,[status(thm),theory(equality)],[c_164,c_209]) ).
tff(c_352,plain,
multiply(sk_c11,sk_c1) = multiply(sk_c1,identity),
inference(superposition,[status(thm),theory(equality)],[c_141,c_325]) ).
tff(c_470,plain,
multiply(sk_c1,identity) = multiply(identity,sk_c1),
inference(demodulation,[status(thm),theory(equality)],[c_467,c_352]) ).
tff(c_476,plain,
multiply(sk_c1,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_470]) ).
tff(c_574,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_561,c_476]) ).
tff(c_492,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_462,c_137]) ).
tff(c_576,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_574,c_492]) ).
tff(c_923,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_921,c_576]) ).
tff(c_924,plain,
! [X5_6,X4_13,X1_10,X7_9,X2_11] :
( ( inverse(X4_13) != sk_c10 )
| ( multiply(X4_13,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_297]) ).
tff(c_8651,plain,
! [X5_6,X4_13,X1_10,X7_9,X2_11] :
( ( inverse(X4_13) != identity )
| ( identity != X4_13 )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( multiply(X5_6,inverse(X7_9)) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( inverse(X5_6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1205,c_1020,c_1191,c_1017,c_1020,c_1769,c_1191,c_1017,c_1017,c_1017,c_1191,c_1017,c_1020,c_1020,c_1191,c_1017,c_1017,c_1017,c_924]) ).
tff(c_35262,plain,
! [X5_247,X7_248] :
( ( multiply(X5_247,inverse(X7_248)) != inverse(X5_247) )
| ( multiply(X7_248,inverse(X5_247)) != inverse(X7_248) )
| ( inverse(X5_247) != identity ) ),
inference(splitLeft,[status(thm)],[c_8651]) ).
tff(c_35332,plain,
! [X7_248] :
( ( inverse(identity) != inverse(X7_248) )
| ( multiply(X7_248,inverse(identity)) != inverse(X7_248) )
| ( inverse(identity) != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_35262]) ).
tff(c_35362,plain,
! [X7_249] :
( ( inverse(X7_249) != identity )
| ( inverse(X7_249) != X7_249 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1077,c_1191,c_1077,c_1077,c_35332]) ).
tff(c_35374,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_1077,c_35362]) ).
tff(c_35383,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1077,c_35374]) ).
tff(c_35384,plain,
! [X4_13,X1_10,X2_11] :
( ( inverse(X4_13) != identity )
| ( identity != X4_13 )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_8651]) ).
tff(c_60957,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_35384]) ).
tff(c_60959,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60957,c_1077]) ).
tff(c_60960,plain,
! [X1_10,X4_13] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X4_13) != identity )
| ( identity != X4_13 ) ),
inference(splitRight,[status(thm)],[c_35384]) ).
tff(c_61978,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_60960]) ).
tff(c_61980,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61978,c_1077]) ).
tff(c_61982,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_60960]) ).
tff(c_61984,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61982,c_1077]) ).
tff(c_61986,plain,
multiply(sk_c2,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_70,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_62000,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_61986,c_70]) ).
tff(c_68,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_62084,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_61986,c_68]) ).
tff(c_62574,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_62084,c_62505]) ).
tff(c_62639,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_62000,c_62574]) ).
tff(c_62727,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_62637,c_2,c_62637,c_62639]) ).
tff(c_62312,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62308,c_157]) ).
tff(c_62323,plain,
inverse(sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62312,c_125]) ).
tff(c_62732,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_62727,c_62323]) ).
tff(c_62753,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_62732,c_4]) ).
tff(c_62168,plain,
! [X_2,Z_376] : ( multiply(inverse(X_2),multiply(X_2,Z_376)) = Z_376 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62153]) ).
tff(c_62927,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_62753,c_62168]) ).
tff(c_62939,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_62927]) ).
tff(c_62321,plain,
multiply(sk_c2,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62312,c_61986]) ).
tff(c_62731,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_62727,c_62727,c_62321]) ).
tff(c_63011,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62939,c_62731]) ).
tff(c_63013,plain,
multiply(sk_c1,sk_c10) != sk_c11,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_30,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_63044,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_63013,c_30]) ).
tff(c_28,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_63124,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_63013,c_28]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_63031,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_63013,c_34]) ).
tff(c_32,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_63100,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_63013,c_32]) ).
tff(c_78,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_63026,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_78]) ).
tff(c_63129,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_63183,plain,
! [Z_393] : ( multiply(sk_c9,multiply(sk_c2,Z_393)) = multiply(identity,Z_393) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_63129]) ).
tff(c_63541,plain,
! [Z_402] : ( multiply(sk_c9,multiply(sk_c2,Z_402)) = Z_402 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63183]) ).
tff(c_63553,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_63026,c_63541]) ).
tff(c_63186,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_63129]) ).
tff(c_63985,plain,
! [X_414,Z_415] : ( multiply(inverse(X_414),multiply(X_414,Z_415)) = Z_415 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63186]) ).
tff(c_64075,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_63553,c_63985]) ).
tff(c_64171,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_64075]) ).
tff(c_64208,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64171,c_137]) ).
tff(c_64331,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_64208,c_4]) ).
tff(c_63201,plain,
! [X_2,Z_393] : ( multiply(inverse(X_2),multiply(X_2,Z_393)) = Z_393 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63186]) ).
tff(c_64360,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_64331,c_63201]) ).
tff(c_64372,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_64360]) ).
tff(c_64376,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64372,c_64208]) ).
tff(c_42,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_63059,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_63013,c_42]) ).
tff(c_63063,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_63059,c_4]) ).
tff(c_63012,plain,
inverse(sk_c6) = sk_c8,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_63018,plain,
multiply(sk_c8,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_63012,c_4]) ).
tff(c_63174,plain,
! [Z_393] : ( multiply(sk_c8,multiply(sk_c6,Z_393)) = multiply(identity,Z_393) ),
inference(superposition,[status(thm),theory(equality)],[c_63018,c_63129]) ).
tff(c_63735,plain,
! [Z_409] : ( multiply(sk_c8,multiply(sk_c6,Z_409)) = Z_409 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63174]) ).
tff(c_63753,plain,
multiply(sk_c8,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_63063,c_63735]) ).
tff(c_36,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_63108,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_63013,c_36]) ).
tff(c_38,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_63073,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_63013,c_38]) ).
tff(c_63077,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_63073,c_4]) ).
tff(c_63159,plain,
! [Z_393] : ( multiply(sk_c8,multiply(sk_c5,Z_393)) = multiply(identity,Z_393) ),
inference(superposition,[status(thm),theory(equality)],[c_63077,c_63129]) ).
tff(c_63655,plain,
! [Z_406] : ( multiply(sk_c8,multiply(sk_c5,Z_406)) = Z_406 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63159]) ).
tff(c_63667,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_63108,c_63655]) ).
tff(c_64048,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_63667,c_63985]) ).
tff(c_64164,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_64048]) ).
tff(c_64224,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_64164,c_63667]) ).
tff(c_64229,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_63753,c_64224]) ).
tff(c_40,plain,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_63115,plain,
multiply(sk_c8,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_63013,c_40]) ).
tff(c_63147,plain,
! [Z_393] : ( multiply(sk_c8,multiply(sk_c10,Z_393)) = multiply(sk_c11,Z_393) ),
inference(superposition,[status(thm),theory(equality)],[c_63115,c_63129]) ).
tff(c_64522,plain,
! [Z_393] : ( multiply(sk_c7,Z_393) = Z_393 ),
inference(demodulation,[status(thm),theory(equality)],[c_64229,c_2,c_64164,c_2,c_64171,c_63147]) ).
tff(c_63162,plain,
! [Z_393] : ( multiply(sk_c6,multiply(sk_c7,Z_393)) = multiply(identity,Z_393) ),
inference(superposition,[status(thm),theory(equality)],[c_63063,c_63129]) ).
tff(c_63195,plain,
! [Z_393] : ( multiply(sk_c6,multiply(sk_c7,Z_393)) = Z_393 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63162]) ).
tff(c_63821,plain,
! [Z_412] : ( multiply(sk_c8,Z_412) = multiply(sk_c7,Z_412) ),
inference(superposition,[status(thm),theory(equality)],[c_63195,c_63735]) ).
tff(c_63863,plain,
multiply(sk_c7,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_63753,c_63821]) ).
tff(c_64525,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64522,c_63863]) ).
tff(c_64559,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64525,c_64229]) ).
tff(c_63217,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X3_8) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_108]) ).
tff(c_63339,plain,
! [X3_399] :
( ( inverse(X3_399) != sk_c10 )
| ( multiply(X3_399,sk_c10) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_63217]) ).
tff(c_63355,plain,
( ( inverse(sk_c4) != sk_c10 )
| ( sk_c9 != sk_c11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_63100,c_63339]) ).
tff(c_63366,plain,
sk_c9 != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_63031,c_63355]) ).
tff(c_63219,plain,
! [Z_395] : ( multiply(sk_c9,multiply(sk_c2,Z_395)) = Z_395 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63183]) ).
tff(c_63231,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_63026,c_63219]) ).
tff(c_63376,plain,
! [X_400,Z_401] : ( multiply(inverse(X_400),multiply(X_400,Z_401)) = Z_401 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63186]) ).
tff(c_63418,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_63231,c_63376]) ).
tff(c_63505,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_63418]) ).
tff(c_63531,plain,
multiply(identity,sk_c11) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_63505,c_157]) ).
tff(c_63537,plain,
sk_c9 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63531]) ).
tff(c_63539,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_63366,c_63537]) ).
tff(c_63540,plain,
! [X5_6,X4_13,X1_10,X7_9,X2_11] :
( ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_63217]) ).
tff(c_63765,plain,
! [X7_410,X5_411] :
( ( inverse(multiply(X7_410,inverse(X5_411))) != inverse(X5_411) )
| ( multiply(X7_410,inverse(X5_411)) != inverse(X7_410) )
| ( multiply(inverse(X5_411),sk_c10) != sk_c11 )
| ( multiply(X5_411,inverse(X5_411)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_63540]) ).
tff(c_63770,plain,
! [X7_410] :
( ( inverse(multiply(X7_410,sk_c8)) != inverse(sk_c5) )
| ( multiply(X7_410,inverse(sk_c5)) != inverse(X7_410) )
| ( multiply(inverse(sk_c5),sk_c10) != sk_c11 )
| ( multiply(sk_c5,inverse(sk_c5)) != sk_c11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_63073,c_63765]) ).
tff(c_63791,plain,
! [X7_410] :
( ( inverse(multiply(X7_410,sk_c8)) != sk_c8 )
| ( multiply(X7_410,sk_c8) != inverse(X7_410) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_63108,c_63073,c_63115,c_63073,c_63073,c_63073,c_63770]) ).
tff(c_64622,plain,
! [X7_420] :
( ( inverse(multiply(X7_420,identity)) != identity )
| ( multiply(X7_420,identity) != inverse(X7_420) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_64559,c_64559,c_64559,c_63791]) ).
tff(c_64630,plain,
( ( inverse(identity) != identity )
| ( multiply(inverse(identity),identity) != inverse(inverse(identity)) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_64622]) ).
tff(c_64638,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_64376,c_64376,c_4,c_64376,c_64630]) ).
tff(c_64639,plain,
! [X2_11,X1_10,X4_13] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_63540]) ).
tff(c_64928,plain,
! [X4_427] :
( ( inverse(X4_427) != sk_c9 )
| ( multiply(X4_427,sk_c9) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_64639]) ).
tff(c_64942,plain,
inverse(sk_c2) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_63026,c_64928]) ).
tff(c_64955,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_125,c_64942]) ).
tff(c_64956,plain,
! [X1_10,X2_11] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_64639]) ).
tff(c_65202,plain,
! [X2_431] :
( ( inverse(X2_431) != sk_c10 )
| ( multiply(X2_431,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_64956]) ).
tff(c_65228,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_63100,c_65202]) ).
tff(c_65243,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_63031,c_65228]) ).
tff(c_65335,plain,
! [X1_433] :
( ( inverse(X1_433) != sk_c11 )
| ( multiply(X1_433,sk_c11) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_64956]) ).
tff(c_65355,plain,
inverse(sk_c3) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_63124,c_65335]) ).
tff(c_65374,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_63044,c_65355]) ).
tff(c_65376,plain,
multiply(sk_c2,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_78]) ).
tff(c_72,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_65456,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_65376,c_72]) ).
tff(c_65388,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_63013,c_34]) ).
tff(c_65392,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_65388,c_4]) ).
tff(c_65485,plain,
! [X_434,Y_435,Z_436] : ( multiply(multiply(X_434,Y_435),Z_436) = multiply(X_434,multiply(Y_435,Z_436)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_65521,plain,
! [Z_436] : ( multiply(sk_c10,multiply(sk_c4,Z_436)) = multiply(identity,Z_436) ),
inference(superposition,[status(thm),theory(equality)],[c_65392,c_65485]) ).
tff(c_66135,plain,
! [Z_450] : ( multiply(sk_c10,multiply(sk_c4,Z_450)) = Z_450 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65521]) ).
tff(c_66147,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_65456,c_66135]) ).
tff(c_65539,plain,
! [X_2,Z_436] : ( multiply(inverse(X_2),multiply(X_2,Z_436)) = multiply(identity,Z_436) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65485]) ).
tff(c_66441,plain,
! [X_457,Z_458] : ( multiply(inverse(X_457),multiply(X_457,Z_458)) = Z_458 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65539]) ).
tff(c_66492,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_66147,c_66441]) ).
tff(c_66569,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_66492]) ).
tff(c_66605,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66569,c_129]) ).
tff(c_65554,plain,
! [X_2,Z_436] : ( multiply(inverse(X_2),multiply(X_2,Z_436)) = Z_436 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65539]) ).
tff(c_66753,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_66605,c_65554]) ).
tff(c_66765,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_66753]) ).
tff(c_65473,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_63013,c_28]) ).
tff(c_65402,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_63013,c_30]) ).
tff(c_65406,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_65402,c_4]) ).
tff(c_65518,plain,
! [Z_436] : ( multiply(sk_c11,multiply(sk_c3,Z_436)) = multiply(identity,Z_436) ),
inference(superposition,[status(thm),theory(equality)],[c_65406,c_65485]) ).
tff(c_66074,plain,
! [Z_448] : ( multiply(sk_c11,multiply(sk_c3,Z_448)) = Z_448 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65518]) ).
tff(c_66089,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_65473,c_66074]) ).
tff(c_65530,plain,
! [Z_436] : ( multiply(sk_c10,multiply(sk_c11,Z_436)) = multiply(sk_c9,Z_436) ),
inference(superposition,[status(thm),theory(equality)],[c_157,c_65485]) ).
tff(c_66096,plain,
multiply(sk_c9,sk_c10) = multiply(sk_c10,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_66089,c_65530]) ).
tff(c_66102,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_157,c_66096]) ).
tff(c_66501,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_66102,c_66441]) ).
tff(c_66570,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_66501]) ).
tff(c_66604,plain,
multiply(sk_c2,identity) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_66569,c_65376]) ).
tff(c_66890,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66765,c_66570,c_66604]) ).
tff(c_66892,plain,
multiply(sk_c10,sk_c11) != sk_c9,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_18,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_68096,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_66892,c_18]) ).
tff(c_16,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_68135,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_66892,c_16]) ).
tff(c_68169,plain,
! [X_482,Y_483,Z_484] : ( multiply(multiply(X_482,Y_483),Z_484) = multiply(X_482,multiply(Y_483,Z_484)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_68223,plain,
! [X_2,Z_484] : ( multiply(inverse(X_2),multiply(X_2,Z_484)) = multiply(identity,Z_484) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_68169]) ).
tff(c_68315,plain,
! [X_489,Z_490] : ( multiply(inverse(X_489),multiply(X_489,Z_490)) = Z_490 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68223]) ).
tff(c_68363,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_68135,c_68315]) ).
tff(c_68426,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_68096,c_68363]) ).
tff(c_68238,plain,
! [X_2,Z_484] : ( multiply(inverse(X_2),multiply(X_2,Z_484)) = Z_484 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68223]) ).
tff(c_68532,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_68426,c_68238]) ).
tff(c_68538,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_68532]) ).
tff(c_76,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_68130,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_76]) ).
tff(c_68220,plain,
! [Z_484] : ( multiply(sk_c9,multiply(sk_c2,Z_484)) = multiply(identity,Z_484) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_68169]) ).
tff(c_68253,plain,
! [Z_486] : ( multiply(sk_c9,multiply(sk_c2,Z_486)) = Z_486 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68220]) ).
tff(c_68265,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_68130,c_68253]) ).
tff(c_68342,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_68265,c_68315]) ).
tff(c_68423,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_68342]) ).
tff(c_66906,plain,
multiply(sk_c1,sk_c10) = sk_c11,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_67561,plain,
! [X_472,Y_473,Z_474] : ( multiply(multiply(X_472,Y_473),Z_474) = multiply(X_472,multiply(Y_473,Z_474)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_67609,plain,
! [Z_474] : ( multiply(sk_c10,multiply(sk_c1,Z_474)) = multiply(identity,Z_474) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_67561]) ).
tff(c_67632,plain,
! [Z_475] : ( multiply(sk_c10,multiply(sk_c1,Z_475)) = Z_475 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67609]) ).
tff(c_67644,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_66906,c_67632]) ).
tff(c_67615,plain,
! [X_2,Z_474] : ( multiply(inverse(X_2),multiply(X_2,Z_474)) = multiply(identity,Z_474) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_67561]) ).
tff(c_67782,plain,
! [X_480,Z_481] : ( multiply(inverse(X_480),multiply(X_480,Z_481)) = Z_481 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67615]) ).
tff(c_67830,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_67644,c_67782]) ).
tff(c_67910,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_67830]) ).
tff(c_66913,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_74]) ).
tff(c_67015,plain,
! [X_461,Y_462,Z_463] : ( multiply(multiply(X_461,Y_462),Z_463) = multiply(X_461,multiply(Y_462,Z_463)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_67069,plain,
! [Z_463] : ( multiply(sk_c9,multiply(sk_c2,Z_463)) = multiply(identity,Z_463) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_67015]) ).
tff(c_67114,plain,
! [Z_465] : ( multiply(sk_c9,multiply(sk_c2,Z_465)) = Z_465 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67069]) ).
tff(c_67126,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_66913,c_67114]) ).
tff(c_67072,plain,
! [X_2,Z_463] : ( multiply(inverse(X_2),multiply(X_2,Z_463)) = multiply(identity,Z_463) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_67015]) ).
tff(c_67233,plain,
! [X_469,Z_470] : ( multiply(inverse(X_469),multiply(X_469,Z_470)) = Z_470 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67072]) ).
tff(c_67272,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_67126,c_67233]) ).
tff(c_67363,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_67272]) ).
tff(c_12,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_66983,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_66892,c_12]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_66952,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_66892,c_14]) ).
tff(c_66956,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_66952,c_4]) ).
tff(c_67048,plain,
! [Z_463] : ( multiply(sk_c10,multiply(sk_c4,Z_463)) = multiply(identity,Z_463) ),
inference(superposition,[status(thm),theory(equality)],[c_66956,c_67015]) ).
tff(c_67196,plain,
! [Z_468] : ( multiply(sk_c10,multiply(sk_c4,Z_468)) = Z_468 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67048]) ).
tff(c_67211,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_66983,c_67196]) ).
tff(c_67254,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_67211,c_67233]) ).
tff(c_67358,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_67254]) ).
tff(c_67066,plain,
! [Z_463] : ( multiply(sk_c10,multiply(sk_c1,Z_463)) = multiply(identity,Z_463) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_67015]) ).
tff(c_67089,plain,
! [Z_464] : ( multiply(sk_c10,multiply(sk_c1,Z_464)) = Z_464 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67066]) ).
tff(c_67101,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_66906,c_67089]) ).
tff(c_67105,plain,
sk_c9 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_67101,c_66892]) ).
tff(c_67380,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_67358,c_67105]) ).
tff(c_67451,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_67363,c_67380]) ).
tff(c_67453,plain,
multiply(sk_c2,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_67467,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_67453,c_70]) ).
tff(c_8,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_67529,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_66892,c_8]) ).
tff(c_67848,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_67529,c_67782]) ).
tff(c_67913,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_67467,c_67848]) ).
tff(c_67990,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67910,c_2,c_67910,c_67913]) ).
tff(c_67648,plain,
sk_c9 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_67644,c_66892]) ).
tff(c_67991,plain,
sk_c9 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_67990,c_67648]) ).
tff(c_67452,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_67548,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_66892,c_12]) ).
tff(c_67839,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_67548,c_67782]) ).
tff(c_67911,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_67452,c_67839]) ).
tff(c_68052,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67990,c_2,c_67990,c_67911]) ).
tff(c_68053,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_67991,c_68052]) ).
tff(c_68055,plain,
multiply(sk_c1,sk_c10) != sk_c11,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_68125,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_68055,c_32]) ).
tff(c_68082,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_68055,c_34]) ).
tff(c_68086,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68082,c_4]) ).
tff(c_68205,plain,
! [Z_484] : ( multiply(sk_c10,multiply(sk_c4,Z_484)) = multiply(identity,Z_484) ),
inference(superposition,[status(thm),theory(equality)],[c_68086,c_68169]) ).
tff(c_68276,plain,
! [Z_487] : ( multiply(sk_c10,multiply(sk_c4,Z_487)) = Z_487 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68205]) ).
tff(c_68288,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_68125,c_68276]) ).
tff(c_68336,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_68288,c_68315]) ).
tff(c_68422,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_68336]) ).
tff(c_68439,plain,
multiply(sk_c10,sk_c11) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_68422,c_66892]) ).
tff(c_68924,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_68538,c_2,c_68423,c_68439]) ).
tff(c_68925,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_68100,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68096,c_4]) ).
tff(c_68966,plain,
! [X_495,Y_496,Z_497] : ( multiply(multiply(X_495,Y_496),Z_497) = multiply(X_495,multiply(Y_496,Z_497)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_68996,plain,
! [Z_497] : ( multiply(sk_c8,multiply(sk_c5,Z_497)) = multiply(identity,Z_497) ),
inference(superposition,[status(thm),theory(equality)],[c_68100,c_68966]) ).
tff(c_69060,plain,
! [Z_500] : ( multiply(sk_c8,multiply(sk_c5,Z_500)) = Z_500 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68996]) ).
tff(c_69072,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_68925,c_69060]) ).
tff(c_69017,plain,
! [X_2,Z_497] : ( multiply(inverse(X_2),multiply(X_2,Z_497)) = multiply(identity,Z_497) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_68966]) ).
tff(c_69099,plain,
! [X_502,Z_503] : ( multiply(inverse(X_502),multiply(X_502,Z_503)) = Z_503 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69017]) ).
tff(c_69120,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_69072,c_69099]) ).
tff(c_69199,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_69120]) ).
tff(c_68054,plain,
inverse(sk_c3) = sk_c11,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_68926,plain,
multiply(sk_c2,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_68931,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_68926,c_68]) ).
tff(c_69141,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_68931,c_69099]) ).
tff(c_69201,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_68054,c_69141]) ).
tff(c_69384,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69199,c_2,c_69199,c_69201]) ).
tff(c_69147,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_68125,c_69099]) ).
tff(c_69203,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_68082,c_69147]) ).
tff(c_69032,plain,
! [X_2,Z_497] : ( multiply(inverse(X_2),multiply(X_2,Z_497)) = Z_497 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69017]) ).
tff(c_69325,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_69203,c_69032]) ).
tff(c_69332,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_69325]) ).
tff(c_69340,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69332,c_125]) ).
tff(c_69352,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69340,c_4]) ).
tff(c_69359,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_69352,c_69032]) ).
tff(c_69371,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_69359]) ).
tff(c_69337,plain,
multiply(sk_c2,identity) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69332,c_68926]) ).
tff(c_69497,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_69384,c_2,c_69371,c_69337]) ).
tff(c_69499,plain,
inverse(sk_c1) != sk_c10,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_50,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_69533,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_69499,c_50]) ).
tff(c_48,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_69577,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_69499,c_48]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_69507,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_69499,c_54]) ).
tff(c_52,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_69596,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_69499,c_52]) ).
tff(c_69537,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69533,c_4]) ).
tff(c_69623,plain,
! [X_506,Y_507,Z_508] : ( multiply(multiply(X_506,Y_507),Z_508) = multiply(X_506,multiply(Y_507,Z_508)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_69656,plain,
! [Z_508] : ( multiply(sk_c11,multiply(sk_c3,Z_508)) = multiply(identity,Z_508) ),
inference(superposition,[status(thm),theory(equality)],[c_69537,c_69623]) ).
tff(c_70162,plain,
! [Z_520] : ( multiply(sk_c11,multiply(sk_c3,Z_520)) = Z_520 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69656]) ).
tff(c_70174,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_69577,c_70162]) ).
tff(c_69671,plain,
! [X_2,Z_508] : ( multiply(inverse(X_2),multiply(X_2,Z_508)) = multiply(identity,Z_508) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_69623]) ).
tff(c_70489,plain,
! [X_528,Z_529] : ( multiply(inverse(X_528),multiply(X_528,Z_529)) = Z_529 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69671]) ).
tff(c_70552,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_70174,c_70489]) ).
tff(c_70647,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_70552]) ).
tff(c_70675,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_70647,c_69507]) ).
tff(c_70804,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_70675,c_4]) ).
tff(c_69685,plain,
! [X_2,Z_508] : ( multiply(inverse(X_2),multiply(X_2,Z_508)) = Z_508 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69671]) ).
tff(c_70816,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_70804,c_69685]) ).
tff(c_70828,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_70816]) ).
tff(c_56,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_69567,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_69499,c_56]) ).
tff(c_69498,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_69503,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69498,c_4]) ).
tff(c_69665,plain,
! [Z_508] : ( multiply(sk_c8,multiply(sk_c5,Z_508)) = multiply(identity,Z_508) ),
inference(superposition,[status(thm),theory(equality)],[c_69503,c_69623]) ).
tff(c_70139,plain,
! [Z_519] : ( multiply(sk_c8,multiply(sk_c5,Z_519)) = Z_519 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69665]) ).
tff(c_70151,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69567,c_70139]) ).
tff(c_70558,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_70151,c_70489]) ).
tff(c_70648,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_70558]) ).
tff(c_62,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_69549,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_69499,c_62]) ).
tff(c_69553,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69549,c_4]) ).
tff(c_64,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_69525,plain,
inverse(sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_69499,c_64]) ).
tff(c_69529,plain,
multiply(sk_c8,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69525,c_4]) ).
tff(c_69659,plain,
! [Z_508] : ( multiply(sk_c8,multiply(sk_c6,Z_508)) = multiply(identity,Z_508) ),
inference(superposition,[status(thm),theory(equality)],[c_69529,c_69623]) ).
tff(c_70186,plain,
! [Z_521] : ( multiply(sk_c8,multiply(sk_c6,Z_521)) = Z_521 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69659]) ).
tff(c_70204,plain,
multiply(sk_c8,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_69553,c_70186]) ).
tff(c_69511,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69507,c_4]) ).
tff(c_60,plain,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_69603,plain,
multiply(sk_c8,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_69499,c_60]) ).
tff(c_70216,plain,
! [Z_522] : ( multiply(sk_c8,multiply(sk_c10,Z_522)) = multiply(sk_c11,Z_522) ),
inference(superposition,[status(thm),theory(equality)],[c_69603,c_69623]) ).
tff(c_70237,plain,
multiply(sk_c8,identity) = multiply(sk_c11,sk_c4),
inference(superposition,[status(thm),theory(equality)],[c_69511,c_70216]) ).
tff(c_70242,plain,
multiply(sk_c11,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70204,c_70237]) ).
tff(c_70687,plain,
multiply(identity,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70648,c_70242]) ).
tff(c_70695,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70687]) ).
tff(c_70835,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_70828,c_70695]) ).
tff(c_70769,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_70695,c_69549]) ).
tff(c_70808,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_70675,c_70769]) ).
tff(c_70689,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_70648,c_70151]) ).
tff(c_70696,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70204,c_70689]) ).
tff(c_70753,plain,
inverse(sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70696,c_69525]) ).
tff(c_70874,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_70835,c_70808,c_70753]) ).
tff(c_69653,plain,
! [Z_508] : ( multiply(sk_c6,multiply(sk_c7,Z_508)) = multiply(identity,Z_508) ),
inference(superposition,[status(thm),theory(equality)],[c_69553,c_69623]) ).
tff(c_69679,plain,
! [Z_508] : ( multiply(sk_c6,multiply(sk_c7,Z_508)) = Z_508 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69653]) ).
tff(c_70319,plain,
! [Z_526] : ( multiply(sk_c8,Z_526) = multiply(sk_c7,Z_526) ),
inference(superposition,[status(thm),theory(equality)],[c_69679,c_70186]) ).
tff(c_70337,plain,
multiply(sk_c7,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_70319,c_70204]) ).
tff(c_70343,plain,
multiply(sk_c7,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_70319,c_70151]) ).
tff(c_70684,plain,
multiply(sk_c7,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_70648,c_70343]) ).
tff(c_70693,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70337,c_70684]) ).
tff(c_70774,plain,
sk_c8 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_70695,c_70693]) ).
tff(c_70834,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_70828,c_70774]) ).
tff(c_69724,plain,
! [Z_511] : ( multiply(sk_c11,multiply(sk_c3,Z_511)) = Z_511 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69656]) ).
tff(c_69736,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_69577,c_69724]) ).
tff(c_69831,plain,
! [X_514,Z_515] : ( multiply(inverse(X_514),multiply(X_514,Z_515)) = Z_515 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69671]) ).
tff(c_69861,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69736,c_69831]) ).
tff(c_69942,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_69861]) ).
tff(c_69885,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69596,c_69831]) ).
tff(c_69946,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69507,c_69885]) ).
tff(c_70051,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69942,c_2,c_69942,c_69946]) ).
tff(c_69710,plain,
multiply(sk_c10,sk_c11) != sk_c9,
inference(splitLeft,[status(thm)],[c_108]) ).
tff(c_69956,plain,
multiply(identity,sk_c11) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_69942,c_69710]) ).
tff(c_69963,plain,
sk_c9 != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69956]) ).
tff(c_70052,plain,
sk_c11 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_70051,c_69963]) ).
tff(c_69792,plain,
! [Z_513] : ( multiply(sk_c8,multiply(sk_c6,Z_513)) = Z_513 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69659]) ).
tff(c_69816,plain,
multiply(sk_c8,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_69553,c_69792]) ).
tff(c_66,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_69588,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_69499,c_66]) ).
tff(c_69687,plain,
! [Z_509] : ( multiply(sk_c6,multiply(sk_c7,Z_509)) = Z_509 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69653]) ).
tff(c_69699,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69588,c_69687]) ).
tff(c_69740,plain,
! [Z_512] : ( multiply(sk_c7,multiply(sk_c8,Z_512)) = multiply(sk_c6,Z_512) ),
inference(superposition,[status(thm),theory(equality)],[c_69588,c_69623]) ).
tff(c_69758,plain,
multiply(sk_c7,identity) = multiply(sk_c6,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_69529,c_69740]) ).
tff(c_69765,plain,
multiply(sk_c7,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_69699,c_69758]) ).
tff(c_69776,plain,
multiply(sk_c6,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69765,c_69679]) ).
tff(c_69855,plain,
multiply(inverse(sk_c6),identity) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69776,c_69831]) ).
tff(c_69940,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_69816,c_69525,c_69855]) ).
tff(c_69894,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69567,c_69831]) ).
tff(c_69949,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_69498,c_69894]) ).
tff(c_70088,plain,
multiply(sk_c7,sk_c11) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_69940,c_69940,c_69949]) ).
tff(c_70095,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_70088,c_69685]) ).
tff(c_70104,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_70095]) ).
tff(c_70106,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_70052,c_70104]) ).
tff(c_70107,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(X3_8) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_108]) ).
tff(c_70285,plain,
! [X7_524,X5_525] :
( ( inverse(multiply(X7_524,inverse(X5_525))) != inverse(X5_525) )
| ( multiply(X7_524,inverse(X5_525)) != inverse(X7_524) )
| ( multiply(inverse(X5_525),sk_c10) != sk_c11 )
| ( multiply(X5_525,inverse(X5_525)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_70107]) ).
tff(c_70298,plain,
! [X7_524] :
( ( inverse(multiply(X7_524,sk_c8)) != inverse(sk_c5) )
| ( multiply(X7_524,inverse(sk_c5)) != inverse(X7_524) )
| ( multiply(inverse(sk_c5),sk_c10) != sk_c11 )
| ( multiply(sk_c5,inverse(sk_c5)) != sk_c11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_69498,c_70285]) ).
tff(c_70315,plain,
! [X7_524] :
( ( inverse(multiply(X7_524,sk_c8)) != sk_c8 )
| ( multiply(X7_524,sk_c8) != inverse(X7_524) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_69567,c_69498,c_69603,c_69498,c_69498,c_69498,c_70298]) ).
tff(c_70978,plain,
! [X7_532] :
( ( inverse(multiply(X7_532,identity)) != identity )
| ( multiply(X7_532,identity) != inverse(X7_532) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_70834,c_70834,c_70834,c_70315]) ).
tff(c_70986,plain,
( ( inverse(identity) != identity )
| ( multiply(inverse(identity),identity) != inverse(inverse(identity)) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_70978]) ).
tff(c_70994,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_70874,c_70874,c_4,c_70874,c_70986]) ).
tff(c_70995,plain,
! [X2_11,X1_10,X4_13,X3_8] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X3_8) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_70107]) ).
tff(c_71279,plain,
! [X3_538] :
( ( inverse(X3_538) != sk_c10 )
| ( multiply(X3_538,sk_c10) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_70995]) ).
tff(c_71299,plain,
( ( inverse(sk_c4) != sk_c10 )
| ( sk_c9 != sk_c11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_69596,c_71279]) ).
tff(c_71315,plain,
sk_c9 != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_69507,c_71299]) ).
tff(c_71428,plain,
! [X_540,Z_541] : ( multiply(inverse(X_540),multiply(X_540,Z_541)) = Z_541 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69671]) ).
tff(c_71485,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_70174,c_71428]) ).
tff(c_71552,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_71485]) ).
tff(c_70108,plain,
multiply(sk_c10,sk_c11) = sk_c9,
inference(splitRight,[status(thm)],[c_108]) ).
tff(c_71572,plain,
multiply(identity,sk_c11) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_71552,c_70108]) ).
tff(c_71580,plain,
sk_c9 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71572]) ).
tff(c_71582,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_71315,c_71580]) ).
tff(c_71583,plain,
! [X4_13,X1_10,X2_11] :
( ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_70995]) ).
tff(c_71828,plain,
! [X2_545] :
( ( inverse(X2_545) != sk_c10 )
| ( multiply(X2_545,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_71583]) ).
tff(c_71854,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69596,c_71828]) ).
tff(c_71869,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_69507,c_71854]) ).
tff(c_71870,plain,
! [X1_10,X4_13] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_71583]) ).
tff(c_72033,plain,
! [X4_547] :
( ( inverse(X4_547) != sk_c9 )
| ( multiply(X4_547,sk_c9) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_71870]) ).
tff(c_72061,plain,
( ( inverse(identity) != sk_c9 )
| ( sk_c9 != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_72033]) ).
tff(c_72080,plain,
sk_c9 != sk_c10,
inference(splitLeft,[status(thm)],[c_72061]) ).
tff(c_71003,plain,
! [Z_533] : ( multiply(sk_c8,multiply(sk_c6,Z_533)) = Z_533 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69659]) ).
tff(c_71021,plain,
multiply(sk_c8,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_69553,c_71003]) ).
tff(c_71033,plain,
! [Z_534] : ( multiply(sk_c8,multiply(sk_c10,Z_534)) = multiply(sk_c11,Z_534) ),
inference(superposition,[status(thm),theory(equality)],[c_69603,c_69623]) ).
tff(c_71054,plain,
multiply(sk_c8,identity) = multiply(sk_c11,sk_c4),
inference(superposition,[status(thm),theory(equality)],[c_69511,c_71033]) ).
tff(c_71059,plain,
multiply(sk_c11,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_71021,c_71054]) ).
tff(c_71671,plain,
! [Z_543] : ( multiply(sk_c3,multiply(sk_c11,Z_543)) = multiply(sk_c10,Z_543) ),
inference(superposition,[status(thm),theory(equality)],[c_69577,c_69623]) ).
tff(c_71689,plain,
multiply(sk_c3,sk_c7) = multiply(sk_c10,sk_c4),
inference(superposition,[status(thm),theory(equality)],[c_71059,c_71671]) ).
tff(c_71703,plain,
multiply(sk_c3,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69511,c_71689]) ).
tff(c_69680,plain,
! [Z_508] : ( multiply(sk_c11,multiply(sk_c3,Z_508)) = Z_508 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69656]) ).
tff(c_71740,plain,
multiply(sk_c11,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_71703,c_69680]) ).
tff(c_69647,plain,
! [Z_508] : ( multiply(sk_c3,multiply(sk_c11,Z_508)) = multiply(sk_c10,Z_508) ),
inference(superposition,[status(thm),theory(equality)],[c_69577,c_69623]) ).
tff(c_71973,plain,
multiply(sk_c3,sk_c7) = multiply(sk_c10,identity),
inference(superposition,[status(thm),theory(equality)],[c_71740,c_69647]) ).
tff(c_71979,plain,
multiply(sk_c10,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71703,c_71973]) ).
tff(c_72099,plain,
! [Z_5] : ( multiply(sk_c10,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_71979,c_6]) ).
tff(c_72112,plain,
! [Z_548] : ( multiply(sk_c10,Z_548) = Z_548 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_72099]) ).
tff(c_69662,plain,
! [Z_508] : ( multiply(sk_c10,multiply(sk_c4,Z_508)) = multiply(identity,Z_508) ),
inference(superposition,[status(thm),theory(equality)],[c_69511,c_69623]) ).
tff(c_70116,plain,
! [Z_518] : ( multiply(sk_c10,multiply(sk_c4,Z_518)) = Z_518 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69662]) ).
tff(c_70128,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69596,c_70116]) ).
tff(c_72122,plain,
sk_c9 = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_72112,c_70128]) ).
tff(c_72146,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72080,c_72122]) ).
tff(c_72148,plain,
sk_c9 = sk_c10,
inference(splitRight,[status(thm)],[c_72061]) ).
tff(c_72057,plain,
( ( inverse(inverse(sk_c9)) != sk_c9 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_72033]) ).
tff(c_72226,plain,
( ( inverse(inverse(sk_c10)) != sk_c10 )
| ( sk_c10 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_72148,c_72148,c_72057]) ).
tff(c_72227,plain,
sk_c10 != identity,
inference(splitLeft,[status(thm)],[c_72226]) ).
tff(c_71692,plain,
multiply(sk_c3,sk_c11) = multiply(sk_c10,sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_70174,c_71671]) ).
tff(c_71704,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69577,c_71692]) ).
tff(c_72334,plain,
! [X_551,Z_552] : ( multiply(inverse(X_551),multiply(X_551,Z_552)) = Z_552 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69671]) ).
tff(c_72400,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_71704,c_72334]) ).
tff(c_72488,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_72400]) ).
tff(c_72490,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72227,c_72488]) ).
tff(c_72492,plain,
sk_c10 = identity,
inference(splitRight,[status(thm)],[c_72226]) ).
tff(c_72147,plain,
inverse(identity) != sk_c9,
inference(splitRight,[status(thm)],[c_72061]) ).
tff(c_72178,plain,
inverse(identity) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_72148,c_72147]) ).
tff(c_72497,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_72492,c_72178]) ).
tff(c_72509,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_72492,c_69511]) ).
tff(c_72565,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_72509,c_2]) ).
tff(c_72510,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_72492,c_69507]) ).
tff(c_72574,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_72565,c_72510]) ).
tff(c_72578,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72497,c_72574]) ).
tff(c_72661,plain,
! [X1_553] :
( ( inverse(X1_553) != sk_c11 )
| ( multiply(X1_553,sk_c11) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_71870]) ).
tff(c_72681,plain,
inverse(sk_c3) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_69577,c_72661]) ).
tff(c_72695,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_69533,c_72681]) ).
tff(c_72697,plain,
inverse(sk_c2) != sk_c9,
inference(splitRight,[status(thm)],[c_102]) ).
tff(c_90,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_72709,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_72697,c_90]) ).
tff(c_88,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_72810,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_72697,c_88]) ).
tff(c_72713,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_72709,c_4]) ).
tff(c_72833,plain,
! [X_554,Y_555,Z_556] : ( multiply(multiply(X_554,Y_555),Z_556) = multiply(X_554,multiply(Y_555,Z_556)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_72875,plain,
! [Z_556] : ( multiply(sk_c11,multiply(sk_c3,Z_556)) = multiply(identity,Z_556) ),
inference(superposition,[status(thm),theory(equality)],[c_72713,c_72833]) ).
tff(c_74236,plain,
! [Z_581] : ( multiply(sk_c11,multiply(sk_c3,Z_581)) = Z_581 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72875]) ).
tff(c_74248,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_72810,c_74236]) ).
tff(c_100,plain,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_203]) ).
tff(c_72801,plain,
multiply(sk_c8,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_72697,c_100]) ).
tff(c_96,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_72775,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_72697,c_96]) ).
tff(c_73415,plain,
! [Z_566] : ( multiply(sk_c5,multiply(sk_c8,Z_566)) = multiply(sk_c11,Z_566) ),
inference(superposition,[status(thm),theory(equality)],[c_72775,c_72833]) ).
tff(c_73427,plain,
multiply(sk_c5,sk_c11) = multiply(sk_c11,sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_72801,c_73415]) ).
tff(c_74760,plain,
multiply(sk_c5,sk_c11) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_74248,c_73427]) ).
tff(c_98,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_72733,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_72697,c_98]) ).
tff(c_72737,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_72733,c_4]) ).
tff(c_72869,plain,
! [Z_556] : ( multiply(sk_c8,multiply(sk_c5,Z_556)) = multiply(identity,Z_556) ),
inference(superposition,[status(thm),theory(equality)],[c_72737,c_72833]) ).
tff(c_72891,plain,
! [Z_556] : ( multiply(sk_c8,multiply(sk_c5,Z_556)) = Z_556 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72869]) ).
tff(c_74764,plain,
multiply(sk_c8,sk_c11) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_74760,c_72891]) ).
tff(c_74134,plain,
! [Z_579] : ( multiply(sk_c8,multiply(sk_c5,Z_579)) = Z_579 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72869]) ).
tff(c_74155,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_72775,c_74134]) ).
tff(c_74771,plain,
sk_c8 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_74764,c_74155]) ).
tff(c_106,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_212]) ).
tff(c_72794,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_72697,c_106]) ).
tff(c_72696,plain,
inverse(sk_c7) = sk_c6,
inference(splitRight,[status(thm)],[c_102]) ).
tff(c_72701,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_72696,c_4]) ).
tff(c_72878,plain,
! [Z_556] : ( multiply(sk_c6,multiply(sk_c7,Z_556)) = multiply(identity,Z_556) ),
inference(superposition,[status(thm),theory(equality)],[c_72701,c_72833]) ).
tff(c_73460,plain,
! [Z_568] : ( multiply(sk_c6,multiply(sk_c7,Z_568)) = Z_568 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72878]) ).
tff(c_73472,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_72794,c_73460]) ).
tff(c_104,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_72759,plain,
inverse(sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_72697,c_104]) ).
tff(c_72763,plain,
multiply(sk_c8,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_72759,c_4]) ).
tff(c_74177,plain,
! [Z_580] : ( multiply(sk_c7,multiply(sk_c8,Z_580)) = multiply(sk_c6,Z_580) ),
inference(superposition,[status(thm),theory(equality)],[c_72794,c_72833]) ).
tff(c_74201,plain,
multiply(sk_c7,identity) = multiply(sk_c6,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_72763,c_74177]) ).
tff(c_74209,plain,
multiply(sk_c7,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_73472,c_74201]) ).
tff(c_72894,plain,
! [Z_556] : ( multiply(sk_c6,multiply(sk_c7,Z_556)) = Z_556 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72878]) ).
tff(c_74213,plain,
multiply(sk_c6,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_74209,c_72894]) ).
tff(c_74907,plain,
multiply(sk_c6,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74771,c_74213]) ).
tff(c_74192,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c6,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_74155,c_74177]) ).
tff(c_74208,plain,
multiply(sk_c6,sk_c11) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_72794,c_74192]) ).
tff(c_74971,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74907,c_74208]) ).
tff(c_74985,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74971,c_72701]) ).
tff(c_75012,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_74985,c_2]) ).
tff(c_74986,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74971,c_72696]) ).
tff(c_75021,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_75012,c_74986]) ).
tff(c_94,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_72741,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_72697,c_94]) ).
tff(c_92,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_72781,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_72697,c_92]) ).
tff(c_74277,plain,
multiply(sk_c5,sk_c11) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_74248,c_73427]) ).
tff(c_74281,plain,
multiply(sk_c8,sk_c11) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_74277,c_72891]) ).
tff(c_74330,plain,
sk_c8 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_74281,c_74155]) ).
tff(c_74348,plain,
multiply(sk_c6,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74330,c_74213]) ).
tff(c_74452,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74348,c_74208]) ).
tff(c_74352,plain,
multiply(sk_c6,sk_c6) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_74330,c_73472]) ).
tff(c_74464,plain,
multiply(identity,identity) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_74452,c_74452,c_74352]) ).
tff(c_74469,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_74464]) ).
tff(c_73492,plain,
! [Z_569] : ( multiply(sk_c8,multiply(sk_c5,Z_569)) = Z_569 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72869]) ).
tff(c_73513,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_72775,c_73492]) ).
tff(c_73535,plain,
! [Z_570] : ( multiply(sk_c7,multiply(sk_c8,Z_570)) = multiply(sk_c6,Z_570) ),
inference(superposition,[status(thm),theory(equality)],[c_72794,c_72833]) ).
tff(c_73550,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c6,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_73513,c_73535]) ).
tff(c_73566,plain,
multiply(sk_c6,sk_c11) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_72794,c_73550]) ).
tff(c_72881,plain,
! [X_2,Z_556] : ( multiply(inverse(X_2),multiply(X_2,Z_556)) = multiply(identity,Z_556) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_72833]) ).
tff(c_73770,plain,
! [X_575,Z_576] : ( multiply(inverse(X_575),multiply(X_575,Z_576)) = Z_576 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72881]) ).
tff(c_73806,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_73566,c_73770]) ).
tff(c_73861,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_73806]) ).
tff(c_73594,plain,
! [Z_571] : ( multiply(sk_c11,multiply(sk_c3,Z_571)) = Z_571 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72875]) ).
tff(c_73606,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_72810,c_73594]) ).
tff(c_73668,plain,
multiply(sk_c5,sk_c11) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_73606,c_73427]) ).
tff(c_72895,plain,
! [X_2,Z_556] : ( multiply(inverse(X_2),multiply(X_2,Z_556)) = Z_556 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72881]) ).
tff(c_73433,plain,
multiply(sk_c5,identity) = multiply(sk_c11,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_72737,c_73415]) ).
tff(c_73430,plain,
multiply(sk_c5,identity) = multiply(sk_c11,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_72763,c_73415]) ).
tff(c_73651,plain,
multiply(sk_c11,sk_c6) = multiply(sk_c11,sk_c5),
inference(demodulation,[status(thm),theory(equality)],[c_73433,c_73430]) ).
tff(c_73797,plain,
multiply(inverse(sk_c11),multiply(sk_c11,sk_c5)) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_73651,c_73770]) ).
tff(c_73859,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_72895,c_73797]) ).
tff(c_73871,plain,
multiply(sk_c5,sk_c11) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_73859,c_73859,c_73566]) ).
tff(c_73875,plain,
sk_c5 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_73668,c_73871]) ).
tff(c_73922,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_73861,c_73875]) ).
tff(c_73672,plain,
multiply(sk_c8,sk_c11) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_73668,c_72891]) ).
tff(c_73721,plain,
sk_c8 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_73672,c_73513]) ).
tff(c_73751,plain,
inverse(sk_c5) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_73721,c_72733]) ).
tff(c_74007,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_73922,c_73861,c_73751]) ).
tff(c_73923,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_73861,c_73721]) ).
tff(c_73004,plain,
! [X_561,Z_562] : ( multiply(inverse(X_561),multiply(X_561,Z_562)) = Z_562 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72881]) ).
tff(c_73061,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_72775,c_73004]) ).
tff(c_73116,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_72733,c_73061]) ).
tff(c_73201,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_73116,c_72895]) ).
tff(c_73207,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_73201]) ).
tff(c_72898,plain,
! [Z_557] : ( multiply(sk_c11,multiply(sk_c3,Z_557)) = Z_557 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72875]) ).
tff(c_72910,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_72810,c_72898]) ).
tff(c_73040,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_72910,c_73004]) ).
tff(c_73112,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_73040]) ).
tff(c_72897,plain,
multiply(sk_c10,sk_c11) != sk_c9,
inference(splitLeft,[status(thm)],[c_108]) ).
tff(c_73125,plain,
multiply(identity,sk_c11) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_73112,c_72897]) ).
tff(c_73136,plain,
sk_c9 != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_73125]) ).
tff(c_73210,plain,
sk_c9 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_73207,c_73136]) ).
tff(c_73058,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_72781,c_73004]) ).
tff(c_73115,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_72741,c_73058]) ).
tff(c_73404,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_73112,c_2,c_73112,c_73115]) ).
tff(c_73405,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_73210,c_73404]) ).
tff(c_73406,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(X3_8) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_108]) ).
tff(c_73617,plain,
! [X7_572,X5_573] :
( ( inverse(multiply(X7_572,inverse(X5_573))) != inverse(X5_573) )
| ( multiply(X7_572,inverse(X5_573)) != inverse(X7_572) )
| ( multiply(inverse(X5_573),sk_c10) != sk_c11 )
| ( multiply(X5_573,inverse(X5_573)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_73406]) ).
tff(c_73626,plain,
! [X7_572] :
( ( inverse(multiply(X7_572,sk_c8)) != inverse(sk_c5) )
| ( multiply(X7_572,inverse(sk_c5)) != inverse(X7_572) )
| ( multiply(inverse(sk_c5),sk_c10) != sk_c11 )
| ( multiply(sk_c5,inverse(sk_c5)) != sk_c11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_72733,c_73617]) ).
tff(c_73644,plain,
! [X7_572] :
( ( inverse(multiply(X7_572,sk_c8)) != sk_c8 )
| ( multiply(X7_572,sk_c8) != inverse(X7_572) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_72775,c_72733,c_72801,c_72733,c_72733,c_72733,c_73626]) ).
tff(c_74116,plain,
! [X7_578] :
( ( inverse(multiply(X7_578,identity)) != identity )
| ( multiply(X7_578,identity) != inverse(X7_578) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_73923,c_73923,c_73923,c_73644]) ).
tff(c_74124,plain,
( ( inverse(identity) != identity )
| ( multiply(inverse(identity),identity) != inverse(inverse(identity)) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_74116]) ).
tff(c_74132,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_74007,c_74007,c_4,c_74007,c_74124]) ).
tff(c_74133,plain,
! [X2_11,X1_10,X4_13,X3_8] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X3_8) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_73406]) ).
tff(c_74375,plain,
! [X3_583] :
( ( inverse(X3_583) != sk_c10 )
| ( multiply(X3_583,sk_c10) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_74133]) ).
tff(c_74390,plain,
( ( inverse(identity) != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_74375]) ).
tff(c_74474,plain,
sk_c11 != sk_c10,
inference(splitLeft,[status(thm)],[c_74390]) ).
tff(c_74475,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_74469,c_74474]) ).
tff(c_74488,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74469,c_72713]) ).
tff(c_74572,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_74488,c_2]) ).
tff(c_74487,plain,
multiply(sk_c3,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_74469,c_72810]) ).
tff(c_74639,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_74572,c_74487]) ).
tff(c_74640,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74475,c_74639]) ).
tff(c_74642,plain,
sk_c11 = sk_c10,
inference(splitRight,[status(thm)],[c_74390]) ).
tff(c_74674,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74469,c_74642]) ).
tff(c_74641,plain,
inverse(identity) != sk_c10,
inference(splitRight,[status(thm)],[c_74390]) ).
tff(c_74708,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_74674,c_74641]) ).
tff(c_74656,plain,
inverse(sk_c3) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_74642,c_72709]) ).
tff(c_74700,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74674,c_74656]) ).
tff(c_74704,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_74700,c_4]) ).
tff(c_74729,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_74704,c_2]) ).
tff(c_74738,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_74729,c_74700]) ).
tff(c_74741,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74708,c_74738]) ).
tff(c_74742,plain,
! [X4_13,X1_10,X2_11] :
( ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_74133]) ).
tff(c_74881,plain,
! [X2_586] :
( ( inverse(X2_586) != sk_c10 )
| ( multiply(X2_586,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_74742]) ).
tff(c_74891,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_72781,c_74881]) ).
tff(c_74903,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_72741,c_74891]) ).
tff(c_74904,plain,
! [X1_10,X4_13] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_74742]) ).
tff(c_75068,plain,
! [X4_587] :
( ( inverse(X4_587) != sk_c9 )
| ( multiply(X4_587,sk_c9) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_74904]) ).
tff(c_75079,plain,
( ( inverse(inverse(sk_c9)) != sk_c9 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_75068]) ).
tff(c_75106,plain,
sk_c10 != identity,
inference(splitLeft,[status(thm)],[c_75079]) ).
tff(c_74908,plain,
multiply(sk_c7,identity) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_74771,c_74209]) ).
tff(c_75022,plain,
multiply(identity,identity) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_75012,c_74908]) ).
tff(c_75024,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_75022]) ).
tff(c_75040,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_75024,c_72713]) ).
tff(c_75113,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_75040,c_2]) ).
tff(c_75039,plain,
multiply(sk_c3,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_75024,c_72810]) ).
tff(c_75132,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_75113,c_75039]) ).
tff(c_75133,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_75106,c_75132]) ).
tff(c_75135,plain,
sk_c10 = identity,
inference(splitRight,[status(thm)],[c_75079]) ).
tff(c_72745,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_72741,c_4]) ).
tff(c_72866,plain,
! [Z_556] : ( multiply(sk_c10,multiply(sk_c4,Z_556)) = multiply(identity,Z_556) ),
inference(superposition,[status(thm),theory(equality)],[c_72745,c_72833]) ).
tff(c_73437,plain,
! [Z_567] : ( multiply(sk_c10,multiply(sk_c4,Z_567)) = Z_567 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72866]) ).
tff(c_73449,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_72781,c_73437]) ).
tff(c_75084,plain,
inverse(sk_c10) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_73449,c_75068]) ).
tff(c_75136,plain,
inverse(identity) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_75135,c_75084]) ).
tff(c_75145,plain,
sk_c9 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_75021,c_75136]) ).
tff(c_75141,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_75135,c_72745]) ).
tff(c_75170,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_75141,c_2]) ).
tff(c_75140,plain,
multiply(sk_c4,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_75135,c_72781]) ).
tff(c_75187,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_75170,c_75140]) ).
tff(c_75188,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_75145,c_75187]) ).
tff(c_75221,plain,
! [X1_588] :
( ( inverse(X1_588) != sk_c11 )
| ( multiply(X1_588,sk_c11) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_74904]) ).
tff(c_75237,plain,
inverse(sk_c3) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_72810,c_75221]) ).
tff(c_75251,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_72709,c_75237]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : GRP330-1 : TPTP v9.0.0. Released v2.5.0.
% 0.00/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.08/0.29 % Computer : n018.cluster.edu
% 0.08/0.29 % Model : x86_64 x86_64
% 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.29 % Memory : 8042.1875MB
% 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.29 % CPULimit : 300
% 0.08/0.29 % WCLimit : 300
% 0.08/0.29 % DateTime : Mon Apr 7 21:42:32 EDT 2025
% 0.08/0.29 % CPUTime :
% 25.74/11.38 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.13/11.45
% 26.13/11.45 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------