%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP350-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:26:01 PM UTC 2025
% Result : Unsatisfiable 85.09s 66.70s
% Output : CNFRefutation 85.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 46
% Syntax : Number of formulae : 785 ( 657 unt; 0 typ; 0 def)
% Number of atoms : 1101 (1071 equ)
% Maximal formula atoms : 17 ( 1 avg)
% Number of connectives : 650 ( 334 ~; 316 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 406 ( 406 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c11 > sk_c10 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c10,type,
sk_c10: $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c11,type,
sk_c11: $i ).
tff(sk_c9,type,
sk_c9: $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_239,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_269,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_200,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_179,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_323,axiom,
! [X5,X6,X3,X7,X1,X2,X8,X4] :
( ( multiply(sk_c10,sk_c11) != sk_c9 )
| ( inverse(sk_c10) != sk_c9 )
| ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( multiply(X3,sk_c10) != sk_c11 )
| ( inverse(X4) != sk_c10 )
| ( multiply(X4,sk_c9) != sk_c10 )
| ( multiply(X1,sk_c11) != sk_c10 )
| ( inverse(X1) != sk_c11 )
| ( multiply(X2,sk_c10) != sk_c9 )
| ( inverse(X2) != sk_c10 )
| ( multiply(X5,X6) != sk_c11 )
| ( inverse(X5) != X6 )
| ( multiply(X6,sk_c10) != sk_c11 )
| ( inverse(X7) != X8 )
| ( inverse(X8) != X6 )
| ( multiply(X7,X6) != X8 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_254,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_251,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_194,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_191,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_188,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c10,sk_c11) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_221,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_224,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_227,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_230,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_215,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_218,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c3) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_236,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_233,axiom,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_371770,plain,
! [X_1500,Y_1501,Z_1502] : ( multiply(multiply(X_1500,Y_1501),Z_1502) = multiply(X_1500,multiply(Y_1501,Z_1502)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_371821,plain,
! [X_2,Z_1502] : ( multiply(inverse(X_2),multiply(X_2,Z_1502)) = multiply(identity,Z_1502) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_371770]) ).
tff(c_371836,plain,
! [X_2,Z_1502] : ( multiply(inverse(X_2),multiply(X_2,Z_1502)) = Z_1502 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371821]) ).
tff(c_374883,plain,
! [X_1557,Z_1558] : ( multiply(inverse(X_1557),multiply(X_1557,Z_1558)) = Z_1558 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371821]) ).
tff(c_375292,plain,
! [X_1562,Z_1563] : ( multiply(inverse(inverse(X_1562)),Z_1563) = multiply(X_1562,Z_1563) ),
inference(superposition,[status(thm),theory(equality)],[c_371836,c_374883]) ).
tff(c_374922,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_374883]) ).
tff(c_375299,plain,
! [X_1562] : ( multiply(X_1562,identity) = X_1562 ),
inference(superposition,[status(thm),theory(equality)],[c_375292,c_374922]) ).
tff(c_28,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_371691,plain,
inverse(sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_371695,plain,
multiply(sk_c9,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_371691,c_4]) ).
tff(c_51517,plain,
inverse(sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_51521,plain,
multiply(sk_c9,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_51517,c_4]) ).
tff(c_124,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_165,plain,
inverse(sk_c2) = sk_c10,
inference(splitLeft,[status(thm)],[c_124]) ).
tff(c_169,plain,
multiply(sk_c10,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_165,c_4]) ).
tff(c_51595,plain,
! [X_468,Y_469,Z_470] : ( multiply(multiply(X_468,Y_469),Z_470) = multiply(X_468,multiply(Y_469,Z_470)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_51622,plain,
! [Z_470] : ( multiply(sk_c9,multiply(sk_c10,Z_470)) = multiply(identity,Z_470) ),
inference(superposition,[status(thm),theory(equality)],[c_51521,c_51595]) ).
tff(c_51663,plain,
! [Z_471] : ( multiply(sk_c9,multiply(sk_c10,Z_471)) = Z_471 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51622]) ).
tff(c_51678,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_169,c_51663]) ).
tff(c_44,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_196,plain,
inverse(sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_200,plain,
multiply(sk_c9,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_196,c_4]) ).
tff(c_49645,plain,
! [X_435,Y_436,Z_437] : ( multiply(multiply(X_435,Y_436),Z_437) = multiply(X_435,multiply(Y_436,Z_437)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_49696,plain,
! [Z_437] : ( multiply(sk_c9,multiply(sk_c10,Z_437)) = multiply(identity,Z_437) ),
inference(superposition,[status(thm),theory(equality)],[c_200,c_49645]) ).
tff(c_49723,plain,
! [Z_438] : ( multiply(sk_c9,multiply(sk_c10,Z_438)) = Z_438 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49696]) ).
tff(c_49741,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_169,c_49723]) ).
tff(c_46654,plain,
! [X_387,Y_388,Z_389] : ( multiply(multiply(X_387,Y_388),Z_389) = multiply(X_387,multiply(Y_388,Z_389)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_46708,plain,
! [Z_389] : ( multiply(sk_c9,multiply(sk_c10,Z_389)) = multiply(identity,Z_389) ),
inference(superposition,[status(thm),theory(equality)],[c_200,c_46654]) ).
tff(c_46735,plain,
! [Z_390] : ( multiply(sk_c9,multiply(sk_c10,Z_390)) = Z_390 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46708]) ).
tff(c_46753,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_169,c_46735]) ).
tff(c_144,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_269]) ).
tff(c_221,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_144]) ).
tff(c_45505,plain,
! [X_369,Y_370,Z_371] : ( multiply(multiply(X_369,Y_370),Z_371) = multiply(X_369,multiply(Y_370,Z_371)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_45565,plain,
! [Z_371] : ( multiply(sk_c10,multiply(sk_c2,Z_371)) = multiply(identity,Z_371) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_45505]) ).
tff(c_45642,plain,
! [Z_373] : ( multiply(sk_c10,multiply(sk_c2,Z_373)) = Z_373 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45565]) ).
tff(c_45660,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_221,c_45642]) ).
tff(c_45559,plain,
! [Z_371] : ( multiply(sk_c9,multiply(sk_c10,Z_371)) = multiply(identity,Z_371) ),
inference(superposition,[status(thm),theory(equality)],[c_200,c_45505]) ).
tff(c_45581,plain,
! [Z_371] : ( multiply(sk_c9,multiply(sk_c10,Z_371)) = Z_371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45559]) ).
tff(c_45667,plain,
multiply(sk_c9,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_45660,c_45581]) ).
tff(c_24,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_45391,plain,
multiply(sk_c10,sk_c11) = sk_c9,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_45586,plain,
! [Z_372] : ( multiply(sk_c9,multiply(sk_c10,Z_372)) = Z_372 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45559]) ).
tff(c_45598,plain,
multiply(sk_c9,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_45391,c_45586]) ).
tff(c_45699,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45667,c_45598]) ).
tff(c_98,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_216,plain,
multiply(sk_c1,sk_c10) = sk_c11,
inference(splitLeft,[status(thm)],[c_98]) ).
tff(c_84,plain,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_177,plain,
inverse(sk_c1) = sk_c11,
inference(splitLeft,[status(thm)],[c_84]) ).
tff(c_181,plain,
multiply(sk_c11,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_177,c_4]) ).
tff(c_44881,plain,
! [X_359,Y_360,Z_361] : ( multiply(multiply(X_359,Y_360),Z_361) = multiply(X_359,multiply(Y_360,Z_361)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_44938,plain,
! [Z_361] : ( multiply(sk_c11,multiply(sk_c1,Z_361)) = multiply(identity,Z_361) ),
inference(superposition,[status(thm),theory(equality)],[c_181,c_44881]) ).
tff(c_45006,plain,
! [Z_363] : ( multiply(sk_c11,multiply(sk_c1,Z_363)) = Z_363 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44938]) ).
tff(c_45018,plain,
multiply(sk_c11,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_216,c_45006]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_222,plain,
multiply(sk_c9,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_45063,plain,
! [Z_365] : ( multiply(sk_c9,multiply(sk_c11,Z_365)) = multiply(sk_c10,Z_365) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_44881]) ).
tff(c_45075,plain,
multiply(sk_c9,sk_c10) = multiply(sk_c10,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_45018,c_45063]) ).
tff(c_45088,plain,
multiply(sk_c10,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_45075]) ).
tff(c_284,plain,
! [X_16,Y_17,Z_18] : ( multiply(multiply(X_16,Y_17),Z_18) = multiply(X_16,multiply(Y_17,Z_18)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_314,plain,
! [Z_18] : ( multiply(sk_c11,multiply(sk_c1,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_181,c_284]) ).
tff(c_488,plain,
! [Z_23] : ( multiply(sk_c11,multiply(sk_c1,Z_23)) = Z_23 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_314]) ).
tff(c_500,plain,
multiply(sk_c11,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_216,c_488]) ).
tff(c_22,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_238,plain,
multiply(sk_c10,sk_c11) = sk_c9,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_511,plain,
! [Z_24] : ( multiply(sk_c1,multiply(sk_c10,Z_24)) = multiply(sk_c11,Z_24) ),
inference(superposition,[status(thm),theory(equality)],[c_216,c_284]) ).
tff(c_526,plain,
multiply(sk_c11,sk_c11) = multiply(sk_c1,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_238,c_511]) ).
tff(c_533,plain,
multiply(sk_c1,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_500,c_526]) ).
tff(c_329,plain,
! [Z_18] : ( multiply(sk_c11,multiply(sk_c1,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_314]) ).
tff(c_537,plain,
multiply(sk_c11,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_533,c_329]) ).
tff(c_317,plain,
! [Z_18] : ( multiply(sk_c10,multiply(sk_c2,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_284]) ).
tff(c_551,plain,
! [Z_25] : ( multiply(sk_c10,multiply(sk_c2,Z_25)) = Z_25 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_317]) ).
tff(c_569,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_221,c_551]) ).
tff(c_308,plain,
! [Z_18] : ( multiply(sk_c1,multiply(sk_c10,Z_18)) = multiply(sk_c11,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_216,c_284]) ).
tff(c_576,plain,
multiply(sk_c11,sk_c10) = multiply(sk_c1,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_569,c_308]) ).
tff(c_585,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_537,c_533,c_576]) ).
tff(c_597,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_585,c_196]) ).
tff(c_21308,plain,
multiply(sk_c10,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_597,c_4]) ).
tff(c_311,plain,
! [Z_18] : ( multiply(sk_c9,multiply(sk_c10,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_200,c_284]) ).
tff(c_328,plain,
! [Z_18] : ( multiply(sk_c9,multiply(sk_c10,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_311]) ).
tff(c_579,plain,
multiply(sk_c9,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_569,c_328]) ).
tff(c_21312,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_585,c_585,c_579]) ).
tff(c_21324,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21308,c_21312]) ).
tff(c_320,plain,
! [X_2,Z_18] : ( multiply(inverse(X_2),multiply(X_2,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_284]) ).
tff(c_331,plain,
! [X_2,Z_18] : ( multiply(inverse(X_2),multiply(X_2,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_320]) ).
tff(c_21382,plain,
! [X_188,Z_189] : ( multiply(inverse(X_188),multiply(X_188,Z_189)) = Z_189 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_320]) ).
tff(c_21583,plain,
! [X_191,Z_192] : ( multiply(inverse(inverse(X_191)),Z_192) = multiply(X_191,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_331,c_21382]) ).
tff(c_21421,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_21382]) ).
tff(c_21590,plain,
! [X_191] : ( multiply(X_191,identity) = X_191 ),
inference(superposition,[status(thm),theory(equality)],[c_21583,c_21421]) ).
tff(c_593,plain,
multiply(sk_c10,sk_c11) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_585,c_238]) ).
tff(c_21488,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21324,c_2,c_21324,c_593]) ).
tff(c_607,plain,
multiply(sk_c10,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_597,c_4]) ).
tff(c_611,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_585,c_585,c_579]) ).
tff(c_634,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_607,c_611]) ).
tff(c_648,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_634,c_634,c_597]) ).
tff(c_689,plain,
! [X_26,Z_27] : ( multiply(inverse(X_26),multiply(X_26,Z_27)) = Z_27 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_320]) ).
tff(c_812,plain,
! [X_29,Z_30] : ( multiply(inverse(inverse(X_29)),Z_30) = multiply(X_29,Z_30) ),
inference(superposition,[status(thm),theory(equality)],[c_689,c_331]) ).
tff(c_716,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_689]) ).
tff(c_819,plain,
! [X_29] : ( multiply(X_29,identity) = X_29 ),
inference(superposition,[status(thm),theory(equality)],[c_812,c_716]) ).
tff(c_833,plain,
! [X_29] : ( multiply(X_29,inverse(X_29)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_812,c_4]) ).
tff(c_681,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_634,c_2,c_634,c_593]) ).
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_1075,plain,
! [X_36,Y_37,Z_38] : ( multiply(inverse(multiply(X_36,Y_37)),multiply(X_36,multiply(Y_37,Z_38))) = Z_38 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_689]) ).
tff(c_1154,plain,
! [X_36,X_2] : ( multiply(inverse(multiply(X_36,inverse(X_2))),multiply(X_36,identity)) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1075]) ).
tff(c_1187,plain,
! [X_36,X_2] : ( multiply(inverse(multiply(X_36,inverse(X_2))),X_36) = X_2 ),
inference(demodulation,[status(thm),theory(equality)],[c_819,c_1154]) ).
tff(c_855,plain,
! [X_31] : ( multiply(X_31,identity) = X_31 ),
inference(superposition,[status(thm),theory(equality)],[c_812,c_716]) ).
tff(c_692,plain,
! [X_26,Z_27] : ( multiply(inverse(inverse(X_26)),Z_27) = multiply(X_26,Z_27) ),
inference(superposition,[status(thm),theory(equality)],[c_689,c_331]) ).
tff(c_862,plain,
! [X_26] : ( inverse(inverse(X_26)) = multiply(X_26,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_855,c_692]) ).
tff(c_907,plain,
! [X_26] : ( inverse(inverse(X_26)) = X_26 ),
inference(demodulation,[status(thm),theory(equality)],[c_819,c_862]) ).
tff(c_1196,plain,
! [X_39,X_40] : ( multiply(inverse(multiply(X_39,inverse(X_40))),X_39) = X_40 ),
inference(demodulation,[status(thm),theory(equality)],[c_819,c_1154]) ).
tff(c_826,plain,
! [X_29,Z_18] : ( multiply(X_29,multiply(inverse(X_29),Z_18)) = Z_18 ),
inference(superposition,[status(thm),theory(equality)],[c_812,c_331]) ).
tff(c_1269,plain,
! [X_41,X_42] : ( multiply(multiply(X_41,inverse(X_42)),X_42) = X_41 ),
inference(superposition,[status(thm),theory(equality)],[c_1196,c_826]) ).
tff(c_1360,plain,
! [X_43,X_44] : ( multiply(multiply(X_43,X_44),inverse(X_44)) = X_43 ),
inference(superposition,[status(thm),theory(equality)],[c_907,c_1269]) ).
tff(c_1399,plain,
! [X_36,X_2] : ( inverse(multiply(X_36,inverse(X_2))) = multiply(X_2,inverse(X_36)) ),
inference(superposition,[status(thm),theory(equality)],[c_1187,c_1360]) ).
tff(c_370,plain,
! [Z_20] : ( multiply(sk_c11,multiply(sk_c1,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_314]) ).
tff(c_382,plain,
multiply(sk_c11,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_216,c_370]) ).
tff(c_393,plain,
! [Z_21] : ( multiply(sk_c9,multiply(sk_c11,Z_21)) = multiply(sk_c10,Z_21) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_284]) ).
tff(c_405,plain,
multiply(sk_c9,sk_c10) = multiply(sk_c10,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_382,c_393]) ).
tff(c_415,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_238,c_200,c_405]) ).
tff(c_333,plain,
! [Z_19] : ( multiply(sk_c9,multiply(sk_c10,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_311]) ).
tff(c_345,plain,
multiply(sk_c9,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_238,c_333]) ).
tff(c_419,plain,
multiply(identity,identity) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_415,c_415,c_345]) ).
tff(c_427,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_419]) ).
tff(c_432,plain,
multiply(identity,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_427,c_427,c_382]) ).
tff(c_437,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_432]) ).
tff(c_425,plain,
inverse(sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_415,c_196]) ).
tff(c_452,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_437,c_425]) ).
tff(c_148,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( inverse(sk_c10) != sk_c9 )
| ( multiply(sk_c10,sk_c11) != sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_360,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_238,c_196,c_222,c_148]) ).
tff(c_361,plain,
! [X3_8] :
( ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_360]) ).
tff(c_462,plain,
! [X3_22] :
( ( multiply(X3_22,identity) != identity )
| ( inverse(X3_22) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_427,c_437,c_427,c_361]) ).
tff(c_470,plain,
inverse(inverse(identity)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_462]) ).
tff(c_478,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_452,c_452,c_470]) ).
tff(c_479,plain,
! [X5_6,X4_13,X1_10,X7_9,X2_11] :
( ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_360]) ).
tff(c_602,plain,
! [X5_6,X4_13,X1_10,X7_9,X2_11] :
( ( multiply(X4_13,sk_c10) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_585,c_585,c_479]) ).
tff(c_603,plain,
! [X7_9,X5_6] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_602]) ).
tff(c_21191,plain,
! [X5_185,X7_186] :
( ( multiply(X5_185,inverse(X7_186)) != inverse(X5_185) )
| ( multiply(X7_186,inverse(X5_185)) != inverse(X7_186) )
| ( inverse(X5_185) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_833,c_681,c_819,c_681,c_634,c_1399,c_603]) ).
tff(c_21255,plain,
! [X7_186] :
( ( inverse(identity) != inverse(X7_186) )
| ( multiply(X7_186,inverse(identity)) != inverse(X7_186) )
| ( inverse(identity) != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_21191]) ).
tff(c_21282,plain,
! [X7_187] :
( ( inverse(X7_187) != identity )
| ( inverse(X7_187) != X7_187 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_648,c_819,c_648,c_648,c_21255]) ).
tff(c_21294,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_648,c_21282]) ).
tff(c_21303,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_648,c_21294]) ).
tff(c_21304,plain,
! [X2_11,X1_10,X4_13] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,sk_c10) != sk_c10 )
| ( inverse(X4_13) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_602]) ).
tff(c_43625,plain,
! [X2_11,X1_10,X4_13] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( identity != X4_13 )
| ( inverse(X4_13) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21324,c_21590,c_21324,c_21324,c_21590,c_21488,c_21324,c_21488,c_21590,c_21324,c_21324,c_21324,c_21304]) ).
tff(c_43627,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_43625]) ).
tff(c_21337,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21324,c_21324,c_597]) ).
tff(c_43629,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43627,c_21337]) ).
tff(c_43630,plain,
! [X1_10,X2_11] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_43625]) ).
tff(c_43632,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_43630]) ).
tff(c_43634,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43632,c_21337]) ).
tff(c_44760,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_43630]) ).
tff(c_44762,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44760,c_21337]) ).
tff(c_44764,plain,
multiply(sk_c10,sk_c11) != sk_c9,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_45118,plain,
sk_c9 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_45088,c_44764]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_44789,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_44764,c_10]) ).
tff(c_8,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_44864,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_44764,c_8]) ).
tff(c_44944,plain,
! [X_2,Z_361] : ( multiply(inverse(X_2),multiply(X_2,Z_361)) = multiply(identity,Z_361) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_44881]) ).
tff(c_45130,plain,
! [X_366,Z_367] : ( multiply(inverse(X_366),multiply(X_366,Z_367)) = Z_367 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44944]) ).
tff(c_45193,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_44864,c_45130]) ).
tff(c_45264,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_44789,c_45193]) ).
tff(c_44960,plain,
! [X_2,Z_361] : ( multiply(inverse(X_2),multiply(X_2,Z_361)) = Z_361 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44944]) ).
tff(c_45341,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_45264,c_44960]) ).
tff(c_45350,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_45341]) ).
tff(c_44941,plain,
! [Z_361] : ( multiply(sk_c10,multiply(sk_c2,Z_361)) = multiply(identity,Z_361) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_44881]) ).
tff(c_45031,plain,
! [Z_364] : ( multiply(sk_c10,multiply(sk_c2,Z_364)) = Z_364 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44941]) ).
tff(c_45049,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_221,c_45031]) ).
tff(c_45358,plain,
multiply(identity,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_45350,c_45350,c_45049]) ).
tff(c_45368,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45358]) ).
tff(c_45370,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_45118,c_45368]) ).
tff(c_45372,plain,
multiply(sk_c9,sk_c11) != sk_c10,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_45714,plain,
multiply(sk_c9,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45699,c_45372]) ).
tff(c_45719,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_45714]) ).
tff(c_45604,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_169,c_45586]) ).
tff(c_45371,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_45376,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_45371,c_4]) ).
tff(c_45601,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_45376,c_45586]) ).
tff(c_45623,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_45604,c_45601]) ).
tff(c_52,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_45470,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_45372,c_52]) ).
tff(c_45624,plain,
multiply(sk_c2,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_45623,c_45470]) ).
tff(c_45657,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_45624,c_45642]) ).
tff(c_45568,plain,
! [X_2,Z_371] : ( multiply(inverse(X_2),multiply(X_2,Z_371)) = multiply(identity,Z_371) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_45505]) ).
tff(c_45584,plain,
! [X_2,Z_371] : ( multiply(inverse(X_2),multiply(X_2,Z_371)) = Z_371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45568]) ).
tff(c_45903,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_45657,c_45584]) ).
tff(c_45912,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_196,c_45903]) ).
tff(c_45916,plain,
multiply(identity,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_45912,c_45912,c_45667]) ).
tff(c_45921,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45916]) ).
tff(c_45923,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_45719,c_45921]) ).
tff(c_45925,plain,
multiply(sk_c10,sk_c11) != sk_c9,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_45940,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_45925,c_10]) ).
tff(c_48,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_46007,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_45372,c_48]) ).
tff(c_46045,plain,
! [X_377,Y_378,Z_379] : ( multiply(multiply(X_377,Y_378),Z_379) = multiply(X_377,multiply(Y_378,Z_379)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_46105,plain,
! [X_2,Z_379] : ( multiply(inverse(X_2),multiply(X_2,Z_379)) = multiply(identity,Z_379) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_46045]) ).
tff(c_46214,plain,
! [X_383,Z_384] : ( multiply(inverse(X_383),multiply(X_383,Z_384)) = Z_384 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46105]) ).
tff(c_46259,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_46007,c_46214]) ).
tff(c_46323,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_45940,c_46259]) ).
tff(c_46121,plain,
! [X_2,Z_379] : ( multiply(inverse(X_2),multiply(X_2,Z_379)) = Z_379 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46105]) ).
tff(c_46407,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_46323,c_46121]) ).
tff(c_46413,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_46407]) ).
tff(c_46289,plain,
multiply(inverse(sk_c2),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_221,c_46214]) ).
tff(c_46326,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_165,c_46289]) ).
tff(c_46416,plain,
multiply(identity,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_46413,c_46413,c_46326]) ).
tff(c_46431,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46416]) ).
tff(c_46423,plain,
multiply(identity,sk_c11) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_46413,c_45925]) ).
tff(c_46433,plain,
sk_c9 != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46423]) ).
tff(c_46444,plain,
sk_c11 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_46431,c_46433]) ).
tff(c_18,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_45960,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_45925,c_18]) ).
tff(c_56,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_46001,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_45372,c_56]) ).
tff(c_46262,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_46001,c_46214]) ).
tff(c_46324,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_45960,c_46262]) ).
tff(c_46510,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_46324,c_46121]) ).
tff(c_46516,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_46510]) ).
tff(c_46518,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46444,c_46516]) ).
tff(c_46520,plain,
multiply(sk_c2,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_144]) ).
tff(c_134,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_254]) ).
tff(c_46601,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_46520,c_134]) ).
tff(c_46605,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_46601,c_4]) ).
tff(c_46747,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_46605,c_46735]) ).
tff(c_46772,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_46753,c_46747]) ).
tff(c_132,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_251]) ).
tff(c_46614,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_46520,c_132]) ).
tff(c_46773,plain,
multiply(sk_c2,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_46772,c_46614]) ).
tff(c_46714,plain,
! [Z_389] : ( multiply(sk_c10,multiply(sk_c2,Z_389)) = multiply(identity,Z_389) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_46654]) ).
tff(c_46973,plain,
! [Z_394] : ( multiply(sk_c10,multiply(sk_c2,Z_394)) = Z_394 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46714]) ).
tff(c_46988,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_46773,c_46973]) ).
tff(c_46730,plain,
! [Z_389] : ( multiply(sk_c9,multiply(sk_c10,Z_389)) = Z_389 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46708]) ).
tff(c_46996,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_46988,c_46730]) ).
tff(c_47002,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_46996]) ).
tff(c_47006,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_47002,c_46753]) ).
tff(c_47014,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47006]) ).
tff(c_47005,plain,
multiply(sk_c2,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47002,c_46773]) ).
tff(c_47148,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47014,c_47005]) ).
tff(c_47011,plain,
multiply(sk_c2,identity) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_47002,c_46520]) ).
tff(c_47171,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_47148,c_2,c_47014,c_47011]) ).
tff(c_47173,plain,
multiply(sk_c1,sk_c10) != sk_c11,
inference(splitRight,[status(thm)],[c_98]) ).
tff(c_94,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_49551,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_47173,c_94]) ).
tff(c_49555,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_49551,c_4]) ).
tff(c_49735,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_49555,c_49723]) ).
tff(c_50471,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_49741,c_49735]) ).
tff(c_92,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_49609,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_47173,c_92]) ).
tff(c_50472,plain,
multiply(sk_c2,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_50471,c_49609]) ).
tff(c_49702,plain,
! [Z_437] : ( multiply(sk_c10,multiply(sk_c2,Z_437)) = multiply(identity,Z_437) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_49645]) ).
tff(c_50488,plain,
! [Z_450] : ( multiply(sk_c10,multiply(sk_c2,Z_450)) = Z_450 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49702]) ).
tff(c_50503,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_50472,c_50488]) ).
tff(c_49718,plain,
! [Z_437] : ( multiply(sk_c9,multiply(sk_c10,Z_437)) = Z_437 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49696]) ).
tff(c_50510,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_50503,c_49718]) ).
tff(c_50516,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_50510]) ).
tff(c_50527,plain,
multiply(identity,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_50516,c_200]) ).
tff(c_50612,plain,
sk_c10 = identity,
inference(superposition,[status(thm),theory(equality)],[c_50527,c_2]) ).
tff(c_50521,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50516,c_49741]) ).
tff(c_50530,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50521]) ).
tff(c_47172,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_98]) ).
tff(c_48206,plain,
multiply(sk_c10,sk_c11) = sk_c9,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_48278,plain,
! [X_415,Y_416,Z_417] : ( multiply(multiply(X_415,Y_416),Z_417) = multiply(X_415,multiply(Y_416,Z_417)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_48329,plain,
! [Z_417] : ( multiply(sk_c9,multiply(sk_c10,Z_417)) = multiply(identity,Z_417) ),
inference(superposition,[status(thm),theory(equality)],[c_200,c_48278]) ).
tff(c_48356,plain,
! [Z_418] : ( multiply(sk_c9,multiply(sk_c10,Z_418)) = Z_418 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48329]) ).
tff(c_48368,plain,
multiply(sk_c9,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_48206,c_48356]) ).
tff(c_47186,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_144]) ).
tff(c_48338,plain,
! [X_2,Z_417] : ( multiply(inverse(X_2),multiply(X_2,Z_417)) = multiply(identity,Z_417) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_48278]) ).
tff(c_48434,plain,
! [X_420,Z_421] : ( multiply(inverse(X_420),multiply(X_420,Z_421)) = Z_421 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48338]) ).
tff(c_48503,plain,
multiply(inverse(sk_c2),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_47186,c_48434]) ).
tff(c_48544,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_165,c_48503]) ).
tff(c_48354,plain,
! [X_2,Z_417] : ( multiply(inverse(X_2),multiply(X_2,Z_417)) = Z_417 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48338]) ).
tff(c_48551,plain,
multiply(inverse(sk_c10),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_48544,c_48354]) ).
tff(c_48560,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_48368,c_196,c_48551]) ).
tff(c_47191,plain,
multiply(sk_c9,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_47312,plain,
! [X_399,Y_400,Z_401] : ( multiply(multiply(X_399,Y_400),Z_401) = multiply(X_399,multiply(Y_400,Z_401)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_47366,plain,
! [Z_401] : ( multiply(sk_c9,multiply(sk_c10,Z_401)) = multiply(identity,Z_401) ),
inference(superposition,[status(thm),theory(equality)],[c_200,c_47312]) ).
tff(c_47393,plain,
! [Z_402] : ( multiply(sk_c9,multiply(sk_c10,Z_402)) = Z_402 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47366]) ).
tff(c_47411,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_169,c_47393]) ).
tff(c_47599,plain,
! [Z_405] : ( multiply(sk_c9,multiply(sk_c11,Z_405)) = multiply(sk_c10,Z_405) ),
inference(superposition,[status(thm),theory(equality)],[c_47191,c_47312]) ).
tff(c_47614,plain,
multiply(sk_c9,identity) = multiply(sk_c10,sk_c1),
inference(superposition,[status(thm),theory(equality)],[c_181,c_47599]) ).
tff(c_47619,plain,
multiply(sk_c10,sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_47411,c_47614]) ).
tff(c_47388,plain,
! [Z_401] : ( multiply(sk_c9,multiply(sk_c10,Z_401)) = Z_401 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47366]) ).
tff(c_47640,plain,
multiply(sk_c9,sk_c2) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_47619,c_47388]) ).
tff(c_90,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_47222,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_47173,c_90]) ).
tff(c_47226,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_47222,c_4]) ).
tff(c_47611,plain,
multiply(sk_c9,identity) = multiply(sk_c10,sk_c3),
inference(superposition,[status(thm),theory(equality)],[c_47226,c_47599]) ).
tff(c_47618,plain,
multiply(sk_c10,sk_c3) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_47411,c_47611]) ).
tff(c_47630,plain,
multiply(sk_c9,sk_c2) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_47618,c_47388]) ).
tff(c_47654,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_47640,c_47630]) ).
tff(c_88,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_47293,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_47173,c_88]) ).
tff(c_47664,plain,
multiply(sk_c1,sk_c11) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_47654,c_47293]) ).
tff(c_47369,plain,
! [Z_401] : ( multiply(sk_c11,multiply(sk_c1,Z_401)) = multiply(identity,Z_401) ),
inference(superposition,[status(thm),theory(equality)],[c_181,c_47312]) ).
tff(c_47681,plain,
! [Z_406] : ( multiply(sk_c11,multiply(sk_c1,Z_406)) = Z_406 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47369]) ).
tff(c_47696,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_47664,c_47681]) ).
tff(c_47357,plain,
! [Z_401] : ( multiply(sk_c9,multiply(sk_c11,Z_401)) = multiply(sk_c10,Z_401) ),
inference(superposition,[status(thm),theory(equality)],[c_47191,c_47312]) ).
tff(c_47739,plain,
multiply(sk_c9,sk_c11) = multiply(sk_c10,sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_47696,c_47357]) ).
tff(c_47745,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_47191,c_47739]) ).
tff(c_47758,plain,
multiply(sk_c9,sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_47745,c_47388]) ).
tff(c_47764,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_47758]) ).
tff(c_47770,plain,
multiply(identity,sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_47764,c_47619]) ).
tff(c_47785,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47770]) ).
tff(c_47782,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47764,c_165]) ).
tff(c_47837,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_177,c_47785,c_47782]) ).
tff(c_47842,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47837,c_181]) ).
tff(c_47898,plain,
sk_c1 = identity,
inference(superposition,[status(thm),theory(equality)],[c_47842,c_2]) ).
tff(c_47778,plain,
multiply(sk_c1,identity) != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_47764,c_47173]) ).
tff(c_48149,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47898,c_47837,c_47778]) ).
tff(c_48151,plain,
multiply(sk_c9,sk_c11) != sk_c10,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_48569,plain,
multiply(sk_c9,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_48560,c_48151]) ).
tff(c_48574,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_48569]) ).
tff(c_48266,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_48151,c_56]) ).
tff(c_48470,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_48266,c_48434]) ).
tff(c_48539,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_47172,c_48470]) ).
tff(c_48708,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_48560,c_48539]) ).
tff(c_48712,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_48708,c_48354]) ).
tff(c_48718,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_48712]) ).
tff(c_48720,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48574,c_48718]) ).
tff(c_48722,plain,
multiply(sk_c10,sk_c11) != sk_c9,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_16,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_48760,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_48722,c_16]) ).
tff(c_48799,plain,
! [X_424,Y_425,Z_426] : ( multiply(multiply(X_424,Y_425),Z_426) = multiply(X_424,multiply(Y_425,Z_426)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_48856,plain,
! [X_2,Z_426] : ( multiply(inverse(X_2),multiply(X_2,Z_426)) = multiply(identity,Z_426) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_48799]) ).
tff(c_49049,plain,
! [X_430,Z_431] : ( multiply(inverse(X_430),multiply(X_430,Z_431)) = Z_431 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48856]) ).
tff(c_49070,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_48760,c_49049]) ).
tff(c_49113,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_47172,c_49070]) ).
tff(c_48872,plain,
! [X_2,Z_426] : ( multiply(inverse(X_2),multiply(X_2,Z_426)) = Z_426 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48856]) ).
tff(c_49175,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_49113,c_48872]) ).
tff(c_49181,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_49175]) ).
tff(c_49188,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49181,c_177]) ).
tff(c_49259,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_49188,c_4]) ).
tff(c_49438,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_49259,c_48872]) ).
tff(c_49450,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_49438]) ).
tff(c_48847,plain,
! [Z_426] : ( multiply(sk_c9,multiply(sk_c10,Z_426)) = multiply(identity,Z_426) ),
inference(superposition,[status(thm),theory(equality)],[c_200,c_48799]) ).
tff(c_48874,plain,
! [Z_427] : ( multiply(sk_c9,multiply(sk_c10,Z_427)) = Z_427 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48847]) ).
tff(c_48889,plain,
multiply(sk_c9,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_169,c_48874]) ).
tff(c_48853,plain,
! [Z_426] : ( multiply(sk_c10,multiply(sk_c2,Z_426)) = multiply(identity,Z_426) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_48799]) ).
tff(c_48920,plain,
! [Z_428] : ( multiply(sk_c10,multiply(sk_c2,Z_428)) = Z_428 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48853]) ).
tff(c_48938,plain,
multiply(sk_c10,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_47186,c_48920]) ).
tff(c_48959,plain,
! [Z_429] : ( multiply(sk_c2,multiply(sk_c9,Z_429)) = multiply(sk_c10,Z_429) ),
inference(superposition,[status(thm),theory(equality)],[c_47186,c_48799]) ).
tff(c_48983,plain,
multiply(sk_c2,identity) = multiply(sk_c10,sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_200,c_48959]) ).
tff(c_48988,plain,
multiply(sk_c2,identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_48938,c_48983]) ).
tff(c_48871,plain,
! [Z_426] : ( multiply(sk_c10,multiply(sk_c2,Z_426)) = Z_426 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48853]) ).
tff(c_48992,plain,
multiply(sk_c10,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_48988,c_48871]) ).
tff(c_48869,plain,
! [Z_426] : ( multiply(sk_c9,multiply(sk_c10,Z_426)) = Z_426 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48847]) ).
tff(c_49003,plain,
multiply(sk_c9,identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_48992,c_48869]) ).
tff(c_49009,plain,
sk_c9 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_48889,c_49003]) ).
tff(c_48150,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_48155,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_48150,c_4]) ).
tff(c_48886,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_48155,c_48874]) ).
tff(c_48901,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_48889,c_48886]) ).
tff(c_12,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_48772,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_48722,c_12]) ).
tff(c_48902,plain,
multiply(sk_c2,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_48901,c_48772]) ).
tff(c_48935,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_48902,c_48920]) ).
tff(c_49037,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_169,c_49009,c_48935]) ).
tff(c_49042,plain,
multiply(sk_c1,identity) != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_49037,c_47173]) ).
tff(c_49511,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49450,c_49181,c_49042]) ).
tff(c_49513,plain,
multiply(sk_c2,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_144]) ).
tff(c_50526,plain,
multiply(sk_c2,identity) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_50516,c_49513]) ).
tff(c_50771,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50612,c_2,c_50530,c_50526]) ).
tff(c_50773,plain,
inverse(sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_38,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_50809,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_50773,c_38]) ).
tff(c_36,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_50834,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_50773,c_36]) ).
tff(c_50909,plain,
! [X_455,Y_456,Z_457] : ( multiply(multiply(X_455,Y_456),Z_457) = multiply(X_455,multiply(Y_456,Z_457)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_50960,plain,
! [X_2,Z_457] : ( multiply(inverse(X_2),multiply(X_2,Z_457)) = multiply(identity,Z_457) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_50909]) ).
tff(c_51108,plain,
! [X_464,Z_465] : ( multiply(inverse(X_464),multiply(X_464,Z_465)) = Z_465 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50960]) ).
tff(c_51168,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_50834,c_51108]) ).
tff(c_51227,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_50809,c_51168]) ).
tff(c_50975,plain,
! [X_2,Z_457] : ( multiply(inverse(X_2),multiply(X_2,Z_457)) = Z_457 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50960]) ).
tff(c_51285,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_51227,c_50975]) ).
tff(c_51291,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_51285]) ).
tff(c_51301,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51291,c_177]) ).
tff(c_51334,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_51301,c_4]) ).
tff(c_51390,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_51334,c_50975]) ).
tff(c_51402,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_51390]) ).
tff(c_51406,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51402,c_51301]) ).
tff(c_30,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_50781,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_50773,c_30]) ).
tff(c_50842,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_50773,c_28]) ).
tff(c_51165,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_50842,c_51108]) ).
tff(c_51226,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_50781,c_51165]) ).
tff(c_51428,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51291,c_2,c_51291,c_51226]) ).
tff(c_32,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_50847,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_50773,c_32]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_50822,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_50773,c_34]) ).
tff(c_50826,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_50822,c_4]) ).
tff(c_50939,plain,
! [Z_457] : ( multiply(sk_c10,multiply(sk_c4,Z_457)) = multiply(identity,Z_457) ),
inference(superposition,[status(thm),theory(equality)],[c_50826,c_50909]) ).
tff(c_51003,plain,
! [Z_460] : ( multiply(sk_c10,multiply(sk_c4,Z_460)) = Z_460 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50939]) ).
tff(c_51015,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_50847,c_51003]) ).
tff(c_51138,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_51015,c_51108]) ).
tff(c_51222,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_51138]) ).
tff(c_51238,plain,
inverse(sk_c10) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_51222,c_50773]) ).
tff(c_51429,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_51428,c_51238]) ).
tff(c_51438,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_51406,c_51429]) ).
tff(c_51440,plain,
inverse(sk_c1) != sk_c11,
inference(splitRight,[status(thm)],[c_84]) ).
tff(c_74,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_51479,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_51440,c_74]) ).
tff(c_51483,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_51479,c_4]) ).
tff(c_51675,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_51483,c_51663]) ).
tff(c_52292,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_51678,c_51675]) ).
tff(c_72,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_51549,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_51440,c_72]) ).
tff(c_52301,plain,
multiply(sk_c2,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_52292,c_51549]) ).
tff(c_51643,plain,
! [Z_470] : ( multiply(sk_c10,multiply(sk_c2,Z_470)) = multiply(identity,Z_470) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_51595]) ).
tff(c_53145,plain,
! [Z_493] : ( multiply(sk_c10,multiply(sk_c2,Z_493)) = Z_493 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51643]) ).
tff(c_53163,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_52301,c_53145]) ).
tff(c_51654,plain,
! [Z_470] : ( multiply(sk_c9,multiply(sk_c10,Z_470)) = Z_470 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51622]) ).
tff(c_53173,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_53163,c_51654]) ).
tff(c_53180,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51521,c_53173]) ).
tff(c_76,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_51566,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_51440,c_76]) ).
tff(c_78,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_51491,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_51440,c_78]) ).
tff(c_51495,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_51491,c_4]) ).
tff(c_51628,plain,
! [Z_470] : ( multiply(sk_c8,multiply(sk_c5,Z_470)) = multiply(identity,Z_470) ),
inference(superposition,[status(thm),theory(equality)],[c_51495,c_51595]) ).
tff(c_51740,plain,
! [Z_473] : ( multiply(sk_c8,multiply(sk_c5,Z_473)) = Z_473 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51628]) ).
tff(c_51758,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_51566,c_51740]) ).
tff(c_51646,plain,
! [X_2,Z_470] : ( multiply(inverse(X_2),multiply(X_2,Z_470)) = multiply(identity,Z_470) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_51595]) ).
tff(c_51791,plain,
! [X_474,Z_475] : ( multiply(inverse(X_474),multiply(X_474,Z_475)) = Z_475 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51646]) ).
tff(c_51815,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_51758,c_51791]) ).
tff(c_51893,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_51815]) ).
tff(c_70,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_51467,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_51440,c_70]) ).
tff(c_51912,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51893,c_51467]) ).
tff(c_51928,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_51912,c_4]) ).
tff(c_51661,plain,
! [X_2,Z_470] : ( multiply(inverse(X_2),multiply(X_2,Z_470)) = Z_470 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51646]) ).
tff(c_51935,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_51928,c_51661]) ).
tff(c_51947,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_51935]) ).
tff(c_51951,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51947,c_51912]) ).
tff(c_68,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_51556,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_51440,c_68]) ).
tff(c_51839,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_51556,c_51791]) ).
tff(c_51897,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_51467,c_51839]) ).
tff(c_51992,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51893,c_2,c_51893,c_51897]) ).
tff(c_51997,plain,
inverse(identity) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_51992,c_51517]) ).
tff(c_52002,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51951,c_51997]) ).
tff(c_51691,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( multiply(sk_c10,sk_c11) != sk_c9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_51517,c_148]) ).
tff(c_51692,plain,
multiply(sk_c10,sk_c11) != sk_c9,
inference(splitLeft,[status(thm)],[c_51691]) ).
tff(c_51907,plain,
multiply(sk_c10,identity) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_51893,c_51692]) ).
tff(c_52257,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52002,c_2,c_51992,c_51907]) ).
tff(c_52259,plain,
multiply(sk_c10,sk_c11) = sk_c9,
inference(splitRight,[status(thm)],[c_51691]) ).
tff(c_52285,plain,
multiply(sk_c9,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_52259,c_51654]) ).
tff(c_53185,plain,
multiply(identity,identity) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_53180,c_53180,c_52285]) ).
tff(c_53191,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_53185]) ).
tff(c_53202,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_53191,c_51467]) ).
tff(c_247505,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_53202,c_4]) ).
tff(c_247650,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_247505,c_51661]) ).
tff(c_247662,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_247650]) ).
tff(c_247666,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_247662,c_53202]) ).
tff(c_53186,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_53180,c_51678]) ).
tff(c_53192,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_53186]) ).
tff(c_247462,plain,
inverse(identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_53192,c_165]) ).
tff(c_247712,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_247666,c_247462]) ).
tff(c_247527,plain,
! [X_1053,Z_1054] : ( multiply(inverse(X_1053),multiply(X_1053,Z_1054)) = Z_1054 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51646]) ).
tff(c_247993,plain,
! [X_1057,Z_1058] : ( multiply(inverse(inverse(X_1057)),Z_1058) = multiply(X_1057,Z_1058) ),
inference(superposition,[status(thm),theory(equality)],[c_51661,c_247527]) ).
tff(c_247590,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_247527]) ).
tff(c_248000,plain,
! [X_1057] : ( multiply(X_1057,identity) = X_1057 ),
inference(superposition,[status(thm),theory(equality)],[c_247993,c_247590]) ).
tff(c_53257,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_53202,c_4]) ).
tff(c_53418,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_53257,c_51661]) ).
tff(c_53430,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_53418]) ).
tff(c_53434,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_53430,c_53202]) ).
tff(c_53287,plain,
! [X_495,Z_496] : ( multiply(inverse(X_495),multiply(X_495,Z_496)) = Z_496 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51646]) ).
tff(c_53747,plain,
! [X_500,Z_501] : ( multiply(inverse(inverse(X_500)),Z_501) = multiply(X_500,Z_501) ),
inference(superposition,[status(thm),theory(equality)],[c_53287,c_51661]) ).
tff(c_53353,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_53287]) ).
tff(c_53754,plain,
! [X_500] : ( multiply(X_500,identity) = X_500 ),
inference(superposition,[status(thm),theory(equality)],[c_53747,c_53353]) ).
tff(c_53785,plain,
! [X_500] : ( multiply(X_500,inverse(X_500)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_53747]) ).
tff(c_53214,plain,
inverse(identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_53192,c_165]) ).
tff(c_53480,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_53434,c_53214]) ).
tff(c_53790,plain,
! [X_502] : ( multiply(X_502,identity) = X_502 ),
inference(superposition,[status(thm),theory(equality)],[c_53747,c_53353]) ).
tff(c_53290,plain,
! [X_495,Z_496] : ( multiply(inverse(inverse(X_495)),Z_496) = multiply(X_495,Z_496) ),
inference(superposition,[status(thm),theory(equality)],[c_53287,c_51661]) ).
tff(c_53797,plain,
! [X_495] : ( inverse(inverse(X_495)) = multiply(X_495,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_53790,c_53290]) ).
tff(c_53842,plain,
! [X_495] : ( inverse(inverse(X_495)) = X_495 ),
inference(demodulation,[status(thm),theory(equality)],[c_53754,c_53797]) ).
tff(c_54020,plain,
! [X_507,Y_508,Z_509] : ( multiply(inverse(multiply(X_507,Y_508)),multiply(X_507,multiply(Y_508,Z_509))) = Z_509 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_53287]) ).
tff(c_54068,plain,
! [X_507,X_500] : ( multiply(inverse(multiply(X_507,X_500)),multiply(X_507,identity)) = inverse(X_500) ),
inference(superposition,[status(thm),theory(equality)],[c_53785,c_54020]) ).
tff(c_54394,plain,
! [X_516,X_517] : ( multiply(inverse(multiply(X_516,X_517)),X_516) = inverse(X_517) ),
inference(demodulation,[status(thm),theory(equality)],[c_53754,c_54068]) ).
tff(c_54758,plain,
! [Z_522,X_523] : ( multiply(inverse(Z_522),inverse(X_523)) = inverse(multiply(X_523,Z_522)) ),
inference(superposition,[status(thm),theory(equality)],[c_51661,c_54394]) ).
tff(c_54844,plain,
! [X_523,X_495] : ( inverse(multiply(X_523,inverse(X_495))) = multiply(X_495,inverse(X_523)) ),
inference(superposition,[status(thm),theory(equality)],[c_53842,c_54758]) ).
tff(c_52993,plain,
! [Z_490] : ( multiply(sk_c10,multiply(sk_c2,Z_490)) = Z_490 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51643]) ).
tff(c_53011,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_52301,c_52993]) ).
tff(c_53021,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_53011,c_51654]) ).
tff(c_53028,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51521,c_53021]) ).
tff(c_53034,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_53028,c_51678]) ).
tff(c_53040,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_53034]) ).
tff(c_53086,plain,
inverse(identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_53040,c_165]) ).
tff(c_53038,plain,
inverse(sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_53028,c_51517]) ).
tff(c_53033,plain,
multiply(identity,identity) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_53028,c_53028,c_52285]) ).
tff(c_53039,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_53033]) ).
tff(c_52431,plain,
! [X_483,Z_484] : ( multiply(inverse(X_483),multiply(X_483,Z_484)) = Z_484 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51646]) ).
tff(c_52494,plain,
multiply(inverse(sk_c5),sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_51566,c_52431]) ).
tff(c_52557,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_51491,c_52494]) ).
tff(c_52671,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_52557,c_51661]) ).
tff(c_52677,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_52671]) ).
tff(c_51471,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_51467,c_4]) ).
tff(c_51634,plain,
! [Z_470] : ( multiply(sk_c11,multiply(sk_c3,Z_470)) = multiply(identity,Z_470) ),
inference(superposition,[status(thm),theory(equality)],[c_51471,c_51595]) ).
tff(c_52380,plain,
! [Z_482] : ( multiply(sk_c11,multiply(sk_c3,Z_482)) = Z_482 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51634]) ).
tff(c_52401,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_51556,c_52380]) ).
tff(c_52452,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_52401,c_52431]) ).
tff(c_52550,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_52452]) ).
tff(c_52571,plain,
multiply(identity,sk_c11) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_52550,c_52259]) ).
tff(c_52583,plain,
sk_c9 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52571]) ).
tff(c_52710,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52677,c_52583]) ).
tff(c_52258,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_51691]) ).
tff(c_52324,plain,
multiply(sk_c9,sk_c11) != sk_c10,
inference(splitLeft,[status(thm)],[c_52258]) ).
tff(c_52569,plain,
multiply(sk_c9,sk_c11) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_52550,c_52324]) ).
tff(c_52959,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52710,c_52677,c_52569]) ).
tff(c_52960,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_52258]) ).
tff(c_52992,plain,
! [X3_8] :
( ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_52960]) ).
tff(c_53104,plain,
! [X3_492] :
( ( multiply(X3_492,sk_c10) != identity )
| ( inverse(X3_492) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_53039,c_53039,c_52992]) ).
tff(c_53112,plain,
inverse(inverse(sk_c10)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_53104]) ).
tff(c_53118,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_53038,c_53112]) ).
tff(c_53133,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_53086,c_53118]) ).
tff(c_53032,plain,
multiply(sk_c2,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_53028,c_52301]) ).
tff(c_53142,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_53040,c_53032]) ).
tff(c_53143,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_53133,c_53142]) ).
tff(c_53144,plain,
! [X5_6,X4_13,X1_10,X7_9,X2_11] :
( ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_52960]) ).
tff(c_53209,plain,
! [X5_6,X4_13,X1_10,X7_9,X2_11] :
( ( multiply(X4_13,identity) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( inverse(X1_10) != identity )
| ( multiply(X1_10,identity) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != identity )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != identity )
| ( multiply(X5_6,inverse(X5_6)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_53191,c_53191,c_53180,c_53191,c_53191,c_53180,c_53144]) ).
tff(c_53210,plain,
! [X7_9,X5_6] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != identity )
| ( multiply(X5_6,inverse(X5_6)) != identity ) ),
inference(splitLeft,[status(thm)],[c_53209]) ).
tff(c_247265,plain,
! [X5_1049,X7_1050] :
( ( multiply(X5_1049,inverse(X7_1050)) != inverse(X5_1049) )
| ( multiply(X7_1050,inverse(X5_1049)) != inverse(X7_1050) )
| ( inverse(X5_1049) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_53785,c_53754,c_53480,c_54844,c_53210]) ).
tff(c_247379,plain,
! [X7_1050] :
( ( inverse(identity) != inverse(X7_1050) )
| ( multiply(X7_1050,inverse(identity)) != inverse(X7_1050) )
| ( inverse(identity) != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_247265]) ).
tff(c_247427,plain,
! [X7_1051] :
( ( inverse(X7_1051) != identity )
| ( inverse(X7_1051) != X7_1051 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_53434,c_53754,c_53434,c_53434,c_247379]) ).
tff(c_247445,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_53434,c_247427]) ).
tff(c_247457,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_53434,c_247445]) ).
tff(c_247458,plain,
! [X2_11,X1_10,X4_13] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != identity )
| ( inverse(X1_10) != identity )
| ( multiply(X1_10,identity) != sk_c10 )
| ( multiply(X4_13,identity) != sk_c10 )
| ( inverse(X4_13) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_53209]) ).
tff(c_371027,plain,
! [X2_11,X1_10,X4_13] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( identity != X4_13 )
| ( inverse(X4_13) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_247712,c_248000,c_247712,c_248000,c_247712,c_248000,c_247712,c_247712,c_247458]) ).
tff(c_371029,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_371027]) ).
tff(c_371031,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_371029,c_247666]) ).
tff(c_371032,plain,
! [X1_10,X2_11] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_371027]) ).
tff(c_371034,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_371032]) ).
tff(c_371036,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_371034,c_247666]) ).
tff(c_371039,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_371032]) ).
tff(c_371041,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_371039,c_247666]) ).
tff(c_371043,plain,
inverse(sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_371067,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_371043,c_36]) ).
tff(c_371115,plain,
! [X_1487,Y_1488,Z_1489] : ( multiply(multiply(X_1487,Y_1488),Z_1489) = multiply(X_1487,multiply(Y_1488,Z_1489)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_371145,plain,
! [Z_1489] : ( multiply(sk_c8,multiply(sk_c5,Z_1489)) = multiply(identity,Z_1489) ),
inference(superposition,[status(thm),theory(equality)],[c_51495,c_371115]) ).
tff(c_371179,plain,
! [Z_1490] : ( multiply(sk_c8,multiply(sk_c5,Z_1490)) = Z_1490 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371145]) ).
tff(c_371191,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_371067,c_371179]) ).
tff(c_371163,plain,
! [X_2,Z_1489] : ( multiply(inverse(X_2),multiply(X_2,Z_1489)) = multiply(identity,Z_1489) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_371115]) ).
tff(c_371322,plain,
! [X_1496,Z_1497] : ( multiply(inverse(X_1496),multiply(X_1496,Z_1497)) = Z_1497 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371163]) ).
tff(c_371364,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_371191,c_371322]) ).
tff(c_371436,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_371364]) ).
tff(c_371042,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_371382,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_371042,c_371322]) ).
tff(c_371439,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_51467,c_371382]) ).
tff(c_371516,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_371436,c_2,c_371436,c_371439]) ).
tff(c_371048,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_371043,c_32]) ).
tff(c_371148,plain,
! [Z_1489] : ( multiply(sk_c10,multiply(sk_c4,Z_1489)) = multiply(identity,Z_1489) ),
inference(superposition,[status(thm),theory(equality)],[c_51483,c_371115]) ).
tff(c_371215,plain,
! [Z_1492] : ( multiply(sk_c10,multiply(sk_c4,Z_1492)) = Z_1492 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371148]) ).
tff(c_371227,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_371048,c_371215]) ).
tff(c_371352,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_371227,c_371322]) ).
tff(c_371434,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_371352]) ).
tff(c_371451,plain,
inverse(sk_c10) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_371434,c_371043]) ).
tff(c_371517,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_371516,c_371451]) ).
tff(c_371463,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_371436,c_51467]) ).
tff(c_371512,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_371463,c_4]) ).
tff(c_371177,plain,
! [X_2,Z_1489] : ( multiply(inverse(X_2),multiply(X_2,Z_1489)) = Z_1489 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371163]) ).
tff(c_371580,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_371512,c_371177]) ).
tff(c_371592,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_371580]) ).
tff(c_371597,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_371592,c_371463]) ).
tff(c_371601,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_371517,c_371597]) ).
tff(c_371603,plain,
inverse(sk_c2) != sk_c10,
inference(splitRight,[status(thm)],[c_124]) ).
tff(c_112,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_221]) ).
tff(c_371728,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_371603,c_112]) ).
tff(c_114,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_224]) ).
tff(c_371615,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_371603,c_114]) ).
tff(c_371619,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_371615,c_4]) ).
tff(c_371815,plain,
! [Z_1502] : ( multiply(sk_c10,multiply(sk_c4,Z_1502)) = multiply(identity,Z_1502) ),
inference(superposition,[status(thm),theory(equality)],[c_371619,c_371770]) ).
tff(c_372955,plain,
! [Z_1524] : ( multiply(sk_c10,multiply(sk_c4,Z_1524)) = Z_1524 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371815]) ).
tff(c_372970,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_371728,c_372955]) ).
tff(c_371797,plain,
! [Z_1502] : ( multiply(sk_c9,multiply(sk_c10,Z_1502)) = multiply(identity,Z_1502) ),
inference(superposition,[status(thm),theory(equality)],[c_371695,c_371770]) ).
tff(c_373896,plain,
! [Z_1541] : ( multiply(sk_c9,multiply(sk_c10,Z_1541)) = Z_1541 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371797]) ).
tff(c_373908,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_372970,c_373896]) ).
tff(c_373921,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_371695,c_373908]) ).
tff(c_373978,plain,
inverse(sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373921,c_371691]) ).
tff(c_373973,plain,
multiply(sk_c10,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_373921,c_372970]) ).
tff(c_374994,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_373973,c_371836]) ).
tff(c_375000,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_373978,c_374994]) ).
tff(c_116,plain,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_371744,plain,
multiply(sk_c5,sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_371603,c_116]) ).
tff(c_118,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_230]) ).
tff(c_371642,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_371603,c_118]) ).
tff(c_371646,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_371642,c_4]) ).
tff(c_371809,plain,
! [Z_1502] : ( multiply(sk_c8,multiply(sk_c5,Z_1502)) = multiply(identity,Z_1502) ),
inference(superposition,[status(thm),theory(equality)],[c_371646,c_371770]) ).
tff(c_371861,plain,
! [Z_1504] : ( multiply(sk_c8,multiply(sk_c5,Z_1504)) = Z_1504 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371809]) ).
tff(c_371873,plain,
multiply(sk_c8,sk_c11) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_371744,c_371861]) ).
tff(c_371983,plain,
! [X_1508,Z_1509] : ( multiply(inverse(X_1508),multiply(X_1508,Z_1509)) = Z_1509 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371821]) ).
tff(c_372022,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_371873,c_371983]) ).
tff(c_372107,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_372022]) ).
tff(c_371887,plain,
! [Z_1505] : ( multiply(sk_c10,multiply(sk_c4,Z_1505)) = Z_1505 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371815]) ).
tff(c_371899,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_371728,c_371887]) ).
tff(c_372013,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_371899,c_371983]) ).
tff(c_372104,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_372013]) ).
tff(c_108,plain,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_215]) ).
tff(c_371721,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_371603,c_108]) ).
tff(c_110,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_218]) ).
tff(c_371654,plain,
inverse(sk_c3) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_371603,c_110]) ).
tff(c_371658,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_371654,c_4]) ).
tff(c_371806,plain,
! [Z_1502] : ( multiply(sk_c11,multiply(sk_c3,Z_1502)) = multiply(identity,Z_1502) ),
inference(superposition,[status(thm),theory(equality)],[c_371658,c_371770]) ).
tff(c_371949,plain,
! [Z_1507] : ( multiply(sk_c11,multiply(sk_c3,Z_1507)) = Z_1507 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371806]) ).
tff(c_371961,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_371721,c_371949]) ).
tff(c_372004,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_371961,c_371983]) ).
tff(c_372102,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_372004]) ).
tff(c_371878,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( multiply(sk_c10,sk_c11) != sk_c9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_371691,c_148]) ).
tff(c_371879,plain,
multiply(sk_c10,sk_c11) != sk_c9,
inference(splitLeft,[status(thm)],[c_371878]) ).
tff(c_372141,plain,
multiply(identity,sk_c11) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_372102,c_371879]) ).
tff(c_372149,plain,
sk_c9 != sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_372141]) ).
tff(c_372212,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_372107,c_372104,c_372149]) ).
tff(c_372214,plain,
multiply(sk_c10,sk_c11) = sk_c9,
inference(splitRight,[status(thm)],[c_371878]) ).
tff(c_373914,plain,
multiply(sk_c9,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_372214,c_373896]) ).
tff(c_374841,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_373921,c_373921,c_373914]) ).
tff(c_374021,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373921,c_2,c_373921,c_373914]) ).
tff(c_374031,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_374021,c_371654]) ).
tff(c_374059,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_374031,c_4]) ).
tff(c_374069,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_374059,c_2]) ).
tff(c_374078,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_374069,c_374031]) ).
tff(c_373917,plain,
multiply(sk_c9,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_371619,c_373896]) ).
tff(c_374002,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_373921,c_373917]) ).
tff(c_374006,plain,
inverse(identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_374002,c_371615]) ).
tff(c_374163,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_374078,c_374006]) ).
tff(c_374106,plain,
! [X_1543,Z_1544] : ( multiply(inverse(X_1543),multiply(X_1543,Z_1544)) = Z_1544 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371821]) ).
tff(c_374442,plain,
! [X_1547,Z_1548] : ( multiply(inverse(inverse(X_1547)),Z_1548) = multiply(X_1547,Z_1548) ),
inference(superposition,[status(thm),theory(equality)],[c_374106,c_371836]) ).
tff(c_374151,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_374106]) ).
tff(c_374449,plain,
! [X_1547] : ( multiply(X_1547,identity) = X_1547 ),
inference(superposition,[status(thm),theory(equality)],[c_374442,c_374151]) ).
tff(c_373364,plain,
! [Z_1532] : ( multiply(sk_c9,multiply(sk_c10,Z_1532)) = Z_1532 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371797]) ).
tff(c_373376,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_372970,c_373364]) ).
tff(c_373389,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_371695,c_373376]) ).
tff(c_373382,plain,
multiply(sk_c9,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_372214,c_373364]) ).
tff(c_373525,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373389,c_2,c_373389,c_373382]) ).
tff(c_373536,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373525,c_371654]) ).
tff(c_373564,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_373536,c_4]) ).
tff(c_373574,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_373564,c_2]) ).
tff(c_373583,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373574,c_373536]) ).
tff(c_122,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_236]) ).
tff(c_371667,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_371603,c_122]) ).
tff(c_371671,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_371667,c_4]) ).
tff(c_371602,plain,
inverse(sk_c6) = sk_c8,
inference(splitRight,[status(thm)],[c_124]) ).
tff(c_371607,plain,
multiply(sk_c8,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_371602,c_4]) ).
tff(c_371818,plain,
! [Z_1502] : ( multiply(sk_c8,multiply(sk_c6,Z_1502)) = multiply(identity,Z_1502) ),
inference(superposition,[status(thm),theory(equality)],[c_371607,c_371770]) ).
tff(c_372891,plain,
! [Z_1522] : ( multiply(sk_c8,multiply(sk_c6,Z_1522)) = Z_1522 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371818]) ).
tff(c_372909,plain,
multiply(sk_c8,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_371671,c_372891]) ).
tff(c_120,plain,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_233]) ).
tff(c_371684,plain,
multiply(sk_c8,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_371603,c_120]) ).
tff(c_372928,plain,
! [Z_1523] : ( multiply(sk_c8,multiply(sk_c10,Z_1523)) = multiply(sk_c11,Z_1523) ),
inference(superposition,[status(thm),theory(equality)],[c_371684,c_371770]) ).
tff(c_372940,plain,
multiply(sk_c8,sk_c9) = multiply(sk_c11,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_372214,c_372928]) ).
tff(c_373439,plain,
multiply(sk_c8,identity) = multiply(sk_c11,sk_c11),
inference(demodulation,[status(thm),theory(equality)],[c_373389,c_372940]) ).
tff(c_373447,plain,
multiply(sk_c11,sk_c11) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_372909,c_373439]) ).
tff(c_373703,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373525,c_2,c_373525,c_373447]) ).
tff(c_373531,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_373525,c_371873]) ).
tff(c_373540,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_372909,c_373531]) ).
tff(c_373706,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373703,c_373540]) ).
tff(c_373024,plain,
! [Z_1526] : ( multiply(sk_c9,multiply(sk_c10,Z_1526)) = Z_1526 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371797]) ).
tff(c_373036,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_372970,c_373024]) ).
tff(c_373049,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_371695,c_373036]) ).
tff(c_373107,plain,
inverse(sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373049,c_371691]) ).
tff(c_373116,plain,
multiply(identity,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_373107,c_4]) ).
tff(c_373212,plain,
sk_c10 = identity,
inference(superposition,[status(thm),theory(equality)],[c_373116,c_2]) ).
tff(c_373042,plain,
multiply(sk_c9,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_372214,c_373024]) ).
tff(c_373130,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373049,c_2,c_373049,c_373042]) ).
tff(c_372943,plain,
multiply(sk_c8,identity) = multiply(sk_c11,sk_c4),
inference(superposition,[status(thm),theory(equality)],[c_371619,c_372928]) ).
tff(c_372947,plain,
multiply(sk_c11,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_372909,c_372943]) ).
tff(c_373135,plain,
multiply(identity,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_373130,c_372947]) ).
tff(c_373146,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_373135]) ).
tff(c_373157,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_373146,c_371667]) ).
tff(c_373158,plain,
sk_c6 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_371615,c_373157]) ).
tff(c_373222,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373212,c_373158]) ).
tff(c_373137,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_373130,c_371873]) ).
tff(c_373148,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_372909,c_373137]) ).
tff(c_373179,plain,
sk_c8 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_373146,c_373148]) ).
tff(c_373187,plain,
inverse(sk_c6) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_373179,c_371602]) ).
tff(c_373246,plain,
inverse(identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_373222,c_373187]) ).
tff(c_372336,plain,
! [X_1515,Z_1516] : ( multiply(inverse(X_1515),multiply(X_1515,Z_1516)) = Z_1516 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371821]) ).
tff(c_372378,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_371873,c_372336]) ).
tff(c_372463,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_372378]) ).
tff(c_372402,plain,
multiply(inverse(sk_c3),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_371721,c_372336]) ).
tff(c_372469,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_371654,c_372402]) ).
tff(c_372624,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_372463,c_2,c_372463,c_372469]) ).
tff(c_372286,plain,
! [Z_1513] : ( multiply(sk_c10,multiply(sk_c4,Z_1513)) = Z_1513 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_371815]) ).
tff(c_372298,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_371728,c_372286]) ).
tff(c_372360,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_372298,c_372336]) ).
tff(c_372460,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_371695,c_371691,c_372360]) ).
tff(c_372213,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_371878]) ).
tff(c_372229,plain,
multiply(sk_c9,sk_c11) != sk_c10,
inference(splitLeft,[status(thm)],[c_372213]) ).
tff(c_372480,plain,
multiply(sk_c9,identity) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_372463,c_372229]) ).
tff(c_372881,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_372624,c_2,c_372460,c_372480]) ).
tff(c_372882,plain,
! [X5_6,X4_13,X3_8,X1_10,X7_9,X2_11] :
( ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_372213]) ).
tff(c_373008,plain,
! [X3_8] :
( ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_372882]) ).
tff(c_373164,plain,
! [X3_1528] :
( ( multiply(X3_1528,sk_c10) != identity )
| ( inverse(X3_1528) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_373130,c_373130,c_373008]) ).
tff(c_373172,plain,
inverse(inverse(sk_c10)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_373164]) ).
tff(c_373178,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_373107,c_373172]) ).
tff(c_373303,plain,
sk_c4 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_373246,c_373178]) ).
tff(c_373224,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373212,c_373107]) ).
tff(c_373331,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_373224,c_373246]) ).
tff(c_373333,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_373303,c_373331]) ).
tff(c_373334,plain,
! [X5_6,X4_13,X1_10,X7_9,X2_11] :
( ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(multiply(X7_9,inverse(X5_6))) != inverse(X5_6) )
| ( multiply(X7_9,inverse(X5_6)) != inverse(X7_9) )
| ( multiply(inverse(X5_6),sk_c10) != sk_c11 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_372882]) ).
tff(c_373487,plain,
! [X7_1534,X5_1535] :
( ( inverse(multiply(X7_1534,inverse(X5_1535))) != inverse(X5_1535) )
| ( multiply(X7_1534,inverse(X5_1535)) != inverse(X7_1534) )
| ( multiply(inverse(X5_1535),sk_c10) != sk_c11 )
| ( multiply(X5_1535,inverse(X5_1535)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_373334]) ).
tff(c_373500,plain,
! [X7_1534] :
( ( inverse(multiply(X7_1534,sk_c8)) != inverse(sk_c5) )
| ( multiply(X7_1534,inverse(sk_c5)) != inverse(X7_1534) )
| ( multiply(inverse(sk_c5),sk_c10) != sk_c11 )
| ( multiply(sk_c5,inverse(sk_c5)) != sk_c11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_371642,c_373487]) ).
tff(c_373518,plain,
! [X7_1534] :
( ( inverse(multiply(X7_1534,sk_c8)) != sk_c8 )
| ( multiply(X7_1534,sk_c8) != inverse(X7_1534) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_371744,c_371642,c_371684,c_371642,c_371642,c_371642,c_373500]) ).
tff(c_373853,plain,
! [X7_1539] :
( ( inverse(multiply(X7_1539,identity)) != identity )
| ( multiply(X7_1539,identity) != inverse(X7_1539) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_373706,c_373706,c_373706,c_373518]) ).
tff(c_373864,plain,
( ( inverse(identity) != identity )
| ( multiply(inverse(identity),identity) != inverse(inverse(identity)) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_373853]) ).
tff(c_373873,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_373583,c_373583,c_4,c_373583,c_373864]) ).
tff(c_373874,plain,
! [X2_11,X1_10,X4_13] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_373334]) ).
tff(c_374019,plain,
! [X2_11,X1_10,X4_13] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != identity )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( multiply(X4_13,identity) != sk_c10 )
| ( inverse(X4_13) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_373921,c_373921,c_373874]) ).
tff(c_374020,plain,
! [X4_13] :
( ( multiply(X4_13,identity) != sk_c10 )
| ( inverse(X4_13) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_374019]) ).
tff(c_374837,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_374163,c_374449,c_374163,c_374020]) ).
tff(c_374839,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_374837,c_374078]) ).
tff(c_374840,plain,
! [X1_10,X2_11] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != identity ) ),
inference(splitRight,[status(thm)],[c_374019]) ).
tff(c_387264,plain,
! [X1_10,X2_11] :
( ( inverse(X1_10) != identity )
| ( identity != X1_10 )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_375299,c_375000,c_375000,c_375299,c_375000,c_374841,c_374841,c_374840]) ).
tff(c_387266,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_387264]) ).
tff(c_375004,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_375000,c_374006]) ).
tff(c_387268,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_387266,c_375004]) ).
tff(c_387270,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_387264]) ).
tff(c_387272,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_387270,c_375004]) ).
tff(c_387273,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_387347,plain,
! [X_1677,Y_1678,Z_1679] : ( multiply(multiply(X_1677,Y_1678),Z_1679) = multiply(X_1677,multiply(Y_1678,Z_1679)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_387380,plain,
! [Z_1679] : ( multiply(sk_c11,multiply(sk_c3,Z_1679)) = multiply(identity,Z_1679) ),
inference(superposition,[status(thm),theory(equality)],[c_371658,c_387347]) ).
tff(c_387513,plain,
! [Z_1684] : ( multiply(sk_c11,multiply(sk_c3,Z_1684)) = Z_1684 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_387380]) ).
tff(c_387531,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_387273,c_387513]) ).
tff(c_387395,plain,
! [X_2,Z_1679] : ( multiply(inverse(X_2),multiply(X_2,Z_1679)) = multiply(identity,Z_1679) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_387347]) ).
tff(c_387569,plain,
! [X_1686,Z_1687] : ( multiply(inverse(X_1686),multiply(X_1686,Z_1687)) = Z_1687 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_387395]) ).
tff(c_387593,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_387531,c_387569]) ).
tff(c_387685,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_387593]) ).
tff(c_387709,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_387685,c_371615]) ).
tff(c_387823,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_387709,c_4]) ).
tff(c_387409,plain,
! [X_2,Z_1679] : ( multiply(inverse(X_2),multiply(X_2,Z_1679)) = Z_1679 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_387395]) ).
tff(c_387850,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_387823,c_387409]) ).
tff(c_387862,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_387850]) ).
tff(c_387866,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_387862,c_387709]) ).
tff(c_387274,plain,
inverse(sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_387706,plain,
inverse(identity) != sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_387685,c_387274]) ).
tff(c_387876,plain,
sk_c9 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_387866,c_387706]) ).
tff(c_387280,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_387274,c_32]) ).
tff(c_387632,plain,
multiply(inverse(sk_c4),sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_387280,c_387569]) ).
tff(c_387692,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_371615,c_387632]) ).
tff(c_387910,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_387685,c_2,c_387685,c_387692]) ).
tff(c_387911,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_387876,c_387910]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.08 % Problem : GRP350-1 : TPTP v9.0.0. Released v2.5.0.
% 0.07/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.09/0.27 % Computer : n032.cluster.edu
% 0.09/0.27 % Model : x86_64 x86_64
% 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.27 % Memory : 8042.1875MB
% 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.27 % CPULimit : 300
% 0.09/0.27 % WCLimit : 300
% 0.09/0.27 % DateTime : Mon Apr 7 21:43:16 EDT 2025
% 0.09/0.27 % CPUTime :
% 85.09/66.70 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 85.41/66.79
% 85.41/66.79 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------