%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP240-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n015.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:39 PM UTC 2025
% Result : Unsatisfiable 17.35s 6.47s
% Output : CNFRefutation 17.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 46
% Syntax : Number of formulae : 766 ( 641 unt; 0 typ; 0 def)
% Number of atoms : 1031 ( 995 equ)
% Maximal formula atoms : 15 ( 1 avg)
% Number of connectives : 544 ( 279 ~; 265 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 326 ( 326 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c10 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c10,type,
sk_c10: $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c9,type,
sk_c9: $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_209,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c7) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c9) = sk_c10 )
| ( inverse(sk_c7) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
( ( multiply(sk_c2,sk_c10) = sk_c3 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_275,axiom,
! [X5,X6,X3,X7,X1,X2,X8,X4] :
( ( inverse(sk_c10) != sk_c9 )
| ( inverse(sk_c9) != sk_c10 )
| ( multiply(X4,sk_c9) != sk_c10 )
| ( inverse(X4) != sk_c9 )
| ( multiply(sk_c10,X5) != sk_c9 )
| ( multiply(X6,sk_c10) != X5 )
| ( inverse(X6) != sk_c10 )
| ( inverse(X1) != sk_c10 )
| ( multiply(X1,sk_c9) != sk_c10 )
| ( multiply(X3,X2) != sk_c9 )
| ( inverse(X3) != X2 )
| ( multiply(X2,sk_c10) != sk_c9 )
| ( multiply(sk_c10,X7) != sk_c9 )
| ( multiply(X8,sk_c10) != X7 )
| ( inverse(X8) != sk_c10 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_206,axiom,
( ( multiply(sk_c2,sk_c10) = sk_c3 )
| ( inverse(sk_c7) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_182,axiom,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ( inverse(sk_c7) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_179,axiom,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_197,axiom,
( ( multiply(sk_c2,sk_c10) = sk_c3 )
| ( multiply(sk_c6,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_176,axiom,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_200,axiom,
( ( multiply(sk_c2,sk_c10) = sk_c3 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c5,sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c9) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c6,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c5,sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c9) = sk_c10 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c7) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_227,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_230,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c7) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_224,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_212,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c6,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c5,sk_c6) = 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_39013,plain,
! [X_478,Y_479,Z_480] : ( multiply(multiply(X_478,Y_479),Z_480) = multiply(X_478,multiply(Y_479,Z_480)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_39058,plain,
! [X_2,Z_480] : ( multiply(inverse(X_2),multiply(X_2,Z_480)) = multiply(identity,Z_480) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39013]) ).
tff(c_39071,plain,
! [X_2,Z_480] : ( multiply(inverse(X_2),multiply(X_2,Z_480)) = Z_480 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39058]) ).
tff(c_39136,plain,
! [X_482,Z_483] : ( multiply(inverse(X_482),multiply(X_482,Z_483)) = Z_483 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39058]) ).
tff(c_39497,plain,
! [X_486,Z_487] : ( multiply(inverse(inverse(X_486)),Z_487) = multiply(X_486,Z_487) ),
inference(superposition,[status(thm),theory(equality)],[c_39071,c_39136]) ).
tff(c_39190,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39136]) ).
tff(c_39504,plain,
! [X_486] : ( multiply(X_486,identity) = X_486 ),
inference(superposition,[status(thm),theory(equality)],[c_39497,c_39190]) ).
tff(c_104,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_137,plain,
inverse(sk_c2) = sk_c10,
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_141,plain,
multiply(sk_c10,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_137,c_4]) ).
tff(c_22,plain,
( ( inverse(sk_c7) = sk_c10 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_34105,plain,
inverse(sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_34109,plain,
multiply(sk_c9,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34105,c_4]) ).
tff(c_34198,plain,
! [X_389,Y_390,Z_391] : ( multiply(multiply(X_389,Y_390),Z_391) = multiply(X_389,multiply(Y_390,Z_391)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_34231,plain,
! [Z_391] : ( multiply(sk_c9,multiply(sk_c10,Z_391)) = multiply(identity,Z_391) ),
inference(superposition,[status(thm),theory(equality)],[c_34109,c_34198]) ).
tff(c_34847,plain,
! [Z_402] : ( multiply(sk_c9,multiply(sk_c10,Z_402)) = Z_402 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34231]) ).
tff(c_34871,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_34847]) ).
tff(c_38,plain,
( ( inverse(sk_c7) = sk_c10 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_34080,plain,
inverse(sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_34085,plain,
multiply(sk_c10,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34080,c_4]) ).
tff(c_34868,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_34085,c_34847]) ).
tff(c_35039,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_34871,c_34868]) ).
tff(c_35047,plain,
inverse(sk_c10) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_35039,c_34105]) ).
tff(c_35060,plain,
multiply(sk_c2,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_35047,c_4]) ).
tff(c_35040,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_35039,c_34871]) ).
tff(c_18,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_33117,plain,
inverse(sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_33121,plain,
multiply(sk_c9,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33117,c_4]) ).
tff(c_33190,plain,
! [X_369,Y_370,Z_371] : ( multiply(multiply(X_369,Y_370),Z_371) = multiply(X_369,multiply(Y_370,Z_371)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33220,plain,
! [Z_371] : ( multiply(sk_c9,multiply(sk_c10,Z_371)) = multiply(identity,Z_371) ),
inference(superposition,[status(thm),theory(equality)],[c_33121,c_33190]) ).
tff(c_33254,plain,
! [Z_372] : ( multiply(sk_c9,multiply(sk_c10,Z_372)) = Z_372 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33220]) ).
tff(c_33275,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_33254]) ).
tff(c_62,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_149,plain,
inverse(sk_c1) = sk_c9,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_153,plain,
multiply(sk_c9,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_149,c_4]) ).
tff(c_163,plain,
inverse(sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_167,plain,
multiply(sk_c10,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_163,c_4]) ).
tff(c_31960,plain,
! [X_345,Y_346,Z_347] : ( multiply(multiply(X_345,Y_346),Z_347) = multiply(X_345,multiply(Y_346,Z_347)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_32002,plain,
! [Z_347] : ( multiply(sk_c10,multiply(sk_c9,Z_347)) = multiply(identity,Z_347) ),
inference(superposition,[status(thm),theory(equality)],[c_167,c_31960]) ).
tff(c_32396,plain,
! [Z_357] : ( multiply(sk_c10,multiply(sk_c9,Z_357)) = Z_357 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32002]) ).
tff(c_32414,plain,
multiply(sk_c10,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_153,c_32396]) ).
tff(c_175,plain,
inverse(sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_179,plain,
multiply(sk_c9,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_175,c_4]) ).
tff(c_32411,plain,
multiply(sk_c10,identity) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_179,c_32396]) ).
tff(c_32426,plain,
sk_c10 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_32414,c_32411]) ).
tff(c_32452,plain,
inverse(sk_c9) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_32426,c_163]) ).
tff(c_32464,plain,
multiply(sk_c1,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_32452,c_4]) ).
tff(c_21333,plain,
! [X_207,Y_208,Z_209] : ( multiply(multiply(X_207,Y_208),Z_209) = multiply(X_207,multiply(Y_208,Z_209)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_21387,plain,
! [X_2,Z_209] : ( multiply(inverse(X_2),multiply(X_2,Z_209)) = multiply(identity,Z_209) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_21333]) ).
tff(c_21402,plain,
! [X_2,Z_209] : ( multiply(inverse(X_2),multiply(X_2,Z_209)) = Z_209 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21387]) ).
tff(c_23624,plain,
! [X_249,Z_250] : ( multiply(inverse(X_249),multiply(X_249,Z_250)) = Z_250 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21387]) ).
tff(c_24090,plain,
! [X_256,Z_257] : ( multiply(inverse(inverse(X_256)),Z_257) = multiply(X_256,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_21402,c_23624]) ).
tff(c_24128,plain,
! [X_256] : ( multiply(X_256,inverse(X_256)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_24090]) ).
tff(c_21375,plain,
! [Z_209] : ( multiply(sk_c9,multiply(sk_c10,Z_209)) = multiply(identity,Z_209) ),
inference(superposition,[status(thm),theory(equality)],[c_179,c_21333]) ).
tff(c_21708,plain,
! [Z_215] : ( multiply(sk_c9,multiply(sk_c10,Z_215)) = Z_215 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21375]) ).
tff(c_21732,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_21708]) ).
tff(c_21729,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_167,c_21708]) ).
tff(c_21744,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21732,c_21729]) ).
tff(c_22179,plain,
multiply(sk_c2,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_179]) ).
tff(c_22171,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_21732]) ).
tff(c_22180,plain,
inverse(sk_c10) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_175]) ).
tff(c_20220,plain,
! [X_190,Y_191,Z_192] : ( multiply(multiply(X_190,Y_191),Z_192) = multiply(X_190,multiply(Y_191,Z_192)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20262,plain,
! [Z_192] : ( multiply(sk_c9,multiply(sk_c10,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_179,c_20220]) ).
tff(c_20291,plain,
! [Z_193] : ( multiply(sk_c9,multiply(sk_c10,Z_193)) = Z_193 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20262]) ).
tff(c_20318,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_20291]) ).
tff(c_20315,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_167,c_20291]) ).
tff(c_20340,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_20318,c_20315]) ).
tff(c_20359,plain,
inverse(sk_c10) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_20340,c_175]) ).
tff(c_20373,plain,
multiply(sk_c2,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20359,c_4]) ).
tff(c_18724,plain,
! [X_169,Y_170,Z_171] : ( multiply(multiply(X_169,Y_170),Z_171) = multiply(X_169,multiply(Y_170,Z_171)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_18769,plain,
! [Z_171] : ( multiply(sk_c9,multiply(sk_c10,Z_171)) = multiply(identity,Z_171) ),
inference(superposition,[status(thm),theory(equality)],[c_179,c_18724]) ).
tff(c_19128,plain,
! [Z_177] : ( multiply(sk_c9,multiply(sk_c10,Z_177)) = Z_177 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18769]) ).
tff(c_19155,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_19128]) ).
tff(c_19152,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_167,c_19128]) ).
tff(c_19175,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19155,c_19152]) ).
tff(c_19193,plain,
multiply(sk_c2,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19175,c_179]) ).
tff(c_88,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_200,plain,
multiply(sk_c2,sk_c10) = sk_c3,
inference(splitLeft,[status(thm)],[c_88]) ).
tff(c_19233,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19193,c_200]) ).
tff(c_72,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_193,plain,
multiply(sk_c10,sk_c3) = sk_c9,
inference(splitLeft,[status(thm)],[c_72]) ).
tff(c_19149,plain,
multiply(sk_c9,sk_c9) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_193,c_19128]) ).
tff(c_19185,plain,
multiply(sk_c2,sk_c2) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_19175,c_19175,c_19149]) ).
tff(c_19306,plain,
multiply(sk_c2,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19233,c_19185]) ).
tff(c_19184,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19175,c_19155]) ).
tff(c_249,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_285,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_249]) ).
tff(c_405,plain,
! [X_20,Z_21] : ( multiply(inverse(X_20),multiply(X_20,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_285]) ).
tff(c_297,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_285]) ).
tff(c_559,plain,
! [X_23,Z_24] : ( multiply(inverse(inverse(X_23)),Z_24) = multiply(X_23,Z_24) ),
inference(superposition,[status(thm),theory(equality)],[c_405,c_297]) ).
tff(c_444,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_405]) ).
tff(c_566,plain,
! [X_23] : ( multiply(X_23,identity) = X_23 ),
inference(superposition,[status(thm),theory(equality)],[c_559,c_444]) ).
tff(c_273,plain,
! [Z_18] : ( multiply(sk_c9,multiply(sk_c10,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_179,c_249]) ).
tff(c_299,plain,
! [Z_19] : ( multiply(sk_c9,multiply(sk_c10,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_273]) ).
tff(c_317,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_299]) ).
tff(c_314,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_167,c_299]) ).
tff(c_336,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_317,c_314]) ).
tff(c_351,plain,
inverse(sk_c10) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_336,c_175]) ).
tff(c_371,plain,
multiply(sk_c2,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_351,c_4]) ).
tff(c_355,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_336,c_149]) ).
tff(c_46,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_208,plain,
multiply(sk_c1,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_348,plain,
multiply(sk_c1,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_336,c_208]) ).
tff(c_469,plain,
multiply(inverse(sk_c1),sk_c10) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_348,c_297]) ).
tff(c_475,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_371,c_355,c_469]) ).
tff(c_392,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_355,c_4]) ).
tff(c_491,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_475,c_392]) ).
tff(c_480,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_475,c_355]) ).
tff(c_500,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_491,c_480]) ).
tff(c_485,plain,
inverse(identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_475,c_137]) ).
tff(c_513,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_500,c_485]) ).
tff(c_597,plain,
! [X_23] : ( multiply(X_23,inverse(X_23)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_559]) ).
tff(c_120,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c9 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c9 )
| ( multiply(X1_10,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c9 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(sk_c9) != sk_c10 )
| ( inverse(sk_c10) != sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_275]) ).
tff(c_363,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c2 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c2 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c2 )
| ( multiply(X1_10,sk_c2) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c2 )
| ( inverse(X4_13) != sk_c2 )
| ( multiply(X4_13,sk_c2) != sk_c10 )
| ( inverse(sk_c10) != sk_c2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_336,c_137,c_336,c_336,c_336,c_336,c_336,c_336,c_336,c_336,c_120]) ).
tff(c_364,plain,
inverse(sk_c10) != sk_c2,
inference(splitLeft,[status(thm)],[c_363]) ).
tff(c_365,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_351]) ).
tff(c_366,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(X4_13) != sk_c2 )
| ( multiply(X4_13,sk_c2) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c2 )
| ( multiply(X1_10,sk_c2) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c2 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c2 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c2 ) ),
inference(splitRight,[status(thm)],[c_363]) ).
tff(c_9107,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(X4_13) != identity )
| ( identity != X4_13 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( identity != X1_10 )
| ( inverse(X1_10) != identity )
| ( inverse(X3_8) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_566,c_513,c_2,c_513,c_475,c_513,c_597,c_475,c_566,c_513,c_475,c_513,c_566,c_513,c_475,c_566,c_513,c_2,c_513,c_475,c_513,c_566,c_513,c_475,c_475,c_366]) ).
tff(c_9109,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9107]) ).
tff(c_9111,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9109,c_500]) ).
tff(c_9112,plain,
! [X3_8,X4_13,X6_7,X1_10] :
( ( inverse(X3_8) != identity )
| ( inverse(X4_13) != identity )
| ( identity != X4_13 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( identity != X1_10 )
| ( inverse(X1_10) != identity ) ),
inference(splitRight,[status(thm)],[c_9107]) ).
tff(c_17793,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9112]) ).
tff(c_17795,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17793,c_500]) ).
tff(c_17796,plain,
! [X6_7,X4_13,X3_8] :
( ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X4_13) != identity )
| ( identity != X4_13 )
| ( inverse(X3_8) != identity ) ),
inference(splitRight,[status(thm)],[c_9112]) ).
tff(c_17797,plain,
! [X3_8] : ( inverse(X3_8) != identity ),
inference(splitLeft,[status(thm)],[c_17796]) ).
tff(c_17799,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17797,c_500]) ).
tff(c_17800,plain,
! [X6_7,X4_13] :
( ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X4_13) != identity )
| ( identity != X4_13 ) ),
inference(splitRight,[status(thm)],[c_17796]) ).
tff(c_18626,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_17800]) ).
tff(c_18628,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18626,c_500]) ).
tff(c_18630,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_17800]) ).
tff(c_18632,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18630,c_500]) ).
tff(c_18634,plain,
multiply(sk_c1,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_40,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_18642,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_18634,c_40]) ).
tff(c_18646,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18642,c_4]) ).
tff(c_19146,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_18646,c_19128]) ).
tff(c_19322,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19184,c_19175,c_19146]) ).
tff(c_42,plain,
( ( multiply(sk_c4,sk_c9) = sk_c10 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_18706,plain,
multiply(sk_c4,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_18634,c_42]) ).
tff(c_19189,plain,
multiply(sk_c4,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_19175,c_18706]) ).
tff(c_19448,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19306,c_19322,c_19189]) ).
tff(c_19192,plain,
multiply(sk_c10,sk_c3) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19175,c_193]) ).
tff(c_19434,plain,
multiply(sk_c10,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19233,c_19192]) ).
tff(c_19449,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19448,c_19434]) ).
tff(c_19457,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19449]) ).
tff(c_19198,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19175,c_149]) ).
tff(c_19469,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19457,c_19198]) ).
tff(c_19509,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_19469,c_4]) ).
tff(c_18781,plain,
! [X_2,Z_171] : ( multiply(inverse(X_2),multiply(X_2,Z_171)) = multiply(identity,Z_171) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18724]) ).
tff(c_18796,plain,
! [X_2,Z_171] : ( multiply(inverse(X_2),multiply(X_2,Z_171)) = Z_171 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18781]) ).
tff(c_19517,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_19509,c_18796]) ).
tff(c_19529,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19517]) ).
tff(c_19191,plain,
multiply(sk_c1,sk_c2) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_19175,c_18634]) ).
tff(c_19451,plain,
multiply(sk_c1,sk_c2) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_19448,c_19191]) ).
tff(c_19546,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19529,c_19457,c_19451]) ).
tff(c_19548,plain,
multiply(sk_c2,sk_c10) != sk_c3,
inference(splitRight,[status(thm)],[c_88]) ).
tff(c_20377,plain,
sk_c3 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20373,c_19548]) ).
tff(c_20349,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_20340,c_20318]) ).
tff(c_102,plain,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_206]) ).
tff(c_20154,plain,
inverse(sk_c7) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_19548,c_102]) ).
tff(c_20158,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20154,c_4]) ).
tff(c_20274,plain,
! [X_2,Z_192] : ( multiply(inverse(X_2),multiply(X_2,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20220]) ).
tff(c_20469,plain,
! [X_195,Z_196] : ( multiply(inverse(X_195),multiply(X_195,Z_196)) = Z_196 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20274]) ).
tff(c_20514,plain,
multiply(inverse(sk_c10),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20158,c_20469]) ).
tff(c_20551,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_20349,c_20359,c_20514]) ).
tff(c_20312,plain,
multiply(sk_c9,sk_c9) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_193,c_20291]) ).
tff(c_20350,plain,
multiply(sk_c2,sk_c2) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_20340,c_20340,c_20312]) ).
tff(c_19646,plain,
! [X_182,Y_183,Z_184] : ( multiply(multiply(X_182,Y_183),Z_184) = multiply(X_182,multiply(Y_183,Z_184)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_19691,plain,
! [Z_184] : ( multiply(sk_c9,multiply(sk_c10,Z_184)) = multiply(identity,Z_184) ),
inference(superposition,[status(thm),theory(equality)],[c_179,c_19646]) ).
tff(c_19720,plain,
! [Z_185] : ( multiply(sk_c9,multiply(sk_c10,Z_185)) = Z_185 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19691]) ).
tff(c_19747,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_19720]) ).
tff(c_19744,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_167,c_19720]) ).
tff(c_19906,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19747,c_19744]) ).
tff(c_19917,plain,
multiply(sk_c2,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19906,c_179]) ).
tff(c_19945,plain,
sk_c3 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_19917,c_19548]) ).
tff(c_19922,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_19906,c_149]) ).
tff(c_19563,plain,
multiply(sk_c1,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_19915,plain,
multiply(sk_c1,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_19906,c_19563]) ).
tff(c_19703,plain,
! [X_2,Z_184] : ( multiply(inverse(X_2),multiply(X_2,Z_184)) = multiply(identity,Z_184) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_19646]) ).
tff(c_19999,plain,
! [X_188,Z_189] : ( multiply(inverse(X_188),multiply(X_188,Z_189)) = Z_189 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19703]) ).
tff(c_20026,plain,
multiply(inverse(sk_c1),sk_c10) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_19915,c_19999]) ).
tff(c_20084,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19917,c_19922,c_20026]) ).
tff(c_19741,plain,
multiply(sk_c9,sk_c9) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_193,c_19720]) ).
tff(c_19907,plain,
multiply(sk_c2,sk_c2) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_19906,c_19906,c_19741]) ).
tff(c_20119,plain,
multiply(identity,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_20084,c_20084,c_19907]) ).
tff(c_20129,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20119]) ).
tff(c_20131,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19945,c_20129]) ).
tff(c_20133,plain,
multiply(sk_c1,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_50,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_20199,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_20133,c_50]) ).
tff(c_20303,plain,
multiply(sk_c9,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_20199,c_20291]) ).
tff(c_20450,plain,
sk_c8 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_20350,c_20340,c_20340,c_20303]) ).
tff(c_52,plain,
( ( multiply(sk_c7,sk_c10) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_20188,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20133,c_52]) ).
tff(c_20451,plain,
multiply(sk_c7,sk_c10) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_20450,c_20188]) ).
tff(c_20634,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_20373,c_20551,c_20451]) ).
tff(c_20635,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20377,c_20634]) ).
tff(c_20637,plain,
multiply(sk_c10,sk_c3) != sk_c9,
inference(splitRight,[status(thm)],[c_72]) ).
tff(c_86,plain,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_20672,plain,
inverse(sk_c7) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_20637,c_86]) ).
tff(c_20676,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20672,c_4]) ).
tff(c_23660,plain,
multiply(inverse(sk_c10),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20676,c_23624]) ).
tff(c_23694,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_22171,c_22180,c_23660]) ).
tff(c_84,plain,
( ( multiply(sk_c7,sk_c10) = sk_c8 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_21303,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20637,c_84]) ).
tff(c_23697,plain,
multiply(sk_c2,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_23694,c_21303]) ).
tff(c_23700,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22179,c_23697]) ).
tff(c_23657,plain,
multiply(inverse(sk_c7),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_21303,c_23624]) ).
tff(c_23693,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20672,c_23657]) ).
tff(c_23720,plain,
multiply(sk_c10,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_23700,c_23693]) ).
tff(c_20743,plain,
! [X_198,Y_199,Z_200] : ( multiply(multiply(X_198,Y_199),Z_200) = multiply(X_198,multiply(Y_199,Z_200)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20788,plain,
! [Z_200] : ( multiply(sk_c9,multiply(sk_c10,Z_200)) = multiply(identity,Z_200) ),
inference(superposition,[status(thm),theory(equality)],[c_179,c_20743]) ).
tff(c_20817,plain,
! [Z_201] : ( multiply(sk_c9,multiply(sk_c10,Z_201)) = Z_201 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20788]) ).
tff(c_20841,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_20817]) ).
tff(c_20838,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_167,c_20817]) ).
tff(c_21103,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_20841,c_20838]) ).
tff(c_21120,plain,
multiply(sk_c2,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21103,c_179]) ).
tff(c_96,plain,
( ( multiply(sk_c6,sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c10) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_20707,plain,
multiply(sk_c2,sk_c10) = sk_c3,
inference(splitLeft,[status(thm)],[c_96]) ).
tff(c_21148,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21120,c_20707]) ).
tff(c_21119,plain,
multiply(sk_c10,sk_c3) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21103,c_20637]) ).
tff(c_21291,plain,
multiply(sk_c10,identity) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21148,c_21119]) ).
tff(c_21112,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21103,c_20841]) ).
tff(c_20832,plain,
multiply(sk_c9,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20676,c_20817]) ).
tff(c_21193,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21112,c_21103,c_20832]) ).
tff(c_20718,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20637,c_84]) ).
tff(c_21194,plain,
multiply(sk_c2,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_21193,c_20718]) ).
tff(c_21197,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21120,c_21194]) ).
tff(c_82,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_20737,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_20637,c_82]) ).
tff(c_21114,plain,
multiply(sk_c10,sk_c8) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21103,c_20737]) ).
tff(c_21293,plain,
multiply(sk_c10,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21197,c_21114]) ).
tff(c_21294,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21291,c_21293]) ).
tff(c_21296,plain,
multiply(sk_c2,sk_c10) != sk_c3,
inference(splitRight,[status(thm)],[c_96]) ).
tff(c_98,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c2,sk_c10) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_21324,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_21296,c_98]) ).
tff(c_22173,plain,
multiply(sk_c10,sk_c8) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_21324]) ).
tff(c_23743,plain,
sk_c2 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_23720,c_23700,c_22173]) ).
tff(c_23754,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_23743,c_137]) ).
tff(c_22184,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_149]) ).
tff(c_22201,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22184,c_4]) ).
tff(c_23799,plain,
multiply(sk_c10,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23743,c_22201]) ).
tff(c_23803,plain,
multiply(inverse(sk_c10),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_23799,c_21402]) ).
tff(c_23809,plain,
sk_c10 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_23720,c_23754,c_23803]) ).
tff(c_20636,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_72]) ).
tff(c_20641,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20636,c_4]) ).
tff(c_23672,plain,
multiply(inverse(sk_c10),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_20641,c_23624]) ).
tff(c_23695,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_22171,c_22180,c_23672]) ).
tff(c_23746,plain,
sk_c4 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_23743,c_23695]) ).
tff(c_23816,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_23809,c_23746]) ).
tff(c_23752,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_23743,c_21744]) ).
tff(c_23815,plain,
sk_c9 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_23809,c_23752]) ).
tff(c_21726,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_20641,c_21708]) ).
tff(c_23909,plain,
multiply(sk_c1,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_23816,c_23815,c_21726]) ).
tff(c_23795,plain,
multiply(sk_c10,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23754,c_4]) ).
tff(c_23878,plain,
multiply(sk_c1,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23809,c_23809,c_23795]) ).
tff(c_74,plain,
( ( multiply(sk_c4,sk_c9) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_21311,plain,
multiply(sk_c4,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_20637,c_74]) ).
tff(c_21354,plain,
! [Z_209] : ( multiply(sk_c4,multiply(sk_c9,Z_209)) = multiply(sk_c10,Z_209) ),
inference(superposition,[status(thm),theory(equality)],[c_21311,c_21333]) ).
tff(c_23839,plain,
! [Z_209] : ( multiply(sk_c1,multiply(sk_c1,Z_209)) = multiply(sk_c1,Z_209) ),
inference(demodulation,[status(thm),theory(equality)],[c_23816,c_23815,c_23809,c_21354]) ).
tff(c_23913,plain,
multiply(sk_c1,sk_c1) = multiply(sk_c1,identity),
inference(superposition,[status(thm),theory(equality)],[c_23909,c_23839]) ).
tff(c_23922,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23909,c_23878,c_23913]) ).
tff(c_23817,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_23809,c_23743]) ).
tff(c_23931,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23922,c_23817]) ).
tff(c_23684,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_23624]) ).
tff(c_24097,plain,
! [X_256] : ( multiply(X_256,identity) = X_256 ),
inference(superposition,[status(thm),theory(equality)],[c_24090,c_23684]) ).
tff(c_23935,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23922,c_23809]) ).
tff(c_22271,plain,
! [X_222,Z_223] : ( multiply(inverse(X_222),multiply(X_222,Z_223)) = Z_223 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21387]) ).
tff(c_22623,plain,
! [X_227,Z_228] : ( multiply(inverse(inverse(X_227)),Z_228) = multiply(X_227,Z_228) ),
inference(superposition,[status(thm),theory(equality)],[c_21402,c_22271]) ).
tff(c_22331,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_22271]) ).
tff(c_22630,plain,
! [X_227] : ( multiply(X_227,identity) = X_227 ),
inference(superposition,[status(thm),theory(equality)],[c_22623,c_22331]) ).
tff(c_20699,plain,
multiply(sk_c1,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_22177,plain,
multiply(sk_c1,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_20699]) ).
tff(c_22368,plain,
multiply(inverse(sk_c1),sk_c10) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_22177,c_21402]) ).
tff(c_22374,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22179,c_22184,c_22368]) ).
tff(c_22386,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22374,c_22184]) ).
tff(c_22415,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22386,c_4]) ).
tff(c_22474,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_22415,c_21402]) ).
tff(c_22486,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22474]) ).
tff(c_22491,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22486,c_22386]) ).
tff(c_22390,plain,
inverse(identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22374,c_137]) ).
tff(c_22500,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22491,c_22390]) ).
tff(c_21763,plain,
inverse(sk_c10) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_175]) ).
tff(c_21777,plain,
multiply(sk_c2,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21763,c_4]) ).
tff(c_21754,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_21732]) ).
tff(c_21723,plain,
multiply(sk_c9,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20676,c_21708]) ).
tff(c_21847,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21754,c_21744,c_21723]) ).
tff(c_21848,plain,
multiply(sk_c2,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_21847,c_21303]) ).
tff(c_21851,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21777,c_21848]) ).
tff(c_21720,plain,
multiply(sk_c9,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_21324,c_21708]) ).
tff(c_21879,plain,
multiply(sk_c2,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21851,c_21744,c_21744,c_21720]) ).
tff(c_21899,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21754,c_21744,c_21726]) ).
tff(c_21758,plain,
multiply(sk_c4,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_21311]) ).
tff(c_21900,plain,
multiply(sk_c2,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_21899,c_21758]) ).
tff(c_21903,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21879,c_21900]) ).
tff(c_21756,plain,
multiply(sk_c10,sk_c8) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_21324]) ).
tff(c_21863,plain,
multiply(sk_c10,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21851,c_21756]) ).
tff(c_21985,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21903,c_21863]) ).
tff(c_21993,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21985]) ).
tff(c_21990,plain,
inverse(identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21903,c_21763]) ).
tff(c_22075,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21993,c_21990]) ).
tff(c_21407,plain,
! [Z_210] : ( multiply(sk_c9,multiply(sk_c10,Z_210)) = Z_210 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21375]) ).
tff(c_21431,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_21407]) ).
tff(c_21428,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_167,c_21407]) ).
tff(c_21443,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21431,c_21428]) ).
tff(c_21491,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_21443,c_149]) ).
tff(c_21484,plain,
multiply(sk_c1,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_21443,c_20699]) ).
tff(c_21405,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c9 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c9 )
| ( multiply(X1_10,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c9 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_175,c_163,c_120]) ).
tff(c_21406,plain,
! [X4_13] :
( ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_21405]) ).
tff(c_21529,plain,
! [X4_13] :
( ( inverse(X4_13) != sk_c2 )
| ( multiply(X4_13,sk_c2) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21443,c_21443,c_21406]) ).
tff(c_21696,plain,
inverse(sk_c1) != sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_21484,c_21529]) ).
tff(c_21706,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21491,c_21696]) ).
tff(c_21707,plain,
! [X6_7,X1_10,X3_8,X8_12] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c9 )
| ( multiply(X1_10,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c9 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c9 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_21405]) ).
tff(c_21753,plain,
! [X8_12] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_21707]) ).
tff(c_21815,plain,
! [X8_216] :
( ( inverse(X8_216) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_216,sk_c10)) != sk_c2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_21753]) ).
tff(c_21833,plain,
( ( inverse(identity) != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_21815]) ).
tff(c_22169,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21993,c_21903,c_2,c_21903,c_22075,c_21903,c_21833]) ).
tff(c_22170,plain,
! [X3_8,X1_10,X6_7] :
( ( multiply(inverse(X3_8),sk_c10) != sk_c9 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c9 )
| ( multiply(X1_10,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_21707]) ).
tff(c_22222,plain,
! [X3_8,X1_10,X6_7] :
( ( multiply(inverse(X3_8),sk_c10) != sk_c2 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c2 )
| ( multiply(X1_10,sk_c2) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21744,c_21744,c_21744,c_21744,c_22170]) ).
tff(c_22223,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c2 ) ),
inference(splitLeft,[status(thm)],[c_22222]) ).
tff(c_23620,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_22630,c_22500,c_2,c_22500,c_22374,c_22500,c_22223]) ).
tff(c_23622,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23620,c_22491]) ).
tff(c_23623,plain,
! [X1_10,X3_8] :
( ( multiply(X1_10,sk_c2) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c2 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c2 ) ),
inference(splitRight,[status(thm)],[c_22222]) ).
tff(c_31911,plain,
! [X1_10,X3_8] :
( ( identity != X1_10 )
| ( inverse(X1_10) != identity )
| ( inverse(X3_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_24128,c_23931,c_24097,c_23935,c_23931,c_23935,c_24097,c_23935,c_23931,c_23623]) ).
tff(c_31912,plain,
! [X3_8] : ( inverse(X3_8) != identity ),
inference(splitLeft,[status(thm)],[c_31911]) ).
tff(c_23751,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_23743,c_22180]) ).
tff(c_23865,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_23809,c_23809,c_23751]) ).
tff(c_23929,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23922,c_23922,c_23865]) ).
tff(c_31914,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31912,c_23929]) ).
tff(c_31916,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_31911]) ).
tff(c_31918,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31916,c_23929]) ).
tff(c_31920,plain,
multiply(sk_c1,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_32441,plain,
multiply(sk_c1,sk_c9) != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_32426,c_31920]) ).
tff(c_32575,plain,
sk_c1 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_32464,c_32441]) ).
tff(c_78,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_20649,plain,
inverse(sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_20637,c_78]) ).
tff(c_44,plain,
( ( multiply(sk_c5,sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_31930,plain,
multiply(sk_c5,sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_31920,c_44]) ).
tff(c_32011,plain,
! [X_2,Z_347] : ( multiply(inverse(X_2),multiply(X_2,Z_347)) = multiply(identity,Z_347) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_31960]) ).
tff(c_32587,plain,
! [X_359,Z_360] : ( multiply(inverse(X_359),multiply(X_359,Z_360)) = Z_360 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32011]) ).
tff(c_32644,plain,
multiply(inverse(sk_c5),sk_c9) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_31930,c_32587]) ).
tff(c_32673,plain,
multiply(sk_c6,sk_c9) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20649,c_32644]) ).
tff(c_32026,plain,
! [X_2,Z_347] : ( multiply(inverse(X_2),multiply(X_2,Z_347)) = Z_347 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32011]) ).
tff(c_32679,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_32673,c_32026]) ).
tff(c_32685,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_32679]) ).
tff(c_32697,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_32685,c_153]) ).
tff(c_32746,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_32697,c_32026]) ).
tff(c_32758,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_32746]) ).
tff(c_32760,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32575,c_32758]) ).
tff(c_32762,plain,
inverse(sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_20,plain,
( ( multiply(sk_c7,sk_c10) = sk_c8 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_32838,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_32762,c_20]) ).
tff(c_32761,plain,
inverse(sk_c7) = sk_c10,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_32766,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_32761,c_4]) ).
tff(c_32866,plain,
! [X_361,Y_362,Z_363] : ( multiply(multiply(X_361,Y_362),Z_363) = multiply(X_361,multiply(Y_362,Z_363)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_32902,plain,
! [Z_363] : ( multiply(sk_c10,multiply(sk_c7,Z_363)) = multiply(identity,Z_363) ),
inference(superposition,[status(thm),theory(equality)],[c_32766,c_32866]) ).
tff(c_32983,plain,
! [Z_367] : ( multiply(sk_c10,multiply(sk_c7,Z_367)) = Z_367 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32902]) ).
tff(c_32995,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_32838,c_32983]) ).
tff(c_32822,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_32762,c_18]) ).
tff(c_33001,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_32995,c_32822]) ).
tff(c_33014,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33001,c_32762]) ).
tff(c_33016,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33001,c_163]) ).
tff(c_33072,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33014,c_33016]) ).
tff(c_33073,plain,
inverse(sk_c7) = sk_c10,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_33078,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33073,c_4]) ).
tff(c_33272,plain,
multiply(sk_c9,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33078,c_33254]) ).
tff(c_33306,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_33275,c_33272]) ).
tff(c_33074,plain,
inverse(sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_36,plain,
( ( multiply(sk_c7,sk_c10) = sk_c8 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_33130,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_33074,c_36]) ).
tff(c_33307,plain,
multiply(sk_c2,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_33306,c_33130]) ).
tff(c_33235,plain,
! [Z_371] : ( multiply(sk_c10,multiply(sk_c2,Z_371)) = multiply(identity,Z_371) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_33190]) ).
tff(c_33359,plain,
! [Z_374] : ( multiply(sk_c10,multiply(sk_c2,Z_374)) = Z_374 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33235]) ).
tff(c_33377,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_33307,c_33359]) ).
tff(c_34,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_33138,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_33074,c_34]) ).
tff(c_33384,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33377,c_33138]) ).
tff(c_33404,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33384,c_33117]) ).
tff(c_33405,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33384,c_33074]) ).
tff(c_33485,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_33404,c_33405]) ).
tff(c_33487,plain,
inverse(sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_33493,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_33487,c_20]) ).
tff(c_33554,plain,
! [X_377,Y_378,Z_379] : ( multiply(multiply(X_377,Y_378),Z_379) = multiply(X_377,multiply(Y_378,Z_379)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33590,plain,
! [Z_379] : ( multiply(sk_c10,multiply(sk_c7,Z_379)) = multiply(identity,Z_379) ),
inference(superposition,[status(thm),theory(equality)],[c_33078,c_33554]) ).
tff(c_33720,plain,
! [Z_385] : ( multiply(sk_c10,multiply(sk_c7,Z_385)) = Z_385 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33590]) ).
tff(c_33738,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_33493,c_33720]) ).
tff(c_33486,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_33742,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33738,c_33486]) ).
tff(c_10,plain,
( ( multiply(sk_c4,sk_c9) = sk_c10 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_33527,plain,
multiply(sk_c4,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_33487,c_10]) ).
tff(c_24,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_33100,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_33074,c_24]) ).
tff(c_33104,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33100,c_4]) ).
tff(c_33584,plain,
! [Z_379] : ( multiply(sk_c10,multiply(sk_c4,Z_379)) = multiply(identity,Z_379) ),
inference(superposition,[status(thm),theory(equality)],[c_33104,c_33554]) ).
tff(c_33663,plain,
! [Z_383] : ( multiply(sk_c10,multiply(sk_c4,Z_383)) = Z_383 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33584]) ).
tff(c_33675,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_33527,c_33663]) ).
tff(c_33754,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33742,c_33675]) ).
tff(c_33599,plain,
! [X_2,Z_379] : ( multiply(inverse(X_2),multiply(X_2,Z_379)) = multiply(identity,Z_379) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_33554]) ).
tff(c_33612,plain,
! [X_2,Z_379] : ( multiply(inverse(X_2),multiply(X_2,Z_379)) = Z_379 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33599]) ).
tff(c_33924,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_33754,c_33612]) ).
tff(c_33930,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33924]) ).
tff(c_32,plain,
( ( multiply(sk_c6,sk_c10) = sk_c9 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_33513,plain,
multiply(sk_c6,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_33074,c_32]) ).
tff(c_33759,plain,
multiply(sk_c6,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33742,c_33513]) ).
tff(c_12,plain,
( ( multiply(sk_c5,sk_c6) = sk_c9 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_33522,plain,
multiply(sk_c5,sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_33487,c_12]) ).
tff(c_30,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_33086,plain,
inverse(sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_33074,c_30]) ).
tff(c_33090,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33086,c_4]) ).
tff(c_33587,plain,
! [Z_379] : ( multiply(sk_c6,multiply(sk_c5,Z_379)) = multiply(identity,Z_379) ),
inference(superposition,[status(thm),theory(equality)],[c_33090,c_33554]) ).
tff(c_33640,plain,
! [Z_382] : ( multiply(sk_c6,multiply(sk_c5,Z_382)) = Z_382 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33587]) ).
tff(c_33652,plain,
multiply(sk_c6,sk_c9) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_33522,c_33640]) ).
tff(c_33755,plain,
multiply(sk_c6,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33742,c_33652]) ).
tff(c_33902,plain,
sk_c6 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33759,c_33755]) ).
tff(c_33906,plain,
inverse(sk_c5) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33902,c_33086]) ).
tff(c_33917,plain,
multiply(sk_c10,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33906,c_4]) ).
tff(c_34017,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33930,c_33917]) ).
tff(c_33987,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33930,c_33906]) ).
tff(c_34022,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34017,c_33987]) ).
tff(c_33760,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_33742,c_33487]) ).
tff(c_33992,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_33930,c_33930,c_33760]) ).
tff(c_34066,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34022,c_33992]) ).
tff(c_34068,plain,
inverse(sk_c1) != sk_c9,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_70,plain,
( ( inverse(sk_c7) = sk_c10 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_34122,plain,
inverse(sk_c7) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_34068,c_70]) ).
tff(c_34126,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34122,c_4]) ).
tff(c_34862,plain,
multiply(sk_c9,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34126,c_34847]) ).
tff(c_36955,plain,
multiply(sk_c2,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35039,c_34862]) ).
tff(c_36993,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_35040,c_36955]) ).
tff(c_68,plain,
( ( multiply(sk_c7,sk_c10) = sk_c8 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_34177,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_34068,c_68]) ).
tff(c_37002,plain,
multiply(sk_c2,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_36993,c_34177]) ).
tff(c_37005,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35060,c_37002]) ).
tff(c_56,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_34093,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_34068,c_56]) ).
tff(c_34097,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34093,c_4]) ).
tff(c_34865,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_34097,c_34847]) ).
tff(c_35028,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_34871,c_34865]) ).
tff(c_58,plain,
( ( multiply(sk_c4,sk_c9) = sk_c10 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_34142,plain,
multiply(sk_c4,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_34068,c_58]) ).
tff(c_35030,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_35028,c_34142]) ).
tff(c_35064,plain,
multiply(sk_c2,sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_35039,c_35030]) ).
tff(c_66,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_34158,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_34068,c_66]) ).
tff(c_34859,plain,
multiply(sk_c9,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_34158,c_34847]) ).
tff(c_35041,plain,
multiply(sk_c2,sk_c2) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_35039,c_35039,c_34859]) ).
tff(c_37081,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37005,c_35064,c_35041]) ).
tff(c_34246,plain,
! [X_2,Z_391] : ( multiply(inverse(X_2),multiply(X_2,Z_391)) = multiply(identity,Z_391) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34198]) ).
tff(c_34260,plain,
! [X_2,Z_391] : ( multiply(inverse(X_2),multiply(X_2,Z_391)) = Z_391 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34246]) ).
tff(c_37018,plain,
! [X_439,Z_440] : ( multiply(inverse(X_439),multiply(X_439,Z_440)) = Z_440 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34246]) ).
tff(c_37295,plain,
! [X_442,Z_443] : ( multiply(inverse(inverse(X_442)),Z_443) = multiply(X_442,Z_443) ),
inference(superposition,[status(thm),theory(equality)],[c_34260,c_37018]) ).
tff(c_37069,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_37018]) ).
tff(c_37302,plain,
! [X_442] : ( multiply(X_442,identity) = X_442 ),
inference(superposition,[status(thm),theory(equality)],[c_37295,c_37069]) ).
tff(c_37085,plain,
inverse(identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_37081,c_35047]) ).
tff(c_37098,plain,
multiply(sk_c2,identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37085,c_4]) ).
tff(c_37113,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37098,c_35040]) ).
tff(c_35137,plain,
! [X_405,Z_406] : ( multiply(inverse(X_405),multiply(X_405,Z_406)) = Z_406 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34246]) ).
tff(c_35433,plain,
! [X_409,Z_410] : ( multiply(inverse(inverse(X_409)),Z_410) = multiply(X_409,Z_410) ),
inference(superposition,[status(thm),theory(equality)],[c_34260,c_35137]) ).
tff(c_35471,plain,
! [X_409] : ( multiply(X_409,inverse(X_409)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_35433]) ).
tff(c_35074,plain,
multiply(sk_c2,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35039,c_34862]) ).
tff(c_35112,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_35040,c_35074]) ).
tff(c_35121,plain,
multiply(sk_c2,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_35112,c_34177]) ).
tff(c_35124,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35060,c_35121]) ).
tff(c_35200,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35124,c_35064,c_35041]) ).
tff(c_35204,plain,
inverse(identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_35200,c_35047]) ).
tff(c_35217,plain,
multiply(sk_c2,identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_35204,c_4]) ).
tff(c_35232,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35217,c_35040]) ).
tff(c_35188,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_35137]) ).
tff(c_35440,plain,
! [X_409] : ( multiply(X_409,identity) = X_409 ),
inference(superposition,[status(thm),theory(equality)],[c_35433,c_35188]) ).
tff(c_34891,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_34871,c_34868]) ).
tff(c_34896,plain,
multiply(sk_c10,sk_c8) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_34891,c_34158]) ).
tff(c_34925,plain,
multiply(sk_c2,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34891,c_34862]) ).
tff(c_34934,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34925,c_34891,c_34865]) ).
tff(c_34936,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_34934,c_34177]) ).
tff(c_34649,plain,
! [Z_399] : ( multiply(sk_c9,multiply(sk_c10,Z_399)) = Z_399 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34231]) ).
tff(c_34673,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_34649]) ).
tff(c_34670,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_34085,c_34649]) ).
tff(c_34720,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_34673,c_34670]) ).
tff(c_34733,plain,
multiply(sk_c10,sk_c8) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_34720,c_34158]) ).
tff(c_34667,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_34097,c_34649]) ).
tff(c_34754,plain,
multiply(sk_c2,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34720,c_34667]) ).
tff(c_34664,plain,
multiply(sk_c9,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34126,c_34649]) ).
tff(c_34784,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34754,c_34720,c_34664]) ).
tff(c_34786,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_34784,c_34177]) ).
tff(c_34263,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c9 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c9 )
| ( multiply(X1_10,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c9 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(X4_13,sk_c9) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34105,c_34080,c_120]) ).
tff(c_34339,plain,
! [X4_395] :
( ( inverse(X4_395) != sk_c9 )
| ( multiply(X4_395,sk_c9) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_34263]) ).
tff(c_34359,plain,
( ( inverse(inverse(sk_c9)) != sk_c9 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34339]) ).
tff(c_34370,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_34105,c_34080,c_34359]) ).
tff(c_34301,plain,
! [Z_394] : ( multiply(sk_c9,multiply(sk_c10,Z_394)) = Z_394 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34231]) ).
tff(c_34322,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_34097,c_34301]) ).
tff(c_34325,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_34085,c_34301]) ).
tff(c_34397,plain,
sk_c9 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34322,c_34325]) ).
tff(c_34328,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_34301]) ).
tff(c_34483,plain,
multiply(sk_c4,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_34397,c_34328]) ).
tff(c_34398,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34397,c_34322]) ).
tff(c_34513,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_34483,c_34398]) ).
tff(c_34409,plain,
inverse(sk_c10) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34397,c_34105]) ).
tff(c_34479,plain,
multiply(sk_c4,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34409,c_4]) ).
tff(c_34319,plain,
multiply(sk_c9,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34126,c_34301]) ).
tff(c_34379,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_34322,c_34319]) ).
tff(c_34388,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_34379,c_34177]) ).
tff(c_34508,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34479,c_34388]) ).
tff(c_34316,plain,
multiply(sk_c9,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_34158,c_34301]) ).
tff(c_34401,plain,
multiply(sk_c4,sk_c4) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_34397,c_34397,c_34316]) ).
tff(c_34570,plain,
multiply(sk_c2,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34513,c_34513,c_34508,c_34401]) ).
tff(c_34407,plain,
multiply(sk_c4,sk_c4) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_34397,c_34142]) ).
tff(c_34645,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34570,c_34513,c_34513,c_34407]) ).
tff(c_34646,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34370,c_34645]) ).
tff(c_34647,plain,
! [X6_7,X1_10,X3_8,X8_12] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c9 )
| ( multiply(X1_10,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c9 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c9 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_34263]) ).
tff(c_34648,plain,
! [X8_12] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_34647]) ).
tff(c_34763,plain,
! [X8_12] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34720,c_34648]) ).
tff(c_34837,plain,
( ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_34786,c_34763]) ).
tff(c_34845,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34733,c_34093,c_34837]) ).
tff(c_34846,plain,
! [X3_8,X1_10,X6_7] :
( ( multiply(inverse(X3_8),sk_c10) != sk_c9 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c9 )
| ( multiply(X1_10,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_34647]) ).
tff(c_34882,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_34846]) ).
tff(c_34953,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34891,c_34882]) ).
tff(c_34984,plain,
( ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_34936,c_34953]) ).
tff(c_34992,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34896,c_34093,c_34984]) ).
tff(c_34993,plain,
! [X1_10,X3_8] :
( ( multiply(X1_10,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c9 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c9 ) ),
inference(splitRight,[status(thm)],[c_34846]) ).
tff(c_35072,plain,
! [X1_10,X3_8] :
( ( multiply(X1_10,sk_c2) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c2 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35039,c_35039,c_35039,c_34993]) ).
tff(c_35073,plain,
! [X3_8] :
( ( multiply(inverse(X3_8),sk_c10) != sk_c2 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c2 ) ),
inference(splitLeft,[status(thm)],[c_35072]) ).
tff(c_36951,plain,
! [X3_8] : ( inverse(X3_8) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_35471,c_35232,c_35440,c_35232,c_35200,c_35073]) ).
tff(c_35206,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35200,c_137]) ).
tff(c_35246,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35232,c_35206]) ).
tff(c_36953,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_36951,c_35246]) ).
tff(c_36954,plain,
! [X1_10] :
( ( multiply(X1_10,sk_c2) != sk_c10 )
| ( inverse(X1_10) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_35072]) ).
tff(c_37555,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_37081,c_37302,c_37113,c_37081,c_36954]) ).
tff(c_37087,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37081,c_137]) ).
tff(c_37127,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37113,c_37087]) ).
tff(c_37557,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37555,c_37127]) ).
tff(c_37559,plain,
inverse(sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_37580,plain,
multiply(sk_c5,sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_37559,c_12]) ).
tff(c_34067,plain,
inverse(sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_34072,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34067,c_4]) ).
tff(c_37649,plain,
! [X_449,Y_450,Z_451] : ( multiply(multiply(X_449,Y_450),Z_451) = multiply(X_449,multiply(Y_450,Z_451)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_37688,plain,
! [Z_451] : ( multiply(sk_c6,multiply(sk_c5,Z_451)) = multiply(identity,Z_451) ),
inference(superposition,[status(thm),theory(equality)],[c_34072,c_37649]) ).
tff(c_37732,plain,
! [Z_453] : ( multiply(sk_c6,multiply(sk_c5,Z_453)) = Z_453 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37688]) ).
tff(c_37744,plain,
multiply(sk_c6,sk_c9) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_37580,c_37732]) ).
tff(c_37694,plain,
! [X_2,Z_451] : ( multiply(inverse(X_2),multiply(X_2,Z_451)) = multiply(identity,Z_451) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_37649]) ).
tff(c_37807,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_37694]) ).
tff(c_37837,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_37744,c_37807]) ).
tff(c_37902,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_37837]) ).
tff(c_37590,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_34068,c_68]) ).
tff(c_37558,plain,
inverse(sk_c7) = sk_c10,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_37563,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37558,c_4]) ).
tff(c_37679,plain,
! [Z_451] : ( multiply(sk_c10,multiply(sk_c7,Z_451)) = multiply(identity,Z_451) ),
inference(superposition,[status(thm),theory(equality)],[c_37563,c_37649]) ).
tff(c_37783,plain,
! [Z_456] : ( multiply(sk_c10,multiply(sk_c7,Z_456)) = Z_456 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37679]) ).
tff(c_37795,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_37590,c_37783]) ).
tff(c_37585,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_37559,c_18]) ).
tff(c_37799,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_37795,c_37585]) ).
tff(c_37925,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37902,c_37799]) ).
tff(c_37919,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_37799,c_34080]) ).
tff(c_37986,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37925,c_37925,c_37919]) ).
tff(c_37917,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_37799,c_37559]) ).
tff(c_38002,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_37986,c_37925,c_37925,c_37917]) ).
tff(c_38004,plain,
inverse(sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_38072,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_38004,c_34]) ).
tff(c_8,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_38016,plain,
inverse(sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_38020,plain,
multiply(sk_c9,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38016,c_4]) ).
tff(c_38119,plain,
! [X_460,Y_461,Z_462] : ( multiply(multiply(X_460,Y_461),Z_462) = multiply(X_460,multiply(Y_461,Z_462)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_38152,plain,
! [Z_462] : ( multiply(sk_c9,multiply(sk_c10,Z_462)) = multiply(identity,Z_462) ),
inference(superposition,[status(thm),theory(equality)],[c_38020,c_38119]) ).
tff(c_38204,plain,
! [Z_464] : ( multiply(sk_c9,multiply(sk_c10,Z_464)) = Z_464 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38152]) ).
tff(c_38231,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_141,c_38204]) ).
tff(c_38003,plain,
inverse(sk_c7) = sk_c10,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_38008,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38003,c_4]) ).
tff(c_38228,plain,
multiply(sk_c9,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_38008,c_38204]) ).
tff(c_38278,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_38231,c_38228]) ).
tff(c_38058,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_38004,c_36]) ).
tff(c_38279,plain,
multiply(sk_c2,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_38278,c_38058]) ).
tff(c_38164,plain,
! [X_2,Z_462] : ( multiply(inverse(X_2),multiply(X_2,Z_462)) = multiply(identity,Z_462) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_38119]) ).
tff(c_38306,plain,
! [X_466,Z_467] : ( multiply(inverse(X_466),multiply(X_466,Z_467)) = Z_467 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38164]) ).
tff(c_38324,plain,
multiply(inverse(sk_c2),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_38279,c_38306]) ).
tff(c_38382,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_38072,c_137,c_38324]) ).
tff(c_38400,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_38382,c_38016]) ).
tff(c_38401,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_38382,c_38004]) ).
tff(c_38435,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_38400,c_38401]) ).
tff(c_38437,plain,
inverse(sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_38468,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_38437,c_20]) ).
tff(c_38537,plain,
! [X_468,Y_469,Z_470] : ( multiply(multiply(X_468,Y_469),Z_470) = multiply(X_468,multiply(Y_469,Z_470)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_38570,plain,
! [Z_470] : ( multiply(sk_c10,multiply(sk_c7,Z_470)) = multiply(identity,Z_470) ),
inference(superposition,[status(thm),theory(equality)],[c_38008,c_38537]) ).
tff(c_38639,plain,
! [Z_473] : ( multiply(sk_c10,multiply(sk_c7,Z_473)) = Z_473 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38570]) ).
tff(c_38651,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_38468,c_38639]) ).
tff(c_38478,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_38437,c_18]) ).
tff(c_38655,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_38651,c_38478]) ).
tff(c_38463,plain,
multiply(sk_c5,sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_38437,c_12]) ).
tff(c_38573,plain,
! [Z_470] : ( multiply(sk_c6,multiply(sk_c5,Z_470)) = multiply(identity,Z_470) ),
inference(superposition,[status(thm),theory(equality)],[c_34072,c_38537]) ).
tff(c_38616,plain,
! [Z_472] : ( multiply(sk_c6,multiply(sk_c5,Z_472)) = Z_472 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38573]) ).
tff(c_38628,plain,
multiply(sk_c6,sk_c9) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_38463,c_38616]) ).
tff(c_38663,plain,
multiply(sk_c6,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38655,c_38628]) ).
tff(c_38579,plain,
! [X_2,Z_470] : ( multiply(inverse(X_2),multiply(X_2,Z_470)) = multiply(identity,Z_470) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_38537]) ).
tff(c_38591,plain,
! [X_2,Z_470] : ( multiply(inverse(X_2),multiply(X_2,Z_470)) = Z_470 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38579]) ).
tff(c_38792,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_38663,c_38591]) ).
tff(c_38798,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_38792]) ).
tff(c_38669,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_38655,c_38004]) ).
tff(c_38801,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_38798,c_38798,c_38669]) ).
tff(c_38811,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38798,c_137]) ).
tff(c_38843,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38811,c_4]) ).
tff(c_38861,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_38843,c_38591]) ).
tff(c_38873,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_38861]) ).
tff(c_38877,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38873,c_38811]) ).
tff(c_38880,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38801,c_38877]) ).
tff(c_38882,plain,
inverse(sk_c2) != sk_c10,
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_116,plain,
( ( multiply(sk_c7,sk_c10) = sk_c8 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_38954,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_38882,c_116]) ).
tff(c_118,plain,
( ( inverse(sk_c7) = sk_c10 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_230]) ).
tff(c_38915,plain,
inverse(sk_c7) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_38882,c_118]) ).
tff(c_38919,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38915,c_4]) ).
tff(c_39046,plain,
! [Z_480] : ( multiply(sk_c10,multiply(sk_c7,Z_480)) = multiply(identity,Z_480) ),
inference(superposition,[status(thm),theory(equality)],[c_38919,c_39013]) ).
tff(c_39073,plain,
! [Z_481] : ( multiply(sk_c10,multiply(sk_c7,Z_481)) = Z_481 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39046]) ).
tff(c_39085,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_38954,c_39073]) ).
tff(c_114,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_224]) ).
tff(c_38962,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_38882,c_114]) ).
tff(c_39089,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_39085,c_38962]) ).
tff(c_38895,plain,
inverse(sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_39103,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_39089,c_38895]) ).
tff(c_39124,plain,
multiply(sk_c10,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39103,c_4]) ).
tff(c_38881,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_106,plain,
( ( multiply(sk_c4,sk_c9) = sk_c10 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_212]) ).
tff(c_38980,plain,
multiply(sk_c4,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_38882,c_106]) ).
tff(c_39097,plain,
multiply(sk_c4,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_39089,c_38980]) ).
tff(c_39245,plain,
multiply(inverse(sk_c4),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_39097,c_39071]) ).
tff(c_39251,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39124,c_38881,c_39245]) ).
tff(c_39535,plain,
! [X_486] : ( multiply(X_486,inverse(X_486)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39497]) ).
tff(c_39258,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39251,c_39251,c_39103]) ).
tff(c_39108,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c10 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X4_13,sk_c10) != sk_c10 )
| ( inverse(sk_c10) != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_39089,c_39089,c_39089,c_39089,c_39089,c_39089,c_39089,c_39089,c_39089,c_120]) ).
tff(c_39109,plain,
inverse(sk_c10) != sk_c10,
inference(splitLeft,[status(thm)],[c_39108]) ).
tff(c_39118,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_39103,c_39109]) ).
tff(c_39119,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(sk_c10) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X4_13,sk_c10) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(inverse(X3_8),sk_c10) != sk_c10 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_39108]) ).
tff(c_47377,plain,
! [X4_13,X3_8,X8_12,X1_10,X6_7] :
( ( inverse(X4_13) != identity )
| ( identity != X4_13 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( identity != X1_10 )
| ( inverse(X1_10) != identity )
| ( inverse(X3_8) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_39504,c_39251,c_39251,c_2,c_39251,c_39251,c_39535,c_39251,c_39504,c_39251,c_39251,c_39251,c_39504,c_39251,c_39251,c_39504,c_39251,c_39251,c_2,c_39251,c_39251,c_39504,c_39251,c_39251,c_39251,c_39258,c_39251,c_39251,c_39119]) ).
tff(c_47379,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_47377]) ).
tff(c_47381,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_47379,c_39258]) ).
tff(c_47382,plain,
! [X3_8,X4_13,X6_7,X1_10] :
( ( inverse(X3_8) != identity )
| ( inverse(X4_13) != identity )
| ( identity != X4_13 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( identity != X1_10 )
| ( inverse(X1_10) != identity ) ),
inference(splitRight,[status(thm)],[c_47377]) ).
tff(c_55510,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_47382]) ).
tff(c_55512,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_55510,c_39258]) ).
tff(c_55513,plain,
! [X6_7,X4_13,X3_8] :
( ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X4_13) != identity )
| ( identity != X4_13 )
| ( inverse(X3_8) != identity ) ),
inference(splitRight,[status(thm)],[c_47382]) ).
tff(c_55514,plain,
! [X3_8] : ( inverse(X3_8) != identity ),
inference(splitLeft,[status(thm)],[c_55513]) ).
tff(c_55516,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_55514,c_39258]) ).
tff(c_55517,plain,
! [X6_7,X4_13] :
( ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X4_13) != identity )
| ( identity != X4_13 ) ),
inference(splitRight,[status(thm)],[c_55513]) ).
tff(c_56325,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_55517]) ).
tff(c_56327,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56325,c_39258]) ).
tff(c_56329,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_55517]) ).
tff(c_56331,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56329,c_39258]) ).
tff(c_56333,plain,
inverse(sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_56612,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_56333,c_36]) ).
tff(c_56332,plain,
inverse(sk_c7) = sk_c10,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_56337,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_56332,c_4]) ).
tff(c_56680,plain,
! [X_631,Y_632,Z_633] : ( multiply(multiply(X_631,Y_632),Z_633) = multiply(X_631,multiply(Y_632,Z_633)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_56716,plain,
! [Z_633] : ( multiply(sk_c10,multiply(sk_c7,Z_633)) = multiply(identity,Z_633) ),
inference(superposition,[status(thm),theory(equality)],[c_56337,c_56680]) ).
tff(c_56759,plain,
! [Z_635] : ( multiply(sk_c10,multiply(sk_c7,Z_635)) = Z_635 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56716]) ).
tff(c_56771,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_56612,c_56759]) ).
tff(c_56617,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_38882,c_114]) ).
tff(c_56775,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_56771,c_56617]) ).
tff(c_26,plain,
( ( multiply(sk_c4,sk_c9) = sk_c10 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_56650,plain,
multiply(sk_c4,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_56333,c_26]) ).
tff(c_38886,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38881,c_4]) ).
tff(c_56719,plain,
! [Z_633] : ( multiply(sk_c10,multiply(sk_c4,Z_633)) = multiply(identity,Z_633) ),
inference(superposition,[status(thm),theory(equality)],[c_38886,c_56680]) ).
tff(c_56736,plain,
! [Z_634] : ( multiply(sk_c10,multiply(sk_c4,Z_634)) = Z_634 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56719]) ).
tff(c_56748,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_56650,c_56736]) ).
tff(c_56783,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_56775,c_56748]) ).
tff(c_56722,plain,
! [X_2,Z_633] : ( multiply(inverse(X_2),multiply(X_2,Z_633)) = multiply(identity,Z_633) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_56680]) ).
tff(c_56734,plain,
! [X_2,Z_633] : ( multiply(inverse(X_2),multiply(X_2,Z_633)) = Z_633 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56722]) ).
tff(c_56912,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_56783,c_56734]) ).
tff(c_56918,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_56912]) ).
tff(c_56790,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_56775,c_56333]) ).
tff(c_56922,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_56918,c_56918,c_56790]) ).
tff(c_56341,plain,
inverse(sk_c1) = sk_c9,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_56789,plain,
inverse(sk_c1) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_56775,c_56341]) ).
tff(c_56905,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_56789,c_4]) ).
tff(c_56978,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56918,c_56905]) ).
tff(c_56921,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_56918,c_56789]) ).
tff(c_56983,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_56978,c_56921]) ).
tff(c_56984,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56922,c_56983]) ).
tff(c_56986,plain,
inverse(sk_c1) != sk_c9,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_57017,plain,
multiply(sk_c7,sk_c10) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_56986,c_68]) ).
tff(c_57293,plain,
! [X_645,Y_646,Z_647] : ( multiply(multiply(X_645,Y_646),Z_647) = multiply(X_645,multiply(Y_646,Z_647)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_57326,plain,
! [Z_647] : ( multiply(sk_c10,multiply(sk_c7,Z_647)) = multiply(identity,Z_647) ),
inference(superposition,[status(thm),theory(equality)],[c_56337,c_57293]) ).
tff(c_57368,plain,
! [Z_649] : ( multiply(sk_c10,multiply(sk_c7,Z_649)) = Z_649 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_57326]) ).
tff(c_57380,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_57017,c_57368]) ).
tff(c_57101,plain,
! [X_640,Y_641,Z_642] : ( multiply(multiply(X_640,Y_641),Z_642) = multiply(X_640,multiply(Y_641,Z_642)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_57137,plain,
! [Z_642] : ( multiply(sk_c10,multiply(sk_c7,Z_642)) = multiply(identity,Z_642) ),
inference(superposition,[status(thm),theory(equality)],[c_56337,c_57101]) ).
tff(c_57180,plain,
! [Z_644] : ( multiply(sk_c10,multiply(sk_c7,Z_644)) = Z_644 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_57137]) ).
tff(c_57192,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_57017,c_57180]) ).
tff(c_57036,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_56986,c_66]) ).
tff(c_57196,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57192,c_57036]) ).
tff(c_57211,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57196,c_56333]) ).
tff(c_57022,plain,
inverse(sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_57209,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57196,c_57022]) ).
tff(c_57218,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57211,c_57209]) ).
tff(c_57219,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_57384,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57380,c_57219]) ).
tff(c_64,plain,
( ( multiply(sk_c6,sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_57226,plain,
multiply(sk_c6,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_56986,c_64]) ).
tff(c_57395,plain,
multiply(sk_c6,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57384,c_57226]) ).
tff(c_60,plain,
( ( multiply(sk_c5,sk_c6) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_57240,plain,
multiply(sk_c5,sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_56986,c_60]) ).
tff(c_56985,plain,
inverse(sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_56990,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_56985,c_4]) ).
tff(c_57323,plain,
! [Z_647] : ( multiply(sk_c6,multiply(sk_c5,Z_647)) = multiply(identity,Z_647) ),
inference(superposition,[status(thm),theory(equality)],[c_56990,c_57293]) ).
tff(c_57345,plain,
! [Z_648] : ( multiply(sk_c6,multiply(sk_c5,Z_648)) = Z_648 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_57323]) ).
tff(c_57357,plain,
multiply(sk_c6,sk_c9) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_57240,c_57345]) ).
tff(c_57392,plain,
multiply(sk_c6,sk_c10) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_57384,c_57357]) ).
tff(c_57424,plain,
sk_c6 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57395,c_57392]) ).
tff(c_57501,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57424,c_57395]) ).
tff(c_57332,plain,
! [X_2,Z_647] : ( multiply(inverse(X_2),multiply(X_2,Z_647)) = multiply(identity,Z_647) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_57293]) ).
tff(c_57343,plain,
! [X_2,Z_647] : ( multiply(inverse(X_2),multiply(X_2,Z_647)) = Z_647 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_57332]) ).
tff(c_57565,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_57501,c_57343]) ).
tff(c_57571,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_57565]) ).
tff(c_57220,plain,
inverse(sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_57396,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57384,c_57220]) ).
tff(c_57580,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_57571,c_57571,c_57396]) ).
tff(c_57504,plain,
inverse(sk_c5) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_57424,c_56985]) ).
tff(c_57577,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_57571,c_57504]) ).
tff(c_57672,plain,
multiply(identity,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_57577,c_4]) ).
tff(c_57709,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_57672,c_57343]) ).
tff(c_57721,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_57709]) ).
tff(c_57725,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_57721,c_57577]) ).
tff(c_57728,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57580,c_57725]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.15 % Problem : GRP240-1 : TPTP v9.0.0. Released v2.5.0.
% 0.08/0.16 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.16/0.36 % Computer : n015.cluster.edu
% 0.16/0.36 % Model : x86_64 x86_64
% 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.36 % Memory : 8042.1875MB
% 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.36 % CPULimit : 300
% 0.16/0.36 % WCLimit : 300
% 0.16/0.36 % DateTime : Mon Apr 7 21:38:20 EDT 2025
% 0.16/0.36 % CPUTime :
% 17.35/6.47 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.58/6.53
% 17.58/6.53 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------