%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP327-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n023.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:56 PM UTC 2025
% Result : Unsatisfiable 22.36s 10.29s
% Output : CNFRefutation 22.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 30
% Syntax : Number of formulae : 541 ( 450 unt; 0 typ; 0 def)
% Number of atoms : 757 ( 729 equ)
% Maximal formula atoms : 12 ( 1 avg)
% Number of connectives : 466 ( 250 ~; 216 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 255 ( 255 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_120,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c3 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_144,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_63,axiom,
multiply(sk_c7,sk_c8) = sk_c6,
file(unknown,unknown) ).
tff(f_72,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_96,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_126,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c3 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_108,axiom,
( ( multiply(sk_c8,sk_c3) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_189,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( multiply(X3,sk_c7) != sk_c8 )
| ( inverse(X3) != sk_c7 )
| ( multiply(sk_c8,X4) != sk_c7 )
| ( multiply(X5,sk_c8) != X4 )
| ( inverse(X5) != sk_c8 )
| ( inverse(sk_c7) != sk_c6 )
| ( multiply(sk_c6,sk_c8) != sk_c7 )
| ( inverse(X1) != sk_c8 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( inverse(X2) != sk_c7 )
| ( multiply(X2,sk_c6) != sk_c7 ) ),
file(unknown,unknown) ).
tff(f_132,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c3 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_135,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c3 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_66,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_69,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_75,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_102,axiom,
( ( multiply(sk_c8,sk_c3) = sk_c7 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_78,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_114,axiom,
( ( multiply(sk_c8,sk_c3) = sk_c7 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_117,axiom,
( ( multiply(sk_c8,sk_c3) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_105,axiom,
( ( multiply(sk_c8,sk_c3) = sk_c7 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_111,axiom,
( ( multiply(sk_c8,sk_c3) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_84,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_99,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_87,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_138,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_153,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_147,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_150,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_141,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_48914,plain,
! [X_412,Y_413,Z_414] : ( multiply(multiply(X_412,Y_413),Z_414) = multiply(X_412,multiply(Y_413,Z_414)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_48950,plain,
! [X_2,Z_414] : ( multiply(inverse(X_2),multiply(X_2,Z_414)) = multiply(identity,Z_414) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_48914]) ).
tff(c_48965,plain,
! [X_2,Z_414] : ( multiply(inverse(X_2),multiply(X_2,Z_414)) = Z_414 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48950]) ).
tff(c_49433,plain,
! [X_425,Z_426] : ( multiply(inverse(X_425),multiply(X_425,Z_426)) = Z_426 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48950]) ).
tff(c_49608,plain,
! [X_428,Z_429] : ( multiply(inverse(inverse(X_428)),Z_429) = multiply(X_428,Z_429) ),
inference(superposition,[status(thm),theory(equality)],[c_48965,c_49433]) ).
tff(c_49457,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_49433]) ).
tff(c_49615,plain,
! [X_428] : ( multiply(X_428,identity) = X_428 ),
inference(superposition,[status(thm),theory(equality)],[c_49608,c_49457]) ).
tff(c_46,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c8) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_17110,plain,
multiply(sk_c2,sk_c8) = sk_c3,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_62,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_93,plain,
inverse(sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_97,plain,
multiply(sk_c8,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_93,c_4]) ).
tff(c_17596,plain,
! [X_190,Y_191,Z_192] : ( multiply(multiply(X_190,Y_191),Z_192) = multiply(X_190,multiply(Y_191,Z_192)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_17635,plain,
! [Z_192] : ( multiply(sk_c8,multiply(sk_c2,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_97,c_17596]) ).
tff(c_17669,plain,
! [Z_194] : ( multiply(sk_c8,multiply(sk_c2,Z_194)) = Z_194 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17635]) ).
tff(c_17681,plain,
multiply(sk_c8,sk_c3) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_17110,c_17669]) ).
tff(c_8,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_128,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_30,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_101,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_105,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_101,c_4]) ).
tff(c_15569,plain,
! [X_154,Y_155,Z_156] : ( multiply(multiply(X_154,Y_155),Z_156) = multiply(X_154,multiply(Y_155,Z_156)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_15608,plain,
! [Z_156] : ( multiply(sk_c7,multiply(sk_c1,Z_156)) = multiply(identity,Z_156) ),
inference(superposition,[status(thm),theory(equality)],[c_105,c_15569]) ).
tff(c_15632,plain,
! [Z_157] : ( multiply(sk_c7,multiply(sk_c1,Z_157)) = Z_157 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15608]) ).
tff(c_15644,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_128,c_15632]) ).
tff(c_15648,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_15644]) ).
tff(c_15661,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15648,c_8]) ).
tff(c_15614,plain,
! [X_2,Z_156] : ( multiply(inverse(X_2),multiply(X_2,Z_156)) = multiply(identity,Z_156) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_15569]) ).
tff(c_15766,plain,
! [X_159,Z_160] : ( multiply(inverse(X_159),multiply(X_159,Z_160)) = Z_160 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15614]) ).
tff(c_15814,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_15661,c_15766]) ).
tff(c_15848,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15814]) ).
tff(c_15859,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15848,c_93]) ).
tff(c_15937,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_15859,c_4]) ).
tff(c_15630,plain,
! [X_2,Z_156] : ( multiply(inverse(X_2),multiply(X_2,Z_156)) = Z_156 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15614]) ).
tff(c_15992,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_15937,c_15630]) ).
tff(c_16004,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15992]) ).
tff(c_157,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_181,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_105,c_157]) ).
tff(c_202,plain,
! [Z_16] : ( multiply(sk_c7,multiply(sk_c1,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_181]) ).
tff(c_214,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_128,c_202]) ).
tff(c_218,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_214]) ).
tff(c_224,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_218,c_8]) ).
tff(c_187,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_157]) ).
tff(c_200,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_187]) ).
tff(c_493,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_224,c_200]) ).
tff(c_499,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_493]) ).
tff(c_50,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_133,plain,
multiply(sk_c2,sk_c8) = sk_c3,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_419,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_187]) ).
tff(c_446,plain,
multiply(inverse(sk_c2),sk_c3) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_133,c_419]) ).
tff(c_462,plain,
multiply(sk_c8,sk_c3) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_93,c_446]) ).
tff(c_476,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_462,c_200]) ).
tff(c_482,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_476]) ).
tff(c_38,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c8,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_122,plain,
multiply(sk_c8,sk_c3) = sk_c7,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_221,plain,
multiply(sk_c8,sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_218,c_122]) ).
tff(c_546,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_499,c_482,c_221]) ).
tff(c_647,plain,
! [X_23,Z_24] : ( multiply(inverse(inverse(X_23)),Z_24) = multiply(X_23,Z_24) ),
inference(superposition,[status(thm),theory(equality)],[c_419,c_200]) ).
tff(c_455,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_419]) ).
tff(c_654,plain,
! [X_23] : ( multiply(X_23,identity) = X_23 ),
inference(superposition,[status(thm),theory(equality)],[c_647,c_455]) ).
tff(c_184,plain,
! [Z_15] : ( multiply(sk_c8,multiply(sk_c2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_97,c_157]) ).
tff(c_268,plain,
! [Z_17] : ( multiply(sk_c8,multiply(sk_c2,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_184]) ).
tff(c_280,plain,
multiply(sk_c8,sk_c3) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_133,c_268]) ).
tff(c_284,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_221,c_280]) ).
tff(c_287,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_284,c_224]) ).
tff(c_359,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_287,c_200]) ).
tff(c_365,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_359]) ).
tff(c_291,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_284,c_93]) ).
tff(c_299,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_291,c_4]) ).
tff(c_379,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_365,c_299]) ).
tff(c_368,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_365,c_291]) ).
tff(c_392,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_379,c_368]) ).
tff(c_70,plain,
! [X2_9,X1_8,X5_6,X3_7] :
( ( 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_c6,sk_c8) != sk_c7 )
| ( inverse(sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_72,plain,
! [X2_9,X1_8,X5_6,X3_7] :
( ( 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_c6,sk_c8) != sk_c7 )
| ( inverse(sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_70]) ).
tff(c_244,plain,
! [X2_9,X1_8,X5_6,X3_7] :
( ( multiply(X2_9,sk_c6) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(sk_c6,sk_c8) != sk_c6 )
| ( inverse(sk_c6) != sk_c6 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c6 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_218,c_218,c_218,c_218,c_218,c_218,c_218,c_218,c_72]) ).
tff(c_245,plain,
inverse(sk_c6) != sk_c6,
inference(splitLeft,[status(thm)],[c_244]) ).
tff(c_370,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_365,c_365,c_245]) ).
tff(c_416,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_392,c_370]) ).
tff(c_417,plain,
! [X3_7,X5_6,X1_8,X2_9] :
( ( multiply(sk_c6,sk_c8) != sk_c6 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_244]) ).
tff(c_8731,plain,
! [X3_7,X5_6,X1_8,X2_9] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( identity != X2_9 )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_546,c_654,c_546,c_546,c_499,c_654,c_546,c_499,c_654,c_546,c_499,c_2,c_499,c_499,c_654,c_546,c_499,c_546,c_546,c_2,c_546,c_499,c_417]) ).
tff(c_8733,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8731]) ).
tff(c_418,plain,
inverse(sk_c6) = sk_c6,
inference(splitRight,[status(thm)],[c_244]) ).
tff(c_548,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_546,c_546,c_418]) ).
tff(c_8735,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8733,c_548]) ).
tff(c_8736,plain,
! [X1_8,X5_6,X3_7] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_8731]) ).
tff(c_14687,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8736]) ).
tff(c_14689,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14687,c_548]) ).
tff(c_14690,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_8736]) ).
tff(c_14692,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_14690]) ).
tff(c_14694,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14692,c_548]) ).
tff(c_15500,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_14690]) ).
tff(c_15502,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15500,c_548]) ).
tff(c_15504,plain,
multiply(sk_c2,sk_c8) != sk_c3,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_15535,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_15504,c_46]) ).
tff(c_15539,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_15535,c_4]) ).
tff(c_15653,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15648,c_15539]) ).
tff(c_54,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_15521,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_15504,c_54]) ).
tff(c_15656,plain,
inverse(sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15648,c_15521]) ).
tff(c_56,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_15550,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_15504,c_56]) ).
tff(c_15652,plain,
multiply(sk_c5,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15648,c_15550]) ).
tff(c_15793,plain,
multiply(inverse(sk_c5),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_15652,c_15766]) ).
tff(c_15844,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15653,c_15656,c_15793]) ).
tff(c_15658,plain,
multiply(sk_c8,sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15648,c_122]) ).
tff(c_15852,plain,
multiply(identity,sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15848,c_15658]) ).
tff(c_15860,plain,
sk_c6 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15852]) ).
tff(c_15917,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15844,c_15860]) ).
tff(c_15856,plain,
multiply(sk_c2,identity) != sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_15848,c_15504]) ).
tff(c_16131,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16004,c_15917,c_15856]) ).
tff(c_16133,plain,
multiply(sk_c1,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_10,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_16156,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_16133,c_10]) ).
tff(c_16160,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16156,c_4]) ).
tff(c_16150,plain,
multiply(sk_c2,sk_c8) = sk_c3,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_16203,plain,
! [X_163,Y_164,Z_165] : ( multiply(multiply(X_163,Y_164),Z_165) = multiply(X_163,multiply(Y_164,Z_165)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16245,plain,
! [Z_165] : ( multiply(sk_c8,multiply(sk_c2,Z_165)) = multiply(identity,Z_165) ),
inference(superposition,[status(thm),theory(equality)],[c_97,c_16203]) ).
tff(c_16301,plain,
! [Z_168] : ( multiply(sk_c8,multiply(sk_c2,Z_168)) = Z_168 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16245]) ).
tff(c_16316,plain,
multiply(sk_c8,sk_c3) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_16150,c_16301]) ).
tff(c_16320,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_122,c_16316]) ).
tff(c_12,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_16195,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16133,c_12]) ).
tff(c_16323,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16320,c_16195]) ).
tff(c_16333,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16160,c_16323]) ).
tff(c_16346,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16333,c_101]) ).
tff(c_16409,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16346,c_4]) ).
tff(c_16248,plain,
! [X_2,Z_165] : ( multiply(inverse(X_2),multiply(X_2,Z_165)) = multiply(identity,Z_165) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16203]) ).
tff(c_16264,plain,
! [X_2,Z_165] : ( multiply(inverse(X_2),multiply(X_2,Z_165)) = Z_165 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16248]) ).
tff(c_16486,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_16409,c_16264]) ).
tff(c_16498,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16486]) ).
tff(c_16327,plain,
multiply(sk_c1,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16320,c_16133]) ).
tff(c_16567,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16498,c_16333,c_16333,c_16327]) ).
tff(c_16569,plain,
multiply(sk_c2,sk_c8) != sk_c3,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_16585,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_16569,c_46]) ).
tff(c_16589,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16585,c_4]) ).
tff(c_16604,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16133,c_12]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_16599,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_16133,c_16]) ).
tff(c_16132,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_16137,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16132,c_4]) ).
tff(c_16623,plain,
! [X_171,Y_172,Z_173] : ( multiply(multiply(X_171,Y_172),Z_173) = multiply(X_171,multiply(Y_172,Z_173)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16653,plain,
! [Z_173] : ( multiply(sk_c8,multiply(sk_c4,Z_173)) = multiply(identity,Z_173) ),
inference(superposition,[status(thm),theory(equality)],[c_16137,c_16623]) ).
tff(c_16712,plain,
! [Z_176] : ( multiply(sk_c8,multiply(sk_c4,Z_176)) = Z_176 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16653]) ).
tff(c_16724,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16599,c_16712]) ).
tff(c_16735,plain,
! [Z_177] : ( multiply(sk_c7,multiply(sk_c8,Z_177)) = multiply(sk_c6,Z_177) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_16623]) ).
tff(c_16747,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_16724,c_16735]) ).
tff(c_16766,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16604,c_16747]) ).
tff(c_16647,plain,
! [Z_173] : ( multiply(sk_c6,multiply(sk_c7,Z_173)) = multiply(identity,Z_173) ),
inference(superposition,[status(thm),theory(equality)],[c_16589,c_16623]) ).
tff(c_16790,plain,
! [Z_178] : ( multiply(sk_c6,multiply(sk_c7,Z_178)) = Z_178 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16647]) ).
tff(c_16805,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16766,c_16790]) ).
tff(c_16824,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16589,c_16805]) ).
tff(c_16842,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16824,c_101]) ).
tff(c_16817,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_105,c_16790]) ).
tff(c_16568,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_16573,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16568,c_4]) ).
tff(c_16814,plain,
multiply(sk_c6,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16573,c_16790]) ).
tff(c_16904,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_16817,c_16814]) ).
tff(c_16614,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16569,c_56]) ).
tff(c_16832,plain,
multiply(sk_c5,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16824,c_16614]) ).
tff(c_16919,plain,
multiply(sk_c1,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16904,c_16832]) ).
tff(c_16665,plain,
! [X_2,Z_173] : ( multiply(inverse(X_2),multiply(X_2,Z_173)) = multiply(identity,Z_173) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16623]) ).
tff(c_16936,plain,
! [X_180,Z_181] : ( multiply(inverse(X_180),multiply(X_180,Z_181)) = Z_181 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16665]) ).
tff(c_16957,plain,
multiply(inverse(sk_c1),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16919,c_16936]) ).
tff(c_17003,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16842,c_16957]) ).
tff(c_16820,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_8,c_16790]) ).
tff(c_17011,plain,
multiply(identity,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_17003,c_17003,c_16820]) ).
tff(c_17014,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17011]) ).
tff(c_17010,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_17003,c_16817]) ).
tff(c_17013,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17010]) ).
tff(c_16839,plain,
multiply(sk_c1,identity) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_16824,c_16133]) ).
tff(c_17095,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_17014,c_2,c_17013,c_16839]) ).
tff(c_17097,plain,
multiply(sk_c8,sk_c3) != sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_17688,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_17681,c_17097]) ).
tff(c_34,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c8,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_102]) ).
tff(c_17116,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_17097,c_34]) ).
tff(c_17120,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_17116,c_4]) ).
tff(c_17623,plain,
! [Z_192] : ( multiply(sk_c6,multiply(sk_c7,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_17120,c_17596]) ).
tff(c_17696,plain,
! [Z_195] : ( multiply(sk_c6,multiply(sk_c7,Z_195)) = Z_195 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17623]) ).
tff(c_17714,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_105,c_17696]) ).
tff(c_18,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_17134,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_17173,plain,
! [X_183,Y_184,Z_185] : ( multiply(multiply(X_183,Y_184),Z_185) = multiply(X_183,multiply(Y_184,Z_185)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_17212,plain,
! [Z_185] : ( multiply(sk_c7,multiply(sk_c1,Z_185)) = multiply(identity,Z_185) ),
inference(superposition,[status(thm),theory(equality)],[c_105,c_17173]) ).
tff(c_17236,plain,
! [Z_186] : ( multiply(sk_c7,multiply(sk_c1,Z_186)) = Z_186 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17212]) ).
tff(c_17248,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_17134,c_17236]) ).
tff(c_17252,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_17248]) ).
tff(c_17260,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17252,c_17120]) ).
tff(c_42,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c8,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_17140,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_17097,c_42]) ).
tff(c_17258,plain,
inverse(sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17252,c_17140]) ).
tff(c_44,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_17168,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_17097,c_44]) ).
tff(c_17254,plain,
multiply(sk_c5,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17252,c_17168]) ).
tff(c_17218,plain,
! [X_2,Z_185] : ( multiply(inverse(X_2),multiply(X_2,Z_185)) = multiply(identity,Z_185) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17173]) ).
tff(c_17350,plain,
! [X_187,Z_188] : ( multiply(inverse(X_187),multiply(X_187,Z_188)) = Z_188 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17218]) ).
tff(c_17371,plain,
multiply(inverse(sk_c5),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17254,c_17350]) ).
tff(c_17424,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17260,c_17258,c_17371]) ).
tff(c_17265,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17252,c_8]) ).
tff(c_17395,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_17265,c_17350]) ).
tff(c_17429,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17395]) ).
tff(c_17262,plain,
multiply(sk_c8,sk_c3) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17252,c_17097]) ).
tff(c_17432,plain,
multiply(identity,sk_c3) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17429,c_17262]) ).
tff(c_17440,plain,
sk_c6 != sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17432]) ).
tff(c_17458,plain,
sk_c3 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_17424,c_17440]) ).
tff(c_17401,plain,
multiply(inverse(sk_c2),sk_c3) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_17110,c_17350]) ).
tff(c_17430,plain,
multiply(sk_c8,sk_c3) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_93,c_17401]) ).
tff(c_17554,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17429,c_2,c_17429,c_17430]) ).
tff(c_17555,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17458,c_17554]) ).
tff(c_17556,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_17561,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_17556,c_4]) ).
tff(c_17711,plain,
multiply(sk_c6,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_17561,c_17696]) ).
tff(c_17736,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_17714,c_17711]) ).
tff(c_17572,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_17097,c_44]) ).
tff(c_17737,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_17736,c_17572]) ).
tff(c_17632,plain,
! [Z_192] : ( multiply(sk_c7,multiply(sk_c1,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_105,c_17596]) ).
tff(c_17652,plain,
! [Z_192] : ( multiply(sk_c7,multiply(sk_c1,Z_192)) = Z_192 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17632]) ).
tff(c_17749,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17737,c_17652]) ).
tff(c_17650,plain,
! [Z_192] : ( multiply(sk_c6,multiply(sk_c7,Z_192)) = Z_192 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17623]) ).
tff(c_17759,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_17749,c_17650]) ).
tff(c_17717,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_8,c_17696]) ).
tff(c_17766,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_17759,c_17717]) ).
tff(c_17768,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17688,c_17766]) ).
tff(c_17769,plain,
inverse(sk_c7) = sk_c6,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_17774,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_17769,c_4]) ).
tff(c_17770,plain,
multiply(sk_c2,sk_c8) != sk_c3,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_48104,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_17770,c_56]) ).
tff(c_17788,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_17770,c_54]) ).
tff(c_17792,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_17788,c_4]) ).
tff(c_48121,plain,
! [X_397,Y_398,Z_399] : ( multiply(multiply(X_397,Y_398),Z_399) = multiply(X_397,multiply(Y_398,Z_399)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_48145,plain,
! [Z_399] : ( multiply(sk_c7,multiply(sk_c5,Z_399)) = multiply(identity,Z_399) ),
inference(superposition,[status(thm),theory(equality)],[c_17792,c_48121]) ).
tff(c_48204,plain,
! [Z_402] : ( multiply(sk_c7,multiply(sk_c5,Z_402)) = Z_402 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48145]) ).
tff(c_48216,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_48104,c_48204]) ).
tff(c_48148,plain,
! [Z_399] : ( multiply(sk_c6,multiply(sk_c7,Z_399)) = multiply(identity,Z_399) ),
inference(superposition,[status(thm),theory(equality)],[c_17774,c_48121]) ).
tff(c_48266,plain,
! [Z_404] : ( multiply(sk_c6,multiply(sk_c7,Z_404)) = Z_404 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48148]) ).
tff(c_48281,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_48216,c_48266]) ).
tff(c_48299,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_8,c_48266]) ).
tff(c_48666,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_48281,c_48299]) ).
tff(c_36,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_17807,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_17097,c_36]) ).
tff(c_48678,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_48666,c_17807]) ).
tff(c_48686,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17774,c_48678]) ).
tff(c_48697,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_48686,c_48686,c_48216]) ).
tff(c_48705,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48697]) ).
tff(c_48296,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_105,c_48266]) ).
tff(c_48716,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_48705,c_48296]) ).
tff(c_48718,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48716]) ).
tff(c_17812,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_17835,plain,
! [X_196,Y_197,Z_198] : ( multiply(multiply(X_196,Y_197),Z_198) = multiply(X_196,multiply(Y_197,Z_198)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_17871,plain,
! [Z_198] : ( multiply(sk_c7,multiply(sk_c1,Z_198)) = multiply(identity,Z_198) ),
inference(superposition,[status(thm),theory(equality)],[c_105,c_17835]) ).
tff(c_17895,plain,
! [Z_199] : ( multiply(sk_c7,multiply(sk_c1,Z_199)) = Z_199 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17871]) ).
tff(c_17907,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_17812,c_17895]) ).
tff(c_17911,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_17907]) ).
tff(c_17924,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17911,c_8]) ).
tff(c_17877,plain,
! [X_2,Z_198] : ( multiply(inverse(X_2),multiply(X_2,Z_198)) = multiply(identity,Z_198) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17835]) ).
tff(c_17986,plain,
! [X_200,Z_201] : ( multiply(inverse(X_200),multiply(X_200,Z_201)) = Z_201 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17877]) ).
tff(c_18013,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_17924,c_17986]) ).
tff(c_18050,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_18013]) ).
tff(c_17096,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_18055,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18050,c_17096]) ).
tff(c_40,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_17822,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_17097,c_40]) ).
tff(c_17913,plain,
multiply(sk_c4,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_17911,c_17822]) ).
tff(c_18083,plain,
multiply(sk_c4,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18050,c_17913]) ).
tff(c_17893,plain,
! [X_2,Z_198] : ( multiply(inverse(X_2),multiply(X_2,Z_198)) = Z_198 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17877]) ).
tff(c_18087,plain,
multiply(inverse(sk_c4),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_18083,c_17893]) ).
tff(c_18093,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18055,c_18087]) ).
tff(c_18286,plain,
! [X_203,Z_204] : ( multiply(inverse(inverse(X_203)),Z_204) = multiply(X_203,Z_204) ),
inference(superposition,[status(thm),theory(equality)],[c_17986,c_17893]) ).
tff(c_18040,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17986]) ).
tff(c_18293,plain,
! [X_203] : ( multiply(X_203,identity) = X_203 ),
inference(superposition,[status(thm),theory(equality)],[c_18286,c_18040]) ).
tff(c_17943,plain,
! [X2_9,X1_8,X5_6,X3_7] :
( ( multiply(X2_9,sk_c6) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(sk_c6,sk_c8) != sk_c6 )
| ( inverse(sk_c6) != sk_c6 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c6 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17911,c_17911,c_17911,c_17911,c_17911,c_17911,c_17911,c_17911,c_72]) ).
tff(c_17944,plain,
inverse(sk_c6) != sk_c6,
inference(splitLeft,[status(thm)],[c_17943]) ).
tff(c_17920,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17911,c_17769]) ).
tff(c_17945,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17944,c_17920]) ).
tff(c_17946,plain,
! [X3_7,X5_6,X1_8,X2_9] :
( ( multiply(sk_c6,sk_c8) != sk_c6 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_17943]) ).
tff(c_25759,plain,
! [X3_7,X5_6,X1_8,X2_9] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( identity != X2_9 )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18093,c_18293,c_18093,c_18093,c_18050,c_18293,c_18093,c_18050,c_18293,c_18093,c_18050,c_2,c_18050,c_18050,c_18293,c_18093,c_18050,c_18093,c_18093,c_2,c_18093,c_18050,c_17946]) ).
tff(c_25761,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25759]) ).
tff(c_18099,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18093,c_18093,c_17920]) ).
tff(c_25763,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25761,c_18099]) ).
tff(c_25764,plain,
! [X1_8,X5_6,X3_7] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_25759]) ).
tff(c_48086,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25764]) ).
tff(c_48088,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48086,c_18099]) ).
tff(c_48089,plain,
! [X5_6,X1_8] :
( ( inverse(X5_6) != identity )
| ( identity != X5_6 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_25764]) ).
tff(c_48091,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_48089]) ).
tff(c_48093,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48091,c_18099]) ).
tff(c_48095,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_48089]) ).
tff(c_48097,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48095,c_18099]) ).
tff(c_48099,plain,
multiply(sk_c1,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_48676,plain,
multiply(sk_c1,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_48666,c_48099]) ).
tff(c_48834,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48718,c_48686,c_48686,c_48676]) ).
tff(c_48836,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_22,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_48866,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_48836,c_22]) ).
tff(c_48870,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_48866,c_4]) ).
tff(c_32,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_48890,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_48836,c_32]) ).
tff(c_48835,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_48840,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_48835,c_4]) ).
tff(c_48944,plain,
! [Z_414] : ( multiply(sk_c7,multiply(sk_c5,Z_414)) = multiply(identity,Z_414) ),
inference(superposition,[status(thm),theory(equality)],[c_48840,c_48914]) ).
tff(c_49137,plain,
! [Z_419] : ( multiply(sk_c7,multiply(sk_c5,Z_419)) = Z_419 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48944]) ).
tff(c_49152,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_48890,c_49137]) ).
tff(c_48938,plain,
! [Z_414] : ( multiply(sk_c6,multiply(sk_c7,Z_414)) = multiply(identity,Z_414) ),
inference(superposition,[status(thm),theory(equality)],[c_48870,c_48914]) ).
tff(c_48961,plain,
! [Z_414] : ( multiply(sk_c6,multiply(sk_c7,Z_414)) = Z_414 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48938]) ).
tff(c_49159,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_49152,c_48961]) ).
tff(c_48967,plain,
! [Z_415] : ( multiply(sk_c6,multiply(sk_c7,Z_415)) = Z_415 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48938]) ).
tff(c_48982,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_8,c_48967]) ).
tff(c_49166,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_49159,c_48982]) ).
tff(c_24,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_48879,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_48836,c_24]) ).
tff(c_49175,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_49166,c_48879]) ).
tff(c_49181,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_48870,c_49175]) ).
tff(c_49187,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49181,c_49166]) ).
tff(c_49189,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49181,c_49181,c_49152]) ).
tff(c_49198,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49189]) ).
tff(c_49194,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49181,c_48866]) ).
tff(c_49237,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49198,c_49194]) ).
tff(c_49247,plain,
! [X_420,Z_421] : ( multiply(inverse(X_420),multiply(X_420,Z_421)) = Z_421 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48950]) ).
tff(c_49345,plain,
! [X_422] : ( multiply(inverse(inverse(X_422)),identity) = X_422 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_49247]) ).
tff(c_49351,plain,
! [X_422] : ( multiply(inverse(inverse(inverse(X_422))),X_422) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_49345,c_48965]) ).
tff(c_49004,plain,
! [Z_416] : ( multiply(sk_c7,multiply(sk_c5,Z_416)) = Z_416 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48944]) ).
tff(c_49019,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_48890,c_49004]) ).
tff(c_49026,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_49019,c_48961]) ).
tff(c_49033,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_49026,c_48982]) ).
tff(c_49065,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_49033,c_48879]) ).
tff(c_49071,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_48870,c_49065]) ).
tff(c_49079,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49071,c_49071,c_49019]) ).
tff(c_49088,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49079]) ).
tff(c_48979,plain,
multiply(sk_c6,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_48840,c_48967]) ).
tff(c_49098,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_49088,c_48979]) ).
tff(c_49099,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49098]) ).
tff(c_49087,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49071,c_48835]) ).
tff(c_49124,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49099,c_49087]) ).
tff(c_49077,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49071,c_49033]) ).
tff(c_49002,plain,
! [X2_9,X1_8,X5_6,X3_7] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_48866,c_48879,c_72]) ).
tff(c_49003,plain,
! [X3_7] :
( ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_49002]) ).
tff(c_49109,plain,
! [X3_418] :
( ( inverse(X3_418) != identity )
| ( multiply(X3_418,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_49077,c_49071,c_49071,c_49003]) ).
tff(c_49123,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_49109]) ).
tff(c_49135,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49124,c_49123]) ).
tff(c_49136,plain,
! [X5_6,X1_8,X2_9] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( 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_49002]) ).
tff(c_49204,plain,
! [X5_6,X1_8,X2_9] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != identity )
| ( multiply(X1_8,identity) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X2_9,sk_c6) != identity )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_49181,c_49181,c_49181,c_49181,c_49136]) ).
tff(c_49205,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != identity )
| ( inverse(X2_9) != identity ) ),
inference(splitLeft,[status(thm)],[c_49204]) ).
tff(c_49404,plain,
! [X2_424] :
( ( multiply(X2_424,identity) != identity )
| ( inverse(X2_424) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_49198,c_49205]) ).
tff(c_49408,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_49351,c_49404]) ).
tff(c_49427,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49237,c_49237,c_49237,c_49237,c_49408]) ).
tff(c_49428,plain,
! [X1_8,X5_6] :
( ( multiply(X1_8,identity) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != identity ) ),
inference(splitRight,[status(thm)],[c_49204]) ).
tff(c_66943,plain,
! [X1_8,X5_6] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_49615,c_49187,c_2,c_49187,c_49187,c_49187,c_49615,c_49187,c_49428]) ).
tff(c_66945,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_66943]) ).
tff(c_49512,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49198,c_49194]) ).
tff(c_66947,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_66945,c_49512]) ).
tff(c_66949,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_66943]) ).
tff(c_66951,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_66949,c_49512]) ).
tff(c_66953,plain,
inverse(sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_58,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_138]) ).
tff(c_67915,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_66953,c_58]) ).
tff(c_67919,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_67915,c_4]) ).
tff(c_68,plain,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_67948,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_66953,c_68]) ).
tff(c_66952,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_64,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_67016,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_66953,c_64]) ).
tff(c_66977,plain,
inverse(sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_66953,c_58]) ).
tff(c_66981,plain,
multiply(sk_c6,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_66977,c_4]) ).
tff(c_66961,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_66965,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_66961,c_4]) ).
tff(c_67039,plain,
! [X_570,Y_571,Z_572] : ( multiply(multiply(X_570,Y_571),Z_572) = multiply(X_570,multiply(Y_571,Z_572)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_67066,plain,
! [Z_572] : ( multiply(sk_c6,multiply(sk_c7,Z_572)) = multiply(identity,Z_572) ),
inference(superposition,[status(thm),theory(equality)],[c_66981,c_67039]) ).
tff(c_67334,plain,
! [Z_577] : ( multiply(sk_c6,multiply(sk_c7,Z_577)) = Z_577 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67066]) ).
tff(c_67349,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_66965,c_67334]) ).
tff(c_66,plain,
( ( inverse(sk_c5) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_150]) ).
tff(c_66991,plain,
inverse(sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_66953,c_66]) ).
tff(c_66995,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_66991,c_4]) ).
tff(c_67346,plain,
multiply(sk_c6,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_66995,c_67334]) ).
tff(c_67693,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_67349,c_67346]) ).
tff(c_67004,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_66953,c_68]) ).
tff(c_67702,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_67693,c_67004]) ).
tff(c_67063,plain,
! [Z_572] : ( multiply(sk_c7,multiply(sk_c5,Z_572)) = multiply(identity,Z_572) ),
inference(superposition,[status(thm),theory(equality)],[c_66995,c_67039]) ).
tff(c_67086,plain,
! [Z_572] : ( multiply(sk_c7,multiply(sk_c5,Z_572)) = Z_572 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67063]) ).
tff(c_67719,plain,
! [Z_584] : ( multiply(sk_c7,multiply(sk_c1,Z_584)) = Z_584 ),
inference(demodulation,[status(thm),theory(equality)],[c_67693,c_67086]) ).
tff(c_67734,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_67702,c_67719]) ).
tff(c_67087,plain,
! [Z_572] : ( multiply(sk_c6,multiply(sk_c7,Z_572)) = Z_572 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67066]) ).
tff(c_67742,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_67734,c_67087]) ).
tff(c_67352,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_8,c_67334]) ).
tff(c_67749,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_67742,c_67352]) ).
tff(c_60,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_67022,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_66953,c_60]) ).
tff(c_67757,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_67749,c_67022]) ).
tff(c_67763,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66981,c_67757]) ).
tff(c_67803,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67763,c_67749]) ).
tff(c_66957,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_66952,c_4]) ).
tff(c_67072,plain,
! [Z_572] : ( multiply(sk_c8,multiply(sk_c4,Z_572)) = multiply(identity,Z_572) ),
inference(superposition,[status(thm),theory(equality)],[c_66957,c_67039]) ).
tff(c_67416,plain,
! [Z_579] : ( multiply(sk_c8,multiply(sk_c4,Z_579)) = Z_579 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67072]) ).
tff(c_67431,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_67016,c_67416]) ).
tff(c_67081,plain,
! [Z_572] : ( multiply(sk_c7,multiply(sk_c8,Z_572)) = multiply(sk_c6,Z_572) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_67039]) ).
tff(c_67438,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_67431,c_67081]) ).
tff(c_67444,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_67022,c_67438]) ).
tff(c_67449,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_67444,c_67087]) ).
tff(c_67455,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66981,c_67449]) ).
tff(c_67461,plain,
! [Z_572] : ( multiply(sk_c6,multiply(identity,Z_572)) = Z_572 ),
inference(demodulation,[status(thm),theory(equality)],[c_67455,c_67087]) ).
tff(c_67470,plain,
! [Z_572] : ( multiply(sk_c6,Z_572) = Z_572 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67461]) ).
tff(c_67611,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67470,c_67349]) ).
tff(c_67467,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67455,c_66961]) ).
tff(c_67639,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67611,c_67467]) ).
tff(c_67468,plain,
multiply(identity,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_67455,c_8]) ).
tff(c_67513,plain,
sk_c8 = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_67468,c_2]) ).
tff(c_67462,plain,
multiply(sk_c6,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67455,c_67022]) ).
tff(c_67539,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67513,c_67462]) ).
tff(c_67612,plain,
! [Z_583] : ( multiply(sk_c6,Z_583) = Z_583 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67461]) ).
tff(c_67634,plain,
sk_c6 = identity,
inference(superposition,[status(thm),theory(equality)],[c_67539,c_67612]) ).
tff(c_67176,plain,
! [Z_575] : ( multiply(sk_c8,multiply(sk_c4,Z_575)) = Z_575 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67072]) ).
tff(c_67191,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_67016,c_67176]) ).
tff(c_67198,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_67191,c_67081]) ).
tff(c_67204,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_67022,c_67198]) ).
tff(c_67234,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_67204,c_67087]) ).
tff(c_67241,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66981,c_67234]) ).
tff(c_67256,plain,
multiply(identity,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_67241,c_8]) ).
tff(c_67269,plain,
sk_c8 = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_67256,c_2]) ).
tff(c_67093,plain,
! [X2_9,X1_8,X5_6,X3_7] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_66977,c_67022,c_72]) ).
tff(c_67206,plain,
! [X3_576] :
( ( inverse(X3_576) != sk_c7 )
| ( multiply(X3_576,sk_c7) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_67093]) ).
tff(c_67213,plain,
inverse(sk_c4) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_67016,c_67206]) ).
tff(c_67226,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_66952,c_67213]) ).
tff(c_67244,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_67241,c_67226]) ).
tff(c_67276,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_67269,c_67244]) ).
tff(c_67253,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_67241,c_66977]) ).
tff(c_67292,plain,
multiply(sk_c6,identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_67253,c_4]) ).
tff(c_67095,plain,
! [Z_573] : ( multiply(sk_c6,multiply(sk_c7,Z_573)) = Z_573 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67066]) ).
tff(c_67110,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_66965,c_67095]) ).
tff(c_67311,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67292,c_67110]) ).
tff(c_67255,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67241,c_66961]) ).
tff(c_67320,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67311,c_67255]) ).
tff(c_67330,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67320,c_67253]) ).
tff(c_67332,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_67276,c_67330]) ).
tff(c_67333,plain,
! [X5_6,X1_8,X2_9] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( 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_67093]) ).
tff(c_67364,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_67333]) ).
tff(c_67476,plain,
! [X2_580] :
( ( multiply(X2_580,sk_c6) != identity )
| ( inverse(X2_580) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_67455,c_67455,c_67364]) ).
tff(c_67492,plain,
inverse(inverse(sk_c6)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_67476]) ).
tff(c_67684,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_67639,c_67639,c_67634,c_67492]) ).
tff(c_67685,plain,
! [X1_8,X5_6] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_67333]) ).
tff(c_67738,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_67685]) ).
tff(c_67838,plain,
! [X5_586] :
( ( inverse(X5_586) != identity )
| ( multiply(X5_586,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_67803,c_2,c_67803,c_67763,c_67803,c_67738]) ).
tff(c_67852,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_67838]) ).
tff(c_67805,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_67763,c_67763,c_67734]) ).
tff(c_67813,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67805]) ).
tff(c_67809,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_67763,c_66977]) ).
tff(c_67866,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67813,c_67809]) ).
tff(c_67867,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_67852,c_67866]) ).
tff(c_67879,plain,
! [X1_587] :
( ( multiply(X1_587,sk_c7) != sk_c8 )
| ( inverse(X1_587) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_67685]) ).
tff(c_67889,plain,
inverse(sk_c4) != sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_67016,c_67879]) ).
tff(c_67905,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_66952,c_67889]) ).
tff(c_67906,plain,
inverse(sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_67911,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_67906,c_4]) ).
tff(c_67980,plain,
! [X_588,Y_589,Z_590] : ( multiply(multiply(X_588,Y_589),Z_590) = multiply(X_588,multiply(Y_589,Z_590)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_68004,plain,
! [Z_590] : ( multiply(sk_c7,multiply(sk_c5,Z_590)) = multiply(identity,Z_590) ),
inference(superposition,[status(thm),theory(equality)],[c_67911,c_67980]) ).
tff(c_68029,plain,
! [Z_591] : ( multiply(sk_c7,multiply(sk_c5,Z_591)) = Z_591 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68004]) ).
tff(c_68041,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_67948,c_68029]) ).
tff(c_68007,plain,
! [Z_590] : ( multiply(sk_c6,multiply(sk_c7,Z_590)) = multiply(identity,Z_590) ),
inference(superposition,[status(thm),theory(equality)],[c_67919,c_67980]) ).
tff(c_68052,plain,
! [Z_592] : ( multiply(sk_c6,multiply(sk_c7,Z_592)) = Z_592 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68007]) ).
tff(c_68064,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_68041,c_68052]) ).
tff(c_68073,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_8,c_68052]) ).
tff(c_68218,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_68064,c_68073]) ).
tff(c_67941,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_66953,c_60]) ).
tff(c_68319,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_68218,c_67941]) ).
tff(c_68324,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67919,c_68319]) ).
tff(c_68330,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68324,c_68218]) ).
tff(c_68001,plain,
! [Z_590] : ( multiply(sk_c6,multiply(sk_c8,Z_590)) = multiply(sk_c7,Z_590) ),
inference(superposition,[status(thm),theory(equality)],[c_67941,c_67980]) ).
tff(c_68351,plain,
! [Z_590] : ( multiply(sk_c6,Z_590) = Z_590 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68330,c_2,c_68324,c_68001]) ).
tff(c_68070,plain,
multiply(sk_c6,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_67911,c_68052]) ).
tff(c_68352,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68351,c_68070]) ).
tff(c_68340,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68324,c_67906]) ).
tff(c_68384,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68352,c_68340]) ).
tff(c_68013,plain,
! [X_2,Z_590] : ( multiply(inverse(X_2),multiply(X_2,Z_590)) = multiply(identity,Z_590) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_67980]) ).
tff(c_68576,plain,
! [X_603,Z_604] : ( multiply(inverse(X_603),multiply(X_603,Z_604)) = Z_604 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68013]) ).
tff(c_68612,plain,
! [X_605] : ( multiply(inverse(inverse(X_605)),identity) = X_605 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_68576]) ).
tff(c_68027,plain,
! [X_2,Z_590] : ( multiply(inverse(X_2),multiply(X_2,Z_590)) = Z_590 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68013]) ).
tff(c_68618,plain,
! [X_605] : ( multiply(inverse(inverse(inverse(X_605))),X_605) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_68612,c_68027]) ).
tff(c_68434,plain,
! [X_598,Z_599] : ( multiply(inverse(X_598),multiply(X_598,Z_599)) = Z_599 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68013]) ).
tff(c_68470,plain,
! [X_600] : ( multiply(inverse(inverse(X_600)),identity) = X_600 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_68434]) ).
tff(c_68476,plain,
! [X_600] : ( multiply(inverse(inverse(inverse(X_600))),X_600) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_68470,c_68027]) ).
tff(c_68228,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_68218,c_67941]) ).
tff(c_68233,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67919,c_68228]) ).
tff(c_68242,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_68233,c_68233,c_68041]) ).
tff(c_68251,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68242]) ).
tff(c_68247,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_68233,c_67915]) ).
tff(c_68289,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68251,c_68247]) ).
tff(c_68095,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_68064,c_68073]) ).
tff(c_68104,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_68095,c_67941]) ).
tff(c_68109,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67919,c_68104]) ).
tff(c_68149,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68109,c_68095]) ).
tff(c_68086,plain,
! [X2_9,X1_8,X5_6,X3_7] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_67915,c_67941,c_72]) ).
tff(c_68087,plain,
! [X3_7] :
( ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_68086]) ).
tff(c_68181,plain,
! [X3_594] :
( ( inverse(X3_594) != identity )
| ( multiply(X3_594,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_68149,c_68109,c_68109,c_68087]) ).
tff(c_68195,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_68181]) ).
tff(c_68151,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_68109,c_68109,c_68041]) ).
tff(c_68160,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68151]) ).
tff(c_68156,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_68109,c_67915]) ).
tff(c_68208,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68160,c_68156]) ).
tff(c_68209,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_68195,c_68208]) ).
tff(c_68210,plain,
! [X5_6,X1_8,X2_9] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( 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_68086]) ).
tff(c_68226,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_68210]) ).
tff(c_68300,plain,
! [X2_596] :
( ( multiply(X2_596,identity) != identity )
| ( inverse(X2_596) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_68233,c_68251,c_68233,c_68226]) ).
tff(c_68308,plain,
inverse(inverse(identity)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_68300]) ).
tff(c_68316,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_68289,c_68289,c_68308]) ).
tff(c_68317,plain,
! [X1_8,X5_6] :
( ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X1_8) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_68210]) ).
tff(c_68393,plain,
! [X1_8,X5_6] :
( ( multiply(X1_8,identity) != identity )
| ( inverse(X1_8) != identity )
| ( inverse(X5_6) != identity )
| ( multiply(X5_6,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_68330,c_2,c_68330,c_68324,c_68330,c_68330,c_68330,c_68324,c_68317]) ).
tff(c_68525,plain,
! [X5_602] :
( ( inverse(X5_602) != identity )
| ( multiply(X5_602,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_68393]) ).
tff(c_68529,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_68476,c_68525]) ).
tff(c_68548,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_68384,c_68384,c_68384,c_68384,c_68529]) ).
tff(c_68670,plain,
! [X1_607] :
( ( multiply(X1_607,identity) != identity )
| ( inverse(X1_607) != identity ) ),
inference(splitRight,[status(thm)],[c_68393]) ).
tff(c_68674,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_68618,c_68670]) ).
tff(c_68693,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_68384,c_68384,c_68384,c_68384,c_68674]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP327-1 : TPTP v9.0.0. Released v2.5.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.35 % Computer : n023.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Mon Apr 7 21:42:25 EDT 2025
% 0.12/0.35 % CPUTime :
% 22.36/10.29 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.60/10.37
% 22.60/10.37 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------