%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP217-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 : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:25:35 PM UTC 2025
% Result : Unsatisfiable 16.42s 5.83s
% Output : CNFRefutation 17.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 43
% Syntax : Number of formulae : 779 ( 632 unt; 0 typ; 0 def)
% Number of atoms : 1068 (1024 equ)
% Maximal formula atoms : 14 ( 1 avg)
% Number of connectives : 627 ( 338 ~; 289 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 431 ( 431 !; 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_104,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c10 )
| ( inverse(sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( inverse(sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_176,axiom,
( ( multiply(sk_c4,sk_c11) = sk_c5 )
| ( inverse(sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_206,axiom,
( ( inverse(sk_c4) = sk_c11 )
| ( inverse(sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_248,axiom,
! [X5,X6,X3,X9,X7,X1,X2,X8,X4] :
( ( inverse(X5) != sk_c11 )
| ( multiply(X5,sk_c10) != sk_c11 )
| ( multiply(X6,X7) != sk_c10 )
| ( inverse(X6) != X7 )
| ( multiply(X7,sk_c11) != sk_c10 )
| ( multiply(sk_c11,X8) != sk_c10 )
| ( multiply(X9,sk_c11) != X8 )
| ( inverse(X9) != sk_c11 )
| ( multiply(X2,X1) != sk_c11 )
| ( inverse(X2) != X1 )
| ( multiply(X1,sk_c10) != sk_c11 )
| ( multiply(sk_c11,X3) != sk_c10 )
| ( multiply(X4,sk_c11) != X3 )
| ( inverse(X4) != sk_c11 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( inverse(sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_182,axiom,
( ( multiply(sk_c4,sk_c11) = sk_c5 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
( ( multiply(sk_c4,sk_c11) = sk_c5 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_188,axiom,
( ( multiply(sk_c4,sk_c11) = sk_c5 )
| ( inverse(sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( multiply(sk_c11,sk_c5) = sk_c10 )
| ( inverse(sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_173,axiom,
( ( multiply(sk_c4,sk_c11) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c10 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c10 )
| ( inverse(sk_c8) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c10 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_200,axiom,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_203,axiom,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_197,axiom,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_194,axiom,
( ( inverse(sk_c4) = sk_c11 )
| ( inverse(sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_191,axiom,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c6,sk_c7) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c7 ) ),
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_62170,plain,
! [X_848,Y_849,Z_850] : ( multiply(multiply(X_848,Y_849),Z_850) = multiply(X_848,multiply(Y_849,Z_850)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_62209,plain,
! [X_2,Z_850] : ( multiply(inverse(X_2),multiply(X_2,Z_850)) = multiply(identity,Z_850) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_62170]) ).
tff(c_65622,plain,
! [X_897,Z_898] : ( multiply(inverse(X_897),multiply(X_897,Z_898)) = Z_898 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62209]) ).
tff(c_62221,plain,
! [X_2,Z_850] : ( multiply(inverse(X_2),multiply(X_2,Z_850)) = Z_850 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62209]) ).
tff(c_65868,plain,
! [X_901,Z_902] : ( multiply(inverse(inverse(X_901)),Z_902) = multiply(X_901,Z_902) ),
inference(superposition,[status(thm),theory(equality)],[c_65622,c_62221]) ).
tff(c_65915,plain,
! [X_901] : ( multiply(X_901,inverse(X_901)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65868]) ).
tff(c_51840,plain,
! [X_733,Y_734,Z_735] : ( multiply(multiply(X_733,Y_734),Z_735) = multiply(X_733,multiply(Y_734,Z_735)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_51879,plain,
! [X_2,Z_735] : ( multiply(inverse(X_2),multiply(X_2,Z_735)) = multiply(identity,Z_735) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_51840]) ).
tff(c_54935,plain,
! [X_777,Z_778] : ( multiply(inverse(X_777),multiply(X_777,Z_778)) = Z_778 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51879]) ).
tff(c_51891,plain,
! [X_2,Z_735] : ( multiply(inverse(X_2),multiply(X_2,Z_735)) = Z_735 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51879]) ).
tff(c_55248,plain,
! [X_780,Z_781] : ( multiply(inverse(inverse(X_780)),Z_781) = multiply(X_780,Z_781) ),
inference(superposition,[status(thm),theory(equality)],[c_54935,c_51891]) ).
tff(c_55295,plain,
! [X_780] : ( multiply(X_780,inverse(X_780)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_55248]) ).
tff(c_42087,plain,
! [X_604,Y_605,Z_606] : ( multiply(multiply(X_604,Y_605),Z_606) = multiply(X_604,multiply(Y_605,Z_606)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_42126,plain,
! [X_2,Z_606] : ( multiply(inverse(X_2),multiply(X_2,Z_606)) = multiply(identity,Z_606) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42087]) ).
tff(c_42138,plain,
! [X_2,Z_606] : ( multiply(inverse(X_2),multiply(X_2,Z_606)) = Z_606 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42126]) ).
tff(c_43810,plain,
! [X_642,Z_643] : ( multiply(inverse(X_642),multiply(X_642,Z_643)) = Z_643 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42126]) ).
tff(c_44234,plain,
! [X_647,Z_648] : ( multiply(inverse(inverse(X_647)),Z_648) = multiply(X_647,Z_648) ),
inference(superposition,[status(thm),theory(equality)],[c_42138,c_43810]) ).
tff(c_44272,plain,
! [X_647] : ( multiply(X_647,inverse(X_647)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_44234]) ).
tff(c_34,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_161,plain,
multiply(sk_c2,sk_c3) = sk_c10,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_54,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_147,plain,
inverse(sk_c2) = sk_c3,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_151,plain,
multiply(sk_c3,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_147,c_4]) ).
tff(c_38534,plain,
! [X_537,Y_538,Z_539] : ( multiply(multiply(X_537,Y_538),Z_539) = multiply(X_537,multiply(Y_538,Z_539)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_38570,plain,
! [Z_539] : ( multiply(sk_c3,multiply(sk_c2,Z_539)) = multiply(identity,Z_539) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_38534]) ).
tff(c_39327,plain,
! [Z_558] : ( multiply(sk_c3,multiply(sk_c2,Z_558)) = Z_558 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38570]) ).
tff(c_39339,plain,
multiply(sk_c3,sk_c10) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_161,c_39327]) ).
tff(c_38579,plain,
! [X_2,Z_539] : ( multiply(inverse(X_2),multiply(X_2,Z_539)) = multiply(identity,Z_539) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_38534]) ).
tff(c_39514,plain,
! [X_562,Z_563] : ( multiply(inverse(X_562),multiply(X_562,Z_563)) = Z_563 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38579]) ).
tff(c_39565,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_39339,c_39514]) ).
tff(c_39600,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39565]) ).
tff(c_26680,plain,
! [X_389,Y_390,Z_391] : ( multiply(multiply(X_389,Y_390),Z_391) = multiply(X_389,multiply(Y_390,Z_391)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_26719,plain,
! [Z_391] : ( multiply(sk_c3,multiply(sk_c2,Z_391)) = multiply(identity,Z_391) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_26680]) ).
tff(c_26743,plain,
! [Z_392] : ( multiply(sk_c3,multiply(sk_c2,Z_392)) = Z_392 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26719]) ).
tff(c_26755,plain,
multiply(sk_c3,sk_c10) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_161,c_26743]) ).
tff(c_27174,plain,
! [Z_401] : ( multiply(sk_c2,multiply(sk_c3,Z_401)) = multiply(sk_c10,Z_401) ),
inference(superposition,[status(thm),theory(equality)],[c_161,c_26680]) ).
tff(c_27189,plain,
multiply(sk_c2,sk_c3) = multiply(sk_c10,sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_26755,c_27174]) ).
tff(c_27202,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_161,c_27189]) ).
tff(c_26728,plain,
! [X_2,Z_391] : ( multiply(inverse(X_2),multiply(X_2,Z_391)) = multiply(identity,Z_391) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_26680]) ).
tff(c_27341,plain,
! [X_403,Z_404] : ( multiply(inverse(X_403),multiply(X_403,Z_404)) = Z_404 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26728]) ).
tff(c_27380,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_27202,c_27341]) ).
tff(c_27404,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_27380]) ).
tff(c_22349,plain,
! [X_300,Y_301,Z_302] : ( multiply(multiply(X_300,Y_301),Z_302) = multiply(X_300,multiply(Y_301,Z_302)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_22400,plain,
! [X_2,Z_302] : ( multiply(inverse(X_2),multiply(X_2,Z_302)) = multiply(identity,Z_302) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_22349]) ).
tff(c_25077,plain,
! [X_354,Z_355] : ( multiply(inverse(X_354),multiply(X_354,Z_355)) = Z_355 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22400]) ).
tff(c_22413,plain,
! [X_2,Z_302] : ( multiply(inverse(X_2),multiply(X_2,Z_302)) = Z_302 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22400]) ).
tff(c_25360,plain,
! [X_358,Z_359] : ( multiply(inverse(inverse(X_358)),Z_359) = multiply(X_358,Z_359) ),
inference(superposition,[status(thm),theory(equality)],[c_25077,c_22413]) ).
tff(c_25140,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_25077]) ).
tff(c_25367,plain,
! [X_358] : ( multiply(X_358,identity) = X_358 ),
inference(superposition,[status(thm),theory(equality)],[c_25360,c_25140]) ).
tff(c_20851,plain,
! [X_273,Y_274,Z_275] : ( multiply(multiply(X_273,Y_274),Z_275) = multiply(X_273,multiply(Y_274,Z_275)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20896,plain,
! [Z_275] : ( multiply(sk_c3,multiply(sk_c2,Z_275)) = multiply(identity,Z_275) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_20851]) ).
tff(c_20920,plain,
! [Z_276] : ( multiply(sk_c3,multiply(sk_c2,Z_276)) = Z_276 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20896]) ).
tff(c_20932,plain,
multiply(sk_c3,sk_c10) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_161,c_20920]) ).
tff(c_20905,plain,
! [X_2,Z_275] : ( multiply(inverse(X_2),multiply(X_2,Z_275)) = multiply(identity,Z_275) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20851]) ).
tff(c_21781,plain,
! [X_291,Z_292] : ( multiply(inverse(X_291),multiply(X_291,Z_292)) = Z_292 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20905]) ).
tff(c_21823,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_20932,c_21781]) ).
tff(c_21857,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21823]) ).
tff(c_20188,plain,
! [X_261,Y_262,Z_263] : ( multiply(multiply(X_261,Y_262),Z_263) = multiply(X_261,multiply(Y_262,Z_263)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20230,plain,
! [Z_263] : ( multiply(sk_c3,multiply(sk_c2,Z_263)) = multiply(identity,Z_263) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_20188]) ).
tff(c_20254,plain,
! [Z_264] : ( multiply(sk_c3,multiply(sk_c2,Z_264)) = Z_264 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20230]) ).
tff(c_20266,plain,
multiply(sk_c3,sk_c10) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_161,c_20254]) ).
tff(c_20239,plain,
! [X_2,Z_263] : ( multiply(inverse(X_2),multiply(X_2,Z_263)) = multiply(identity,Z_263) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20188]) ).
tff(c_20564,plain,
! [X_270,Z_271] : ( multiply(inverse(X_270),multiply(X_270,Z_271)) = Z_271 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20239]) ).
tff(c_20606,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_20266,c_20564]) ).
tff(c_20639,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20606]) ).
tff(c_70,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_167,plain,
multiply(sk_c11,sk_c5) = sk_c10,
inference(splitLeft,[status(thm)],[c_70]) ).
tff(c_82,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c11) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_168,plain,
multiply(sk_c4,sk_c11) = sk_c5,
inference(splitLeft,[status(thm)],[c_82]) ).
tff(c_102,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_206]) ).
tff(c_133,plain,
inverse(sk_c4) = sk_c11,
inference(splitLeft,[status(thm)],[c_102]) ).
tff(c_137,plain,
multiply(sk_c11,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_133,c_4]) ).
tff(c_20233,plain,
! [Z_263] : ( multiply(sk_c11,multiply(sk_c4,Z_263)) = multiply(identity,Z_263) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_20188]) ).
tff(c_20465,plain,
! [Z_269] : ( multiply(sk_c11,multiply(sk_c4,Z_269)) = Z_269 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20233]) ).
tff(c_20477,plain,
multiply(sk_c11,sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_168,c_20465]) ).
tff(c_20481,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_167,c_20477]) ).
tff(c_18,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_121,plain,
inverse(sk_c1) = sk_c11,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_20496,plain,
inverse(sk_c1) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20481,c_121]) ).
tff(c_20514,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20496,c_4]) ).
tff(c_20666,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20639,c_20514]) ).
tff(c_9498,plain,
! [X_139,Y_140,Z_141] : ( multiply(multiply(X_139,Y_140),Z_141) = multiply(X_139,multiply(Y_140,Z_141)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9552,plain,
! [X_2,Z_141] : ( multiply(inverse(X_2),multiply(X_2,Z_141)) = multiply(identity,Z_141) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9498]) ).
tff(c_12656,plain,
! [X_183,Z_184] : ( multiply(inverse(X_183),multiply(X_183,Z_184)) = Z_184 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9552]) ).
tff(c_9565,plain,
! [X_2,Z_141] : ( multiply(inverse(X_2),multiply(X_2,Z_141)) = Z_141 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9552]) ).
tff(c_13111,plain,
! [X_188,Z_189] : ( multiply(inverse(inverse(X_188)),Z_189) = multiply(X_188,Z_189) ),
inference(superposition,[status(thm),theory(equality)],[c_12656,c_9565]) ).
tff(c_13158,plain,
! [X_188] : ( multiply(X_188,inverse(X_188)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13111]) ).
tff(c_9543,plain,
! [Z_141] : ( multiply(sk_c3,multiply(sk_c2,Z_141)) = multiply(identity,Z_141) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_9498]) ).
tff(c_9635,plain,
! [Z_145] : ( multiply(sk_c3,multiply(sk_c2,Z_145)) = Z_145 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9543]) ).
tff(c_9647,plain,
multiply(sk_c3,sk_c10) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_161,c_9635]) ).
tff(c_12716,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_9647,c_12656]) ).
tff(c_12754,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12716]) ).
tff(c_12740,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12656]) ).
tff(c_13121,plain,
! [X_188] : ( multiply(X_188,identity) = X_188 ),
inference(superposition,[status(thm),theory(equality)],[c_13111,c_12740]) ).
tff(c_9916,plain,
! [X_149,Z_150] : ( multiply(inverse(X_149),multiply(X_149,Z_150)) = Z_150 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9552]) ).
tff(c_10371,plain,
! [X_154,Z_155] : ( multiply(inverse(inverse(X_154)),Z_155) = multiply(X_154,Z_155) ),
inference(superposition,[status(thm),theory(equality)],[c_9916,c_9565]) ).
tff(c_10418,plain,
! [X_154] : ( multiply(X_154,inverse(X_154)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_10371]) ).
tff(c_9976,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_9647,c_9916]) ).
tff(c_10014,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_9976]) ).
tff(c_10000,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9916]) ).
tff(c_10381,plain,
! [X_154] : ( multiply(X_154,identity) = X_154 ),
inference(superposition,[status(thm),theory(equality)],[c_10371,c_10000]) ).
tff(c_9546,plain,
! [Z_141] : ( multiply(sk_c11,multiply(sk_c4,Z_141)) = multiply(identity,Z_141) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_9498]) ).
tff(c_9681,plain,
! [Z_147] : ( multiply(sk_c11,multiply(sk_c4,Z_147)) = Z_147 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9546]) ).
tff(c_9693,plain,
multiply(sk_c11,sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_168,c_9681]) ).
tff(c_9697,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_167,c_9693]) ).
tff(c_9711,plain,
multiply(sk_c10,sk_c5) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_9697,c_167]) ).
tff(c_9713,plain,
inverse(sk_c4) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_9697,c_133]) ).
tff(c_9710,plain,
multiply(sk_c4,sk_c10) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9697,c_168]) ).
tff(c_30,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_181,plain,
multiply(sk_c1,sk_c10) = sk_c11,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_104,plain,
! [X5_6,X2_12,X9_9,X4_14,X6_7] :
( ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( multiply(X5_6,sk_c10) != sk_c11 )
| ( inverse(X5_6) != sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_248]) ).
tff(c_9607,plain,
! [X5_144] :
( ( multiply(X5_144,sk_c10) != sk_c11 )
| ( inverse(X5_144) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_9620,plain,
inverse(sk_c1) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_181,c_9607]) ).
tff(c_9633,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_121,c_9620]) ).
tff(c_9634,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_9698,plain,
! [X4_14] :
( ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_9634]) ).
tff(c_9766,plain,
! [X4_148] :
( ( inverse(X4_148) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_148,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_9697,c_9697,c_9697,c_9698]) ).
tff(c_9769,plain,
( ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c10,sk_c5) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_9710,c_9766]) ).
tff(c_9787,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9711,c_9713,c_9769]) ).
tff(c_9788,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_9634]) ).
tff(c_9855,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_9697,c_9697,c_9697,c_9697,c_9697,c_9697,c_9788]) ).
tff(c_9856,plain,
! [X6_7] :
( ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_9855]) ).
tff(c_12593,plain,
! [X6_7] : ( inverse(X6_7) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_10418,c_10014,c_10381,c_10014,c_10014,c_9856]) ).
tff(c_222,plain,
! [X_17,Y_18,Z_19] : ( multiply(multiply(X_17,Y_18),Z_19) = multiply(X_17,multiply(Y_18,Z_19)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_261,plain,
! [X_2,Z_19] : ( multiply(inverse(X_2),multiply(X_2,Z_19)) = multiply(identity,Z_19) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_222]) ).
tff(c_1877,plain,
! [X_49,Z_50] : ( multiply(inverse(X_49),multiply(X_49,Z_50)) = Z_50 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_261]) ).
tff(c_272,plain,
! [X_2,Z_19] : ( multiply(inverse(X_2),multiply(X_2,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_261]) ).
tff(c_2166,plain,
! [X_53,Z_54] : ( multiply(inverse(inverse(X_53)),Z_54) = multiply(X_53,Z_54) ),
inference(superposition,[status(thm),theory(equality)],[c_1877,c_272]) ).
tff(c_2187,plain,
! [X_53] : ( multiply(X_53,inverse(X_53)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_2166,c_4]) ).
tff(c_255,plain,
! [Z_19] : ( multiply(sk_c11,multiply(sk_c4,Z_19)) = multiply(identity,Z_19) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_222]) ).
tff(c_297,plain,
! [Z_21] : ( multiply(sk_c11,multiply(sk_c4,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_255]) ).
tff(c_309,plain,
multiply(sk_c11,sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_168,c_297]) ).
tff(c_313,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_167,c_309]) ).
tff(c_66,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_188,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_433,plain,
multiply(sk_c3,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_313,c_188]) ).
tff(c_252,plain,
! [Z_19] : ( multiply(sk_c3,multiply(sk_c2,Z_19)) = multiply(identity,Z_19) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_222]) ).
tff(c_274,plain,
! [Z_20] : ( multiply(sk_c3,multiply(sk_c2,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_252]) ).
tff(c_286,plain,
multiply(sk_c3,sk_c10) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_161,c_274]) ).
tff(c_1853,plain,
sk_c3 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_433,c_286]) ).
tff(c_1861,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_1853,c_433]) ).
tff(c_1964,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_1861,c_272]) ).
tff(c_1970,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1964]) ).
tff(c_1922,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1877]) ).
tff(c_2173,plain,
! [X_53] : ( multiply(X_53,identity) = X_53 ),
inference(superposition,[status(thm),theory(equality)],[c_2166,c_1922]) ).
tff(c_523,plain,
! [X_23,Z_24] : ( multiply(inverse(X_23),multiply(X_23,Z_24)) = Z_24 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_261]) ).
tff(c_812,plain,
! [X_27,Z_28] : ( multiply(inverse(inverse(X_27)),Z_28) = multiply(X_27,Z_28) ),
inference(superposition,[status(thm),theory(equality)],[c_523,c_272]) ).
tff(c_568,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_523]) ).
tff(c_819,plain,
! [X_27] : ( multiply(X_27,identity) = X_27 ),
inference(superposition,[status(thm),theory(equality)],[c_812,c_568]) ).
tff(c_499,plain,
sk_c3 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_433,c_286]) ).
tff(c_507,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_499,c_433]) ).
tff(c_610,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_507,c_272]) ).
tff(c_616,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_610]) ).
tff(c_323,plain,
inverse(sk_c1) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_313,c_121]) ).
tff(c_317,plain,
multiply(sk_c1,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_313,c_181]) ).
tff(c_314,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c10) != sk_c11 )
| ( inverse(X5_6) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_382,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c10) != sk_c10 )
| ( inverse(X5_6) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_313,c_313,c_314]) ).
tff(c_421,plain,
inverse(sk_c1) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_317,c_382]) ).
tff(c_430,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_323,c_421]) ).
tff(c_431,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_459,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X4_14) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_14,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_313,c_313,c_313,c_313,c_313,c_313,c_313,c_313,c_313,c_431]) ).
tff(c_460,plain,
! [X4_14] :
( ( inverse(X4_14) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_14,sk_c10)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_459]) ).
tff(c_1811,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_819,c_616,c_616,c_2,c_616,c_616,c_460]) ).
tff(c_511,plain,
inverse(sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_499,c_147]) ).
tff(c_519,plain,
multiply(sk_c10,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_511,c_4]) ).
tff(c_691,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_616,c_519]) ).
tff(c_621,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_616,c_511]) ).
tff(c_692,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_691,c_621]) ).
tff(c_1813,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1811,c_692]) ).
tff(c_1814,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_459]) ).
tff(c_9416,plain,
! [X2_12,X9_9,X6_7] :
( ( inverse(X2_12) != identity )
| ( inverse(X9_9) != identity )
| ( identity != X9_9 )
| ( inverse(X6_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2187,c_1970,c_2173,c_1970,c_1970,c_2173,c_1970,c_1970,c_2,c_1970,c_1970,c_2187,c_1970,c_2173,c_1970,c_1970,c_1814]) ).
tff(c_9417,plain,
! [X6_7] : ( inverse(X6_7) != identity ),
inference(splitLeft,[status(thm)],[c_9416]) ).
tff(c_1865,plain,
inverse(sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_1853,c_147]) ).
tff(c_1873,plain,
multiply(sk_c10,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1865,c_4]) ).
tff(c_2045,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1970,c_1873]) ).
tff(c_1975,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1970,c_1865]) ).
tff(c_2046,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2045,c_1975]) ).
tff(c_9419,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9417,c_2046]) ).
tff(c_9420,plain,
! [X2_12,X9_9] :
( ( inverse(X2_12) != identity )
| ( inverse(X9_9) != identity )
| ( identity != X9_9 ) ),
inference(splitRight,[status(thm)],[c_9416]) ).
tff(c_9422,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9420]) ).
tff(c_9424,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9422,c_2046]) ).
tff(c_9425,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitRight,[status(thm)],[c_9420]) ).
tff(c_9428,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9425,c_2046]) ).
tff(c_9429,plain,
inverse(sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_9798,plain,
inverse(sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_9697,c_9429]) ).
tff(c_9836,plain,
multiply(sk_c10,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9798,c_4]) ).
tff(c_10045,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10014,c_9836]) ).
tff(c_10027,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10014,c_9798]) ).
tff(c_10113,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10045,c_10027]) ).
tff(c_12595,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12593,c_10113]) ).
tff(c_12596,plain,
! [X9_9,X2_12] :
( ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_9855]) ).
tff(c_19270,plain,
! [X9_9,X2_12] :
( ( inverse(X9_9) != identity )
| ( identity != X9_9 )
| ( inverse(X2_12) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13158,c_12754,c_13121,c_12754,c_12754,c_13121,c_12754,c_12754,c_2,c_12754,c_12754,c_12596]) ).
tff(c_19271,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitLeft,[status(thm)],[c_19270]) ).
tff(c_12785,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12754,c_9836]) ).
tff(c_12767,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12754,c_9798]) ).
tff(c_12853,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12785,c_12767]) ).
tff(c_19273,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19271,c_12853]) ).
tff(c_19275,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_19270]) ).
tff(c_19277,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19275,c_12853]) ).
tff(c_19279,plain,
multiply(sk_c1,sk_c10) != sk_c11,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_20489,plain,
multiply(sk_c1,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20481,c_19279]) ).
tff(c_20761,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20666,c_20639,c_20639,c_20489]) ).
tff(c_20763,plain,
multiply(sk_c4,sk_c11) != sk_c5,
inference(splitRight,[status(thm)],[c_82]) ).
tff(c_86,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c11) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_20841,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_20763,c_86]) ).
tff(c_88,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(sk_c4,sk_c11) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_20819,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_20763,c_88]) ).
tff(c_90,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c4,sk_c11) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_20796,plain,
inverse(sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_20763,c_90]) ).
tff(c_20800,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20796,c_4]) ).
tff(c_20878,plain,
! [Z_275] : ( multiply(sk_c11,multiply(sk_c8,Z_275)) = multiply(identity,Z_275) ),
inference(superposition,[status(thm),theory(equality)],[c_20800,c_20851]) ).
tff(c_21683,plain,
! [Z_290] : ( multiply(sk_c11,multiply(sk_c8,Z_290)) = Z_290 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20878]) ).
tff(c_21695,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_20819,c_21683]) ).
tff(c_21699,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20841,c_21695]) ).
tff(c_21714,plain,
multiply(sk_c10,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21699,c_137]) ).
tff(c_21952,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21857,c_21714]) ).
tff(c_21713,plain,
multiply(sk_c10,sk_c5) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_21699,c_167]) ).
tff(c_21940,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21857,c_2,c_21857,c_21713]) ).
tff(c_21712,plain,
multiply(sk_c4,sk_c10) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_21699,c_20763]) ).
tff(c_21864,plain,
multiply(sk_c4,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_21857,c_21712]) ).
tff(c_22039,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21952,c_21940,c_21864]) ).
tff(c_22041,plain,
multiply(sk_c11,sk_c5) != sk_c10,
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_74,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_22331,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_22041,c_74]) ).
tff(c_22072,plain,
multiply(sk_c4,sk_c11) = sk_c5,
inference(splitLeft,[status(thm)],[c_90]) ).
tff(c_22130,plain,
! [X_293,Y_294,Z_295] : ( multiply(multiply(X_293,Y_294),Z_295) = multiply(X_293,multiply(Y_294,Z_295)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_22178,plain,
! [Z_295] : ( multiply(sk_c11,multiply(sk_c4,Z_295)) = multiply(identity,Z_295) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_22130]) ).
tff(c_22222,plain,
! [Z_297] : ( multiply(sk_c11,multiply(sk_c4,Z_297)) = Z_297 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22178]) ).
tff(c_22234,plain,
multiply(sk_c11,sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_22072,c_22222]) ).
tff(c_22238,plain,
sk_c11 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22234,c_22041]) ).
tff(c_22106,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_22041,c_74]) ).
tff(c_76,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_22121,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_22041,c_76]) ).
tff(c_78,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c5) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_22082,plain,
inverse(sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_22041,c_78]) ).
tff(c_22086,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22082,c_4]) ).
tff(c_22157,plain,
! [Z_295] : ( multiply(sk_c11,multiply(sk_c8,Z_295)) = multiply(identity,Z_295) ),
inference(superposition,[status(thm),theory(equality)],[c_22086,c_22130]) ).
tff(c_22270,plain,
! [Z_299] : ( multiply(sk_c11,multiply(sk_c8,Z_299)) = Z_299 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22157]) ).
tff(c_22282,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_22121,c_22270]) ).
tff(c_22286,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22106,c_22282]) ).
tff(c_22288,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22238,c_22286]) ).
tff(c_22290,plain,
multiply(sk_c4,sk_c11) != sk_c5,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_22319,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_22290,c_88]) ).
tff(c_22289,plain,
inverse(sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_22295,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22289,c_4]) ).
tff(c_22376,plain,
! [Z_302] : ( multiply(sk_c11,multiply(sk_c8,Z_302)) = multiply(identity,Z_302) ),
inference(superposition,[status(thm),theory(equality)],[c_22295,c_22349]) ).
tff(c_22870,plain,
! [Z_317] : ( multiply(sk_c11,multiply(sk_c8,Z_317)) = Z_317 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22376]) ).
tff(c_22885,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_22319,c_22870]) ).
tff(c_22889,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22331,c_22885]) ).
tff(c_80,plain,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( multiply(sk_c4,sk_c11) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_22309,plain,
multiply(sk_c6,sk_c7) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_22290,c_80]) ).
tff(c_22040,plain,
inverse(sk_c6) = sk_c7,
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_22045,plain,
multiply(sk_c7,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22040,c_4]) ).
tff(c_22385,plain,
! [Z_302] : ( multiply(sk_c7,multiply(sk_c6,Z_302)) = multiply(identity,Z_302) ),
inference(superposition,[status(thm),theory(equality)],[c_22045,c_22349]) ).
tff(c_22798,plain,
! [Z_315] : ( multiply(sk_c7,multiply(sk_c6,Z_315)) = Z_315 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22385]) ).
tff(c_22810,plain,
multiply(sk_c7,sk_c11) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_22309,c_22798]) ).
tff(c_22999,plain,
multiply(sk_c7,sk_c10) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_22889,c_22810]) ).
tff(c_25113,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_22999,c_25077]) ).
tff(c_25150,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25113]) ).
tff(c_23153,plain,
! [X_320,Z_321] : ( multiply(inverse(X_320),multiply(X_320,Z_321)) = Z_321 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22400]) ).
tff(c_23436,plain,
! [X_324,Z_325] : ( multiply(inverse(inverse(X_324)),Z_325) = multiply(X_324,Z_325) ),
inference(superposition,[status(thm),theory(equality)],[c_23153,c_22413]) ).
tff(c_23457,plain,
! [X_324] : ( multiply(X_324,inverse(X_324)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_23436,c_4]) ).
tff(c_23189,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_22999,c_23153]) ).
tff(c_23226,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_23189]) ).
tff(c_23216,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_23153]) ).
tff(c_23443,plain,
! [X_324] : ( multiply(X_324,identity) = X_324 ),
inference(superposition,[status(thm),theory(equality)],[c_23436,c_23216]) ).
tff(c_22391,plain,
! [Z_302] : ( multiply(sk_c3,multiply(sk_c2,Z_302)) = multiply(identity,Z_302) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_22349]) ).
tff(c_22503,plain,
! [Z_307] : ( multiply(sk_c3,multiply(sk_c2,Z_307)) = Z_307 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22391]) ).
tff(c_22515,plain,
multiply(sk_c3,sk_c10) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_161,c_22503]) ).
tff(c_22064,plain,
multiply(sk_c1,sk_c10) = sk_c11,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_22475,plain,
! [X5_306] :
( ( multiply(X5_306,sk_c10) != sk_c11 )
| ( inverse(X5_306) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_22488,plain,
inverse(sk_c1) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_22064,c_22475]) ).
tff(c_22501,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_121,c_22488]) ).
tff(c_22502,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_22730,plain,
! [X4_314] :
( ( inverse(X4_314) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_314,sk_c11)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_22502]) ).
tff(c_22758,plain,
( ( inverse(sk_c8) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22319,c_22730]) ).
tff(c_22779,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_22331,c_22289,c_22758]) ).
tff(c_22780,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_22502]) ).
tff(c_22890,plain,
! [X6_7] :
( ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_22780]) ).
tff(c_22973,plain,
! [X6_318] :
( ( multiply(inverse(X6_318),sk_c10) != sk_c10 )
| ( multiply(X6_318,inverse(X6_318)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_22889,c_22890]) ).
tff(c_22983,plain,
( ( multiply(sk_c3,sk_c10) != sk_c10 )
| ( multiply(sk_c2,inverse(sk_c2)) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_147,c_22973]) ).
tff(c_22992,plain,
sk_c3 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_161,c_147,c_22515,c_22983]) ).
tff(c_22900,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22889,c_22331]) ).
tff(c_22059,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_22542,plain,
! [Z_309] : ( multiply(sk_c3,multiply(sk_c11,Z_309)) = multiply(sk_c10,Z_309) ),
inference(superposition,[status(thm),theory(equality)],[c_22059,c_22349]) ).
tff(c_22557,plain,
multiply(sk_c3,sk_c10) = multiply(sk_c10,sk_c9),
inference(superposition,[status(thm),theory(equality)],[c_22331,c_22542]) ).
tff(c_22570,plain,
multiply(sk_c10,sk_c9) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_22515,c_22557]) ).
tff(c_22993,plain,
sk_c3 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22900,c_22570]) ).
tff(c_22995,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22992,c_22993]) ).
tff(c_22996,plain,
! [X9_9,X2_12] :
( ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_22780]) ).
tff(c_23084,plain,
! [X9_9,X2_12] :
( ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_22889,c_22889,c_22889,c_22889,c_22889,c_22996]) ).
tff(c_23085,plain,
! [X2_12] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_23084]) ).
tff(c_25006,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_23457,c_23226,c_23443,c_23226,c_23226,c_23085]) ).
tff(c_23017,plain,
inverse(sk_c4) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22889,c_133]) ).
tff(c_23070,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23017,c_4]) ).
tff(c_23252,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23226,c_23070]) ).
tff(c_23243,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23226,c_23017]) ).
tff(c_23265,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23252,c_23243]) ).
tff(c_25008,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25006,c_23265]) ).
tff(c_25009,plain,
! [X9_9] :
( ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_23084]) ).
tff(c_26385,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_25367,c_25150,c_25150,c_2,c_25150,c_25150,c_25009]) ).
tff(c_25176,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25150,c_23070]) ).
tff(c_25167,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25150,c_23017]) ).
tff(c_25189,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25176,c_25167]) ).
tff(c_26387,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26385,c_25189]) ).
tff(c_26389,plain,
multiply(sk_c1,sk_c10) != sk_c11,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_26,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_26656,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_26389,c_26]) ).
tff(c_26424,plain,
multiply(sk_c4,sk_c11) = sk_c5,
inference(splitLeft,[status(thm)],[c_88]) ).
tff(c_26456,plain,
! [X_380,Y_381,Z_382] : ( multiply(multiply(X_380,Y_381),Z_382) = multiply(X_380,multiply(Y_381,Z_382)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_26501,plain,
! [Z_382] : ( multiply(sk_c11,multiply(sk_c4,Z_382)) = multiply(identity,Z_382) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_26456]) ).
tff(c_26546,plain,
! [Z_384] : ( multiply(sk_c11,multiply(sk_c4,Z_384)) = Z_384 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26501]) ).
tff(c_26558,plain,
multiply(sk_c11,sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_26424,c_26546]) ).
tff(c_26562,plain,
sk_c11 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_26558,c_22041]) ).
tff(c_26436,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_22041,c_74]) ).
tff(c_26430,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_22041,c_76]) ).
tff(c_26388,plain,
inverse(sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_26393,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_26388,c_4]) ).
tff(c_26486,plain,
! [Z_382] : ( multiply(sk_c11,multiply(sk_c8,Z_382)) = multiply(identity,Z_382) ),
inference(superposition,[status(thm),theory(equality)],[c_26393,c_26456]) ).
tff(c_26628,plain,
! [Z_388] : ( multiply(sk_c11,multiply(sk_c8,Z_388)) = Z_388 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26486]) ).
tff(c_26640,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_26430,c_26628]) ).
tff(c_26644,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_26436,c_26640]) ).
tff(c_26646,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26562,c_26644]) ).
tff(c_26647,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(splitRight,[status(thm)],[c_88]) ).
tff(c_26707,plain,
! [Z_391] : ( multiply(sk_c11,multiply(sk_c8,Z_391)) = multiply(identity,Z_391) ),
inference(superposition,[status(thm),theory(equality)],[c_26393,c_26680]) ).
tff(c_27232,plain,
! [Z_402] : ( multiply(sk_c11,multiply(sk_c8,Z_402)) = Z_402 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26707]) ).
tff(c_27244,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_26647,c_27232]) ).
tff(c_27248,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_26656,c_27244]) ).
tff(c_125,plain,
multiply(sk_c11,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_121,c_4]) ).
tff(c_27266,plain,
multiply(sk_c10,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27248,c_125]) ).
tff(c_27479,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27404,c_27266]) ).
tff(c_27260,plain,
multiply(sk_c1,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_27248,c_26389]) ).
tff(c_27408,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_27404,c_27404,c_27260]) ).
tff(c_27586,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27479,c_27408]) ).
tff(c_27588,plain,
multiply(sk_c3,sk_c11) != sk_c10,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_62,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_38511,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_27588,c_62]) ).
tff(c_64,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_38500,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_27588,c_64]) ).
tff(c_27587,plain,
inverse(sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_27592,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27587,c_4]) ).
tff(c_38561,plain,
! [Z_539] : ( multiply(sk_c11,multiply(sk_c8,Z_539)) = multiply(identity,Z_539) ),
inference(superposition,[status(thm),theory(equality)],[c_27592,c_38534]) ).
tff(c_39351,plain,
! [Z_559] : ( multiply(sk_c11,multiply(sk_c8,Z_559)) = Z_559 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38561]) ).
tff(c_39363,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_38500,c_39351]) ).
tff(c_39367,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_38511,c_39363]) ).
tff(c_39382,plain,
multiply(sk_c10,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39367,c_125]) ).
tff(c_39609,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39600,c_39382]) ).
tff(c_38592,plain,
! [X_2,Z_539] : ( multiply(inverse(X_2),multiply(X_2,Z_539)) = Z_539 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38579]) ).
tff(c_39749,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_39609,c_38592]) ).
tff(c_39761,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39749]) ).
tff(c_27922,plain,
! [X_416,Y_417,Z_418] : ( multiply(multiply(X_416,Y_417),Z_418) = multiply(X_416,multiply(Y_417,Z_418)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_27970,plain,
! [X_2,Z_418] : ( multiply(inverse(X_2),multiply(X_2,Z_418)) = multiply(identity,Z_418) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_27922]) ).
tff(c_31482,plain,
! [X_465,Z_466] : ( multiply(inverse(X_465),multiply(X_465,Z_466)) = Z_466 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27970]) ).
tff(c_27983,plain,
! [X_2,Z_418] : ( multiply(inverse(X_2),multiply(X_2,Z_418)) = Z_418 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27970]) ).
tff(c_31925,plain,
! [X_471,Z_472] : ( multiply(inverse(inverse(X_471)),Z_472) = multiply(X_471,Z_472) ),
inference(superposition,[status(thm),theory(equality)],[c_31482,c_27983]) ).
tff(c_31949,plain,
! [X_471] : ( multiply(X_471,inverse(X_471)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_31925,c_4]) ).
tff(c_27961,plain,
! [Z_418] : ( multiply(sk_c3,multiply(sk_c2,Z_418)) = multiply(identity,Z_418) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_27922]) ).
tff(c_27985,plain,
! [Z_419] : ( multiply(sk_c3,multiply(sk_c2,Z_419)) = Z_419 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27961]) ).
tff(c_27997,plain,
multiply(sk_c3,sk_c10) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_161,c_27985]) ).
tff(c_31524,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_27997,c_31482]) ).
tff(c_31556,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_31524]) ).
tff(c_31548,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_31482]) ).
tff(c_31935,plain,
! [X_471] : ( multiply(X_471,identity) = X_471 ),
inference(superposition,[status(thm),theory(equality)],[c_31925,c_31548]) ).
tff(c_28329,plain,
! [X_427,Z_428] : ( multiply(inverse(X_427),multiply(X_427,Z_428)) = Z_428 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27970]) ).
tff(c_28772,plain,
! [X_433,Z_434] : ( multiply(inverse(inverse(X_433)),Z_434) = multiply(X_433,Z_434) ),
inference(superposition,[status(thm),theory(equality)],[c_28329,c_27983]) ).
tff(c_28796,plain,
! [X_433] : ( multiply(X_433,inverse(X_433)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_28772,c_4]) ).
tff(c_28371,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_27997,c_28329]) ).
tff(c_28403,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_28371]) ).
tff(c_28395,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_28329]) ).
tff(c_28782,plain,
! [X_433] : ( multiply(X_433,identity) = X_433 ),
inference(superposition,[status(thm),theory(equality)],[c_28772,c_28395]) ).
tff(c_27902,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_22041,c_74]) ).
tff(c_27623,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_27588,c_64]) ).
tff(c_27952,plain,
! [Z_418] : ( multiply(sk_c11,multiply(sk_c8,Z_418)) = multiply(identity,Z_418) ),
inference(superposition,[status(thm),theory(equality)],[c_27592,c_27922]) ).
tff(c_28109,plain,
! [Z_425] : ( multiply(sk_c11,multiply(sk_c8,Z_425)) = Z_425 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27952]) ).
tff(c_28121,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_27623,c_28109]) ).
tff(c_28125,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_27902,c_28121]) ).
tff(c_28131,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_28125,c_27902]) ).
tff(c_28139,plain,
inverse(sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_28125,c_27587]) ).
tff(c_28134,plain,
multiply(sk_c8,sk_c10) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_28125,c_27623]) ).
tff(c_24,plain,
( ( multiply(sk_c7,sk_c10) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_27618,plain,
multiply(sk_c1,sk_c10) = sk_c11,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_28038,plain,
! [X5_422] :
( ( multiply(X5_422,sk_c10) != sk_c11 )
| ( inverse(X5_422) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_28051,plain,
inverse(sk_c1) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_27618,c_28038]) ).
tff(c_28064,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_121,c_28051]) ).
tff(c_28065,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_28126,plain,
! [X4_14] :
( ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_28065]) ).
tff(c_28195,plain,
! [X4_14] :
( ( inverse(X4_14) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_14,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28125,c_28125,c_28125,c_28126]) ).
tff(c_28234,plain,
( ( inverse(sk_c8) != sk_c10 )
| ( multiply(sk_c10,sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_28134,c_28195]) ).
tff(c_28242,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28131,c_28139,c_28234]) ).
tff(c_28243,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_28065]) ).
tff(c_28281,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28125,c_28125,c_28125,c_28125,c_28125,c_28125,c_28243]) ).
tff(c_28282,plain,
! [X6_7] :
( ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_28281]) ).
tff(c_31432,plain,
! [X6_7] : ( inverse(X6_7) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_28796,c_28403,c_28782,c_28403,c_28403,c_28282]) ).
tff(c_28256,plain,
inverse(sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_28125,c_27587]) ).
tff(c_28270,plain,
multiply(sk_c10,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28256,c_4]) ).
tff(c_28425,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28403,c_28270]) ).
tff(c_28415,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28403,c_28256]) ).
tff(c_28434,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28425,c_28415]) ).
tff(c_31434,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31432,c_28434]) ).
tff(c_31435,plain,
! [X9_9,X2_12] :
( ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_28281]) ).
tff(c_38486,plain,
! [X9_9,X2_12] :
( ( inverse(X9_9) != identity )
| ( identity != X9_9 )
| ( inverse(X2_12) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_31949,c_31556,c_31935,c_31556,c_31556,c_31935,c_31556,c_31556,c_2,c_31556,c_31556,c_31435]) ).
tff(c_38487,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitLeft,[status(thm)],[c_38486]) ).
tff(c_31578,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31556,c_28270]) ).
tff(c_31568,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31556,c_28256]) ).
tff(c_31587,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31578,c_31568]) ).
tff(c_38489,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38487,c_31587]) ).
tff(c_38491,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_38486]) ).
tff(c_38493,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38491,c_31587]) ).
tff(c_38495,plain,
multiply(sk_c1,sk_c10) != sk_c11,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_39372,plain,
multiply(sk_c1,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_39367,c_38495]) ).
tff(c_39610,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_39600,c_39600,c_39372]) ).
tff(c_39766,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_39761,c_39610]) ).
tff(c_39771,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39766]) ).
tff(c_39773,plain,
multiply(sk_c2,sk_c3) != sk_c10,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_38,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_39852,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_39773,c_38]) ).
tff(c_40,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_39824,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_39773,c_40]) ).
tff(c_42,plain,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_39804,plain,
inverse(sk_c8) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_39773,c_42]) ).
tff(c_39808,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39804,c_4]) ).
tff(c_39860,plain,
! [X_565,Y_566,Z_567] : ( multiply(multiply(X_565,Y_566),Z_567) = multiply(X_565,multiply(Y_566,Z_567)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_39887,plain,
! [Z_567] : ( multiply(sk_c11,multiply(sk_c8,Z_567)) = multiply(identity,Z_567) ),
inference(superposition,[status(thm),theory(equality)],[c_39808,c_39860]) ).
tff(c_40235,plain,
! [Z_577] : ( multiply(sk_c11,multiply(sk_c8,Z_577)) = Z_577 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39887]) ).
tff(c_40247,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_39824,c_40235]) ).
tff(c_40251,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_39852,c_40247]) ).
tff(c_36,plain,
( ( multiply(sk_c7,sk_c10) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_39838,plain,
multiply(sk_c7,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_39773,c_36]) ).
tff(c_40258,plain,
multiply(sk_c7,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40251,c_39838]) ).
tff(c_32,plain,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_39829,plain,
multiply(sk_c6,sk_c7) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_39773,c_32]) ).
tff(c_39772,plain,
inverse(sk_c6) = sk_c7,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_39777,plain,
multiply(sk_c7,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39772,c_4]) ).
tff(c_39896,plain,
! [Z_567] : ( multiply(sk_c7,multiply(sk_c6,Z_567)) = multiply(identity,Z_567) ),
inference(superposition,[status(thm),theory(equality)],[c_39777,c_39860]) ).
tff(c_40034,plain,
! [Z_574] : ( multiply(sk_c7,multiply(sk_c6,Z_574)) = Z_574 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39896]) ).
tff(c_40046,plain,
multiply(sk_c7,sk_c11) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_39829,c_40034]) ).
tff(c_40253,plain,
multiply(sk_c7,sk_c10) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_40251,c_40046]) ).
tff(c_40353,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40258,c_40253]) ).
tff(c_40362,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40353,c_40258]) ).
tff(c_39908,plain,
! [X_2,Z_567] : ( multiply(inverse(X_2),multiply(X_2,Z_567)) = multiply(identity,Z_567) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39860]) ).
tff(c_39921,plain,
! [X_2,Z_567] : ( multiply(inverse(X_2),multiply(X_2,Z_567)) = Z_567 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39908]) ).
tff(c_40486,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_40362,c_39921]) ).
tff(c_40492,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40486]) ).
tff(c_40266,plain,
inverse(sk_c4) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40251,c_133]) ).
tff(c_40298,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40266,c_4]) ).
tff(c_40513,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40492,c_40298]) ).
tff(c_40502,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40492,c_40266]) ).
tff(c_40595,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40513,c_40502]) ).
tff(c_40506,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40492,c_40251]) ).
tff(c_39793,plain,
multiply(sk_c3,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_39890,plain,
! [Z_567] : ( multiply(sk_c3,multiply(sk_c11,Z_567)) = multiply(sk_c10,Z_567) ),
inference(superposition,[status(thm),theory(equality)],[c_39793,c_39860]) ).
tff(c_40557,plain,
! [Z_581] : ( multiply(sk_c3,Z_581) = Z_581 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40506,c_2,c_40492,c_39890]) ).
tff(c_40572,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_40557,c_151]) ).
tff(c_40587,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_40572,c_147]) ).
tff(c_40615,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40595,c_40587]) ).
tff(c_40507,plain,
multiply(sk_c2,sk_c3) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_40492,c_39773]) ).
tff(c_40686,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40615,c_2,c_40572,c_40507]) ).
tff(c_40688,plain,
multiply(sk_c3,sk_c11) != sk_c10,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_40738,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_40688,c_62]) ).
tff(c_40717,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_39773,c_40]) ).
tff(c_40687,plain,
inverse(sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_40692,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40687,c_4]) ).
tff(c_40757,plain,
! [X_583,Y_584,Z_585] : ( multiply(multiply(X_583,Y_584),Z_585) = multiply(X_583,multiply(Y_584,Z_585)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_40784,plain,
! [Z_585] : ( multiply(sk_c11,multiply(sk_c8,Z_585)) = multiply(identity,Z_585) ),
inference(superposition,[status(thm),theory(equality)],[c_40692,c_40757]) ).
tff(c_41194,plain,
! [Z_595] : ( multiply(sk_c11,multiply(sk_c8,Z_595)) = Z_595 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40784]) ).
tff(c_41206,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_40717,c_41194]) ).
tff(c_41210,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_40738,c_41206]) ).
tff(c_40732,plain,
multiply(sk_c7,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_39773,c_36]) ).
tff(c_41345,plain,
multiply(sk_c7,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_41210,c_40732]) ).
tff(c_40723,plain,
multiply(sk_c6,sk_c7) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_39773,c_32]) ).
tff(c_40790,plain,
! [Z_585] : ( multiply(sk_c7,multiply(sk_c6,Z_585)) = multiply(identity,Z_585) ),
inference(superposition,[status(thm),theory(equality)],[c_39777,c_40757]) ).
tff(c_40866,plain,
! [Z_589] : ( multiply(sk_c7,multiply(sk_c6,Z_589)) = Z_589 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40790]) ).
tff(c_40878,plain,
multiply(sk_c7,sk_c11) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40723,c_40866]) ).
tff(c_41340,plain,
multiply(sk_c7,sk_c10) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_41210,c_40878]) ).
tff(c_41440,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_41345,c_41340]) ).
tff(c_41529,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_41440,c_41345]) ).
tff(c_40802,plain,
! [X_2,Z_585] : ( multiply(inverse(X_2),multiply(X_2,Z_585)) = multiply(identity,Z_585) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_40757]) ).
tff(c_40815,plain,
! [X_2,Z_585] : ( multiply(inverse(X_2),multiply(X_2,Z_585)) = Z_585 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40802]) ).
tff(c_41581,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_41529,c_40815]) ).
tff(c_41587,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_41581]) ).
tff(c_41641,plain,
multiply(sk_c2,sk_c3) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_41587,c_39773]) ).
tff(c_41448,plain,
! [X_597,Z_598] : ( multiply(inverse(X_597),multiply(X_597,Z_598)) = Z_598 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40802]) ).
tff(c_41844,plain,
! [X_601,Z_602] : ( multiply(inverse(inverse(X_601)),Z_602) = multiply(X_601,Z_602) ),
inference(superposition,[status(thm),theory(equality)],[c_41448,c_40815]) ).
tff(c_41517,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_41448]) ).
tff(c_41891,plain,
! [X_603] : ( multiply(X_603,identity) = X_603 ),
inference(superposition,[status(thm),theory(equality)],[c_41844,c_41517]) ).
tff(c_41511,plain,
multiply(inverse(sk_c3),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_151,c_41448]) ).
tff(c_41904,plain,
inverse(sk_c3) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_41891,c_41511]) ).
tff(c_41979,plain,
multiply(sk_c2,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_41904,c_4]) ).
tff(c_41985,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41641,c_41979]) ).
tff(c_41987,plain,
inverse(sk_c2) != sk_c3,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_50,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_42062,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_41987,c_50]) ).
tff(c_52,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_42051,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_41987,c_52]) ).
tff(c_41986,plain,
inverse(sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_42010,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_41986,c_4]) ).
tff(c_42117,plain,
! [Z_606] : ( multiply(sk_c11,multiply(sk_c8,Z_606)) = multiply(identity,Z_606) ),
inference(superposition,[status(thm),theory(equality)],[c_42010,c_42087]) ).
tff(c_42483,plain,
! [Z_615] : ( multiply(sk_c11,multiply(sk_c8,Z_615)) = Z_615 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42117]) ).
tff(c_42495,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_42051,c_42483]) ).
tff(c_42499,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42062,c_42495]) ).
tff(c_48,plain,
( ( multiply(sk_c7,sk_c10) = sk_c11 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_42057,plain,
multiply(sk_c7,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_41987,c_48]) ).
tff(c_42505,plain,
multiply(sk_c7,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42499,c_42057]) ).
tff(c_46,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_41988,plain,
inverse(sk_c2) = sk_c3,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_42004,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_41988,c_41987]) ).
tff(c_42005,plain,
inverse(sk_c6) = sk_c7,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_44,plain,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_42029,plain,
multiply(sk_c6,sk_c7) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_41987,c_44]) ).
tff(c_42507,plain,
multiply(sk_c6,sk_c7) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42499,c_42029]) ).
tff(c_43983,plain,
multiply(inverse(sk_c6),sk_c10) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_42507,c_42138]) ).
tff(c_43992,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42505,c_42005,c_43983]) ).
tff(c_42017,plain,
multiply(sk_c7,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42005,c_4]) ).
tff(c_42114,plain,
! [Z_606] : ( multiply(sk_c7,multiply(sk_c6,Z_606)) = multiply(identity,Z_606) ),
inference(superposition,[status(thm),theory(equality)],[c_42017,c_42087]) ).
tff(c_42166,plain,
! [Z_609] : ( multiply(sk_c7,multiply(sk_c6,Z_609)) = Z_609 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42114]) ).
tff(c_42178,plain,
multiply(sk_c7,sk_c11) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_42029,c_42166]) ).
tff(c_42501,plain,
multiply(sk_c7,sk_c10) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_42499,c_42178]) ).
tff(c_44018,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_43992,c_43992,c_42501]) ).
tff(c_44022,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_44018,c_42138]) ).
tff(c_44028,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_44022]) ).
tff(c_43840,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_43810]) ).
tff(c_44241,plain,
! [X_647] : ( multiply(X_647,identity) = X_647 ),
inference(superposition,[status(thm),theory(equality)],[c_44234,c_43840]) ).
tff(c_42586,plain,
! [X_616,Z_617] : ( multiply(inverse(X_616),multiply(X_616,Z_617)) = Z_617 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42126]) ).
tff(c_42808,plain,
! [X_620,Z_621] : ( multiply(inverse(inverse(X_620)),Z_621) = multiply(X_620,Z_621) ),
inference(superposition,[status(thm),theory(equality)],[c_42586,c_42138]) ).
tff(c_42628,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42586]) ).
tff(c_42815,plain,
! [X_620] : ( multiply(X_620,identity) = X_620 ),
inference(superposition,[status(thm),theory(equality)],[c_42808,c_42628]) ).
tff(c_42570,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42505,c_42501]) ).
tff(c_42571,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42570,c_42505]) ).
tff(c_42646,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_42571,c_42138]) ).
tff(c_42652,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42646]) ).
tff(c_42190,plain,
! [Z_610] : ( multiply(sk_c11,multiply(sk_c8,Z_610)) = Z_610 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42117]) ).
tff(c_42202,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_42051,c_42190]) ).
tff(c_42206,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42062,c_42202]) ).
tff(c_42208,plain,
multiply(sk_c7,sk_c10) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_42206,c_42178]) ).
tff(c_42375,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_42208,c_42138]) ).
tff(c_42384,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42375]) ).
tff(c_42216,plain,
inverse(sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42206,c_41986]) ).
tff(c_42257,plain,
multiply(sk_c10,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42216,c_4]) ).
tff(c_42453,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42384,c_42257]) ).
tff(c_42392,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42384,c_42216]) ).
tff(c_42454,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42453,c_42392]) ).
tff(c_42182,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c10) != sk_c11 )
| ( inverse(X5_6) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_42226,plain,
! [X5_611] :
( ( multiply(X5_611,sk_c10) != sk_c10 )
| ( inverse(X5_611) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42206,c_42206,c_42182]) ).
tff(c_42239,plain,
inverse(identity) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_2,c_42226]) ).
tff(c_42391,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_42384,c_42239]) ).
tff(c_42474,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_42454,c_42391]) ).
tff(c_42475,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_42518,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X4_14) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_14,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42499,c_42499,c_42499,c_42499,c_42499,c_42499,c_42499,c_42499,c_42499,c_42475]) ).
tff(c_42519,plain,
! [X4_14] :
( ( inverse(X4_14) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_14,sk_c10)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_42518]) ).
tff(c_43806,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_42815,c_42652,c_42652,c_2,c_42652,c_42652,c_42519]) ).
tff(c_42513,plain,
inverse(sk_c1) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42499,c_121]) ).
tff(c_42523,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42513,c_4]) ).
tff(c_42667,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42652,c_42523]) ).
tff(c_42660,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42652,c_42513]) ).
tff(c_42690,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42667,c_42660]) ).
tff(c_43808,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43806,c_42690]) ).
tff(c_43809,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_42518]) ).
tff(c_51730,plain,
! [X2_12,X9_9,X6_7] :
( ( inverse(X2_12) != identity )
| ( inverse(X9_9) != identity )
| ( identity != X9_9 )
| ( inverse(X6_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_44272,c_44028,c_44241,c_44028,c_44028,c_44241,c_44028,c_44028,c_2,c_44028,c_44028,c_44272,c_44028,c_44241,c_44028,c_44028,c_43809]) ).
tff(c_51731,plain,
! [X6_7] : ( inverse(X6_7) != identity ),
inference(splitLeft,[status(thm)],[c_51730]) ).
tff(c_42509,plain,
inverse(sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_42499,c_41986]) ).
tff(c_43854,plain,
multiply(sk_c10,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42509,c_4]) ).
tff(c_44082,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44028,c_43854]) ).
tff(c_44038,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44028,c_42509]) ).
tff(c_44083,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44082,c_44038]) ).
tff(c_51733,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_51731,c_44083]) ).
tff(c_51734,plain,
! [X2_12,X9_9] :
( ( inverse(X2_12) != identity )
| ( inverse(X9_9) != identity )
| ( identity != X9_9 ) ),
inference(splitRight,[status(thm)],[c_51730]) ).
tff(c_51736,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_51734]) ).
tff(c_51738,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_51736,c_44083]) ).
tff(c_51739,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitRight,[status(thm)],[c_51734]) ).
tff(c_51742,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_51739,c_44083]) ).
tff(c_51744,plain,
inverse(sk_c4) != sk_c11,
inference(splitRight,[status(thm)],[c_102]) ).
tff(c_98,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_51785,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_51744,c_98]) ).
tff(c_100,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_203]) ).
tff(c_51806,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_51744,c_100]) ).
tff(c_51743,plain,
inverse(sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_102]) ).
tff(c_51748,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_51743,c_4]) ).
tff(c_51873,plain,
! [Z_735] : ( multiply(sk_c11,multiply(sk_c8,Z_735)) = multiply(identity,Z_735) ),
inference(superposition,[status(thm),theory(equality)],[c_51748,c_51840]) ).
tff(c_52176,plain,
! [Z_743] : ( multiply(sk_c11,multiply(sk_c8,Z_743)) = Z_743 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51873]) ).
tff(c_52188,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_51806,c_52176]) ).
tff(c_52192,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_51785,c_52188]) ).
tff(c_96,plain,
( ( multiply(sk_c7,sk_c10) = sk_c11 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_51777,plain,
multiply(sk_c7,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_51744,c_96]) ).
tff(c_52198,plain,
multiply(sk_c7,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_52192,c_51777]) ).
tff(c_94,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_51756,plain,
inverse(sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_51744,c_94]) ).
tff(c_92,plain,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( inverse(sk_c4) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_51811,plain,
multiply(sk_c6,sk_c7) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_51744,c_92]) ).
tff(c_52195,plain,
multiply(sk_c6,sk_c7) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_52192,c_51811]) ).
tff(c_55011,plain,
multiply(inverse(sk_c6),sk_c10) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_52195,c_51891]) ).
tff(c_55017,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_52198,c_51756,c_55011]) ).
tff(c_55020,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_55017,c_52198]) ).
tff(c_55041,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_55020,c_51891]) ).
tff(c_55047,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_55041]) ).
tff(c_54992,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_54935]) ).
tff(c_55258,plain,
! [X_780] : ( multiply(X_780,identity) = X_780 ),
inference(superposition,[status(thm),theory(equality)],[c_55248,c_54992]) ).
tff(c_52262,plain,
! [X_744,Z_745] : ( multiply(inverse(X_744),multiply(X_744,Z_745)) = Z_745 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51879]) ).
tff(c_52575,plain,
! [X_747,Z_748] : ( multiply(inverse(inverse(X_747)),Z_748) = multiply(X_747,Z_748) ),
inference(superposition,[status(thm),theory(equality)],[c_52262,c_51891]) ).
tff(c_52319,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_52262]) ).
tff(c_52585,plain,
! [X_747] : ( multiply(X_747,identity) = X_747 ),
inference(superposition,[status(thm),theory(equality)],[c_52575,c_52319]) ).
tff(c_52338,plain,
multiply(inverse(sk_c6),sk_c10) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_52195,c_51891]) ).
tff(c_52344,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_52198,c_51756,c_52338]) ).
tff(c_52347,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_52344,c_52198]) ).
tff(c_52368,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_52347,c_51891]) ).
tff(c_52374,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_52368]) ).
tff(c_51920,plain,
! [Z_738] : ( multiply(sk_c11,multiply(sk_c8,Z_738)) = Z_738 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51873]) ).
tff(c_51932,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_51806,c_51920]) ).
tff(c_51936,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_51785,c_51932]) ).
tff(c_51942,plain,
multiply(sk_c7,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_51936,c_51777]) ).
tff(c_51939,plain,
multiply(sk_c6,sk_c7) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_51936,c_51811]) ).
tff(c_52105,plain,
multiply(inverse(sk_c6),sk_c10) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_51939,c_51891]) ).
tff(c_52111,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_51942,c_51756,c_52105]) ).
tff(c_52118,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_52111,c_51756]) ).
tff(c_52114,plain,
multiply(sk_c6,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_52111,c_51939]) ).
tff(c_51906,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c10) != sk_c11 )
| ( inverse(X5_6) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_51952,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c10) != sk_c10 )
| ( inverse(X5_6) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_51936,c_51936,c_51906]) ).
tff(c_52151,plain,
inverse(sk_c6) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_52114,c_51952]) ).
tff(c_52161,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52118,c_52151]) ).
tff(c_52162,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_52208,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X4_14) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_14,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_52192,c_52192,c_52192,c_52192,c_52192,c_52192,c_52192,c_52192,c_52192,c_52162]) ).
tff(c_52209,plain,
! [X4_14] :
( ( inverse(X4_14) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_14,sk_c10)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_52208]) ).
tff(c_54879,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_52585,c_52374,c_52374,c_2,c_52374,c_52374,c_52209]) ).
tff(c_52349,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_52344,c_51756]) ).
tff(c_52361,plain,
multiply(sk_c10,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_52349,c_4]) ).
tff(c_52419,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52374,c_52361]) ).
tff(c_52377,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52374,c_52349]) ).
tff(c_52424,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52419,c_52377]) ).
tff(c_54881,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_54879,c_52424]) ).
tff(c_54882,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_52208]) ).
tff(c_62048,plain,
! [X2_12,X9_9,X6_7] :
( ( inverse(X2_12) != identity )
| ( inverse(X9_9) != identity )
| ( identity != X9_9 )
| ( inverse(X6_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_55295,c_55047,c_55258,c_55047,c_55047,c_55258,c_55047,c_55047,c_2,c_55047,c_55047,c_55295,c_55047,c_55258,c_55047,c_55047,c_54882]) ).
tff(c_62049,plain,
! [X6_7] : ( inverse(X6_7) != identity ),
inference(splitLeft,[status(thm)],[c_62048]) ).
tff(c_55022,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_55017,c_51756]) ).
tff(c_55034,plain,
multiply(sk_c10,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_55022,c_4]) ).
tff(c_55092,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_55047,c_55034]) ).
tff(c_55050,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_55047,c_55022]) ).
tff(c_55097,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_55092,c_55050]) ).
tff(c_62051,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62049,c_55097]) ).
tff(c_62052,plain,
! [X2_12,X9_9] :
( ( inverse(X2_12) != identity )
| ( inverse(X9_9) != identity )
| ( identity != X9_9 ) ),
inference(splitRight,[status(thm)],[c_62048]) ).
tff(c_62054,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_62052]) ).
tff(c_62056,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62054,c_55097]) ).
tff(c_62057,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitRight,[status(thm)],[c_62052]) ).
tff(c_62060,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62057,c_55097]) ).
tff(c_62062,plain,
inverse(sk_c1) != sk_c11,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_14,plain,
( ( multiply(sk_c11,sk_c9) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_62121,plain,
multiply(sk_c11,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_62062,c_14]) ).
tff(c_16,plain,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_62133,plain,
multiply(sk_c8,sk_c11) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_62062,c_16]) ).
tff(c_62061,plain,
inverse(sk_c8) = sk_c11,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_62066,plain,
multiply(sk_c11,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_62061,c_4]) ).
tff(c_62206,plain,
! [Z_850] : ( multiply(sk_c11,multiply(sk_c8,Z_850)) = multiply(identity,Z_850) ),
inference(superposition,[status(thm),theory(equality)],[c_62066,c_62170]) ).
tff(c_62476,plain,
! [Z_856] : ( multiply(sk_c11,multiply(sk_c8,Z_856)) = Z_856 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62206]) ).
tff(c_62488,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_62133,c_62476]) ).
tff(c_62492,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62121,c_62488]) ).
tff(c_12,plain,
( ( multiply(sk_c7,sk_c10) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_62145,plain,
multiply(sk_c7,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_62062,c_12]) ).
tff(c_62857,plain,
multiply(sk_c7,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62492,c_62145]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c7) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_62112,plain,
multiply(sk_c6,sk_c7) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_62062,c_8]) ).
tff(c_10,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_62100,plain,
inverse(sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_62062,c_10]) ).
tff(c_62104,plain,
multiply(sk_c7,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_62100,c_4]) ).
tff(c_62197,plain,
! [Z_850] : ( multiply(sk_c7,multiply(sk_c6,Z_850)) = multiply(identity,Z_850) ),
inference(superposition,[status(thm),theory(equality)],[c_62104,c_62170]) ).
tff(c_62223,plain,
! [Z_851] : ( multiply(sk_c7,multiply(sk_c6,Z_851)) = Z_851 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62197]) ).
tff(c_62235,plain,
multiply(sk_c7,sk_c11) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_62112,c_62223]) ).
tff(c_62856,plain,
multiply(sk_c7,sk_c10) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_62492,c_62235]) ).
tff(c_65591,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62857,c_62856]) ).
tff(c_65592,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_65591,c_62857]) ).
tff(c_65640,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_65592,c_65622]) ).
tff(c_65680,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_65640]) ).
tff(c_65673,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65622]) ).
tff(c_65878,plain,
! [X_901] : ( multiply(X_901,identity) = X_901 ),
inference(superposition,[status(thm),theory(equality)],[c_65868,c_65673]) ).
tff(c_62947,plain,
! [X_862,Z_863] : ( multiply(inverse(X_862),multiply(X_862,Z_863)) = Z_863 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62209]) ).
tff(c_63193,plain,
! [X_866,Z_867] : ( multiply(inverse(inverse(X_866)),Z_867) = multiply(X_866,Z_867) ),
inference(superposition,[status(thm),theory(equality)],[c_62947,c_62221]) ).
tff(c_63240,plain,
! [X_866] : ( multiply(X_866,inverse(X_866)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_63193]) ).
tff(c_62916,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62857,c_62856]) ).
tff(c_62917,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62916,c_62857]) ).
tff(c_62965,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_62917,c_62947]) ).
tff(c_63005,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_62965]) ).
tff(c_62998,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_62947]) ).
tff(c_63203,plain,
! [X_866] : ( multiply(X_866,identity) = X_866 ),
inference(superposition,[status(thm),theory(equality)],[c_63193,c_62998]) ).
tff(c_62496,plain,
multiply(sk_c7,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62492,c_62145]) ).
tff(c_62495,plain,
multiply(sk_c7,sk_c10) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_62492,c_62235]) ).
tff(c_62539,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62496,c_62495]) ).
tff(c_62540,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62539,c_62496]) ).
tff(c_62631,plain,
! [X_858,Z_859] : ( multiply(inverse(X_858),multiply(X_858,Z_859)) = Z_859 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62209]) ).
tff(c_62652,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_62540,c_62631]) ).
tff(c_62695,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_62652]) ).
tff(c_62247,plain,
! [Z_852] : ( multiply(sk_c11,multiply(sk_c8,Z_852)) = Z_852 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62206]) ).
tff(c_62259,plain,
multiply(sk_c11,sk_c9) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_62133,c_62247]) ).
tff(c_62263,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62121,c_62259]) ).
tff(c_62266,plain,
multiply(sk_c7,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62263,c_62145]) ).
tff(c_62265,plain,
multiply(sk_c7,sk_c10) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_62263,c_62235]) ).
tff(c_62355,plain,
sk_c7 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62266,c_62265]) ).
tff(c_62371,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62355,c_62100]) ).
tff(c_62269,plain,
multiply(sk_c6,sk_c7) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62263,c_62112]) ).
tff(c_62368,plain,
multiply(sk_c6,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62355,c_62269]) ).
tff(c_62246,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c10) != sk_c11 )
| ( inverse(X5_6) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_62293,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c10) != sk_c10 )
| ( inverse(X5_6) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_62263,c_62263,c_62246]) ).
tff(c_62464,plain,
inverse(sk_c6) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_62368,c_62293]) ).
tff(c_62474,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_62371,c_62464]) ).
tff(c_62475,plain,
! [X6_7,X9_9,X2_12,X4_14] :
( ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_62493,plain,
! [X4_14] :
( ( inverse(X4_14) != sk_c11 )
| ( multiply(sk_c11,multiply(X4_14,sk_c11)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_62475]) ).
tff(c_62555,plain,
! [X4_14] :
( ( inverse(X4_14) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_14,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_62492,c_62492,c_62492,c_62493]) ).
tff(c_62613,plain,
( ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_62540,c_62555]) ).
tff(c_62620,plain,
inverse(sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62540,c_62613]) ).
tff(c_62700,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_62695,c_62695,c_62620]) ).
tff(c_62504,plain,
inverse(sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62492,c_62061]) ).
tff(c_62711,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_62695,c_62504]) ).
tff(c_62784,plain,
multiply(identity,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_62711,c_4]) ).
tff(c_62832,plain,
multiply(inverse(identity),identity) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_62784,c_62221]) ).
tff(c_62844,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_62832]) ).
tff(c_62849,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_62844,c_62711]) ).
tff(c_62853,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62700,c_62849]) ).
tff(c_62854,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X9_9) != sk_c11 )
| ( multiply(sk_c11,multiply(X9_9,sk_c11)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c11) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_62475]) ).
tff(c_62884,plain,
! [X2_12,X9_9,X6_7] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_62492,c_62492,c_62492,c_62492,c_62492,c_62492,c_62854]) ).
tff(c_62885,plain,
! [X6_7] :
( ( multiply(inverse(X6_7),sk_c10) != sk_c10 )
| ( multiply(X6_7,inverse(X6_7)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_62884]) ).
tff(c_65557,plain,
! [X6_7] : ( inverse(X6_7) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_63240,c_63005,c_63203,c_63005,c_63005,c_62885]) ).
tff(c_62920,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_62916,c_62100]) ).
tff(c_62928,plain,
multiply(sk_c10,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_62920,c_4]) ).
tff(c_63033,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_63005,c_62928]) ).
tff(c_63011,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63005,c_62920]) ).
tff(c_63042,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63033,c_63011]) ).
tff(c_65559,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65557,c_63042]) ).
tff(c_65560,plain,
! [X9_9,X2_12] :
( ( inverse(X9_9) != sk_c10 )
| ( multiply(sk_c10,multiply(X9_9,sk_c10)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_62884]) ).
tff(c_71938,plain,
! [X9_9,X2_12] :
( ( inverse(X9_9) != identity )
| ( identity != X9_9 )
| ( inverse(X2_12) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_65915,c_65680,c_65878,c_65680,c_65680,c_65878,c_65680,c_65680,c_2,c_65680,c_65680,c_65560]) ).
tff(c_71939,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitLeft,[status(thm)],[c_71938]) ).
tff(c_65595,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_65591,c_62100]) ).
tff(c_65603,plain,
multiply(sk_c10,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_65595,c_4]) ).
tff(c_65708,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_65680,c_65603]) ).
tff(c_65686,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_65680,c_65595]) ).
tff(c_65717,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_65708,c_65686]) ).
tff(c_71941,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_71939,c_65717]) ).
tff(c_71943,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_71938]) ).
tff(c_71945,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_71943,c_65717]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.12 % Problem : GRP217-1 : TPTP v9.0.0. Released v2.5.0.
% 0.02/0.12 % 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.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 21:37:20 EDT 2025
% 0.12/0.33 % CPUTime :
% 16.42/5.83 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.72/5.92
% 16.72/5.92 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------