%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP255-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 : n021.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:42 PM UTC 2025
% Result : Unsatisfiable 17.48s 6.54s
% Output : CNFRefutation 17.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 32
% Syntax : Number of formulae : 786 ( 662 unt; 0 typ; 0 def)
% Number of atoms : 1048 (1001 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 611 ( 349 ~; 262 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 339 ( 339 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_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_68,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c6 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c3) = sk_c6 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(X3,sk_c8) != sk_c7 )
| ( inverse(X3) != sk_c8 )
| ( multiply(X4,sk_c7) != sk_c6 )
| ( inverse(X4) != sk_c7 )
| ( inverse(X5) != sk_c6 )
| ( multiply(X5,sk_c8) != sk_c6 )
| ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( inverse(X1) != sk_c8 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( inverse(X2) != sk_c7 )
| ( multiply(X2,sk_c6) != sk_c7 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c6 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c3) = sk_c6 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c5,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_10,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_134,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_20,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_110,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_114,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_110,c_4]) ).
tff(c_32635,plain,
! [X_245,Y_246,Z_247] : ( multiply(multiply(X_245,Y_246),Z_247) = multiply(X_245,multiply(Y_246,Z_247)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_32671,plain,
! [Z_247] : ( multiply(sk_c8,multiply(sk_c1,Z_247)) = multiply(identity,Z_247) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_32635]) ).
tff(c_32695,plain,
! [Z_248] : ( multiply(sk_c8,multiply(sk_c1,Z_248)) = Z_248 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32671]) ).
tff(c_32707,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_134,c_32695]) ).
tff(c_32680,plain,
! [X_2,Z_247] : ( multiply(inverse(X_2),multiply(X_2,Z_247)) = multiply(identity,Z_247) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_32635]) ).
tff(c_33040,plain,
! [X_259,Z_260] : ( multiply(inverse(X_259),multiply(X_259,Z_260)) = Z_260 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32680]) ).
tff(c_33094,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_32707,c_33040]) ).
tff(c_33157,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33094]) ).
tff(c_40,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_98,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_33182,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33157,c_98]) ).
tff(c_33257,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33182,c_4]) ).
tff(c_32693,plain,
! [X_2,Z_247] : ( multiply(inverse(X_2),multiply(X_2,Z_247)) = Z_247 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32680]) ).
tff(c_33306,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_33257,c_32693]) ).
tff(c_33318,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33306]) ).
tff(c_160,plain,
! [X_13,Y_14,Z_15] : ( multiply(multiply(X_13,Y_14),Z_15) = multiply(X_13,multiply(Y_14,Z_15)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_193,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_160]) ).
tff(c_1467,plain,
! [X_40,Z_41] : ( multiply(inverse(X_40),multiply(X_40,Z_41)) = Z_41 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_204,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_1706,plain,
! [X_44,Z_45] : ( multiply(inverse(inverse(X_44)),Z_45) = multiply(X_44,Z_45) ),
inference(superposition,[status(thm),theory(equality)],[c_1467,c_204]) ).
tff(c_1515,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1467]) ).
tff(c_1713,plain,
! [X_44] : ( multiply(X_44,identity) = X_44 ),
inference(superposition,[status(thm),theory(equality)],[c_1706,c_1515]) ).
tff(c_60,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_125,plain,
multiply(sk_c3,sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_54,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c3) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_85,plain,
inverse(sk_c3) = sk_c6,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_89,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_190,plain,
! [Z_15] : ( multiply(sk_c6,multiply(sk_c3,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_160]) ).
tff(c_636,plain,
! [Z_25] : ( multiply(sk_c6,multiply(sk_c3,Z_25)) = Z_25 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190]) ).
tff(c_648,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_125,c_636]) ).
tff(c_30,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_139,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_187,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_160]) ).
tff(c_229,plain,
! [Z_17] : ( multiply(sk_c7,multiply(sk_c2,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_187]) ).
tff(c_241,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_139,c_229]) ).
tff(c_659,plain,
! [Z_26] : ( multiply(sk_c2,multiply(sk_c7,Z_26)) = multiply(sk_c6,Z_26) ),
inference(superposition,[status(thm),theory(equality)],[c_139,c_160]) ).
tff(c_674,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c2,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_241,c_659]) ).
tff(c_687,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_648,c_139,c_674]) ).
tff(c_688,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_687,c_648]) ).
tff(c_1497,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_688,c_1467]) ).
tff(c_1524,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1497]) ).
tff(c_317,plain,
! [X_20,Z_21] : ( multiply(inverse(X_20),multiply(X_20,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_350,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_241,c_317]) ).
tff(c_401,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_350]) ).
tff(c_253,plain,
! [Z_18] : ( multiply(sk_c6,multiply(sk_c3,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_190]) ).
tff(c_265,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_125,c_253]) ).
tff(c_411,plain,
multiply(identity,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_401,c_401,c_265]) ).
tff(c_421,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_411]) ).
tff(c_184,plain,
! [Z_15] : ( multiply(sk_c8,multiply(sk_c1,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_160]) ).
tff(c_206,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c1,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_184]) ).
tff(c_218,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_134,c_206]) ).
tff(c_356,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_218,c_317]) ).
tff(c_402,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_356]) ).
tff(c_68,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_245,plain,
multiply(sk_c7,sk_c8) != sk_c6,
inference(splitLeft,[status(thm)],[c_68]) ).
tff(c_415,plain,
multiply(sk_c7,sk_c8) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_401,c_245]) ).
tff(c_619,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_421,c_2,c_402,c_415]) ).
tff(c_621,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_689,plain,
multiply(sk_c7,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_687,c_621]) ).
tff(c_1429,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_689,c_241]) ).
tff(c_1528,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1524,c_1429]) ).
tff(c_805,plain,
! [X_27,Z_28] : ( multiply(inverse(X_27),multiply(X_27,Z_28)) = Z_28 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_841,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_688,c_805]) ).
tff(c_869,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_841]) ).
tff(c_749,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_689,c_241]) ).
tff(c_875,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_869,c_749]) ).
tff(c_1034,plain,
! [X_30,Z_31] : ( multiply(inverse(inverse(X_30)),Z_31) = multiply(X_30,Z_31) ),
inference(superposition,[status(thm),theory(equality)],[c_805,c_204]) ).
tff(c_859,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_805]) ).
tff(c_1041,plain,
! [X_30] : ( multiply(X_30,identity) = X_30 ),
inference(superposition,[status(thm),theory(equality)],[c_1034,c_859]) ).
tff(c_620,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_732,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_687,c_687,c_687,c_687,c_687,c_620]) ).
tff(c_733,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_732]) ).
tff(c_1416,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_875,c_1041,c_875,c_869,c_733]) ).
tff(c_769,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_749,c_98]) ).
tff(c_779,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_769,c_4]) ).
tff(c_897,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_869,c_779]) ).
tff(c_874,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_869,c_769]) ).
tff(c_922,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_897,c_874]) ).
tff(c_1418,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1416,c_922]) ).
tff(c_1419,plain,
! [X1_8,X5_6,X4_10,X3_7] :
( ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_732]) ).
tff(c_25143,plain,
! [X1_8,X5_6,X4_10,X3_7] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( identity != X5_6 )
| ( inverse(X5_6) != identity )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1713,c_1528,c_1524,c_1524,c_1713,c_1528,c_1524,c_1528,c_1524,c_1713,c_1524,c_1524,c_1524,c_1713,c_1528,c_1524,c_1419]) ).
tff(c_25145,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25143]) ).
tff(c_1447,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_1429,c_98]) ).
tff(c_1456,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1447,c_4]) ).
tff(c_1550,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1524,c_1456]) ).
tff(c_1527,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1524,c_1447]) ).
tff(c_1575,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1550,c_1527]) ).
tff(c_25147,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25145,c_1575]) ).
tff(c_25148,plain,
! [X4_10,X5_6,X1_8] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( identity != X5_6 )
| ( inverse(X5_6) != identity )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_25143]) ).
tff(c_32571,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25148]) ).
tff(c_32573,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32571,c_1575]) ).
tff(c_32574,plain,
! [X5_6,X4_10] :
( ( identity != X5_6 )
| ( inverse(X5_6) != identity )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 ) ),
inference(splitRight,[status(thm)],[c_25148]) ).
tff(c_32576,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_32574]) ).
tff(c_32578,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32576,c_1575]) ).
tff(c_32580,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_32574]) ).
tff(c_32582,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32580,c_1575]) ).
tff(c_32584,plain,
multiply(sk_c2,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_36,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_32627,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_32584,c_36]) ).
tff(c_34,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_32597,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_32584,c_34]) ).
tff(c_32601,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_32597,c_4]) ).
tff(c_32659,plain,
! [Z_247] : ( multiply(sk_c7,multiply(sk_c5,Z_247)) = multiply(identity,Z_247) ),
inference(superposition,[status(thm),theory(equality)],[c_32601,c_32635]) ).
tff(c_32903,plain,
! [Z_255] : ( multiply(sk_c7,multiply(sk_c5,Z_255)) = Z_255 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32659]) ).
tff(c_32915,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_32627,c_32903]) ).
tff(c_33170,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33157,c_33157,c_32915]) ).
tff(c_33183,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33170]) ).
tff(c_33179,plain,
multiply(sk_c2,identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33157,c_32584]) ).
tff(c_33470,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33318,c_33183,c_33179]) ).
tff(c_33472,plain,
multiply(sk_c1,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_16,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_34588,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_33472,c_16]) ).
tff(c_33528,plain,
! [X_264,Y_265,Z_266] : ( multiply(multiply(X_264,Y_265),Z_266) = multiply(X_264,multiply(Y_265,Z_266)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33570,plain,
! [Z_266] : ( multiply(sk_c6,multiply(sk_c3,Z_266)) = multiply(identity,Z_266) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_33528]) ).
tff(c_34163,plain,
! [Z_278] : ( multiply(sk_c6,multiply(sk_c3,Z_278)) = Z_278 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33570]) ).
tff(c_34175,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_125,c_34163]) ).
tff(c_33486,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_33567,plain,
! [Z_266] : ( multiply(sk_c7,multiply(sk_c2,Z_266)) = multiply(identity,Z_266) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_33528]) ).
tff(c_34221,plain,
! [Z_281] : ( multiply(sk_c7,multiply(sk_c2,Z_281)) = Z_281 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33567]) ).
tff(c_34239,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33486,c_34221]) ).
tff(c_33555,plain,
! [Z_266] : ( multiply(sk_c2,multiply(sk_c7,Z_266)) = multiply(sk_c6,Z_266) ),
inference(superposition,[status(thm),theory(equality)],[c_33486,c_33528]) ).
tff(c_34246,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c2,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_34239,c_33555]) ).
tff(c_34252,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34175,c_33486,c_34246]) ).
tff(c_34255,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34252,c_34175]) ).
tff(c_33573,plain,
! [X_2,Z_266] : ( multiply(inverse(X_2),multiply(X_2,Z_266)) = multiply(identity,Z_266) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_33528]) ).
tff(c_34344,plain,
! [X_282,Z_283] : ( multiply(inverse(X_282),multiply(X_282,Z_283)) = Z_283 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33573]) ).
tff(c_34365,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_34255,c_34344]) ).
tff(c_34399,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_34365]) ).
tff(c_34263,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34252,c_110]) ).
tff(c_34280,plain,
multiply(sk_c6,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34263,c_4]) ).
tff(c_34426,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34399,c_34280]) ).
tff(c_8,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_33511,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_33472,c_8]) ).
tff(c_34257,plain,
multiply(sk_c7,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34252,c_33511]) ).
tff(c_34318,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34257,c_34239]) ).
tff(c_34402,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34399,c_34318]) ).
tff(c_34259,plain,
multiply(sk_c1,sk_c6) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34252,c_33472]) ).
tff(c_34556,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34426,c_34402,c_34399,c_34259]) ).
tff(c_34557,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_34562,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34557,c_4]) ).
tff(c_34600,plain,
! [X_285,Y_286,Z_287] : ( multiply(multiply(X_285,Y_286),Z_287) = multiply(X_285,multiply(Y_286,Z_287)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_34624,plain,
! [Z_287] : ( multiply(sk_c7,multiply(sk_c5,Z_287)) = multiply(identity,Z_287) ),
inference(superposition,[status(thm),theory(equality)],[c_34562,c_34600]) ).
tff(c_35447,plain,
! [Z_304] : ( multiply(sk_c7,multiply(sk_c5,Z_304)) = Z_304 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34624]) ).
tff(c_35459,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_34588,c_35447]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33471,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_33476,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33471,c_4]) ).
tff(c_35377,plain,
! [Z_302] : ( multiply(sk_c3,multiply(sk_c8,Z_302)) = multiply(sk_c6,Z_302) ),
inference(superposition,[status(thm),theory(equality)],[c_125,c_34600]) ).
tff(c_35395,plain,
multiply(sk_c6,sk_c4) = multiply(sk_c3,identity),
inference(superposition,[status(thm),theory(equality)],[c_33476,c_35377]) ).
tff(c_34558,plain,
multiply(sk_c2,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_28,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_34582,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_34558,c_28]) ).
tff(c_35503,plain,
! [Z_306] : ( multiply(sk_c7,multiply(sk_c8,Z_306)) = multiply(sk_c6,Z_306) ),
inference(superposition,[status(thm),theory(equality)],[c_34582,c_34600]) ).
tff(c_35524,plain,
multiply(sk_c7,identity) = multiply(sk_c6,sk_c4),
inference(superposition,[status(thm),theory(equality)],[c_33476,c_35503]) ).
tff(c_35531,plain,
multiply(sk_c7,identity) = multiply(sk_c3,identity),
inference(demodulation,[status(thm),theory(equality)],[c_35395,c_35524]) ).
tff(c_35543,plain,
! [Z_5] : ( multiply(multiply(sk_c3,identity),Z_5) = multiply(sk_c7,multiply(identity,Z_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_35531,c_6]) ).
tff(c_35550,plain,
! [Z_307] : ( multiply(sk_c7,Z_307) = multiply(sk_c3,Z_307) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_6,c_35543]) ).
tff(c_35556,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_35550,c_35459]) ).
tff(c_34639,plain,
! [Z_287] : ( multiply(sk_c6,multiply(sk_c3,Z_287)) = multiply(identity,Z_287) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_34600]) ).
tff(c_34654,plain,
! [Z_287] : ( multiply(sk_c6,multiply(sk_c3,Z_287)) = Z_287 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34639]) ).
tff(c_35612,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_35556,c_34654]) ).
tff(c_34683,plain,
! [Z_290] : ( multiply(sk_c6,multiply(sk_c3,Z_290)) = Z_290 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34639]) ).
tff(c_34695,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_125,c_34683]) ).
tff(c_36006,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35612,c_34695]) ).
tff(c_32,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_34576,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_34558,c_32]) ).
tff(c_34627,plain,
! [Z_287] : ( multiply(sk_c8,multiply(sk_c4,Z_287)) = multiply(identity,Z_287) ),
inference(superposition,[status(thm),theory(equality)],[c_33476,c_34600]) ).
tff(c_35418,plain,
! [Z_303] : ( multiply(sk_c8,multiply(sk_c4,Z_303)) = Z_303 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34627]) ).
tff(c_35433,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34576,c_35418]) ).
tff(c_36053,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_36006,c_36006,c_35433]) ).
tff(c_36067,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35459,c_36053]) ).
tff(c_36061,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_36006,c_33471]) ).
tff(c_36096,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36067,c_36061]) ).
tff(c_35546,plain,
! [Z_5] : ( multiply(sk_c7,Z_5) = multiply(sk_c3,Z_5) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_6,c_35543]) ).
tff(c_34621,plain,
! [Z_287] : ( multiply(sk_c4,multiply(sk_c7,Z_287)) = multiply(sk_c8,Z_287) ),
inference(superposition,[status(thm),theory(equality)],[c_34576,c_34600]) ).
tff(c_36019,plain,
! [Z_313] : ( multiply(sk_c4,multiply(sk_c3,Z_313)) = multiply(sk_c8,Z_313) ),
inference(demodulation,[status(thm),theory(equality)],[c_35546,c_34621]) ).
tff(c_36046,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_125,c_36019]) ).
tff(c_36050,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35433,c_36046]) ).
tff(c_36153,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36067,c_36050]) ).
tff(c_36075,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36067,c_36006]) ).
tff(c_35864,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35612,c_34695]) ).
tff(c_35877,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35864,c_35864,c_35433]) ).
tff(c_35890,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35459,c_35877]) ).
tff(c_35885,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35864,c_33471]) ).
tff(c_35946,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35890,c_35885]) ).
tff(c_35882,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35864,c_34576]) ).
tff(c_35991,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35890,c_35890,c_35882]) ).
tff(c_35898,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35890,c_35864]) ).
tff(c_34700,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34582,c_68]) ).
tff(c_34810,plain,
! [X3_294] :
( ( inverse(X3_294) != sk_c8 )
| ( multiply(X3_294,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_34700]) ).
tff(c_34826,plain,
( ( inverse(sk_c3) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_125,c_34810]) ).
tff(c_34836,plain,
( ( sk_c8 != sk_c6 )
| ( sk_c7 != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_85,c_34826]) ).
tff(c_34837,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_34836]) ).
tff(c_34709,plain,
! [Z_291] : ( multiply(sk_c7,multiply(sk_c5,Z_291)) = Z_291 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34624]) ).
tff(c_34721,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_34588,c_34709]) ).
tff(c_34834,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_34810]) ).
tff(c_34838,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_34834]) ).
tff(c_34773,plain,
! [Z_293] : ( multiply(sk_c8,multiply(sk_c4,Z_293)) = Z_293 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34627]) ).
tff(c_34788,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34576,c_34773]) ).
tff(c_34630,plain,
! [Z_287] : ( multiply(sk_c3,multiply(sk_c8,Z_287)) = multiply(sk_c6,Z_287) ),
inference(superposition,[status(thm),theory(equality)],[c_125,c_34600]) ).
tff(c_34795,plain,
multiply(sk_c6,sk_c8) = multiply(sk_c3,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_34788,c_34630]) ).
tff(c_35200,plain,
! [Z_301] : ( multiply(sk_c7,multiply(sk_c8,Z_301)) = multiply(sk_c6,Z_301) ),
inference(superposition,[status(thm),theory(equality)],[c_34582,c_34600]) ).
tff(c_35221,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_34788,c_35200]) ).
tff(c_35237,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34795,c_34721,c_35221]) ).
tff(c_34642,plain,
! [X_2,Z_287] : ( multiply(inverse(X_2),multiply(X_2,Z_287)) = multiply(identity,Z_287) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34600]) ).
tff(c_34655,plain,
! [X_2,Z_287] : ( multiply(inverse(X_2),multiply(X_2,Z_287)) = Z_287 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34642]) ).
tff(c_35244,plain,
multiply(inverse(sk_c3),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_35237,c_34655]) ).
tff(c_35253,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34695,c_85,c_35244]) ).
tff(c_35255,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34838,c_35253]) ).
tff(c_35257,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_34834]) ).
tff(c_35261,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35257,c_35257,c_34788]) ).
tff(c_35274,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34721,c_35261]) ).
tff(c_35276,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34837,c_35274]) ).
tff(c_35277,plain,
sk_c8 != sk_c6,
inference(splitRight,[status(thm)],[c_34836]) ).
tff(c_35278,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_34836]) ).
tff(c_35282,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35278,c_35278,c_34721]) ).
tff(c_35366,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35282,c_34695]) ).
tff(c_35368,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35277,c_35366]) ).
tff(c_35369,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_34700]) ).
tff(c_35479,plain,
! [X2_305] :
( ( multiply(X2_305,sk_c6) != sk_c7 )
| ( inverse(X2_305) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_35369]) ).
tff(c_35489,plain,
inverse(sk_c5) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34588,c_35479]) ).
tff(c_35501,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34557,c_35489]) ).
tff(c_35502,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_35369]) ).
tff(c_35713,plain,
! [X4_309] :
( ( inverse(X4_309) != sk_c7 )
| ( multiply(X4_309,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_35502]) ).
tff(c_35719,plain,
inverse(sk_c3) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_35556,c_35713]) ).
tff(c_35744,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_85,c_35719]) ).
tff(c_35773,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35612,c_34695]) ).
tff(c_35787,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35773,c_35773,c_35433]) ).
tff(c_35802,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35459,c_35787]) ).
tff(c_35804,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35744,c_35802]) ).
tff(c_35805,plain,
! [X5_6,X1_8] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_35502]) ).
tff(c_35863,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_35805]) ).
tff(c_35976,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c6) != sk_c6 )
| ( inverse(X1_8) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35898,c_35898,c_35890,c_35863]) ).
tff(c_35995,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_35991,c_35976]) ).
tff(c_36004,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_35946,c_35995]) ).
tff(c_36005,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_35805]) ).
tff(c_36112,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c6) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_36075,c_36005]) ).
tff(c_36157,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_36153,c_36112]) ).
tff(c_36166,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_36096,c_36157]) ).
tff(c_36168,plain,
multiply(sk_c3,sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_66,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_36209,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_36168,c_66]) ).
tff(c_64,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_36184,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_36168,c_64]) ).
tff(c_36188,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_36184,c_4]) ).
tff(c_38994,plain,
! [X_367,Y_368,Z_369] : ( multiply(multiply(X_367,Y_368),Z_369) = multiply(X_367,multiply(Y_368,Z_369)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_39018,plain,
! [Z_369] : ( multiply(sk_c7,multiply(sk_c5,Z_369)) = multiply(identity,Z_369) ),
inference(superposition,[status(thm),theory(equality)],[c_36188,c_38994]) ).
tff(c_39736,plain,
! [Z_386] : ( multiply(sk_c7,multiply(sk_c5,Z_386)) = Z_386 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39018]) ).
tff(c_39751,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_36209,c_39736]) ).
tff(c_62,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_36204,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_36168,c_62]) ).
tff(c_36167,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_36172,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_36167,c_4]) ).
tff(c_39021,plain,
! [Z_369] : ( multiply(sk_c8,multiply(sk_c4,Z_369)) = multiply(identity,Z_369) ),
inference(superposition,[status(thm),theory(equality)],[c_36172,c_38994]) ).
tff(c_39762,plain,
! [Z_387] : ( multiply(sk_c8,multiply(sk_c4,Z_387)) = Z_387 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39021]) ).
tff(c_39774,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36204,c_39762]) ).
tff(c_37213,plain,
! [X_333,Y_334,Z_335] : ( multiply(multiply(X_333,Y_334),Z_335) = multiply(X_333,multiply(Y_334,Z_335)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_37243,plain,
! [Z_335] : ( multiply(sk_c8,multiply(sk_c4,Z_335)) = multiply(identity,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_36172,c_37213]) ).
tff(c_38416,plain,
! [Z_359] : ( multiply(sk_c8,multiply(sk_c4,Z_359)) = Z_359 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37243]) ).
tff(c_38428,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36204,c_38416]) ).
tff(c_58,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_36227,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_36168,c_58]) ).
tff(c_36233,plain,
! [X_315,Y_316,Z_317] : ( multiply(multiply(X_315,Y_316),Z_317) = multiply(X_315,multiply(Y_316,Z_317)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_36266,plain,
! [Z_317] : ( multiply(sk_c8,multiply(sk_c4,Z_317)) = multiply(identity,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_36172,c_36233]) ).
tff(c_36766,plain,
! [Z_328] : ( multiply(sk_c8,multiply(sk_c4,Z_328)) = Z_328 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36266]) ).
tff(c_36778,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36204,c_36766]) ).
tff(c_36220,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_36251,plain,
! [Z_317] : ( multiply(sk_c1,multiply(sk_c8,Z_317)) = multiply(sk_c7,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_36220,c_36233]) ).
tff(c_36817,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c1,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_36778,c_36251]) ).
tff(c_36823,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36227,c_36817]) ).
tff(c_36215,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_36272,plain,
! [Z_317] : ( multiply(sk_c7,multiply(sk_c2,Z_317)) = multiply(identity,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_36233]) ).
tff(c_36329,plain,
! [Z_320] : ( multiply(sk_c7,multiply(sk_c2,Z_320)) = Z_320 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36272]) ).
tff(c_36341,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36215,c_36329]) ).
tff(c_36269,plain,
! [Z_317] : ( multiply(sk_c8,multiply(sk_c1,Z_317)) = multiply(identity,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_36233]) ).
tff(c_36288,plain,
! [Z_317] : ( multiply(sk_c8,multiply(sk_c1,Z_317)) = Z_317 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36269]) ).
tff(c_36835,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36823,c_36288]) ).
tff(c_36845,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c1,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_36835,c_36251]) ).
tff(c_36851,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36823,c_36341,c_36845]) ).
tff(c_36853,plain,
multiply(sk_c8,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36851,c_36835]) ).
tff(c_36862,plain,
multiply(sk_c1,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36851,c_36220]) ).
tff(c_36908,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_36862,c_36288]) ).
tff(c_36914,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36853,c_36908]) ).
tff(c_36861,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36851,c_36227]) ).
tff(c_37007,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36914,c_36861]) ).
tff(c_36278,plain,
! [X_2,Z_317] : ( multiply(inverse(X_2),multiply(X_2,Z_317)) = multiply(identity,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_36233]) ).
tff(c_36291,plain,
! [X_2,Z_317] : ( multiply(inverse(X_2),multiply(X_2,Z_317)) = Z_317 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36278]) ).
tff(c_37011,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_37007,c_36291]) ).
tff(c_37017,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_37011]) ).
tff(c_37029,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37017,c_89]) ).
tff(c_37184,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_37029,c_2]) ).
tff(c_36921,plain,
multiply(sk_c3,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36914,c_36168]) ).
tff(c_37167,plain,
multiply(sk_c3,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_37017,c_37017,c_36921]) ).
tff(c_37194,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_37184,c_37167]) ).
tff(c_37199,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37194]) ).
tff(c_37200,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_38495,plain,
! [Z_361] : ( multiply(sk_c4,multiply(sk_c7,Z_361)) = multiply(sk_c8,Z_361) ),
inference(superposition,[status(thm),theory(equality)],[c_36204,c_37213]) ).
tff(c_38522,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_37200,c_38495]) ).
tff(c_38533,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_38428,c_38522]) ).
tff(c_37264,plain,
! [Z_335] : ( multiply(sk_c8,multiply(sk_c4,Z_335)) = Z_335 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37243]) ).
tff(c_38537,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_38533,c_37264]) ).
tff(c_37240,plain,
! [Z_335] : ( multiply(sk_c7,multiply(sk_c5,Z_335)) = multiply(identity,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_36188,c_37213]) ).
tff(c_38291,plain,
! [Z_355] : ( multiply(sk_c7,multiply(sk_c5,Z_355)) = Z_355 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37240]) ).
tff(c_38303,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_36209,c_38291]) ).
tff(c_38510,plain,
multiply(sk_c8,sk_c7) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_38303,c_38495]) ).
tff(c_38696,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38533,c_38537,c_38510]) ).
tff(c_38712,plain,
inverse(sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38696,c_36184]) ).
tff(c_38724,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38712,c_4]) ).
tff(c_38363,plain,
! [Z_358] : ( multiply(sk_c2,multiply(sk_c7,Z_358)) = multiply(sk_c6,Z_358) ),
inference(superposition,[status(thm),theory(equality)],[c_36215,c_37213]) ).
tff(c_38393,plain,
multiply(sk_c6,sk_c5) = multiply(sk_c2,identity),
inference(superposition,[status(thm),theory(equality)],[c_36188,c_38363]) ).
tff(c_38728,plain,
multiply(sk_c2,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38724,c_38393]) ).
tff(c_38886,plain,
! [Z_5] : ( multiply(sk_c2,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_38728,c_6]) ).
tff(c_38889,plain,
! [Z_5] : ( multiply(sk_c2,Z_5) = Z_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_38886]) ).
tff(c_37249,plain,
! [Z_335] : ( multiply(sk_c7,multiply(sk_c2,Z_335)) = multiply(identity,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_37213]) ).
tff(c_37266,plain,
! [Z_335] : ( multiply(sk_c7,multiply(sk_c2,Z_335)) = Z_335 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37249]) ).
tff(c_38705,plain,
! [Z_335] : ( multiply(sk_c6,multiply(sk_c2,Z_335)) = Z_335 ),
inference(demodulation,[status(thm),theory(equality)],[c_38696,c_37266]) ).
tff(c_38926,plain,
! [Z_366] : ( multiply(sk_c6,Z_366) = Z_366 ),
inference(demodulation,[status(thm),theory(equality)],[c_38889,c_38705]) ).
tff(c_38698,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38696,c_38533]) ).
tff(c_38710,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_38696,c_36204]) ).
tff(c_38787,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38698,c_38710]) ).
tff(c_38808,plain,
multiply(sk_c6,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38787,c_114]) ).
tff(c_38932,plain,
sk_c1 = identity,
inference(superposition,[status(thm),theory(equality)],[c_38926,c_38808]) ).
tff(c_37201,plain,
multiply(sk_c1,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_38706,plain,
multiply(sk_c1,sk_c8) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38696,c_37201]) ).
tff(c_38869,plain,
multiply(sk_c1,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38787,c_38706]) ).
tff(c_38975,plain,
multiply(identity,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38932,c_38869]) ).
tff(c_38980,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38975]) ).
tff(c_38981,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_39814,plain,
! [Z_389] : ( multiply(sk_c7,multiply(sk_c8,Z_389)) = multiply(sk_c6,Z_389) ),
inference(superposition,[status(thm),theory(equality)],[c_38981,c_38994]) ).
tff(c_39826,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_39774,c_39814]) ).
tff(c_39842,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39751,c_39826]) ).
tff(c_39033,plain,
! [X_2,Z_369] : ( multiply(inverse(X_2),multiply(X_2,Z_369)) = multiply(identity,Z_369) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_38994]) ).
tff(c_39949,plain,
! [X_390,Z_391] : ( multiply(inverse(X_390),multiply(X_390,Z_391)) = Z_391 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39033]) ).
tff(c_39994,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_39842,c_39949]) ).
tff(c_40038,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39994]) ).
tff(c_39012,plain,
! [Z_369] : ( multiply(sk_c5,multiply(sk_c6,Z_369)) = multiply(sk_c7,Z_369) ),
inference(superposition,[status(thm),theory(equality)],[c_36209,c_38994]) ).
tff(c_39846,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_39842,c_39012]) ).
tff(c_39852,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36209,c_38981,c_39846]) ).
tff(c_39855,plain,
multiply(sk_c8,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39852,c_39774]) ).
tff(c_40043,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40038,c_40038,c_39855]) ).
tff(c_40052,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40043]) ).
tff(c_40066,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40052,c_89]) ).
tff(c_39046,plain,
! [X_2,Z_369] : ( multiply(inverse(X_2),multiply(X_2,Z_369)) = Z_369 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39033]) ).
tff(c_40239,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_40066,c_39046]) ).
tff(c_40251,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40239]) ).
tff(c_40048,plain,
multiply(sk_c3,identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40038,c_36168]) ).
tff(c_40296,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40251,c_40052,c_40048]) ).
tff(c_40298,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_26,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_40337,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_40298,c_26]) ).
tff(c_24,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_40306,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_40298,c_24]) ).
tff(c_40310,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40306,c_4]) ).
tff(c_40359,plain,
! [X_394,Y_395,Z_396] : ( multiply(multiply(X_394,Y_395),Z_396) = multiply(X_394,multiply(Y_395,Z_396)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_40383,plain,
! [Z_396] : ( multiply(sk_c7,multiply(sk_c5,Z_396)) = multiply(identity,Z_396) ),
inference(superposition,[status(thm),theory(equality)],[c_40310,c_40359]) ).
tff(c_41672,plain,
! [Z_427] : ( multiply(sk_c7,multiply(sk_c5,Z_427)) = Z_427 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40383]) ).
tff(c_41684,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_40337,c_41672]) ).
tff(c_40395,plain,
! [X_2,Z_396] : ( multiply(inverse(X_2),multiply(X_2,Z_396)) = multiply(identity,Z_396) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_40359]) ).
tff(c_41695,plain,
! [X_428,Z_429] : ( multiply(inverse(X_428),multiply(X_428,Z_429)) = Z_429 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40395]) ).
tff(c_41713,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_41684,c_41695]) ).
tff(c_18,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_40343,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_40298,c_18]) ).
tff(c_41734,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_40343,c_41695]) ).
tff(c_42110,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_41713,c_41734]) ).
tff(c_22,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_40328,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_40298,c_22]) ).
tff(c_40297,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_40302,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40297,c_4]) ).
tff(c_40386,plain,
! [Z_396] : ( multiply(sk_c8,multiply(sk_c4,Z_396)) = multiply(identity,Z_396) ),
inference(superposition,[status(thm),theory(equality)],[c_40302,c_40359]) ).
tff(c_41253,plain,
! [Z_418] : ( multiply(sk_c8,multiply(sk_c4,Z_418)) = Z_418 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40386]) ).
tff(c_41265,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40328,c_41253]) ).
tff(c_42124,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_42110,c_42110,c_41265]) ).
tff(c_42132,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41684,c_42124]) ).
tff(c_42176,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42132,c_42132,c_41713]) ).
tff(c_42184,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42176]) ).
tff(c_41761,plain,
multiply(inverse(sk_c6),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_89,c_41695]) ).
tff(c_42196,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_42184,c_41761]) ).
tff(c_42200,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42196]) ).
tff(c_42199,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42184,c_85]) ).
tff(c_42237,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42200,c_42199]) ).
tff(c_40461,plain,
! [Z_400] : ( multiply(sk_c7,multiply(sk_c5,Z_400)) = Z_400 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40383]) ).
tff(c_40473,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_40337,c_40461]) ).
tff(c_40423,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_40343,c_68]) ).
tff(c_40484,plain,
! [X3_401] :
( ( inverse(X3_401) != sk_c8 )
| ( multiply(X3_401,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_40423]) ).
tff(c_40498,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_40484]) ).
tff(c_40505,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_40498]) ).
tff(c_40438,plain,
! [Z_399] : ( multiply(sk_c8,multiply(sk_c4,Z_399)) = Z_399 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40386]) ).
tff(c_40450,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40328,c_40438]) ).
tff(c_40632,plain,
! [Z_405] : ( multiply(sk_c7,multiply(sk_c8,Z_405)) = multiply(sk_c6,Z_405) ),
inference(superposition,[status(thm),theory(equality)],[c_40343,c_40359]) ).
tff(c_40647,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_40450,c_40632]) ).
tff(c_40657,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40473,c_40647]) ).
tff(c_40407,plain,
! [X_2,Z_396] : ( multiply(inverse(X_2),multiply(X_2,Z_396)) = Z_396 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40395]) ).
tff(c_40661,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_40657,c_40407]) ).
tff(c_40670,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40661]) ).
tff(c_40677,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_40670,c_40670,c_40450]) ).
tff(c_40685,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40677]) ).
tff(c_40687,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_40505,c_40685]) ).
tff(c_40689,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_40498]) ).
tff(c_40502,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_40484]) ).
tff(c_40504,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_40502]) ).
tff(c_40690,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_40689,c_40504]) ).
tff(c_40692,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40689,c_40689,c_40473]) ).
tff(c_40703,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40692]) ).
tff(c_40696,plain,
multiply(identity,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40689,c_40343]) ).
tff(c_40823,plain,
multiply(identity,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40703,c_40696]) ).
tff(c_40830,plain,
sk_c8 = identity,
inference(superposition,[status(thm),theory(equality)],[c_40823,c_2]) ).
tff(c_40838,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_40690,c_40830]) ).
tff(c_40840,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_40502]) ).
tff(c_40843,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_40840,c_40840,c_40450]) ).
tff(c_40850,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40473,c_40843]) ).
tff(c_40856,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40850,c_40840]) ).
tff(c_40839,plain,
inverse(identity) != sk_c8,
inference(splitRight,[status(thm)],[c_40502]) ).
tff(c_40884,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40856,c_40839]) ).
tff(c_40403,plain,
! [Z_396] : ( multiply(sk_c7,multiply(sk_c5,Z_396)) = Z_396 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40383]) ).
tff(c_40858,plain,
! [Z_396] : ( multiply(sk_c6,multiply(sk_c5,Z_396)) = Z_396 ),
inference(demodulation,[status(thm),theory(equality)],[c_40850,c_40403]) ).
tff(c_40377,plain,
! [Z_396] : ( multiply(sk_c5,multiply(sk_c6,Z_396)) = multiply(sk_c7,Z_396) ),
inference(superposition,[status(thm),theory(equality)],[c_40337,c_40359]) ).
tff(c_41001,plain,
! [Z_410] : ( multiply(sk_c5,multiply(sk_c6,Z_410)) = multiply(sk_c6,Z_410) ),
inference(demodulation,[status(thm),theory(equality)],[c_40850,c_40377]) ).
tff(c_41016,plain,
! [Z_396] : ( multiply(sk_c6,multiply(sk_c5,Z_396)) = multiply(sk_c5,Z_396) ),
inference(superposition,[status(thm),theory(equality)],[c_40858,c_41001]) ).
tff(c_41044,plain,
! [Z_396] : ( multiply(sk_c5,Z_396) = Z_396 ),
inference(demodulation,[status(thm),theory(equality)],[c_40858,c_41016]) ).
tff(c_41071,plain,
! [Z_412] : ( multiply(sk_c6,Z_412) = Z_412 ),
inference(demodulation,[status(thm),theory(equality)],[c_41044,c_40858]) ).
tff(c_40864,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40850,c_98]) ).
tff(c_40888,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40864,c_4]) ).
tff(c_41083,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_41071,c_40888]) ).
tff(c_41128,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41083,c_40864]) ).
tff(c_41132,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_40884,c_41128]) ).
tff(c_41133,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_40423]) ).
tff(c_41232,plain,
! [X2_417] :
( ( multiply(X2_417,sk_c6) != sk_c7 )
| ( inverse(X2_417) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_41133]) ).
tff(c_41239,plain,
inverse(sk_c5) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40337,c_41232]) ).
tff(c_41251,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40306,c_41239]) ).
tff(c_41252,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_41133]) ).
tff(c_41338,plain,
! [X4_421] :
( ( inverse(X4_421) != sk_c7 )
| ( multiply(X4_421,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_41252]) ).
tff(c_41348,plain,
( ( inverse(sk_c4) != sk_c7 )
| ( sk_c8 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_40328,c_41338]) ).
tff(c_41358,plain,
( ( sk_c8 != sk_c7 )
| ( sk_c8 != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_40297,c_41348]) ).
tff(c_41359,plain,
sk_c8 != sk_c6,
inference(splitLeft,[status(thm)],[c_41358]) ).
tff(c_41356,plain,
( ( inverse(identity) != sk_c7 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_41338]) ).
tff(c_41360,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_41356]) ).
tff(c_41277,plain,
! [Z_419] : ( multiply(sk_c7,multiply(sk_c5,Z_419)) = Z_419 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40383]) ).
tff(c_41289,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_40337,c_41277]) ).
tff(c_41300,plain,
! [Z_420] : ( multiply(sk_c7,multiply(sk_c8,Z_420)) = multiply(sk_c6,Z_420) ),
inference(superposition,[status(thm),theory(equality)],[c_40343,c_40359]) ).
tff(c_41312,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_41265,c_41300]) ).
tff(c_41322,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41289,c_41312]) ).
tff(c_41362,plain,
! [Z_422] : ( multiply(sk_c5,multiply(sk_c6,Z_422)) = multiply(sk_c7,Z_422) ),
inference(superposition,[status(thm),theory(equality)],[c_40337,c_40359]) ).
tff(c_41377,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_41322,c_41362]) ).
tff(c_41387,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40337,c_40343,c_41377]) ).
tff(c_41389,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41360,c_41387]) ).
tff(c_41391,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_41356]) ).
tff(c_41402,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_41391,c_40328]) ).
tff(c_40404,plain,
! [Z_396] : ( multiply(sk_c8,multiply(sk_c4,Z_396)) = Z_396 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40386]) ).
tff(c_41453,plain,
multiply(sk_c8,sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_41402,c_40404]) ).
tff(c_40380,plain,
! [Z_396] : ( multiply(sk_c4,multiply(sk_c7,Z_396)) = multiply(sk_c8,Z_396) ),
inference(superposition,[status(thm),theory(equality)],[c_40328,c_40359]) ).
tff(c_41511,plain,
! [Z_425] : ( multiply(sk_c4,multiply(sk_c6,Z_425)) = multiply(sk_c8,Z_425) ),
inference(demodulation,[status(thm),theory(equality)],[c_41391,c_40380]) ).
tff(c_41541,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_41322,c_41511]) ).
tff(c_41552,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41453,c_41402,c_41541]) ).
tff(c_41554,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41359,c_41552]) ).
tff(c_41556,plain,
sk_c8 = sk_c6,
inference(splitRight,[status(thm)],[c_41358]) ).
tff(c_41555,plain,
sk_c8 != sk_c7,
inference(splitRight,[status(thm)],[c_41358]) ).
tff(c_41570,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41556,c_41555]) ).
tff(c_41563,plain,
multiply(sk_c6,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_41556,c_40302]) ).
tff(c_41318,plain,
multiply(sk_c7,identity) = multiply(sk_c6,sk_c4),
inference(superposition,[status(thm),theory(equality)],[c_40302,c_41300]) ).
tff(c_41590,plain,
multiply(sk_c7,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_41563,c_41318]) ).
tff(c_41610,plain,
! [Z_5] : ( multiply(sk_c7,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_41590,c_6]) ).
tff(c_41617,plain,
! [Z_426] : ( multiply(sk_c7,Z_426) = Z_426 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_41610]) ).
tff(c_41627,plain,
sk_c7 = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_41617,c_41289]) ).
tff(c_41663,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41570,c_41627]) ).
tff(c_41664,plain,
! [X5_6,X1_8] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_41252]) ).
tff(c_41918,plain,
! [X1_432] :
( ( multiply(X1_432,sk_c7) != sk_c8 )
| ( inverse(X1_432) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_41664]) ).
tff(c_41932,plain,
inverse(sk_c4) != sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_40328,c_41918]) ).
tff(c_41944,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40297,c_41932]) ).
tff(c_42083,plain,
! [X5_435] :
( ( multiply(X5_435,sk_c8) != sk_c6 )
| ( inverse(X5_435) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_41664]) ).
tff(c_42106,plain,
inverse(sk_c7) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_40343,c_42083]) ).
tff(c_42177,plain,
inverse(sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42132,c_42106]) ).
tff(c_42310,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_42237,c_42184,c_42184,c_42177]) ).
tff(c_42312,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_46,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_42370,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_42312,c_46]) ).
tff(c_44,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_42320,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_42312,c_44]) ).
tff(c_42324,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42320,c_4]) ).
tff(c_42385,plain,
! [X_439,Y_440,Z_441] : ( multiply(multiply(X_439,Y_440),Z_441) = multiply(X_439,multiply(Y_440,Z_441)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_42412,plain,
! [Z_441] : ( multiply(sk_c7,multiply(sk_c5,Z_441)) = multiply(identity,Z_441) ),
inference(superposition,[status(thm),theory(equality)],[c_42324,c_42385]) ).
tff(c_43462,plain,
! [Z_461] : ( multiply(sk_c7,multiply(sk_c5,Z_461)) = Z_461 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42412]) ).
tff(c_43474,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_42370,c_43462]) ).
tff(c_42421,plain,
! [X_2,Z_441] : ( multiply(inverse(X_2),multiply(X_2,Z_441)) = multiply(identity,Z_441) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42385]) ).
tff(c_43530,plain,
! [X_464,Z_465] : ( multiply(inverse(X_464),multiply(X_464,Z_465)) = Z_465 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42421]) ).
tff(c_43554,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_43474,c_43530]) ).
tff(c_38,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_42339,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_42312,c_38]) ).
tff(c_43581,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_42339,c_43530]) ).
tff(c_44106,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43554,c_43581]) ).
tff(c_42,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_42344,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_42312,c_42]) ).
tff(c_42311,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_42316,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42311,c_4]) ).
tff(c_42415,plain,
! [Z_441] : ( multiply(sk_c8,multiply(sk_c4,Z_441)) = multiply(identity,Z_441) ),
inference(superposition,[status(thm),theory(equality)],[c_42316,c_42385]) ).
tff(c_43485,plain,
! [Z_462] : ( multiply(sk_c8,multiply(sk_c4,Z_462)) = Z_462 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42415]) ).
tff(c_43497,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_42344,c_43485]) ).
tff(c_44121,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_44106,c_44106,c_43497]) ).
tff(c_44126,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_43474,c_44121]) ).
tff(c_44133,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44126,c_44126,c_43554]) ).
tff(c_44142,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_44133]) ).
tff(c_43982,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43554,c_43581]) ).
tff(c_43548,plain,
multiply(inverse(sk_c8),sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_43497,c_43530]) ).
tff(c_43995,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43982,c_43982,c_43548]) ).
tff(c_44004,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_43995]) ).
tff(c_43762,plain,
! [Z_468] : ( multiply(sk_c7,multiply(sk_c8,Z_468)) = multiply(sk_c6,Z_468) ),
inference(superposition,[status(thm),theory(equality)],[c_42339,c_42385]) ).
tff(c_43777,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_43497,c_43762]) ).
tff(c_43787,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_43474,c_43777]) ).
tff(c_42433,plain,
! [X_2,Z_441] : ( multiply(inverse(X_2),multiply(X_2,Z_441)) = Z_441 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42421]) ).
tff(c_43791,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_43787,c_42433]) ).
tff(c_43797,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_43791]) ).
tff(c_43804,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43797,c_43797,c_43497]) ).
tff(c_43811,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43804]) ).
tff(c_43817,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_43811,c_43811,c_43474]) ).
tff(c_43824,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43817]) ).
tff(c_42464,plain,
! [Z_444] : ( multiply(sk_c7,multiply(sk_c5,Z_444)) = Z_444 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42412]) ).
tff(c_42476,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_42370,c_42464]) ).
tff(c_42462,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42339,c_68]) ).
tff(c_42510,plain,
! [X3_446] :
( ( inverse(X3_446) != sk_c8 )
| ( multiply(X3_446,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_42462]) ).
tff(c_42524,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42510]) ).
tff(c_42532,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_42524]) ).
tff(c_42487,plain,
! [Z_445] : ( multiply(sk_c8,multiply(sk_c4,Z_445)) = Z_445 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42415]) ).
tff(c_42499,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_42344,c_42487]) ).
tff(c_42669,plain,
! [Z_450] : ( multiply(sk_c7,multiply(sk_c8,Z_450)) = multiply(sk_c6,Z_450) ),
inference(superposition,[status(thm),theory(equality)],[c_42339,c_42385]) ).
tff(c_42684,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_42499,c_42669]) ).
tff(c_42700,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42476,c_42684]) ).
tff(c_42704,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_42700,c_42433]) ).
tff(c_42713,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42704]) ).
tff(c_42721,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_42713,c_42713,c_42499]) ).
tff(c_42732,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42721]) ).
tff(c_42734,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_42532,c_42732]) ).
tff(c_42736,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_42524]) ).
tff(c_42520,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_42339,c_42510]) ).
tff(c_42531,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_42520]) ).
tff(c_42760,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_42736,c_42531]) ).
tff(c_42764,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42736,c_42736,c_42476]) ).
tff(c_42773,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42764]) ).
tff(c_42778,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_42760,c_42773]) ).
tff(c_42780,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_42520]) ).
tff(c_42844,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42780,c_42524]) ).
tff(c_42845,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_42844]) ).
tff(c_42784,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42780,c_42780,c_42476]) ).
tff(c_42918,plain,
! [X_454,Z_455] : ( multiply(inverse(X_454),multiply(X_454,Z_455)) = Z_455 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42421]) ).
tff(c_42951,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_42784,c_42918]) ).
tff(c_43009,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42951]) ).
tff(c_43011,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_42845,c_43009]) ).
tff(c_43013,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_42844]) ).
tff(c_42528,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_42510]) ).
tff(c_42530,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_42528]) ).
tff(c_42781,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42780,c_42530]) ).
tff(c_43022,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_43013,c_42781]) ).
tff(c_42788,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42780,c_42339]) ).
tff(c_43016,plain,
multiply(identity,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43013,c_43013,c_42788]) ).
tff(c_43123,plain,
sk_c8 = identity,
inference(superposition,[status(thm),theory(equality)],[c_43016,c_2]) ).
tff(c_43131,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43022,c_43123]) ).
tff(c_43133,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_42528]) ).
tff(c_43135,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43133,c_43133,c_42499]) ).
tff(c_43144,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_42476,c_43135]) ).
tff(c_43158,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_43144,c_43133]) ).
tff(c_43251,plain,
( ( inverse(inverse(sk_c6)) != sk_c6 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_43144,c_43158,c_43158,c_42524]) ).
tff(c_43252,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_43251]) ).
tff(c_43159,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_43144,c_43144,c_42476]) ).
tff(c_43253,plain,
! [X_456,Z_457] : ( multiply(inverse(X_456),multiply(X_456,Z_457)) = Z_457 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42421]) ).
tff(c_43277,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_43159,c_43253]) ).
tff(c_43318,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_43277]) ).
tff(c_43321,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43252,c_43318]) ).
tff(c_43323,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_43251]) ).
tff(c_43132,plain,
inverse(identity) != sk_c8,
inference(splitRight,[status(thm)],[c_42528]) ).
tff(c_43173,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_43158,c_43132]) ).
tff(c_43335,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_43323,c_43173]) ).
tff(c_43143,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43133,c_42311]) ).
tff(c_43157,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_43144,c_43143]) ).
tff(c_43330,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43323,c_43157]) ).
tff(c_43387,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_43330,c_4]) ).
tff(c_43441,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_43387,c_42433]) ).
tff(c_43453,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_43441]) ).
tff(c_43457,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43453,c_43330]) ).
tff(c_43460,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43335,c_43457]) ).
tff(c_43461,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_42462]) ).
tff(c_43509,plain,
! [X2_463] :
( ( multiply(X2_463,sk_c6) != sk_c7 )
| ( inverse(X2_463) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_43461]) ).
tff(c_43516,plain,
inverse(sk_c5) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_42370,c_43509]) ).
tff(c_43528,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_42320,c_43516]) ).
tff(c_43529,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_43461]) ).
tff(c_43734,plain,
! [X4_10] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_43529]) ).
tff(c_43843,plain,
! [X4_469] :
( ( inverse(X4_469) != identity )
| ( multiply(X4_469,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_43824,c_43811,c_43811,c_43734]) ).
tff(c_43865,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_43843]) ).
tff(c_43596,plain,
multiply(inverse(sk_c6),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_89,c_43530]) ).
tff(c_43833,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_43824,c_43596]) ).
tff(c_43837,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_43833]) ).
tff(c_43836,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43824,c_85]) ).
tff(c_43879,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43837,c_43836]) ).
tff(c_43880,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43865,c_43879]) ).
tff(c_43881,plain,
! [X5_6,X1_8] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_43529]) ).
tff(c_43910,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_43881]) ).
tff(c_44012,plain,
! [X1_471] :
( ( multiply(X1_471,sk_c7) != sk_c7 )
| ( inverse(X1_471) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_43982,c_43982,c_43910]) ).
tff(c_44033,plain,
inverse(identity) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_2,c_44012]) ).
tff(c_44065,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_44004,c_44033]) ).
tff(c_43605,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_43530]) ).
tff(c_43584,plain,
multiply(inverse(sk_c7),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_42324,c_43530]) ).
tff(c_44038,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_44004,c_43584]) ).
tff(c_44045,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43605,c_44038]) ).
tff(c_44043,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44004,c_42320]) ).
tff(c_44075,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44045,c_44043]) ).
tff(c_44076,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44065,c_44075]) ).
tff(c_44079,plain,
! [X5_472] :
( ( multiply(X5_472,sk_c8) != sk_c6 )
| ( inverse(X5_472) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_43881]) ).
tff(c_44102,plain,
inverse(sk_c7) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_42339,c_44079]) ).
tff(c_44134,plain,
inverse(sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44126,c_44102]) ).
tff(c_44241,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_44142,c_44142,c_44134]) ).
tff(c_44178,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_44142,c_43596]) ).
tff(c_44182,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43605,c_44178]) ).
tff(c_44135,plain,
multiply(inverse(sk_c6),identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_44126,c_43584]) ).
tff(c_44143,plain,
sk_c5 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_43596,c_44135]) ).
tff(c_44205,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44182,c_44143]) ).
tff(c_44140,plain,
inverse(sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44126,c_42320]) ).
tff(c_44242,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44205,c_44142,c_44140]) ).
tff(c_44243,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44241,c_44242]) ).
tff(c_44245,plain,
inverse(sk_c3) != sk_c6,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_52,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c3) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_44295,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_44245,c_52]) ).
tff(c_50,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c3) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_44253,plain,
inverse(sk_c3) = sk_c6,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_44254,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44245,c_44253]) ).
tff(c_44255,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_44260,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_44255,c_4]) ).
tff(c_44323,plain,
! [X_476,Y_477,Z_478] : ( multiply(multiply(X_476,Y_477),Z_478) = multiply(X_476,multiply(Y_477,Z_478)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_44350,plain,
! [Z_478] : ( multiply(sk_c8,multiply(sk_c4,Z_478)) = multiply(identity,Z_478) ),
inference(superposition,[status(thm),theory(equality)],[c_44260,c_44323]) ).
tff(c_44369,plain,
! [Z_479] : ( multiply(sk_c8,multiply(sk_c4,Z_479)) = Z_479 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44350]) ).
tff(c_44381,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_44295,c_44369]) ).
tff(c_48,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c3) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_44302,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_44245,c_48]) ).
tff(c_45168,plain,
! [Z_497] : ( multiply(sk_c4,multiply(sk_c7,Z_497)) = multiply(sk_c8,Z_497) ),
inference(superposition,[status(thm),theory(equality)],[c_44295,c_44323]) ).
tff(c_45186,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_44302,c_45168]) ).
tff(c_45196,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_44381,c_45186]) ).
tff(c_44365,plain,
! [Z_478] : ( multiply(sk_c8,multiply(sk_c4,Z_478)) = Z_478 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44350]) ).
tff(c_45210,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45196,c_44365]) ).
tff(c_56,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_44290,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_44245,c_56]) ).
tff(c_44244,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_44249,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_44244,c_4]) ).
tff(c_44353,plain,
! [Z_478] : ( multiply(sk_c7,multiply(sk_c5,Z_478)) = multiply(identity,Z_478) ),
inference(superposition,[status(thm),theory(equality)],[c_44249,c_44323]) ).
tff(c_45152,plain,
! [Z_496] : ( multiply(sk_c7,multiply(sk_c5,Z_496)) = Z_496 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44353]) ).
tff(c_45164,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_44290,c_45152]) ).
tff(c_44341,plain,
! [Z_478] : ( multiply(sk_c4,multiply(sk_c7,Z_478)) = multiply(sk_c8,Z_478) ),
inference(superposition,[status(thm),theory(equality)],[c_44295,c_44323]) ).
tff(c_45200,plain,
multiply(sk_c8,sk_c7) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_45164,c_44341]) ).
tff(c_45368,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45196,c_45210,c_45200]) ).
tff(c_45372,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45368,c_45368,c_45164]) ).
tff(c_44356,plain,
! [X_2,Z_478] : ( multiply(inverse(X_2),multiply(X_2,Z_478)) = multiply(identity,Z_478) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_44323]) ).
tff(c_46331,plain,
! [X_519,Z_520] : ( multiply(inverse(X_519),multiply(X_519,Z_520)) = Z_520 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44356]) ).
tff(c_46355,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45372,c_46331]) ).
tff(c_46384,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_46355]) ).
tff(c_45371,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45368,c_45196]) ).
tff(c_45377,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_45368,c_44295]) ).
tff(c_46295,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45371,c_45377]) ).
tff(c_46387,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_46384,c_46295]) ).
tff(c_44367,plain,
! [X_2,Z_478] : ( multiply(inverse(X_2),multiply(X_2,Z_478)) = Z_478 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44356]) ).
tff(c_46537,plain,
! [X_523,Z_524] : ( multiply(inverse(inverse(X_523)),Z_524) = multiply(X_523,Z_524) ),
inference(superposition,[status(thm),theory(equality)],[c_46331,c_44367]) ).
tff(c_46376,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_46331]) ).
tff(c_46544,plain,
! [X_523] : ( multiply(X_523,identity) = X_523 ),
inference(superposition,[status(thm),theory(equality)],[c_46537,c_46376]) ).
tff(c_45499,plain,
! [X_501,Z_502] : ( multiply(inverse(X_501),multiply(X_501,Z_502)) = Z_502 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44356]) ).
tff(c_45709,plain,
! [X_505,Z_506] : ( multiply(inverse(inverse(X_505)),Z_506) = multiply(X_505,Z_506) ),
inference(superposition,[status(thm),theory(equality)],[c_44367,c_45499]) ).
tff(c_45547,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_45499]) ).
tff(c_45716,plain,
! [X_505] : ( multiply(X_505,identity) = X_505 ),
inference(superposition,[status(thm),theory(equality)],[c_45709,c_45547]) ).
tff(c_45517,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45372,c_45499]) ).
tff(c_45554,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_45517]) ).
tff(c_45257,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45210,c_45196,c_45200]) ).
tff(c_45271,plain,
inverse(sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45257,c_44244]) ).
tff(c_45267,plain,
multiply(sk_c5,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45257,c_44290]) ).
tff(c_44386,plain,
! [X5_6,X1_8,X3_7,X2_9,X4_10] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_44302,c_68]) ).
tff(c_44431,plain,
! [X3_482] :
( ( inverse(X3_482) != sk_c8 )
| ( multiply(X3_482,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_44386]) ).
tff(c_44445,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_44431]) ).
tff(c_44453,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_44445]) ).
tff(c_44395,plain,
! [Z_480] : ( multiply(sk_c7,multiply(sk_c5,Z_480)) = Z_480 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44353]) ).
tff(c_44407,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_44290,c_44395]) ).
tff(c_44550,plain,
! [Z_485] : ( multiply(sk_c7,multiply(sk_c8,Z_485)) = multiply(sk_c6,Z_485) ),
inference(superposition,[status(thm),theory(equality)],[c_44302,c_44323]) ).
tff(c_44565,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_44381,c_44550]) ).
tff(c_44575,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44407,c_44565]) ).
tff(c_44579,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_44575,c_44367]) ).
tff(c_44588,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_44579]) ).
tff(c_44597,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_44588,c_44588,c_44381]) ).
tff(c_44605,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44597]) ).
tff(c_44607,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44453,c_44605]) ).
tff(c_44609,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_44445]) ).
tff(c_44441,plain,
( ( inverse(sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_44302,c_44431]) ).
tff(c_44451,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_44441]) ).
tff(c_44610,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_44609,c_44451]) ).
tff(c_44613,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44609,c_44609,c_44407]) ).
tff(c_44623,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44613]) ).
tff(c_44655,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44610,c_44623]) ).
tff(c_44657,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_44441]) ).
tff(c_44741,plain,
( ( inverse(inverse(sk_c8)) != sk_c8 )
| ( sk_c6 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_44657,c_44445]) ).
tff(c_44742,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_44741]) ).
tff(c_44660,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44657,c_44657,c_44407]) ).
tff(c_44781,plain,
! [X_489,Z_490] : ( multiply(inverse(X_489),multiply(X_489,Z_490)) = Z_490 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_44356]) ).
tff(c_44805,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_44660,c_44781]) ).
tff(c_44851,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_44805]) ).
tff(c_44853,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44742,c_44851]) ).
tff(c_44855,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_44741]) ).
tff(c_44449,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_44431]) ).
tff(c_44731,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_44657,c_44449]) ).
tff(c_44732,plain,
sk_c8 != sk_c6,
inference(splitLeft,[status(thm)],[c_44731]) ).
tff(c_44857,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_44855,c_44732]) ).
tff(c_44663,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44657,c_44302]) ).
tff(c_44860,plain,
multiply(identity,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44855,c_44855,c_44663]) ).
tff(c_44936,plain,
sk_c8 = identity,
inference(superposition,[status(thm),theory(equality)],[c_44860,c_2]) ).
tff(c_44944,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44857,c_44936]) ).
tff(c_44946,plain,
sk_c8 = sk_c6,
inference(splitRight,[status(thm)],[c_44731]) ).
tff(c_44945,plain,
inverse(identity) != sk_c8,
inference(splitRight,[status(thm)],[c_44731]) ).
tff(c_44965,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44946,c_44945]) ).
tff(c_44668,plain,
multiply(sk_c6,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44657,c_44249]) ).
tff(c_44338,plain,
! [Z_478] : ( multiply(sk_c7,multiply(sk_c8,Z_478)) = multiply(sk_c6,Z_478) ),
inference(superposition,[status(thm),theory(equality)],[c_44302,c_44323]) ).
tff(c_44994,plain,
! [Z_492] : ( multiply(sk_c6,multiply(sk_c6,Z_492)) = multiply(sk_c6,Z_492) ),
inference(demodulation,[status(thm),theory(equality)],[c_44946,c_44657,c_44338]) ).
tff(c_45021,plain,
multiply(sk_c6,sk_c5) = multiply(sk_c6,identity),
inference(superposition,[status(thm),theory(equality)],[c_44668,c_44994]) ).
tff(c_45030,plain,
multiply(sk_c6,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44668,c_45021]) ).
tff(c_45037,plain,
! [Z_5] : ( multiply(sk_c6,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_45030,c_6]) ).
tff(c_45049,plain,
! [Z_493] : ( multiply(sk_c6,Z_493) = Z_493 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_45037]) ).
tff(c_44953,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_44946,c_44255]) ).
tff(c_44961,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_44953,c_4]) ).
tff(c_45055,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_45049,c_44961]) ).
tff(c_45139,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45055,c_44953]) ).
tff(c_45143,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44965,c_45139]) ).
tff(c_45144,plain,
! [X4_10,X5_6,X1_8,X2_9] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_44386]) ).
tff(c_45240,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_45144]) ).
tff(c_45324,plain,
! [X2_499] :
( ( multiply(X2_499,sk_c6) != sk_c6 )
| ( inverse(X2_499) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_45257,c_45257,c_45240]) ).
tff(c_45330,plain,
inverse(sk_c5) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_45267,c_45324]) ).
tff(c_45350,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_45271,c_45330]) ).
tff(c_45351,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_45144]) ).
tff(c_45434,plain,
! [X1_8,X5_6,X4_10] :
( ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_45368,c_45368,c_45368,c_45351]) ).
tff(c_45435,plain,
! [X4_10] :
( ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_45434]) ).
tff(c_46262,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_45716,c_45554,c_45554,c_45554,c_45435]) ).
tff(c_45443,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45371,c_45377]) ).
tff(c_45461,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_45443,c_44255]) ).
tff(c_45478,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_45461,c_4]) ).
tff(c_45582,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_45554,c_45478]) ).
tff(c_45559,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_45554,c_45461]) ).
tff(c_45587,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_45582,c_45559]) ).
tff(c_46264,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46262,c_45587]) ).
tff(c_46265,plain,
! [X5_6,X1_8] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_45434]) ).
tff(c_57899,plain,
! [X5_6,X1_8] :
( ( identity != X5_6 )
| ( inverse(X5_6) != identity )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_46387,c_46544,c_46387,c_46384,c_46384,c_46544,c_46387,c_46384,c_46265]) ).
tff(c_57901,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_57899]) ).
tff(c_46314,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_46295,c_44255]) ).
tff(c_46327,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_46314,c_4]) ).
tff(c_46410,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46384,c_46327]) ).
tff(c_46386,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_46384,c_46314]) ).
tff(c_46415,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_46410,c_46386]) ).
tff(c_57903,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57901,c_46415]) ).
tff(c_57905,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_57899]) ).
tff(c_57907,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57905,c_46415]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP255-1 : TPTP v9.0.0. Released v2.5.0.
% 0.10/0.13 % 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.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:39:28 EDT 2025
% 0.13/0.34 % CPUTime :
% 17.48/6.54 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.65/6.60
% 17.65/6.60 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------