%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP314-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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:25:54 PM UTC 2025
% Result : Unsatisfiable 45.39s 30.97s
% Output : CNFRefutation 45.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 26
% Syntax : Number of formulae : 997 ( 869 unt; 0 typ; 0 def)
% Number of atoms : 1287 (1223 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 726 ( 436 ~; 290 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 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 : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 443 ( 443 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_63,axiom,
multiply(sk_c7,sk_c8) = sk_c6,
file(unknown,unknown) ).
tff(f_168,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( multiply(X3,sk_c8) != sk_c7 )
| ( inverse(X3) != sk_c8 )
| ( multiply(X4,sk_c7) != sk_c6 )
| ( inverse(X4) != sk_c7 )
| ( multiply(X5,sk_c7) != sk_c8 )
| ( inverse(X5) != sk_c7 )
| ( inverse(X1) != sk_c8 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( inverse(X2) != sk_c7 )
| ( multiply(X2,sk_c6) != sk_c7 ) ),
file(unknown,unknown) ).
tff(f_69,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_78,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_126,axiom,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_114,axiom,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_90,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_108,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_123,axiom,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_120,axiom,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_117,axiom,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_75,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_99,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_93,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_111,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_105,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_102,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_87,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_84,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_81,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_135,axiom,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_132,axiom,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_129,axiom,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_216321,plain,
! [X_1369,Y_1370,Z_1371] : ( multiply(multiply(X_1369,Y_1370),Z_1371) = multiply(X_1369,multiply(Y_1370,Z_1371)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_216351,plain,
! [X_2,Z_1371] : ( multiply(inverse(X_2),multiply(X_2,Z_1371)) = multiply(identity,Z_1371) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_216321]) ).
tff(c_216365,plain,
! [X_2,Z_1371] : ( multiply(inverse(X_2),multiply(X_2,Z_1371)) = Z_1371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216351]) ).
tff(c_217256,plain,
! [X_1391,Z_1392] : ( multiply(inverse(X_1391),multiply(X_1391,Z_1392)) = Z_1392 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216351]) ).
tff(c_218039,plain,
! [X_1406,Z_1407] : ( multiply(inverse(inverse(X_1406)),Z_1407) = multiply(X_1406,Z_1407) ),
inference(superposition,[status(thm),theory(equality)],[c_216365,c_217256]) ).
tff(c_217328,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_217256]) ).
tff(c_218046,plain,
! [X_1406] : ( multiply(X_1406,identity) = X_1406 ),
inference(superposition,[status(thm),theory(equality)],[c_218039,c_217328]) ).
tff(c_192095,plain,
! [X_1164,Y_1165,Z_1166] : ( multiply(multiply(X_1164,Y_1165),Z_1166) = multiply(X_1164,multiply(Y_1165,Z_1166)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_192125,plain,
! [X_2,Z_1166] : ( multiply(inverse(X_2),multiply(X_2,Z_1166)) = multiply(identity,Z_1166) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_192095]) ).
tff(c_193104,plain,
! [X_1186,Z_1187] : ( multiply(inverse(X_1186),multiply(X_1186,Z_1187)) = Z_1187 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192125]) ).
tff(c_192139,plain,
! [X_2,Z_1166] : ( multiply(inverse(X_2),multiply(X_2,Z_1166)) = Z_1166 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192125]) ).
tff(c_193888,plain,
! [X_1200,Z_1201] : ( multiply(inverse(inverse(X_1200)),Z_1201) = multiply(X_1200,Z_1201) ),
inference(superposition,[status(thm),theory(equality)],[c_193104,c_192139]) ).
tff(c_193173,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_193104]) ).
tff(c_193895,plain,
! [X_1200] : ( multiply(X_1200,identity) = X_1200 ),
inference(superposition,[status(thm),theory(equality)],[c_193888,c_193173]) ).
tff(c_193425,plain,
! [X_1190,Z_1191] : ( multiply(inverse(inverse(X_1190)),Z_1191) = multiply(X_1190,Z_1191) ),
inference(superposition,[status(thm),theory(equality)],[c_193104,c_192139]) ).
tff(c_193432,plain,
! [X_1190] : ( multiply(X_1190,identity) = X_1190 ),
inference(superposition,[status(thm),theory(equality)],[c_193425,c_193173]) ).
tff(c_60114,plain,
! [X_652,Y_653,Z_654] : ( multiply(multiply(X_652,Y_653),Z_654) = multiply(X_652,multiply(Y_653,Z_654)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_60144,plain,
! [X_2,Z_654] : ( multiply(inverse(X_2),multiply(X_2,Z_654)) = multiply(identity,Z_654) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_60114]) ).
tff(c_60158,plain,
! [X_2,Z_654] : ( multiply(inverse(X_2),multiply(X_2,Z_654)) = Z_654 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60144]) ).
tff(c_60890,plain,
! [X_671,Z_672] : ( multiply(inverse(X_671),multiply(X_671,Z_672)) = Z_672 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60144]) ).
tff(c_61817,plain,
! [X_688,Z_689] : ( multiply(inverse(inverse(X_688)),Z_689) = multiply(X_688,Z_689) ),
inference(superposition,[status(thm),theory(equality)],[c_60158,c_60890]) ).
tff(c_60959,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_60890]) ).
tff(c_61824,plain,
! [X_688] : ( multiply(X_688,identity) = X_688 ),
inference(superposition,[status(thm),theory(equality)],[c_61817,c_60959]) ).
tff(c_8,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_58,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_168]) ).
tff(c_60,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_58]) ).
tff(c_20023,plain,
! [X3_278] :
( ( inverse(X3_278) != sk_c8 )
| ( multiply(X3_278,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_20037,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20023]) ).
tff(c_20048,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_20037]) ).
tff(c_12,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_12965,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_18,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_89,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_93,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_89,c_4]) ).
tff(c_12983,plain,
! [X_156,Y_157,Z_158] : ( multiply(multiply(X_156,Y_157),Z_158) = multiply(X_156,multiply(Y_157,Z_158)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13019,plain,
! [Z_158] : ( multiply(sk_c8,multiply(sk_c1,Z_158)) = multiply(identity,Z_158) ),
inference(superposition,[status(thm),theory(equality)],[c_93,c_12983]) ).
tff(c_13079,plain,
! [Z_161] : ( multiply(sk_c8,multiply(sk_c1,Z_161)) = Z_161 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13019]) ).
tff(c_13091,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_12965,c_13079]) ).
tff(c_13025,plain,
! [X_2,Z_158] : ( multiply(inverse(X_2),multiply(X_2,Z_158)) = multiply(identity,Z_158) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12983]) ).
tff(c_13380,plain,
! [X_170,Z_171] : ( multiply(inverse(X_170),multiply(X_170,Z_171)) = Z_171 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13025]) ).
tff(c_13425,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13091,c_13380]) ).
tff(c_13498,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13425]) ).
tff(c_50,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_81,plain,
inverse(sk_c3) = sk_c7,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_85,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_81,c_4]) ).
tff(c_13575,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13498,c_85]) ).
tff(c_13041,plain,
! [X_2,Z_158] : ( multiply(inverse(X_2),multiply(X_2,Z_158)) = Z_158 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13025]) ).
tff(c_13735,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_13575,c_13041]) ).
tff(c_13747,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13735]) ).
tff(c_42,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_128,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_150,plain,
! [X_13,Y_14,Z_15] : ( multiply(multiply(X_13,Y_14),Z_15) = multiply(X_13,multiply(Y_14,Z_15)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_180,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c3,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_150]) ).
tff(c_238,plain,
! [Z_18] : ( multiply(sk_c7,multiply(sk_c3,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_180]) ).
tff(c_250,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_128,c_238]) ).
tff(c_254,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_250]) ).
tff(c_26,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_120,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_38,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_106,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_110,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_106,c_4]) ).
tff(c_174,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_110,c_150]) ).
tff(c_199,plain,
! [Z_16] : ( multiply(sk_c7,multiply(sk_c2,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_174]) ).
tff(c_211,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_120,c_199]) ).
tff(c_257,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_254,c_254,c_211]) ).
tff(c_183,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_150]) ).
tff(c_1152,plain,
! [X_35,Z_36] : ( multiply(inverse(X_35),multiply(X_35,Z_36)) = Z_36 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_183]) ).
tff(c_1170,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_257,c_1152]) ).
tff(c_1213,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1170]) ).
tff(c_197,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_183]) ).
tff(c_1476,plain,
! [X_40,Z_41] : ( multiply(inverse(inverse(X_40)),Z_41) = multiply(X_40,Z_41) ),
inference(superposition,[status(thm),theory(equality)],[c_1152,c_197]) ).
tff(c_1206,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1152]) ).
tff(c_1483,plain,
! [X_40] : ( multiply(X_40,identity) = X_40 ),
inference(superposition,[status(thm),theory(equality)],[c_1476,c_1206]) ).
tff(c_266,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_254,c_8]) ).
tff(c_1185,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_266,c_1152]) ).
tff(c_1216,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1185]) ).
tff(c_356,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_183]) ).
tff(c_722,plain,
! [X_25,Z_26] : ( multiply(inverse(inverse(X_25)),Z_26) = multiply(X_25,Z_26) ),
inference(superposition,[status(thm),theory(equality)],[c_197,c_356]) ).
tff(c_413,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_356]) ).
tff(c_729,plain,
! [X_25] : ( multiply(X_25,identity) = X_25 ),
inference(superposition,[status(thm),theory(equality)],[c_722,c_413]) ).
tff(c_377,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_257,c_356]) ).
tff(c_420,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_377]) ).
tff(c_392,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_266,c_356]) ).
tff(c_423,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_392]) ).
tff(c_292,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( multiply(X2_9,sk_c6) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_254,c_254,c_254,c_254,c_254,c_254,c_254,c_254,c_60]) ).
tff(c_293,plain,
! [X3_7] :
( ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_292]) ).
tff(c_1102,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_729,c_420,c_423,c_423,c_293]) ).
tff(c_430,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_423,c_93]) ).
tff(c_567,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_430,c_197]) ).
tff(c_579,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_567]) ).
tff(c_431,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_423,c_89]) ).
tff(c_584,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_579,c_431]) ).
tff(c_1104,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1102,c_584]) ).
tff(c_1105,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_292]) ).
tff(c_8872,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( identity != X2_9 )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1213,c_1483,c_1213,c_1213,c_1216,c_1483,c_1213,c_1216,c_1483,c_1213,c_1216,c_1213,c_1483,c_1213,c_1213,c_1213,c_1105]) ).
tff(c_8874,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8872]) ).
tff(c_1221,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1216,c_93]) ).
tff(c_1345,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_1221,c_197]) ).
tff(c_1357,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1345]) ).
tff(c_1222,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1216,c_89]) ).
tff(c_1361,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1357,c_1222]) ).
tff(c_8876,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8874,c_1361]) ).
tff(c_8877,plain,
! [X1_8,X5_6,X4_10] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 ) ),
inference(splitRight,[status(thm)],[c_8872]) ).
tff(c_12345,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8877]) ).
tff(c_12347,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12345,c_1361]) ).
tff(c_12348,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_8877]) ).
tff(c_12350,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_12348]) ).
tff(c_12352,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12350,c_1361]) ).
tff(c_12931,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_12348]) ).
tff(c_12933,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12931,c_1361]) ).
tff(c_12935,plain,
multiply(sk_c3,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_48,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_12978,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_12935,c_48]) ).
tff(c_46,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_12948,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_12935,c_46]) ).
tff(c_12952,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12948,c_4]) ).
tff(c_13007,plain,
! [Z_158] : ( multiply(sk_c7,multiply(sk_c5,Z_158)) = multiply(identity,Z_158) ),
inference(superposition,[status(thm),theory(equality)],[c_12952,c_12983]) ).
tff(c_13244,plain,
! [Z_166] : ( multiply(sk_c7,multiply(sk_c5,Z_166)) = Z_166 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13007]) ).
tff(c_13256,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12978,c_13244]) ).
tff(c_44,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_12972,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_12935,c_44]) ).
tff(c_12934,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_12939,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12934,c_4]) ).
tff(c_13010,plain,
! [Z_158] : ( multiply(sk_c8,multiply(sk_c4,Z_158)) = multiply(identity,Z_158) ),
inference(superposition,[status(thm),theory(equality)],[c_12939,c_12983]) ).
tff(c_13267,plain,
! [Z_167] : ( multiply(sk_c8,multiply(sk_c4,Z_167)) = Z_167 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13010]) ).
tff(c_13279,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_12972,c_13267]) ).
tff(c_13031,plain,
! [Z_158] : ( multiply(sk_c7,multiply(sk_c8,Z_158)) = multiply(sk_c6,Z_158) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_12983]) ).
tff(c_13315,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_13279,c_13031]) ).
tff(c_13321,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13256,c_13315]) ).
tff(c_13404,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_13321,c_13380]) ).
tff(c_13496,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13404]) ).
tff(c_13571,plain,
multiply(sk_c3,identity) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_13498,c_12935]) ).
tff(c_13812,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13747,c_13496,c_13571]) ).
tff(c_13814,plain,
multiply(sk_c1,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_16,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_13821,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_13814,c_16]) ).
tff(c_13830,plain,
! [X_174,Y_175,Z_176] : ( multiply(multiply(X_174,Y_175),Z_176) = multiply(X_174,multiply(Y_175,Z_176)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13851,plain,
! [Z_176] : ( multiply(sk_c7,multiply(sk_c5,Z_176)) = multiply(identity,Z_176) ),
inference(superposition,[status(thm),theory(equality)],[c_12952,c_13830]) ).
tff(c_15907,plain,
! [Z_209] : ( multiply(sk_c7,multiply(sk_c5,Z_209)) = Z_209 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13851]) ).
tff(c_15919,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_13821,c_15907]) ).
tff(c_13813,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_13854,plain,
! [Z_176] : ( multiply(sk_c8,multiply(sk_c4,Z_176)) = multiply(identity,Z_176) ),
inference(superposition,[status(thm),theory(equality)],[c_12939,c_13830]) ).
tff(c_15930,plain,
! [Z_210] : ( multiply(sk_c8,multiply(sk_c4,Z_210)) = Z_210 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13854]) ).
tff(c_15945,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13813,c_15930]) ).
tff(c_13875,plain,
! [Z_176] : ( multiply(sk_c7,multiply(sk_c8,Z_176)) = multiply(sk_c6,Z_176) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_13830]) ).
tff(c_15952,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_15945,c_13875]) ).
tff(c_15958,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15919,c_15952]) ).
tff(c_13869,plain,
! [X_2,Z_176] : ( multiply(inverse(X_2),multiply(X_2,Z_176)) = multiply(identity,Z_176) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13830]) ).
tff(c_16174,plain,
! [X_213,Z_214] : ( multiply(inverse(X_213),multiply(X_213,Z_214)) = Z_214 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13869]) ).
tff(c_16222,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_15958,c_16174]) ).
tff(c_16260,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16222]) ).
tff(c_13860,plain,
! [Z_176] : ( multiply(sk_c7,multiply(sk_c2,Z_176)) = multiply(identity,Z_176) ),
inference(superposition,[status(thm),theory(equality)],[c_110,c_13830]) ).
tff(c_13919,plain,
! [Z_179] : ( multiply(sk_c7,multiply(sk_c2,Z_179)) = Z_179 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13860]) ).
tff(c_13931,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_120,c_13919]) ).
tff(c_16000,plain,
! [Z_212] : ( multiply(sk_c2,multiply(sk_c7,Z_212)) = multiply(sk_c6,Z_212) ),
inference(superposition,[status(thm),theory(equality)],[c_120,c_13830]) ).
tff(c_16024,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c2,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_13931,c_16000]) ).
tff(c_16049,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_120,c_16024]) ).
tff(c_16219,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16049,c_16174]) ).
tff(c_16259,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16219]) ).
tff(c_13885,plain,
! [X_2,Z_176] : ( multiply(inverse(X_2),multiply(X_2,Z_176)) = Z_176 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13869]) ).
tff(c_13887,plain,
! [Z_177] : ( multiply(sk_c7,multiply(sk_c8,Z_177)) = multiply(sk_c6,Z_177) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_13830]) ).
tff(c_13902,plain,
multiply(sk_c7,identity) = multiply(sk_c6,sk_c1),
inference(superposition,[status(thm),theory(equality)],[c_93,c_13887]) ).
tff(c_13899,plain,
multiply(sk_c7,identity) = multiply(sk_c6,sk_c4),
inference(superposition,[status(thm),theory(equality)],[c_12939,c_13887]) ).
tff(c_15898,plain,
multiply(sk_c6,sk_c4) = multiply(sk_c6,sk_c1),
inference(demodulation,[status(thm),theory(equality)],[c_13902,c_13899]) ).
tff(c_16228,plain,
multiply(inverse(sk_c6),multiply(sk_c6,sk_c1)) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_15898,c_16174]) ).
tff(c_16261,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13885,c_16228]) ).
tff(c_16045,plain,
multiply(sk_c6,sk_c8) = multiply(sk_c2,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_8,c_16000]) ).
tff(c_16050,plain,
multiply(sk_c2,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15958,c_16045]) ).
tff(c_13882,plain,
! [Z_176] : ( multiply(sk_c7,multiply(sk_c2,Z_176)) = Z_176 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13860]) ).
tff(c_16061,plain,
multiply(sk_c7,sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16050,c_13882]) ).
tff(c_16068,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16061,c_13931]) ).
tff(c_16091,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_16068,c_13813]) ).
tff(c_16264,plain,
multiply(sk_c1,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_16261,c_16091]) ).
tff(c_16370,plain,
multiply(sk_c1,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16260,c_16259,c_16264]) ).
tff(c_16090,plain,
multiply(sk_c1,sk_c8) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16068,c_13814]) ).
tff(c_16276,plain,
multiply(sk_c1,sk_c8) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_16259,c_16090]) ).
tff(c_16384,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16370,c_16260,c_16276]) ).
tff(c_16386,plain,
multiply(sk_c2,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_32,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_18178,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16386,c_32]) ).
tff(c_16394,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_17165,plain,
! [X_227,Y_228,Z_229] : ( multiply(multiply(X_227,Y_228),Z_229) = multiply(X_227,multiply(Y_228,Z_229)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_17201,plain,
! [Z_229] : ( multiply(sk_c7,multiply(sk_c3,Z_229)) = multiply(identity,Z_229) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_17165]) ).
tff(c_17570,plain,
! [Z_234] : ( multiply(sk_c7,multiply(sk_c3,Z_234)) = Z_234 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17201]) ).
tff(c_17582,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16394,c_17570]) ).
tff(c_17586,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_17582]) ).
tff(c_17722,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17586,c_8]) ).
tff(c_17204,plain,
! [X_2,Z_229] : ( multiply(inverse(X_2),multiply(X_2,Z_229)) = multiply(identity,Z_229) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17165]) ).
tff(c_17795,plain,
! [X_236,Z_237] : ( multiply(inverse(X_236),multiply(X_236,Z_237)) = Z_237 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17204]) ).
tff(c_17825,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_17722,c_17795]) ).
tff(c_17863,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17825]) ).
tff(c_16385,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_16442,plain,
! [X_216,Y_217,Z_218] : ( multiply(multiply(X_216,Y_217),Z_218) = multiply(X_216,multiply(Y_217,Z_218)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16481,plain,
! [Z_218] : ( multiply(sk_c7,multiply(sk_c3,Z_218)) = multiply(identity,Z_218) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_16442]) ).
tff(c_16653,plain,
! [Z_223] : ( multiply(sk_c7,multiply(sk_c3,Z_223)) = Z_223 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16481]) ).
tff(c_16665,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16394,c_16653]) ).
tff(c_16669,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_16665]) ).
tff(c_16424,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_16478,plain,
! [Z_218] : ( multiply(sk_c8,multiply(sk_c1,Z_218)) = multiply(identity,Z_218) ),
inference(superposition,[status(thm),theory(equality)],[c_93,c_16442]) ).
tff(c_16515,plain,
! [Z_220] : ( multiply(sk_c8,multiply(sk_c1,Z_220)) = Z_220 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16478]) ).
tff(c_16527,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_16424,c_16515]) ).
tff(c_16671,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_16669,c_16527]) ).
tff(c_16484,plain,
! [X_2,Z_218] : ( multiply(inverse(X_2),multiply(X_2,Z_218)) = multiply(identity,Z_218) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16442]) ).
tff(c_16784,plain,
! [X_224,Z_225] : ( multiply(inverse(X_224),multiply(X_224,Z_225)) = Z_225 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16484]) ).
tff(c_16802,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16671,c_16784]) ).
tff(c_16863,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16802]) ).
tff(c_16680,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16669,c_110]) ).
tff(c_16887,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16863,c_16680]) ).
tff(c_16500,plain,
! [X_2,Z_218] : ( multiply(inverse(X_2),multiply(X_2,Z_218)) = Z_218 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16484]) ).
tff(c_17119,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_16887,c_16500]) ).
tff(c_17131,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17119]) ).
tff(c_16678,plain,
multiply(sk_c2,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16669,c_16386]) ).
tff(c_16884,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_16863,c_16863,c_16678]) ).
tff(c_17147,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17131,c_16884]) ).
tff(c_17148,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_17713,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_17586,c_17148]) ).
tff(c_17816,plain,
multiply(inverse(sk_c4),sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17713,c_17795]) ).
tff(c_17862,plain,
multiply(sk_c8,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16385,c_17816]) ).
tff(c_18033,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17863,c_2,c_17863,c_17862]) ).
tff(c_17718,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17586,c_110]) ).
tff(c_18040,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18033,c_17718]) ).
tff(c_17220,plain,
! [X_2,Z_229] : ( multiply(inverse(X_2),multiply(X_2,Z_229)) = Z_229 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17204]) ).
tff(c_18127,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_18040,c_17220]) ).
tff(c_18139,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_18127]) ).
tff(c_17716,plain,
multiply(sk_c2,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17586,c_16386]) ).
tff(c_18038,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_18033,c_18033,c_17716]) ).
tff(c_18143,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_18139,c_18038]) ).
tff(c_18148,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18143]) ).
tff(c_18149,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_18154,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18149,c_4]) ).
tff(c_19830,plain,
! [X_269,Y_270,Z_271] : ( multiply(multiply(X_269,Y_270),Z_271) = multiply(X_269,multiply(Y_270,Z_271)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_19851,plain,
! [Z_271] : ( multiply(sk_c7,multiply(sk_c5,Z_271)) = multiply(identity,Z_271) ),
inference(superposition,[status(thm),theory(equality)],[c_18154,c_19830]) ).
tff(c_19947,plain,
! [Z_276] : ( multiply(sk_c7,multiply(sk_c5,Z_276)) = Z_276 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19851]) ).
tff(c_19959,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_18178,c_19947]) ).
tff(c_18183,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_18198,plain,
! [X_239,Y_240,Z_241] : ( multiply(multiply(X_239,Y_240),Z_241) = multiply(X_239,multiply(Y_240,Z_241)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_18231,plain,
! [Z_241] : ( multiply(sk_c8,multiply(sk_c1,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_93,c_18198]) ).
tff(c_18406,plain,
! [Z_249] : ( multiply(sk_c8,multiply(sk_c1,Z_249)) = Z_249 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18231]) ).
tff(c_18418,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_18183,c_18406]) ).
tff(c_18237,plain,
! [X_2,Z_241] : ( multiply(inverse(X_2),multiply(X_2,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18198]) ).
tff(c_19316,plain,
! [X_264,Z_265] : ( multiply(inverse(X_264),multiply(X_264,Z_265)) = Z_265 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18237]) ).
tff(c_19364,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_18418,c_19316]) ).
tff(c_19428,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19364]) ).
tff(c_19617,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19428,c_81]) ).
tff(c_19670,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_19617,c_4]) ).
tff(c_18253,plain,
! [X_2,Z_241] : ( multiply(inverse(X_2),multiply(X_2,Z_241)) = Z_241 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18237]) ).
tff(c_19737,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_19670,c_18253]) ).
tff(c_19749,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19737]) ).
tff(c_18222,plain,
! [Z_241] : ( multiply(sk_c7,multiply(sk_c5,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_18154,c_18198]) ).
tff(c_18483,plain,
! [Z_252] : ( multiply(sk_c7,multiply(sk_c5,Z_252)) = Z_252 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18222]) ).
tff(c_18495,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_18178,c_18483]) ).
tff(c_28,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_18184,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_16386,c_28]) ).
tff(c_16390,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16385,c_4]) ).
tff(c_18225,plain,
! [Z_241] : ( multiply(sk_c8,multiply(sk_c4,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_16390,c_18198]) ).
tff(c_18836,plain,
! [Z_258] : ( multiply(sk_c8,multiply(sk_c4,Z_258)) = Z_258 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18225]) ).
tff(c_18851,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_18184,c_18836]) ).
tff(c_18243,plain,
! [Z_241] : ( multiply(sk_c7,multiply(sk_c8,Z_241)) = multiply(sk_c6,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_18198]) ).
tff(c_18858,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_18851,c_18243]) ).
tff(c_18864,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_18495,c_18858]) ).
tff(c_19337,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_18864,c_19316]) ).
tff(c_19426,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19337]) ).
tff(c_18150,plain,
multiply(sk_c3,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_19611,plain,
multiply(sk_c3,identity) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_19428,c_18150]) ).
tff(c_19815,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19749,c_19426,c_19611]) ).
tff(c_19816,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_19854,plain,
! [Z_271] : ( multiply(sk_c8,multiply(sk_c4,Z_271)) = multiply(identity,Z_271) ),
inference(superposition,[status(thm),theory(equality)],[c_16390,c_19830]) ).
tff(c_19924,plain,
! [Z_275] : ( multiply(sk_c8,multiply(sk_c4,Z_275)) = Z_275 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19854]) ).
tff(c_19936,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_19816,c_19924]) ).
tff(c_19963,plain,
! [Z_277] : ( multiply(sk_c7,multiply(sk_c8,Z_277)) = multiply(sk_c6,Z_277) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_19830]) ).
tff(c_19975,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_19936,c_19963]) ).
tff(c_20015,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_19959,c_19975]) ).
tff(c_19866,plain,
! [X_2,Z_271] : ( multiply(inverse(X_2),multiply(X_2,Z_271)) = multiply(identity,Z_271) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_19830]) ).
tff(c_20049,plain,
! [X_279,Z_280] : ( multiply(inverse(X_279),multiply(X_279,Z_280)) = Z_280 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19866]) ).
tff(c_20067,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_20015,c_20049]) ).
tff(c_20149,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20067]) ).
tff(c_20228,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_20149,c_20149,c_19936]) ).
tff(c_20237,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20228]) ).
tff(c_20239,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20048,c_20237]) ).
tff(c_20241,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_20037]) ).
tff(c_20044,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_20023]) ).
tff(c_20046,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_20044]) ).
tff(c_20243,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20241,c_20046]) ).
tff(c_20246,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20241,c_20241,c_19959]) ).
tff(c_20265,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20246]) ).
tff(c_20299,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20243,c_20265]) ).
tff(c_20301,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_20044]) ).
tff(c_20412,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_20301,c_20037]) ).
tff(c_20413,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_20412]) ).
tff(c_20304,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20301,c_20301,c_19959]) ).
tff(c_20478,plain,
! [X_284,Z_285] : ( multiply(inverse(X_284),multiply(X_284,Z_285)) = Z_285 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19866]) ).
tff(c_20499,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20304,c_20478]) ).
tff(c_20561,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20499]) ).
tff(c_20563,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20413,c_20561]) ).
tff(c_20565,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_20412]) ).
tff(c_20317,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_20301,c_110]) ).
tff(c_20574,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_20565,c_20317]) ).
tff(c_20646,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_20574,c_2]) ).
tff(c_20315,plain,
multiply(sk_c2,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20301,c_16386]) ).
tff(c_20571,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20565,c_20565,c_20315]) ).
tff(c_20655,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20646,c_20571]) ).
tff(c_20660,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20655]) ).
tff(c_20662,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_40,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_20683,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_20662,c_40]) ).
tff(c_20661,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_20666,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20661,c_4]) ).
tff(c_20713,plain,
! [X_287,Y_288,Z_289] : ( multiply(multiply(X_287,Y_288),Z_289) = multiply(X_287,multiply(Y_288,Z_289)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20737,plain,
! [Z_289] : ( multiply(sk_c7,multiply(sk_c5,Z_289)) = multiply(identity,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_20666,c_20713]) ).
tff(c_21776,plain,
! [Z_313] : ( multiply(sk_c7,multiply(sk_c5,Z_313)) = Z_313 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20737]) ).
tff(c_21788,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20683,c_21776]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_20695,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20662,c_36]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_102]) ).
tff(c_20675,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20662,c_34]) ).
tff(c_20679,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20675,c_4]) ).
tff(c_20731,plain,
! [Z_289] : ( multiply(sk_c8,multiply(sk_c4,Z_289)) = multiply(identity,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_20679,c_20713]) ).
tff(c_21738,plain,
! [Z_312] : ( multiply(sk_c8,multiply(sk_c4,Z_312)) = Z_312 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20731]) ).
tff(c_21753,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20695,c_21738]) ).
tff(c_20752,plain,
! [Z_289] : ( multiply(sk_c7,multiply(sk_c8,Z_289)) = multiply(sk_c6,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_20713]) ).
tff(c_21760,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_21753,c_20752]) ).
tff(c_21864,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21788,c_21760]) ).
tff(c_20746,plain,
! [X_2,Z_289] : ( multiply(inverse(X_2),multiply(X_2,Z_289)) = multiply(identity,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20713]) ).
tff(c_22646,plain,
! [X_330,Z_331] : ( multiply(inverse(X_330),multiply(X_330,Z_331)) = Z_331 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20746]) ).
tff(c_22670,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_21864,c_22646]) ).
tff(c_22704,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22670]) ).
tff(c_20761,plain,
! [X_2,Z_289] : ( multiply(inverse(X_2),multiply(X_2,Z_289)) = Z_289 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20746]) ).
tff(c_22937,plain,
! [X_334,Z_335] : ( multiply(inverse(inverse(X_334)),Z_335) = multiply(X_334,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_20761,c_22646]) ).
tff(c_22697,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_22646]) ).
tff(c_22944,plain,
! [X_334] : ( multiply(X_334,identity) = X_334 ),
inference(superposition,[status(thm),theory(equality)],[c_22937,c_22697]) ).
tff(c_22722,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22704,c_89]) ).
tff(c_21708,plain,
! [Z_311] : ( multiply(sk_c7,multiply(sk_c8,Z_311)) = multiply(sk_c6,Z_311) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_20713]) ).
tff(c_21726,plain,
multiply(sk_c7,identity) = multiply(sk_c6,sk_c1),
inference(superposition,[status(thm),theory(equality)],[c_93,c_21708]) ).
tff(c_21723,plain,
multiply(sk_c7,identity) = multiply(sk_c6,sk_c4),
inference(superposition,[status(thm),theory(equality)],[c_20679,c_21708]) ).
tff(c_21767,plain,
multiply(sk_c6,sk_c4) = multiply(sk_c6,sk_c1),
inference(demodulation,[status(thm),theory(equality)],[c_21726,c_21723]) ).
tff(c_22673,plain,
multiply(inverse(sk_c6),multiply(sk_c6,sk_c1)) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_21767,c_22646]) ).
tff(c_22705,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_20761,c_22673]) ).
tff(c_20734,plain,
! [Z_289] : ( multiply(sk_c5,multiply(sk_c6,Z_289)) = multiply(sk_c7,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_20683,c_20713]) ).
tff(c_21868,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_21864,c_20734]) ).
tff(c_21874,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_20683,c_21868]) ).
tff(c_21884,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_21874,c_20695]) ).
tff(c_22759,plain,
multiply(sk_c1,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22704,c_22705,c_21884]) ).
tff(c_22763,plain,
multiply(inverse(sk_c1),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_22759,c_20761]) ).
tff(c_22769,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22722,c_22763]) ).
tff(c_21962,plain,
! [X_316,Z_317] : ( multiply(inverse(X_316),multiply(X_316,Z_317)) = Z_317 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20746]) ).
tff(c_22242,plain,
! [X_320,Z_321] : ( multiply(inverse(inverse(X_320)),Z_321) = multiply(X_320,Z_321) ),
inference(superposition,[status(thm),theory(equality)],[c_21962,c_20761]) ).
tff(c_22031,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_21962]) ).
tff(c_22249,plain,
! [X_320] : ( multiply(X_320,identity) = X_320 ),
inference(superposition,[status(thm),theory(equality)],[c_22242,c_22031]) ).
tff(c_22004,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_21864,c_21962]) ).
tff(c_22041,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22004]) ).
tff(c_21880,plain,
multiply(sk_c8,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21874,c_21753]) ).
tff(c_22057,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_22041,c_22041,c_21880]) ).
tff(c_22062,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22057]) ).
tff(c_20858,plain,
! [Z_294] : ( multiply(sk_c7,multiply(sk_c5,Z_294)) = Z_294 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20737]) ).
tff(c_20870,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20683,c_20858]) ).
tff(c_20881,plain,
! [X3_295] :
( ( inverse(X3_295) != sk_c8 )
| ( multiply(X3_295,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_20899,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_20881]) ).
tff(c_20902,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_20899]) ).
tff(c_20790,plain,
! [Z_292] : ( multiply(sk_c8,multiply(sk_c4,Z_292)) = Z_292 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20731]) ).
tff(c_20802,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20695,c_20790]) ).
tff(c_20834,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_20802,c_20752]) ).
tff(c_20904,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20870,c_20834]) ).
tff(c_21014,plain,
! [Z_298] : ( multiply(sk_c5,multiply(sk_c6,Z_298)) = multiply(sk_c7,Z_298) ),
inference(superposition,[status(thm),theory(equality)],[c_20683,c_20713]) ).
tff(c_21032,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_20904,c_21014]) ).
tff(c_21040,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20683,c_8,c_21032]) ).
tff(c_21042,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20902,c_21040]) ).
tff(c_21044,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_20899]) ).
tff(c_20892,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20881]) ).
tff(c_21122,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21044,c_20892]) ).
tff(c_21123,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_21122]) ).
tff(c_21047,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21044,c_21044,c_20870]) ).
tff(c_21148,plain,
! [X_299,Z_300] : ( multiply(inverse(X_299),multiply(X_299,Z_300)) = Z_300 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20746]) ).
tff(c_21169,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_21047,c_21148]) ).
tff(c_21225,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21169]) ).
tff(c_21227,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21123,c_21225]) ).
tff(c_21229,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_21122]) ).
tff(c_20896,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_20881]) ).
tff(c_20901,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_20896]) ).
tff(c_21045,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21044,c_20901]) ).
tff(c_21239,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_21229,c_21045]) ).
tff(c_21060,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21044,c_8]) ).
tff(c_21237,plain,
multiply(identity,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21229,c_21229,c_21060]) ).
tff(c_21295,plain,
sk_c8 = identity,
inference(superposition,[status(thm),theory(equality)],[c_21237,c_2]) ).
tff(c_21303,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21239,c_21295]) ).
tff(c_21305,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_20896]) ).
tff(c_21308,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21305,c_21305,c_20802]) ).
tff(c_21318,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20870,c_21308]) ).
tff(c_21324,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21318,c_21305]) ).
tff(c_21435,plain,
( ( inverse(inverse(sk_c6)) != sk_c6 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21318,c_21324,c_21324,c_20892]) ).
tff(c_21436,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_21435]) ).
tff(c_21325,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21318,c_21318,c_20870]) ).
tff(c_21495,plain,
! [X_305,Z_306] : ( multiply(inverse(X_305),multiply(X_305,Z_306)) = Z_306 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20746]) ).
tff(c_21528,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_21325,c_21495]) ).
tff(c_21568,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21528]) ).
tff(c_21570,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21436,c_21568]) ).
tff(c_21572,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_21435]) ).
tff(c_21334,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21318,c_81]) ).
tff(c_21365,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21334,c_4]) ).
tff(c_21602,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21572,c_21365]) ).
tff(c_21582,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21572,c_21334]) ).
tff(c_21628,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21602,c_21582]) ).
tff(c_21304,plain,
inverse(identity) != sk_c8,
inference(splitRight,[status(thm)],[c_20896]) ).
tff(c_21361,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21324,c_21304]) ).
tff(c_21583,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_21572,c_21361]) ).
tff(c_21680,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21628,c_21583]) ).
tff(c_21681,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_21808,plain,
! [X2_314] :
( ( multiply(X2_314,sk_c6) != sk_c7 )
| ( inverse(X2_314) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_21681]) ).
tff(c_21815,plain,
inverse(sk_c5) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20683,c_21808]) ).
tff(c_21827,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20661,c_21815]) ).
tff(c_21828,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_21681]) ).
tff(c_21898,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21874,c_21874,c_21874,c_21874,c_21874,c_21828]) ).
tff(c_21899,plain,
! [X4_10] :
( ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_21898]) ).
tff(c_22628,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_22249,c_22062,c_22062,c_22062,c_21899]) ).
tff(c_21888,plain,
inverse(sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21874,c_20661]) ).
tff(c_21910,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21888,c_4]) ).
tff(c_22080,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22062,c_21910]) ).
tff(c_22071,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22062,c_21888]) ).
tff(c_22128,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22080,c_22071]) ).
tff(c_22630,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22628,c_22128]) ).
tff(c_22631,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_21898]) ).
tff(c_44220,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_22704,c_22944,c_22769,c_22704,c_22944,c_22769,c_22704,c_22769,c_22631]) ).
tff(c_44222,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_44220]) ).
tff(c_22721,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22704,c_93]) ).
tff(c_22834,plain,
sk_c1 = identity,
inference(superposition,[status(thm),theory(equality)],[c_22721,c_2]) ).
tff(c_22845,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22834,c_22722]) ).
tff(c_44224,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44222,c_22845]) ).
tff(c_44226,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_44220]) ).
tff(c_44228,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44226,c_22845]) ).
tff(c_44230,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_24,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_60086,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_44230,c_24]) ).
tff(c_44274,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_44230,c_24]) ).
tff(c_22,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_44260,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_44230,c_22]) ).
tff(c_44264,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_44260,c_4]) ).
tff(c_44298,plain,
! [X_494,Y_495,Z_496] : ( multiply(multiply(X_494,Y_495),Z_496) = multiply(X_494,multiply(Y_495,Z_496)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_44319,plain,
! [Z_496] : ( multiply(sk_c7,multiply(sk_c5,Z_496)) = multiply(identity,Z_496) ),
inference(superposition,[status(thm),theory(equality)],[c_44264,c_44298]) ).
tff(c_44364,plain,
! [Z_498] : ( multiply(sk_c7,multiply(sk_c5,Z_498)) = Z_498 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44319]) ).
tff(c_44376,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_44274,c_44364]) ).
tff(c_20,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_44285,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_44230,c_20]) ).
tff(c_44229,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_44235,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_44229,c_4]) ).
tff(c_44325,plain,
! [Z_496] : ( multiply(sk_c8,multiply(sk_c4,Z_496)) = multiply(identity,Z_496) ),
inference(superposition,[status(thm),theory(equality)],[c_44235,c_44298]) ).
tff(c_44975,plain,
! [Z_508] : ( multiply(sk_c8,multiply(sk_c4,Z_508)) = Z_508 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44325]) ).
tff(c_44990,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_44285,c_44975]) ).
tff(c_44337,plain,
! [Z_496] : ( multiply(sk_c7,multiply(sk_c8,Z_496)) = multiply(sk_c6,Z_496) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_44298]) ).
tff(c_44997,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_44990,c_44337]) ).
tff(c_45003,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44376,c_44997]) ).
tff(c_44331,plain,
! [X_2,Z_496] : ( multiply(inverse(X_2),multiply(X_2,Z_496)) = multiply(identity,Z_496) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_44298]) ).
tff(c_46078,plain,
! [X_524,Z_525] : ( multiply(inverse(X_524),multiply(X_524,Z_525)) = Z_525 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44331]) ).
tff(c_46129,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_45003,c_46078]) ).
tff(c_46153,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_46129]) ).
tff(c_44346,plain,
! [X_2,Z_496] : ( multiply(inverse(X_2),multiply(X_2,Z_496)) = Z_496 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44331]) ).
tff(c_46418,plain,
! [X_528,Z_529] : ( multiply(inverse(inverse(X_528)),Z_529) = multiply(X_528,Z_529) ),
inference(superposition,[status(thm),theory(equality)],[c_46078,c_44346]) ).
tff(c_46144,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_46078]) ).
tff(c_46425,plain,
! [X_528] : ( multiply(X_528,identity) = X_528 ),
inference(superposition,[status(thm),theory(equality)],[c_46418,c_46144]) ).
tff(c_45005,plain,
! [Z_509] : ( multiply(sk_c4,multiply(sk_c7,Z_509)) = multiply(sk_c8,Z_509) ),
inference(superposition,[status(thm),theory(equality)],[c_44285,c_44298]) ).
tff(c_45047,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_8,c_45005]) ).
tff(c_45051,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_44990,c_45047]) ).
tff(c_44344,plain,
! [Z_496] : ( multiply(sk_c8,multiply(sk_c4,Z_496)) = Z_496 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44325]) ).
tff(c_45055,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45051,c_44344]) ).
tff(c_45029,plain,
multiply(sk_c8,sk_c7) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_44376,c_45005]) ).
tff(c_45237,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45051,c_45055,c_45029]) ).
tff(c_45245,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45237,c_45237,c_44376]) ).
tff(c_46198,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45245,c_44346]) ).
tff(c_46204,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_46198]) ).
tff(c_45341,plain,
! [X_511,Z_512] : ( multiply(inverse(X_511),multiply(X_511,Z_512)) = Z_512 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44331]) ).
tff(c_45635,plain,
! [X_514,Z_515] : ( multiply(inverse(inverse(X_514)),Z_515) = multiply(X_514,Z_515) ),
inference(superposition,[status(thm),theory(equality)],[c_44346,c_45341]) ).
tff(c_45413,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_45341]) ).
tff(c_45642,plain,
! [X_514] : ( multiply(X_514,identity) = X_514 ),
inference(superposition,[status(thm),theory(equality)],[c_45635,c_45413]) ).
tff(c_45377,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45245,c_45341]) ).
tff(c_45422,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_45377]) ).
tff(c_45113,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45055,c_45051,c_45029]) ).
tff(c_45115,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45113,c_45051]) ).
tff(c_44559,plain,
! [X3_503] :
( ( inverse(X3_503) != sk_c8 )
| ( multiply(X3_503,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_44580,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_44559]) ).
tff(c_44583,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_44580]) ).
tff(c_44422,plain,
! [Z_501] : ( multiply(sk_c8,multiply(sk_c4,Z_501)) = Z_501 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44325]) ).
tff(c_44437,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_44285,c_44422]) ).
tff(c_44459,plain,
! [Z_502] : ( multiply(sk_c4,multiply(sk_c7,Z_502)) = multiply(sk_c8,Z_502) ),
inference(superposition,[status(thm),theory(equality)],[c_44285,c_44298]) ).
tff(c_44501,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_8,c_44459]) ).
tff(c_44505,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_44437,c_44501]) ).
tff(c_44509,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_44505,c_44344]) ).
tff(c_44483,plain,
multiply(sk_c8,sk_c7) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_44376,c_44459]) ).
tff(c_44585,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44509,c_44505,c_44483]) ).
tff(c_44586,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44583,c_44585]) ).
tff(c_44588,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_44580]) ).
tff(c_44577,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_44559]) ).
tff(c_44582,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_44577]) ).
tff(c_44589,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44588,c_44582]) ).
tff(c_44592,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44588,c_44505]) ).
tff(c_44601,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_44588,c_44285]) ).
tff(c_44690,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44592,c_44601]) ).
tff(c_44692,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44589,c_44690]) ).
tff(c_44694,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_44577]) ).
tff(c_44703,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_44694,c_44694,c_44437]) ).
tff(c_44715,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44376,c_44703]) ).
tff(c_44721,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44715,c_44694]) ).
tff(c_44693,plain,
inverse(identity) != sk_c8,
inference(splitRight,[status(thm)],[c_44577]) ).
tff(c_44752,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44721,c_44693]) ).
tff(c_44492,plain,
multiply(sk_c8,sk_c5) = multiply(sk_c4,identity),
inference(superposition,[status(thm),theory(equality)],[c_44264,c_44459]) ).
tff(c_44699,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c4,identity),
inference(demodulation,[status(thm),theory(equality)],[c_44694,c_44492]) ).
tff(c_44713,plain,
multiply(sk_c4,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44264,c_44699]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_44795,plain,
! [Z_5] : ( multiply(sk_c4,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_44713,c_6]) ).
tff(c_44798,plain,
! [Z_5] : ( multiply(sk_c4,Z_5) = Z_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_44795]) ).
tff(c_44704,plain,
! [Z_496] : ( multiply(sk_c7,multiply(sk_c4,Z_496)) = Z_496 ),
inference(demodulation,[status(thm),theory(equality)],[c_44694,c_44344]) ).
tff(c_44868,plain,
! [Z_505] : ( multiply(sk_c6,Z_505) = Z_505 ),
inference(demodulation,[status(thm),theory(equality)],[c_44798,c_44715,c_44704]) ).
tff(c_44733,plain,
multiply(sk_c6,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44715,c_85]) ).
tff(c_44877,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_44868,c_44733]) ).
tff(c_44734,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44715,c_81]) ).
tff(c_44970,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44877,c_44734]) ).
tff(c_44973,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44752,c_44970]) ).
tff(c_44974,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_45101,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_44974]) ).
tff(c_45192,plain,
! [X2_510] :
( ( multiply(X2_510,sk_c6) != sk_c6 )
| ( inverse(X2_510) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_45113,c_45113,c_45101]) ).
tff(c_45195,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45115,c_45192]) ).
tff(c_45212,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44229,c_45195]) ).
tff(c_45124,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_45113,c_44285]) ).
tff(c_45223,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45115,c_45124]) ).
tff(c_45224,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_45212,c_45223]) ).
tff(c_45225,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_44974]) ).
tff(c_45276,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_45237,c_45237,c_45237,c_45237,c_45237,c_45225]) ).
tff(c_45277,plain,
! [X4_10] :
( ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_45276]) ).
tff(c_46026,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_45642,c_45422,c_45422,c_45422,c_45277]) ).
tff(c_45251,plain,
inverse(sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45237,c_44260]) ).
tff(c_45265,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_45251,c_4]) ).
tff(c_45460,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45422,c_45265]) ).
tff(c_45434,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_45422,c_45251]) ).
tff(c_45485,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_45460,c_45434]) ).
tff(c_46028,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46026,c_45485]) ).
tff(c_46029,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_45276]) ).
tff(c_60060,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_46153,c_46425,c_46204,c_46153,c_46425,c_46204,c_46153,c_46204,c_46029]) ).
tff(c_60062,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_60060]) ).
tff(c_44247,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_45253,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45237,c_44247]) ).
tff(c_46033,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_45253,c_4]) ).
tff(c_46273,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46204,c_46033]) ).
tff(c_46211,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_46204,c_45253]) ).
tff(c_46274,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_46273,c_46211]) ).
tff(c_60064,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60062,c_46274]) ).
tff(c_60066,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_60060]) ).
tff(c_60068,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60066,c_46274]) ).
tff(c_60069,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_60074,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_60069,c_4]) ).
tff(c_60135,plain,
! [Z_654] : ( multiply(sk_c7,multiply(sk_c5,Z_654)) = multiply(identity,Z_654) ),
inference(superposition,[status(thm),theory(equality)],[c_60074,c_60114]) ).
tff(c_60160,plain,
! [Z_655] : ( multiply(sk_c7,multiply(sk_c5,Z_655)) = Z_655 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60135]) ).
tff(c_60172,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_60086,c_60160]) ).
tff(c_60070,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_60092,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_60070,c_36]) ).
tff(c_60138,plain,
! [Z_654] : ( multiply(sk_c8,multiply(sk_c4,Z_654)) = multiply(identity,Z_654) ),
inference(superposition,[status(thm),theory(equality)],[c_44235,c_60114]) ).
tff(c_60183,plain,
! [Z_656] : ( multiply(sk_c8,multiply(sk_c4,Z_656)) = Z_656 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60138]) ).
tff(c_60195,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_60092,c_60183]) ).
tff(c_60852,plain,
! [Z_670] : ( multiply(sk_c7,multiply(sk_c8,Z_670)) = multiply(sk_c6,Z_670) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_60114]) ).
tff(c_60864,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_60195,c_60852]) ).
tff(c_60874,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_60172,c_60864]) ).
tff(c_60911,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_60874,c_60890]) ).
tff(c_60969,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_60911]) ).
tff(c_60977,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_60969,c_60969,c_60195]) ).
tff(c_60985,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60977]) ).
tff(c_60983,plain,
multiply(sk_c7,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_60969,c_8]) ).
tff(c_61622,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60985,c_60983]) ).
tff(c_61226,plain,
! [X_676,Z_677] : ( multiply(inverse(inverse(X_676)),Z_677) = multiply(X_676,Z_677) ),
inference(superposition,[status(thm),theory(equality)],[c_60158,c_60890]) ).
tff(c_61233,plain,
! [X_676] : ( multiply(X_676,identity) = X_676 ),
inference(superposition,[status(thm),theory(equality)],[c_61226,c_60959]) ).
tff(c_60992,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_60985,c_60985,c_60172]) ).
tff(c_61001,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60992]) ).
tff(c_60220,plain,
! [X3_658] :
( ( inverse(X3_658) != sk_c8 )
| ( multiply(X3_658,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_60231,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_60220]) ).
tff(c_60242,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_60231]) ).
tff(c_60453,plain,
! [Z_663] : ( multiply(sk_c7,multiply(sk_c8,Z_663)) = multiply(sk_c6,Z_663) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_60114]) ).
tff(c_60468,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_60195,c_60453]) ).
tff(c_60478,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_60172,c_60468]) ).
tff(c_60482,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_60478,c_60158]) ).
tff(c_60491,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_60482]) ).
tff(c_60500,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_60491,c_60491,c_60195]) ).
tff(c_60509,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60500]) ).
tff(c_60511,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60242,c_60509]) ).
tff(c_60513,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_60231]) ).
tff(c_60238,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_60220]) ).
tff(c_60241,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_60238]) ).
tff(c_60514,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_60513,c_60241]) ).
tff(c_60519,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_60513,c_60513,c_60172]) ).
tff(c_60529,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60519]) ).
tff(c_60560,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60514,c_60529]) ).
tff(c_60562,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_60238]) ).
tff(c_60645,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_60562,c_60231]) ).
tff(c_60646,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_60645]) ).
tff(c_60567,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_60562,c_60562,c_60172]) ).
tff(c_60685,plain,
! [X_666,Z_667] : ( multiply(inverse(X_666),multiply(X_666,Z_667)) = Z_667 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60144]) ).
tff(c_60709,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_60567,c_60685]) ).
tff(c_60755,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_60709]) ).
tff(c_60757,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60646,c_60755]) ).
tff(c_60759,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_60645]) ).
tff(c_60561,plain,
inverse(sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_60238]) ).
tff(c_60602,plain,
inverse(sk_c6) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_60562,c_60561]) ).
tff(c_60765,plain,
inverse(identity) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_60759,c_60602]) ).
tff(c_60771,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_60759,c_60562]) ).
tff(c_60150,plain,
! [Z_654] : ( multiply(sk_c7,multiply(sk_c8,Z_654)) = multiply(sk_c6,Z_654) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_60114]) ).
tff(c_60781,plain,
! [Z_668] : ( multiply(sk_c8,Z_668) = Z_668 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60771,c_2,c_60759,c_60150]) ).
tff(c_60793,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_60781,c_44235]) ).
tff(c_60808,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_60793,c_44229]) ).
tff(c_60830,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60765,c_60808]) ).
tff(c_60831,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_61006,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != identity )
| ( multiply(X4_10,identity) != sk_c6 )
| ( inverse(X5_6) != identity )
| ( multiply(X5_6,identity) != identity )
| ( multiply(X1_8,identity) != identity )
| ( inverse(X1_8) != identity )
| ( multiply(X2_9,sk_c6) != identity )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_60985,c_60985,c_60969,c_60985,c_60969,c_60985,c_60969,c_60985,c_60985,c_60985,c_60831]) ).
tff(c_61007,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != identity )
| ( inverse(X2_9) != identity ) ),
inference(splitLeft,[status(thm)],[c_61006]) ).
tff(c_61618,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_61233,c_61001,c_61007]) ).
tff(c_60980,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_60969,c_44235]) ).
tff(c_61059,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_60980,c_60158]) ).
tff(c_61071,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_61059]) ).
tff(c_60982,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_60969,c_44229]) ).
tff(c_61095,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_61071,c_60982]) ).
tff(c_61620,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61618,c_61095]) ).
tff(c_61621,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,identity) != identity )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( multiply(X5_6,identity) != identity )
| ( inverse(X4_10) != identity )
| ( multiply(X4_10,identity) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_61006]) ).
tff(c_187743,plain,
! [X1_8,X5_6,X4_10] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_61824,c_61622,c_61824,c_61824,c_61621]) ).
tff(c_187745,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_187743]) ).
tff(c_60995,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_60985,c_60074]) ).
tff(c_61679,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_60995,c_60158]) ).
tff(c_61691,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_61679]) ).
tff(c_60997,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_60985,c_60069]) ).
tff(c_61695,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_61691,c_60997]) ).
tff(c_187747,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_187745,c_61695]) ).
tff(c_187748,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_187743]) ).
tff(c_187750,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_187748]) ).
tff(c_187752,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_187750,c_61695]) ).
tff(c_190269,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_187748]) ).
tff(c_190271,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_190269,c_61695]) ).
tff(c_190273,plain,
inverse(sk_c3) != sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_56,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_190335,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_190273,c_56]) ).
tff(c_54,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_190299,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_190273,c_54]) ).
tff(c_190303,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_190299,c_4]) ).
tff(c_190349,plain,
! [X_1130,Y_1131,Z_1132] : ( multiply(multiply(X_1130,Y_1131),Z_1132) = multiply(X_1130,multiply(Y_1131,Z_1132)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_190373,plain,
! [Z_1132] : ( multiply(sk_c7,multiply(sk_c5,Z_1132)) = multiply(identity,Z_1132) ),
inference(superposition,[status(thm),theory(equality)],[c_190303,c_190349]) ).
tff(c_190399,plain,
! [Z_1133] : ( multiply(sk_c7,multiply(sk_c5,Z_1133)) = Z_1133 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190373]) ).
tff(c_190411,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_190335,c_190399]) ).
tff(c_190382,plain,
! [X_2,Z_1132] : ( multiply(inverse(X_2),multiply(X_2,Z_1132)) = multiply(identity,Z_1132) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_190349]) ).
tff(c_191226,plain,
! [X_1152,Z_1153] : ( multiply(inverse(X_1152),multiply(X_1152,Z_1153)) = Z_1153 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190382]) ).
tff(c_191259,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_190411,c_191226]) ).
tff(c_191304,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_8,c_191226]) ).
tff(c_191953,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_191259,c_191304]) ).
tff(c_52,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_190330,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_190273,c_52]) ).
tff(c_190272,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_190277,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_190272,c_4]) ).
tff(c_190379,plain,
! [Z_1132] : ( multiply(sk_c8,multiply(sk_c4,Z_1132)) = multiply(identity,Z_1132) ),
inference(superposition,[status(thm),theory(equality)],[c_190277,c_190349]) ).
tff(c_191161,plain,
! [Z_1148] : ( multiply(sk_c8,multiply(sk_c4,Z_1148)) = Z_1148 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190379]) ).
tff(c_191173,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_190330,c_191161]) ).
tff(c_191967,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_191953,c_191953,c_191173]) ).
tff(c_191971,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190411,c_191967]) ).
tff(c_191978,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_191971,c_191971,c_191259]) ).
tff(c_191986,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_191978]) ).
tff(c_191977,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_191971,c_191953]) ).
tff(c_192014,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191986,c_191977]) ).
tff(c_191808,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_191259,c_191304]) ).
tff(c_191822,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_191808,c_191808,c_191173]) ).
tff(c_191826,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190411,c_191822]) ).
tff(c_191833,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_191826,c_191826,c_191259]) ).
tff(c_191841,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_191833]) ).
tff(c_191832,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_191826,c_191808]) ).
tff(c_191869,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191841,c_191832]) ).
tff(c_191870,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191841,c_191826]) ).
tff(c_191674,plain,
! [Z_1159] : ( multiply(sk_c7,multiply(sk_c8,Z_1159)) = multiply(sk_c6,Z_1159) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_190349]) ).
tff(c_191692,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_191173,c_191674]) ).
tff(c_191699,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190411,c_191692]) ).
tff(c_190397,plain,
! [X_2,Z_1132] : ( multiply(inverse(X_2),multiply(X_2,Z_1132)) = Z_1132 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190382]) ).
tff(c_191703,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_191699,c_190397]) ).
tff(c_191709,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_191703]) ).
tff(c_191717,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_191709,c_191709,c_191173]) ).
tff(c_191723,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_191717]) ).
tff(c_191731,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_191723,c_191723,c_190411]) ).
tff(c_191736,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_191731]) ).
tff(c_190285,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_190289,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_190285,c_4]) ).
tff(c_191286,plain,
multiply(inverse(sk_c7),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_190289,c_191226]) ).
tff(c_191277,plain,
multiply(inverse(sk_c7),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_190303,c_191226]) ).
tff(c_191454,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_191286,c_191277]) ).
tff(c_191468,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_191454,c_190335]) ).
tff(c_190488,plain,
! [X3_1138] :
( ( inverse(X3_1138) != sk_c8 )
| ( multiply(X3_1138,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_190506,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_190488]) ).
tff(c_190509,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_190506]) ).
tff(c_190423,plain,
! [Z_1134] : ( multiply(sk_c8,multiply(sk_c4,Z_1134)) = Z_1134 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190379]) ).
tff(c_190435,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_190330,c_190423]) ).
tff(c_190511,plain,
! [Z_1139] : ( multiply(sk_c4,multiply(sk_c7,Z_1139)) = multiply(sk_c8,Z_1139) ),
inference(superposition,[status(thm),theory(equality)],[c_190330,c_190349]) ).
tff(c_190541,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_8,c_190511]) ).
tff(c_190545,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_190435,c_190541]) ).
tff(c_190396,plain,
! [Z_1132] : ( multiply(sk_c8,multiply(sk_c4,Z_1132)) = Z_1132 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190379]) ).
tff(c_190549,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_190545,c_190396]) ).
tff(c_190529,plain,
multiply(sk_c8,sk_c7) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_190411,c_190511]) ).
tff(c_190579,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190549,c_190545,c_190529]) ).
tff(c_190580,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_190509,c_190579]) ).
tff(c_190582,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_190506]) ).
tff(c_190499,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_190488]) ).
tff(c_190666,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_190582,c_190499]) ).
tff(c_190667,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_190666]) ).
tff(c_190588,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190582,c_190582,c_190411]) ).
tff(c_190694,plain,
! [X_1141,Z_1142] : ( multiply(inverse(X_1141),multiply(X_1141,Z_1142)) = Z_1142 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190382]) ).
tff(c_190715,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_190588,c_190694]) ).
tff(c_190770,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_190715]) ).
tff(c_190772,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_190667,c_190770]) ).
tff(c_190774,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_190666]) ).
tff(c_190503,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_190488]) ).
tff(c_190508,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_190503]) ).
tff(c_190583,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190582,c_190508]) ).
tff(c_190785,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_190774,c_190583]) ).
tff(c_190597,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190582,c_8]) ).
tff(c_190782,plain,
multiply(identity,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_190774,c_190774,c_190597]) ).
tff(c_190853,plain,
sk_c8 = identity,
inference(superposition,[status(thm),theory(equality)],[c_190782,c_2]) ).
tff(c_190861,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_190785,c_190853]) ).
tff(c_190863,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_190503]) ).
tff(c_190867,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_190863,c_190863,c_190435]) ).
tff(c_190875,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190411,c_190867]) ).
tff(c_190881,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190875,c_190863]) ).
tff(c_190862,plain,
inverse(identity) != sk_c8,
inference(splitRight,[status(thm)],[c_190503]) ).
tff(c_190924,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190881,c_190862]) ).
tff(c_190889,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_190875,c_190289]) ).
tff(c_190388,plain,
! [Z_1132] : ( multiply(sk_c7,multiply(sk_c8,Z_1132)) = multiply(sk_c6,Z_1132) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_190349]) ).
tff(c_190996,plain,
! [Z_1144] : ( multiply(sk_c6,multiply(sk_c6,Z_1144)) = multiply(sk_c6,Z_1144) ),
inference(demodulation,[status(thm),theory(equality)],[c_190881,c_190875,c_190388]) ).
tff(c_191014,plain,
multiply(sk_c6,sk_c2) = multiply(sk_c6,identity),
inference(superposition,[status(thm),theory(equality)],[c_190889,c_190996]) ).
tff(c_191032,plain,
multiply(sk_c6,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_190889,c_191014]) ).
tff(c_191043,plain,
! [Z_5] : ( multiply(sk_c6,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_191032,c_6]) ).
tff(c_191055,plain,
! [Z_1145] : ( multiply(sk_c6,Z_1145) = Z_1145 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_191043]) ).
tff(c_191061,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_191055,c_190889]) ).
tff(c_190890,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_190875,c_190285]) ).
tff(c_191156,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_191061,c_190890]) ).
tff(c_191159,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_190924,c_191156]) ).
tff(c_191160,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_191337,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_191160]) ).
tff(c_191501,plain,
inverse(sk_c2) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_191468,c_191337]) ).
tff(c_191516,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_190285,c_191501]) ).
tff(c_191517,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_191160]) ).
tff(c_191656,plain,
! [X4_10] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_191517]) ).
tff(c_191751,plain,
! [X4_1160] :
( ( inverse(X4_1160) != identity )
| ( multiply(X4_1160,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_191736,c_191723,c_191723,c_191656]) ).
tff(c_191773,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_191751]) ).
tff(c_190298,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_190310,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_190298,c_4]) ).
tff(c_191274,plain,
multiply(inverse(sk_c8),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_190310,c_191226]) ).
tff(c_191714,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_191709,c_191274]) ).
tff(c_191722,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_191714]) ).
tff(c_191719,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191709,c_190298]) ).
tff(c_191787,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191722,c_191719]) ).
tff(c_191788,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_191773,c_191787]) ).
tff(c_191789,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_191517]) ).
tff(c_191807,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_191789]) ).
tff(c_191885,plain,
! [X1_1162] :
( ( multiply(X1_1162,identity) != identity )
| ( inverse(X1_1162) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_191869,c_191870,c_191869,c_191807]) ).
tff(c_191907,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_191885]) ).
tff(c_191301,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_191226]) ).
tff(c_191824,plain,
inverse(sk_c1) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_191808,c_190298]) ).
tff(c_191933,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191870,c_191824]) ).
tff(c_191298,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_191226]) ).
tff(c_191937,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_191933,c_191298]) ).
tff(c_191946,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191301,c_191937]) ).
tff(c_191948,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191946,c_191933]) ).
tff(c_191951,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_191907,c_191948]) ).
tff(c_191952,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_191789]) ).
tff(c_191992,plain,
! [X5_1163] :
( ( inverse(X5_1163) != sk_c6 )
| ( multiply(X5_1163,sk_c6) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_191971,c_191971,c_191952]) ).
tff(c_192008,plain,
( ( inverse(identity) != sk_c6 )
| ( sk_c8 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_191992]) ).
tff(c_192025,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_192014,c_191986,c_191986,c_192008]) ).
tff(c_192015,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191986,c_191971]) ).
tff(c_191969,plain,
inverse(sk_c1) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_191953,c_190298]) ).
tff(c_192031,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_192015,c_191969]) ).
tff(c_192035,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_192031,c_191298]) ).
tff(c_192044,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_191301,c_192035]) ).
tff(c_192046,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_192044,c_192031]) ).
tff(c_192049,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_192025,c_192046]) ).
tff(c_192051,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_192073,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_192051,c_24]) ).
tff(c_192050,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_192055,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_192050,c_4]) ).
tff(c_192116,plain,
! [Z_1166] : ( multiply(sk_c7,multiply(sk_c5,Z_1166)) = multiply(identity,Z_1166) ),
inference(superposition,[status(thm),theory(equality)],[c_192055,c_192095]) ).
tff(c_192194,plain,
! [Z_1169] : ( multiply(sk_c7,multiply(sk_c5,Z_1169)) = Z_1169 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192116]) ).
tff(c_192206,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_192073,c_192194]) ).
tff(c_192068,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_192051,c_20]) ).
tff(c_192122,plain,
! [Z_1166] : ( multiply(sk_c8,multiply(sk_c4,Z_1166)) = multiply(identity,Z_1166) ),
inference(superposition,[status(thm),theory(equality)],[c_190277,c_192095]) ).
tff(c_192141,plain,
! [Z_1167] : ( multiply(sk_c8,multiply(sk_c4,Z_1167)) = Z_1167 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192122]) ).
tff(c_192153,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_192068,c_192141]) ).
tff(c_192131,plain,
! [Z_1166] : ( multiply(sk_c7,multiply(sk_c8,Z_1166)) = multiply(sk_c6,Z_1166) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_192095]) ).
tff(c_192179,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_192153,c_192131]) ).
tff(c_193074,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192206,c_192179]) ).
tff(c_193122,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_193074,c_193104]) ).
tff(c_193183,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_193122]) ).
tff(c_193190,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_193183,c_193183,c_192153]) ).
tff(c_193198,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193190]) ).
tff(c_193197,plain,
multiply(sk_c7,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_193183,c_8]) ).
tff(c_193216,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_193198,c_193197]) ).
tff(c_193226,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193216]) ).
tff(c_192239,plain,
! [X3_1171] :
( ( inverse(X3_1171) != sk_c8 )
| ( multiply(X3_1171,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_192253,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_192239]) ).
tff(c_192264,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_192253]) ).
tff(c_192231,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192206,c_192179]) ).
tff(c_192265,plain,
! [X_1172,Z_1173] : ( multiply(inverse(X_1172),multiply(X_1172,Z_1173)) = Z_1173 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192125]) ).
tff(c_192283,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_192231,c_192265]) ).
tff(c_192344,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_192283]) ).
tff(c_192354,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_192344,c_192344,c_192153]) ).
tff(c_192362,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192354]) ).
tff(c_192364,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_192264,c_192362]) ).
tff(c_192366,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_192253]) ).
tff(c_192260,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_192239]) ).
tff(c_192263,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_192260]) ).
tff(c_192367,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_192366,c_192263]) ).
tff(c_192371,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192366,c_192366,c_192206]) ).
tff(c_192384,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192371]) ).
tff(c_192417,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_192367,c_192384]) ).
tff(c_192419,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_192260]) ).
tff(c_192499,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_192419,c_192253]) ).
tff(c_192500,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_192499]) ).
tff(c_192423,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192419,c_192419,c_192206]) ).
tff(c_192535,plain,
! [X_1175,Z_1176] : ( multiply(inverse(X_1175),multiply(X_1175,Z_1176)) = Z_1176 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192125]) ).
tff(c_192559,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_192423,c_192535]) ).
tff(c_192606,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_192559]) ).
tff(c_192608,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_192500,c_192606]) ).
tff(c_192610,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_192499]) ).
tff(c_192257,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_192239]) ).
tff(c_192262,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_192257]) ).
tff(c_192420,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192419,c_192262]) ).
tff(c_192620,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_192610,c_192420]) ).
tff(c_192622,plain,
multiply(identity,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_192610,c_192610,c_192231]) ).
tff(c_192816,plain,
multiply(inverse(identity),identity) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_192622,c_192139]) ).
tff(c_192828,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_192816]) ).
tff(c_192830,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_192620,c_192828]) ).
tff(c_192832,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_192257]) ).
tff(c_192836,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_192832,c_192832,c_192153]) ).
tff(c_192844,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192206,c_192836]) ).
tff(c_192850,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192844,c_192832]) ).
tff(c_192831,plain,
inverse(identity) != sk_c8,
inference(splitRight,[status(thm)],[c_192257]) ).
tff(c_192878,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192850,c_192831]) ).
tff(c_192138,plain,
! [Z_1166] : ( multiply(sk_c8,multiply(sk_c4,Z_1166)) = Z_1166 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_192122]) ).
tff(c_192838,plain,
! [Z_1166] : ( multiply(sk_c7,multiply(sk_c4,Z_1166)) = Z_1166 ),
inference(demodulation,[status(thm),theory(equality)],[c_192832,c_192138]) ).
tff(c_192950,plain,
! [Z_1166] : ( multiply(sk_c6,multiply(sk_c4,Z_1166)) = Z_1166 ),
inference(demodulation,[status(thm),theory(equality)],[c_192844,c_192838]) ).
tff(c_192113,plain,
! [Z_1166] : ( multiply(sk_c4,multiply(sk_c7,Z_1166)) = multiply(sk_c8,Z_1166) ),
inference(superposition,[status(thm),theory(equality)],[c_192068,c_192095]) ).
tff(c_192978,plain,
! [Z_1182] : ( multiply(sk_c4,multiply(sk_c6,Z_1182)) = multiply(sk_c6,Z_1182) ),
inference(demodulation,[status(thm),theory(equality)],[c_192850,c_192844,c_192113]) ).
tff(c_192996,plain,
! [Z_1166] : ( multiply(sk_c6,multiply(sk_c4,Z_1166)) = multiply(sk_c4,Z_1166) ),
inference(superposition,[status(thm),theory(equality)],[c_192950,c_192978]) ).
tff(c_193013,plain,
! [Z_1166] : ( multiply(sk_c4,Z_1166) = Z_1166 ),
inference(demodulation,[status(thm),theory(equality)],[c_192950,c_192996]) ).
tff(c_193037,plain,
! [Z_1184] : ( multiply(sk_c6,Z_1184) = Z_1184 ),
inference(demodulation,[status(thm),theory(equality)],[c_193013,c_192950]) ).
tff(c_192859,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_192844,c_190285]) ).
tff(c_192897,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_192859,c_4]) ).
tff(c_193043,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_193037,c_192897]) ).
tff(c_193069,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_193043,c_192859]) ).
tff(c_193072,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_192878,c_193069]) ).
tff(c_193073,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_193083,plain,
! [X2_1185] :
( ( multiply(X2_1185,sk_c6) != sk_c7 )
| ( inverse(X2_1185) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_193073]) ).
tff(c_193090,plain,
inverse(sk_c5) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_192073,c_193083]) ).
tff(c_193102,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_192050,c_193090]) ).
tff(c_193103,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_193073]) ).
tff(c_193257,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,identity) != identity )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( multiply(X5_6,identity) != identity )
| ( inverse(X4_10) != identity )
| ( multiply(X4_10,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_193226,c_193198,c_193198,c_193198,c_193183,c_193198,c_193183,c_193198,c_193183,c_193103]) ).
tff(c_193258,plain,
! [X4_10] :
( ( inverse(X4_10) != identity )
| ( multiply(X4_10,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_193257]) ).
tff(c_193697,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_193432,c_193258]) ).
tff(c_193222,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_193198,c_192050]) ).
tff(c_193253,plain,
multiply(identity,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_193222,c_4]) ).
tff(c_193272,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_193253,c_192139]) ).
tff(c_193284,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_193272]) ).
tff(c_193288,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_193284,c_193222]) ).
tff(c_193699,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_193697,c_193288]) ).
tff(c_193700,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( multiply(X5_6,identity) != identity )
| ( multiply(X1_8,identity) != identity )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_193257]) ).
tff(c_216253,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_193895,c_193895,c_193700]) ).
tff(c_216256,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_216253]) ).
tff(c_193224,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_193198,c_190285]) ).
tff(c_193707,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_193224,c_4]) ).
tff(c_193733,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_193707,c_192139]) ).
tff(c_193745,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_193733]) ).
tff(c_193749,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_193745,c_193224]) ).
tff(c_216258,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216256,c_193749]) ).
tff(c_216260,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_216253]) ).
tff(c_216262,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216260,c_193749]) ).
tff(c_216264,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_216302,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_216264,c_40]) ).
tff(c_216263,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_216268,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_216263,c_4]) ).
tff(c_216345,plain,
! [Z_1371] : ( multiply(sk_c7,multiply(sk_c5,Z_1371)) = multiply(identity,Z_1371) ),
inference(superposition,[status(thm),theory(equality)],[c_216268,c_216321]) ).
tff(c_216367,plain,
! [Z_1372] : ( multiply(sk_c7,multiply(sk_c5,Z_1372)) = Z_1372 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216345]) ).
tff(c_216379,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_216302,c_216367]) ).
tff(c_216282,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_216264,c_36]) ).
tff(c_216348,plain,
! [Z_1371] : ( multiply(sk_c8,multiply(sk_c4,Z_1371)) = multiply(identity,Z_1371) ),
inference(superposition,[status(thm),theory(equality)],[c_190277,c_216321]) ).
tff(c_216390,plain,
! [Z_1373] : ( multiply(sk_c8,multiply(sk_c4,Z_1373)) = Z_1373 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216348]) ).
tff(c_216402,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_216282,c_216390]) ).
tff(c_216357,plain,
! [Z_1371] : ( multiply(sk_c7,multiply(sk_c8,Z_1371)) = multiply(sk_c6,Z_1371) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_216321]) ).
tff(c_216431,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_216402,c_216357]) ).
tff(c_216437,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216379,c_216431]) ).
tff(c_217283,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_216437,c_217256]) ).
tff(c_217339,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_217283]) ).
tff(c_217359,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_217339,c_217339,c_216402]) ).
tff(c_217364,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_217359]) ).
tff(c_217837,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_217364,c_217364,c_216379]) ).
tff(c_217846,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_217837]) ).
tff(c_217539,plain,
! [X_1395,Z_1396] : ( multiply(inverse(inverse(X_1395)),Z_1396) = multiply(X_1395,Z_1396) ),
inference(superposition,[status(thm),theory(equality)],[c_216365,c_217256]) ).
tff(c_217546,plain,
! [X_1395] : ( multiply(X_1395,identity) = X_1395 ),
inference(superposition,[status(thm),theory(equality)],[c_217539,c_217328]) ).
tff(c_217373,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_217364,c_217364,c_216379]) ).
tff(c_217381,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_217373]) ).
tff(c_216488,plain,
! [X3_1376] :
( ( inverse(X3_1376) != sk_c8 )
| ( multiply(X3_1376,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_216502,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_216488]) ).
tff(c_216513,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_216502]) ).
tff(c_216514,plain,
! [X_1377,Z_1378] : ( multiply(inverse(X_1377),multiply(X_1377,Z_1378)) = Z_1378 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216351]) ).
tff(c_216541,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_216437,c_216514]) ).
tff(c_216597,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_216541]) ).
tff(c_216620,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_216597,c_216597,c_216402]) ).
tff(c_216625,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216620]) ).
tff(c_216627,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216513,c_216625]) ).
tff(c_216629,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_216502]) ).
tff(c_216509,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_216488]) ).
tff(c_216512,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_216509]) ).
tff(c_216666,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_216629,c_216512]) ).
tff(c_216672,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216629,c_216629,c_216379]) ).
tff(c_216683,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216672]) ).
tff(c_216688,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216666,c_216683]) ).
tff(c_216690,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_216509]) ).
tff(c_216506,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_216488]) ).
tff(c_216511,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_216506]) ).
tff(c_216691,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216690,c_216511]) ).
tff(c_216702,plain,
inverse(sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216690,c_216263]) ).
tff(c_216713,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_216702,c_4]) ).
tff(c_216336,plain,
! [Z_1371] : ( multiply(sk_c5,multiply(sk_c6,Z_1371)) = multiply(sk_c7,Z_1371) ),
inference(superposition,[status(thm),theory(equality)],[c_216302,c_216321]) ).
tff(c_216762,plain,
! [Z_1380] : ( multiply(sk_c5,multiply(sk_c6,Z_1380)) = multiply(sk_c6,Z_1380) ),
inference(demodulation,[status(thm),theory(equality)],[c_216690,c_216336]) ).
tff(c_216777,plain,
multiply(sk_c6,sk_c5) = multiply(sk_c5,identity),
inference(superposition,[status(thm),theory(equality)],[c_216713,c_216762]) ).
tff(c_216788,plain,
multiply(sk_c5,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_216713,c_216777]) ).
tff(c_216794,plain,
! [Z_5] : ( multiply(sk_c5,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_216788,c_6]) ).
tff(c_216797,plain,
! [Z_5] : ( multiply(sk_c5,Z_5) = Z_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_216794]) ).
tff(c_216363,plain,
! [Z_1371] : ( multiply(sk_c7,multiply(sk_c5,Z_1371)) = Z_1371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216345]) ).
tff(c_216697,plain,
! [Z_1371] : ( multiply(sk_c6,multiply(sk_c5,Z_1371)) = Z_1371 ),
inference(demodulation,[status(thm),theory(equality)],[c_216690,c_216363]) ).
tff(c_216820,plain,
! [Z_1382] : ( multiply(sk_c6,Z_1382) = Z_1382 ),
inference(demodulation,[status(thm),theory(equality)],[c_216797,c_216697]) ).
tff(c_216829,plain,
sk_c8 = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_216820,c_216437]) ).
tff(c_216844,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216691,c_216829]) ).
tff(c_216846,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_216506]) ).
tff(c_216851,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_216846,c_216846,c_216402]) ).
tff(c_216860,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216379,c_216851]) ).
tff(c_216874,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216860,c_216846]) ).
tff(c_216974,plain,
( ( inverse(inverse(sk_c6)) != sk_c6 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_216860,c_216874,c_216874,c_216502]) ).
tff(c_216975,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_216974]) ).
tff(c_216876,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216860,c_216860,c_216379]) ).
tff(c_217034,plain,
! [X_1386,Z_1387] : ( multiply(inverse(X_1386),multiply(X_1386,Z_1387)) = Z_1387 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_216351]) ).
tff(c_217064,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_216876,c_217034]) ).
tff(c_217101,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_217064]) ).
tff(c_217103,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216975,c_217101]) ).
tff(c_217105,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_216974]) ).
tff(c_216845,plain,
inverse(identity) != sk_c8,
inference(splitRight,[status(thm)],[c_216506]) ).
tff(c_216909,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216874,c_216845]) ).
tff(c_217116,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_217105,c_216909]) ).
tff(c_216858,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_216846,c_190272]) ).
tff(c_216873,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216860,c_216858]) ).
tff(c_217115,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_217105,c_216873]) ).
tff(c_217158,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_217115,c_4]) ).
tff(c_217226,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_217158,c_216365]) ).
tff(c_217238,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_217226]) ).
tff(c_217242,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_217238,c_217115]) ).
tff(c_217246,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_217116,c_217242]) ).
tff(c_217247,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c8 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_217370,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != identity )
| ( multiply(X1_8,sk_c7) != identity )
| ( inverse(X1_8) != identity )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_217339,c_217339,c_217339,c_217247]) ).
tff(c_217371,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_217370]) ).
tff(c_217802,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_217364,c_217546,c_217381,c_217364,c_217371]) ).
tff(c_217376,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_217364,c_216268]) ).
tff(c_217446,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_217376,c_216365]) ).
tff(c_217458,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_217446]) ).
tff(c_217378,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_217364,c_216263]) ).
tff(c_217463,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_217458,c_217378]) ).
tff(c_217804,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_217802,c_217463]) ).
tff(c_217805,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != identity )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != identity )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_217370]) ).
tff(c_292127,plain,
! [X1_8,X5_6,X4_10] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_218046,c_217846,c_217364,c_217364,c_218046,c_217364,c_217364,c_218046,c_217364,c_217805]) ).
tff(c_292129,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_292127]) ).
tff(c_217840,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_217364,c_216268]) ).
tff(c_217911,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_217840,c_216365]) ).
tff(c_217923,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_217911]) ).
tff(c_217842,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_217364,c_216263]) ).
tff(c_217928,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_217923,c_217842]) ).
tff(c_292131,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_292129,c_217928]) ).
tff(c_292132,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_292127]) ).
tff(c_292134,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_292132]) ).
tff(c_292136,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_292134,c_217928]) ).
tff(c_293685,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_292132]) ).
tff(c_293687,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_293685,c_217928]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP314-1 : TPTP v9.0.0. Released v2.5.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n003.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Apr 7 21:41:33 EDT 2025
% 0.14/0.34 % CPUTime :
% 45.39/30.97 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 45.70/31.11
% 45.70/31.11 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------