%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP284-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:25:48 PM UTC 2025
% Result : Unsatisfiable 12.70s 4.17s
% Output : CNFRefutation 13.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 27
% Syntax : Number of formulae : 523 ( 437 unt; 0 typ; 0 def)
% Number of atoms : 719 ( 694 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 428 ( 232 ~; 196 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 245 ( 245 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > 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(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_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c7,sk_c6) != sk_c5 )
| ( multiply(X3,sk_c7) != sk_c6 )
| ( inverse(X3) != sk_c7 )
| ( multiply(X4,sk_c7) != sk_c5 )
| ( inverse(X4) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( inverse(X2) != sk_c6 )
| ( multiply(X2,sk_c5) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c5 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
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_14451,plain,
! [X_228,Y_229,Z_230] : ( multiply(multiply(X_228,Y_229),Z_230) = multiply(X_228,multiply(Y_229,Z_230)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14484,plain,
! [X_2,Z_230] : ( multiply(inverse(X_2),multiply(X_2,Z_230)) = multiply(identity,Z_230) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14451]) ).
tff(c_14495,plain,
! [X_2,Z_230] : ( multiply(inverse(X_2),multiply(X_2,Z_230)) = Z_230 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14484]) ).
tff(c_14873,plain,
! [X_240,Z_241] : ( multiply(inverse(X_240),multiply(X_240,Z_241)) = Z_241 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14484]) ).
tff(c_15909,plain,
! [X_257,Z_258] : ( multiply(inverse(inverse(X_257)),Z_258) = multiply(X_257,Z_258) ),
inference(superposition,[status(thm),theory(equality)],[c_14495,c_14873]) ).
tff(c_14939,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14873]) ).
tff(c_15916,plain,
! [X_257] : ( multiply(X_257,identity) = X_257 ),
inference(superposition,[status(thm),theory(equality)],[c_15909,c_14939]) ).
tff(c_15578,plain,
! [X_250,Z_251] : ( multiply(inverse(inverse(X_250)),Z_251) = multiply(X_250,Z_251) ),
inference(superposition,[status(thm),theory(equality)],[c_14873,c_14495]) ).
tff(c_15589,plain,
! [X_250] : ( multiply(X_250,identity) = X_250 ),
inference(superposition,[status(thm),theory(equality)],[c_15578,c_14939]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_20,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_10798,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_30,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_87,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_91,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_87,c_4]) ).
tff(c_10840,plain,
! [X_152,Y_153,Z_154] : ( multiply(multiply(X_152,Y_153),Z_154) = multiply(X_152,multiply(Y_153,Z_154)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_10876,plain,
! [Z_154] : ( multiply(sk_c7,multiply(sk_c1,Z_154)) = multiply(identity,Z_154) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_10840]) ).
tff(c_10896,plain,
! [Z_155] : ( multiply(sk_c7,multiply(sk_c1,Z_155)) = Z_155 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10876]) ).
tff(c_10908,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10798,c_10896]) ).
tff(c_10912,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_10908]) ).
tff(c_10920,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10912,c_102]) ).
tff(c_10882,plain,
! [X_2,Z_154] : ( multiply(inverse(X_2),multiply(X_2,Z_154)) = multiply(identity,Z_154) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_10840]) ).
tff(c_10994,plain,
! [X_156,Z_157] : ( multiply(inverse(X_156),multiply(X_156,Z_157)) = Z_157 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10882]) ).
tff(c_11012,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_10920,c_10994]) ).
tff(c_11049,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11012]) ).
tff(c_44,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c2,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_107,plain,
multiply(sk_c2,sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_50,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_75,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_79,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_75,c_4]) ).
tff(c_9453,plain,
! [X_130,Y_131,Z_132] : ( multiply(multiply(X_130,Y_131),Z_132) = multiply(X_130,multiply(Y_131,Z_132)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9492,plain,
! [Z_132] : ( multiply(sk_c7,multiply(sk_c2,Z_132)) = multiply(identity,Z_132) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_9453]) ).
tff(c_9522,plain,
! [Z_134] : ( multiply(sk_c7,multiply(sk_c2,Z_134)) = Z_134 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9492]) ).
tff(c_9534,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_107,c_9522]) ).
tff(c_10230,plain,
! [Z_145] : ( multiply(sk_c2,multiply(sk_c7,Z_145)) = multiply(sk_c5,Z_145) ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_9453]) ).
tff(c_10245,plain,
multiply(sk_c5,sk_c5) = multiply(sk_c2,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_9534,c_10230]) ).
tff(c_10267,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_107,c_10245]) ).
tff(c_10257,plain,
multiply(sk_c5,sk_c6) = multiply(sk_c2,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_102,c_10230]) ).
tff(c_134,plain,
! [X_12,Y_13,Z_14] : ( multiply(multiply(X_12,Y_13),Z_14) = multiply(X_12,multiply(Y_13,Z_14)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_164,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_134]) ).
tff(c_1122,plain,
! [X_35,Z_36] : ( multiply(inverse(X_35),multiply(X_35,Z_36)) = Z_36 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_174,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_1351,plain,
! [X_39,Z_40] : ( multiply(inverse(inverse(X_39)),Z_40) = multiply(X_39,Z_40) ),
inference(superposition,[status(thm),theory(equality)],[c_1122,c_174]) ).
tff(c_1158,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1122]) ).
tff(c_1358,plain,
! [X_39] : ( multiply(X_39,identity) = X_39 ),
inference(superposition,[status(thm),theory(equality)],[c_1351,c_1158]) ).
tff(c_113,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_158,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_134]) ).
tff(c_412,plain,
! [Z_21] : ( multiply(sk_c7,multiply(sk_c1,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_424,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_113,c_412]) ).
tff(c_428,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_424]) ).
tff(c_161,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_134]) ).
tff(c_389,plain,
! [Z_20] : ( multiply(sk_c7,multiply(sk_c2,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_401,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_107,c_389]) ).
tff(c_466,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_428,c_428,c_401]) ).
tff(c_1199,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_466,c_174]) ).
tff(c_1205,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1199]) ).
tff(c_471,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_428,c_102]) ).
tff(c_1143,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_471,c_1122]) ).
tff(c_1165,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1143]) ).
tff(c_559,plain,
! [X_23,Z_24] : ( multiply(inverse(X_23),multiply(X_23,Z_24)) = Z_24 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_595,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_471,c_559]) ).
tff(c_620,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_595]) ).
tff(c_848,plain,
! [X_28,Z_29] : ( multiply(inverse(inverse(X_28)),Z_29) = multiply(X_28,Z_29) ),
inference(superposition,[status(thm),theory(equality)],[c_559,c_174]) ).
tff(c_610,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_559]) ).
tff(c_855,plain,
! [X_28] : ( multiply(X_28,identity) = X_28 ),
inference(superposition,[status(thm),theory(equality)],[c_848,c_610]) ).
tff(c_583,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_466,c_559]) ).
tff(c_618,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_583]) ).
tff(c_179,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_191,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_107,c_179]) ).
tff(c_202,plain,
! [Z_16] : ( multiply(sk_c2,multiply(sk_c7,Z_16)) = multiply(sk_c5,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_134]) ).
tff(c_217,plain,
multiply(sk_c5,sk_c5) = multiply(sk_c2,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_191,c_202]) ).
tff(c_233,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_107,c_217]) ).
tff(c_292,plain,
! [X_18,Z_19] : ( multiply(inverse(X_18),multiply(X_18,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_316,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_233,c_292]) ).
tff(c_329,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_316]) ).
tff(c_241,plain,
! [Z_17] : ( multiply(sk_c7,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_256,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_113,c_241]) ).
tff(c_260,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_256]) ).
tff(c_270,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_260,c_87]) ).
tff(c_281,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_270,c_4]) ).
tff(c_353,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_329,c_281]) ).
tff(c_266,plain,
multiply(sk_c1,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_260,c_113]) ).
tff(c_372,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_353,c_329,c_266]) ).
tff(c_58,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_177,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_58]) ).
tff(c_178,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_177]) ).
tff(c_265,plain,
multiply(sk_c6,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_260,c_178]) ).
tff(c_379,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_372,c_329,c_329,c_265]) ).
tff(c_380,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_508,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_428,c_428,c_428,c_428,c_428,c_428,c_380]) ).
tff(c_509,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_508]) ).
tff(c_1110,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_620,c_855,c_618,c_620,c_509]) ).
tff(c_472,plain,
multiply(sk_c5,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_428,c_91]) ).
tff(c_633,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_618,c_472]) ).
tff(c_740,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_633,c_174]) ).
tff(c_752,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_740]) ).
tff(c_473,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_428,c_87]) ).
tff(c_635,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_618,c_473]) ).
tff(c_757,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_752,c_635]) ).
tff(c_1112,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1110,c_757]) ).
tff(c_1113,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_508]) ).
tff(c_9386,plain,
! [X1_8,X4_7,X3_6] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X3_6) != identity )
| ( identity != X3_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1358,c_1205,c_1165,c_1205,c_1358,c_1205,c_1205,c_1205,c_1205,c_1358,c_1205,c_1165,c_1113]) ).
tff(c_9388,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9386]) ).
tff(c_475,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_428,c_75]) ).
tff(c_490,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_475,c_4]) ).
tff(c_1264,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1205,c_490]) ).
tff(c_1211,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1205,c_475]) ).
tff(c_1265,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1264,c_1211]) ).
tff(c_9390,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9388,c_1265]) ).
tff(c_9391,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_9386]) ).
tff(c_9393,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9391]) ).
tff(c_9395,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9393,c_1265]) ).
tff(c_9398,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_9391]) ).
tff(c_9400,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9398,c_1265]) ).
tff(c_9402,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_26,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_9433,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_9402,c_26]) ).
tff(c_24,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_9414,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_9402,c_24]) ).
tff(c_9418,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9414,c_4]) ).
tff(c_9477,plain,
! [Z_132] : ( multiply(sk_c6,multiply(sk_c4,Z_132)) = multiply(identity,Z_132) ),
inference(superposition,[status(thm),theory(equality)],[c_9418,c_9453]) ).
tff(c_10207,plain,
! [Z_144] : ( multiply(sk_c6,multiply(sk_c4,Z_144)) = Z_144 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9477]) ).
tff(c_10219,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9433,c_10207]) ).
tff(c_10481,plain,
! [Z_149] : ( multiply(sk_c7,multiply(sk_c6,Z_149)) = multiply(sk_c5,Z_149) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_9453]) ).
tff(c_10496,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_10219,c_10481]) ).
tff(c_10509,plain,
multiply(sk_c2,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_9534,c_10257,c_10496]) ).
tff(c_9506,plain,
! [Z_132] : ( multiply(sk_c7,multiply(sk_c2,Z_132)) = Z_132 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9492]) ).
tff(c_10515,plain,
multiply(sk_c7,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10509,c_9506]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_9440,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9402,c_22]) ).
tff(c_9401,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_9406,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9401,c_4]) ).
tff(c_9480,plain,
! [Z_132] : ( multiply(sk_c7,multiply(sk_c3,Z_132)) = multiply(identity,Z_132) ),
inference(superposition,[status(thm),theory(equality)],[c_9406,c_9453]) ).
tff(c_10299,plain,
! [Z_146] : ( multiply(sk_c7,multiply(sk_c3,Z_146)) = Z_146 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9480]) ).
tff(c_10314,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9440,c_10299]) ).
tff(c_10548,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10515,c_10314]) ).
tff(c_10511,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10509,c_10257]) ).
tff(c_10672,plain,
multiply(sk_c5,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10548,c_10511]) ).
tff(c_10684,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10267,c_10672]) ).
tff(c_10700,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10684,c_9401]) ).
tff(c_10678,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10548,c_9440]) ).
tff(c_10749,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10684,c_10678]) ).
tff(c_10561,plain,
multiply(sk_c5,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10548,c_10511]) ).
tff(c_10573,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10267,c_10561]) ).
tff(c_10589,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10573,c_9401]) ).
tff(c_10567,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10548,c_9440]) ).
tff(c_10638,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10573,c_10567]) ).
tff(c_18,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_9445,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_9402,c_18]) ).
tff(c_9546,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_9445,c_58]) ).
tff(c_9669,plain,
! [X3_138] :
( ( inverse(X3_138) != sk_c7 )
| ( multiply(X3_138,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_9546]) ).
tff(c_9682,plain,
( ( inverse(sk_c2) != sk_c7 )
| ( sk_c6 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_9669]) ).
tff(c_9693,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_9682]) ).
tff(c_9548,plain,
! [Z_135] : ( multiply(sk_c6,multiply(sk_c4,Z_135)) = Z_135 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9477]) ).
tff(c_9560,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9433,c_9548]) ).
tff(c_9495,plain,
! [X_2,Z_132] : ( multiply(inverse(X_2),multiply(X_2,Z_132)) = multiply(identity,Z_132) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9453]) ).
tff(c_9715,plain,
! [X_139,Z_140] : ( multiply(inverse(X_139),multiply(X_139,Z_140)) = Z_140 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9495]) ).
tff(c_9766,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9534,c_9715]) ).
tff(c_9826,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_9766]) ).
tff(c_9843,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_9826,c_9534]) ).
tff(c_9587,plain,
! [Z_137] : ( multiply(sk_c2,multiply(sk_c7,Z_137)) = multiply(sk_c5,Z_137) ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_9453]) ).
tff(c_9623,plain,
multiply(sk_c5,sk_c2) = multiply(sk_c2,identity),
inference(superposition,[status(thm),theory(equality)],[c_79,c_9587]) ).
tff(c_9837,plain,
multiply(sk_c2,identity) = multiply(identity,sk_c2),
inference(demodulation,[status(thm),theory(equality)],[c_9826,c_9623]) ).
tff(c_9850,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9837]) ).
tff(c_9617,plain,
multiply(sk_c5,sk_c6) = multiply(sk_c2,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_102,c_9587]) ).
tff(c_9839,plain,
multiply(sk_c2,identity) = multiply(identity,sk_c6),
inference(demodulation,[status(thm),theory(equality)],[c_9826,c_9826,c_9617]) ).
tff(c_9852,plain,
multiply(sk_c2,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9839]) ).
tff(c_9959,plain,
sk_c6 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_9850,c_9852]) ).
tff(c_9968,plain,
inverse(sk_c4) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_9959,c_9414]) ).
tff(c_9982,plain,
multiply(sk_c2,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9968,c_4]) ).
tff(c_9507,plain,
! [X_2,Z_132] : ( multiply(inverse(X_2),multiply(X_2,Z_132)) = Z_132 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9495]) ).
tff(c_10006,plain,
multiply(inverse(sk_c2),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_9982,c_9507]) ).
tff(c_10015,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_9843,c_75,c_10006]) ).
tff(c_9620,plain,
multiply(sk_c5,sk_c1) = multiply(sk_c2,identity),
inference(superposition,[status(thm),theory(equality)],[c_91,c_9587]) ).
tff(c_9838,plain,
multiply(sk_c2,identity) = multiply(identity,sk_c1),
inference(demodulation,[status(thm),theory(equality)],[c_9826,c_9620]) ).
tff(c_9851,plain,
multiply(sk_c2,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9838]) ).
tff(c_9986,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9851,c_9850]) ).
tff(c_9690,plain,
( ( inverse(identity) != sk_c7 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_9669]) ).
tff(c_9694,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_9690]) ).
tff(c_9962,plain,
sk_c7 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_9959,c_9694]) ).
tff(c_10021,plain,
sk_c7 != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9986,c_9962]) ).
tff(c_10039,plain,
sk_c4 != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_10015,c_10021]) ).
tff(c_10019,plain,
multiply(sk_c1,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9986,c_9851]) ).
tff(c_10020,plain,
inverse(sk_c4) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9986,c_9968]) ).
tff(c_10075,plain,
multiply(sk_c1,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10020,c_4]) ).
tff(c_10023,plain,
sk_c6 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9986,c_9959]) ).
tff(c_9474,plain,
! [Z_132] : ( multiply(sk_c4,multiply(sk_c5,Z_132)) = multiply(sk_c6,Z_132) ),
inference(superposition,[status(thm),theory(equality)],[c_9433,c_9453]) ).
tff(c_10052,plain,
! [Z_132] : ( multiply(sk_c4,Z_132) = multiply(sk_c1,Z_132) ),
inference(demodulation,[status(thm),theory(equality)],[c_10023,c_2,c_9826,c_9474]) ).
tff(c_9468,plain,
! [Z_132] : ( multiply(sk_c6,multiply(sk_c7,Z_132)) = multiply(sk_c5,Z_132) ),
inference(superposition,[status(thm),theory(equality)],[c_9445,c_9453]) ).
tff(c_10148,plain,
! [Z_143] : ( multiply(sk_c1,multiply(sk_c1,Z_143)) = Z_143 ),
inference(demodulation,[status(thm),theory(equality)],[c_10052,c_10015,c_10023,c_2,c_9826,c_9468]) ).
tff(c_10172,plain,
multiply(sk_c1,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_10075,c_10148]) ).
tff(c_10179,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_10019,c_10172]) ).
tff(c_10181,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10039,c_10179]) ).
tff(c_10183,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_9690]) ).
tff(c_9571,plain,
! [Z_136] : ( multiply(sk_c7,multiply(sk_c3,Z_136)) = Z_136 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9480]) ).
tff(c_9583,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9440,c_9571]) ).
tff(c_10186,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10183,c_10183,c_9583]) ).
tff(c_10203,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9560,c_10186]) ).
tff(c_10205,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9693,c_10203]) ).
tff(c_10206,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_9546]) ).
tff(c_10424,plain,
! [X2_148] :
( ( multiply(X2_148,sk_c5) != sk_c6 )
| ( inverse(X2_148) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_10206]) ).
tff(c_10440,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9433,c_10424]) ).
tff(c_10453,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9414,c_10440]) ).
tff(c_10454,plain,
! [X1_8,X4_7] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_10206]) ).
tff(c_10560,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_10454]) ).
tff(c_10648,plain,
! [X4_150] :
( ( inverse(X4_150) != sk_c5 )
| ( multiply(X4_150,sk_c5) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10573,c_10573,c_10560]) ).
tff(c_10651,plain,
inverse(sk_c3) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10638,c_10648]) ).
tff(c_10670,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10589,c_10651]) ).
tff(c_10671,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_10454]) ).
tff(c_10759,plain,
! [X1_151] :
( ( multiply(X1_151,sk_c5) != sk_c5 )
| ( inverse(X1_151) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10684,c_10684,c_10548,c_10671]) ).
tff(c_10762,plain,
inverse(sk_c3) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10749,c_10759]) ).
tff(c_10781,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10700,c_10762]) ).
tff(c_10782,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_10783,plain,
multiply(sk_c2,sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_10834,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10783,c_46]) ).
tff(c_11033,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10834,c_10994]) ).
tff(c_11051,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10782,c_11033]) ).
tff(c_11071,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11049,c_2,c_11049,c_11051]) ).
tff(c_10923,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10912,c_79]) ).
tff(c_11123,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11071,c_10923]) ).
tff(c_10919,plain,
multiply(sk_c2,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10912,c_10783]) ).
tff(c_11133,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11123,c_11071,c_11071,c_10919]) ).
tff(c_11135,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_11170,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_11135,c_26]) ).
tff(c_10787,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10782,c_4]) ).
tff(c_11177,plain,
! [X_158,Y_159,Z_160] : ( multiply(multiply(X_158,Y_159),Z_160) = multiply(X_158,multiply(Y_159,Z_160)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11204,plain,
! [Z_160] : ( multiply(sk_c6,multiply(sk_c4,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_10787,c_11177]) ).
tff(c_11948,plain,
! [Z_178] : ( multiply(sk_c6,multiply(sk_c4,Z_178)) = Z_178 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11204]) ).
tff(c_11960,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11170,c_11948]) ).
tff(c_11216,plain,
! [X_2,Z_160] : ( multiply(inverse(X_2),multiply(X_2,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11177]) ).
tff(c_11228,plain,
! [X_2,Z_160] : ( multiply(inverse(X_2),multiply(X_2,Z_160)) = Z_160 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11216]) ).
tff(c_11971,plain,
! [Z_179] : ( multiply(sk_c7,multiply(sk_c6,Z_179)) = multiply(sk_c5,Z_179) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_11177]) ).
tff(c_11983,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_11960,c_11971]) ).
tff(c_38,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c2,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_11160,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_10783,c_38]) ).
tff(c_11989,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_11160,c_11971]) ).
tff(c_12012,plain,
multiply(sk_c5,sk_c7) = multiply(sk_c5,sk_c6),
inference(demodulation,[status(thm),theory(equality)],[c_11983,c_11989]) ).
tff(c_12029,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_11216]) ).
tff(c_12047,plain,
multiply(inverse(sk_c5),multiply(sk_c5,sk_c6)) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_12012,c_12029]) ).
tff(c_12123,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11228,c_12047]) ).
tff(c_42,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_11153,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_10783,c_42]) ).
tff(c_11134,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_11139,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11134,c_4]) ).
tff(c_11201,plain,
! [Z_160] : ( multiply(sk_c7,multiply(sk_c3,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_11139,c_11177]) ).
tff(c_11256,plain,
! [Z_163] : ( multiply(sk_c7,multiply(sk_c3,Z_163)) = Z_163 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11201]) ).
tff(c_11268,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11153,c_11256]) ).
tff(c_12291,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12123,c_12123,c_11268]) ).
tff(c_12306,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11960,c_12291]) ).
tff(c_12314,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12306,c_12306,c_11960]) ).
tff(c_12469,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_12314,c_11228]) ).
tff(c_12475,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12469]) ).
tff(c_12305,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12123,c_75]) ).
tff(c_12384,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12306,c_12305]) ).
tff(c_12391,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12384,c_4]) ).
tff(c_12551,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12475,c_12391]) ).
tff(c_12489,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12475,c_12306]) ).
tff(c_12300,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12123,c_10783]) ).
tff(c_12579,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12551,c_12489,c_12475,c_12300]) ).
tff(c_12581,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_14002,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12581,c_16]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_13570,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12581,c_14]) ).
tff(c_13574,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13570,c_4]) ).
tff(c_14019,plain,
! [X_217,Y_218,Z_219] : ( multiply(multiply(X_217,Y_218),Z_219) = multiply(X_217,multiply(Y_218,Z_219)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14043,plain,
! [Z_219] : ( multiply(sk_c6,multiply(sk_c4,Z_219)) = multiply(identity,Z_219) ),
inference(superposition,[status(thm),theory(equality)],[c_13574,c_14019]) ).
tff(c_14097,plain,
! [Z_222] : ( multiply(sk_c6,multiply(sk_c4,Z_222)) = Z_222 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14043]) ).
tff(c_14109,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_14002,c_14097]) ).
tff(c_13606,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12581,c_16]) ).
tff(c_13624,plain,
! [X_207,Y_208,Z_209] : ( multiply(multiply(X_207,Y_208),Z_209) = multiply(X_207,multiply(Y_208,Z_209)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13651,plain,
! [Z_209] : ( multiply(sk_c6,multiply(sk_c4,Z_209)) = multiply(identity,Z_209) ),
inference(superposition,[status(thm),theory(equality)],[c_13574,c_13624]) ).
tff(c_13759,plain,
! [Z_213] : ( multiply(sk_c6,multiply(sk_c4,Z_213)) = Z_213 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13651]) ).
tff(c_13771,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_13606,c_13759]) ).
tff(c_13596,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_13657,plain,
! [Z_209] : ( multiply(sk_c7,multiply(sk_c1,Z_209)) = multiply(identity,Z_209) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_13624]) ).
tff(c_13677,plain,
! [Z_210] : ( multiply(sk_c7,multiply(sk_c1,Z_210)) = Z_210 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13657]) ).
tff(c_13689,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13596,c_13677]) ).
tff(c_13717,plain,
! [Z_212] : ( multiply(sk_c1,multiply(sk_c7,Z_212)) = multiply(sk_c6,Z_212) ),
inference(superposition,[status(thm),theory(equality)],[c_13596,c_13624]) ).
tff(c_13735,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c1,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_13689,c_13717]) ).
tff(c_13751,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13596,c_13735]) ).
tff(c_13775,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_13771,c_13751]) ).
tff(c_13786,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13775,c_13689]) ).
tff(c_13663,plain,
! [X_2,Z_209] : ( multiply(inverse(X_2),multiply(X_2,Z_209)) = multiply(identity,Z_209) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13624]) ).
tff(c_13675,plain,
! [X_2,Z_209] : ( multiply(inverse(X_2),multiply(X_2,Z_209)) = Z_209 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13663]) ).
tff(c_13864,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_13786,c_13675]) ).
tff(c_13870,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13864]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_13601,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_12581,c_8]) ).
tff(c_13702,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( sk_c7 != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13689,c_13601,c_58]) ).
tff(c_13703,plain,
sk_c7 != sk_c5,
inference(splitLeft,[status(thm)],[c_13702]) ).
tff(c_13875,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_13870,c_13703]) ).
tff(c_13789,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_13775,c_13601]) ).
tff(c_13936,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13870,c_2,c_13870,c_13789]) ).
tff(c_13937,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13875,c_13936]) ).
tff(c_13939,plain,
sk_c7 = sk_c5,
inference(splitRight,[status(thm)],[c_13702]) ).
tff(c_13693,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_13689,c_12581]) ).
tff(c_13990,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_13939,c_13693]) ).
tff(c_13991,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_12580,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_12585,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12580,c_4]) ).
tff(c_14046,plain,
! [Z_219] : ( multiply(sk_c7,multiply(sk_c3,Z_219)) = multiply(identity,Z_219) ),
inference(superposition,[status(thm),theory(equality)],[c_12585,c_14019]) ).
tff(c_14120,plain,
! [Z_223] : ( multiply(sk_c7,multiply(sk_c3,Z_223)) = Z_223 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14046]) ).
tff(c_14132,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_13991,c_14120]) ).
tff(c_13997,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_12581,c_8]) ).
tff(c_14037,plain,
! [Z_219] : ( multiply(sk_c6,multiply(sk_c7,Z_219)) = multiply(sk_c5,Z_219) ),
inference(superposition,[status(thm),theory(equality)],[c_13997,c_14019]) ).
tff(c_14170,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_14132,c_14037]) ).
tff(c_14176,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14109,c_14170]) ).
tff(c_14055,plain,
! [X_2,Z_219] : ( multiply(inverse(X_2),multiply(X_2,Z_219)) = multiply(identity,Z_219) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14019]) ).
tff(c_14211,plain,
! [X_225,Z_226] : ( multiply(inverse(X_225),multiply(X_225,Z_226)) = Z_226 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14055]) ).
tff(c_14235,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14176,c_14211]) ).
tff(c_14303,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_14235]) ).
tff(c_14323,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14303,c_14303,c_14132]) ).
tff(c_14335,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14323]) ).
tff(c_14330,plain,
multiply(identity,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14303,c_12581]) ).
tff(c_14337,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14330]) ).
tff(c_14390,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_14335,c_14337]) ).
tff(c_14343,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14335,c_14335,c_14109]) ).
tff(c_14349,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14343]) ).
tff(c_14391,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14390,c_14349]) ).
tff(c_14393,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_14437,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_14393,c_36]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_14405,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_14393,c_34]) ).
tff(c_14409,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14405,c_4]) ).
tff(c_14475,plain,
! [Z_230] : ( multiply(sk_c6,multiply(sk_c4,Z_230)) = multiply(identity,Z_230) ),
inference(superposition,[status(thm),theory(equality)],[c_14409,c_14451]) ).
tff(c_14497,plain,
! [Z_231] : ( multiply(sk_c6,multiply(sk_c4,Z_231)) = Z_231 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14475]) ).
tff(c_14509,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_14437,c_14497]) ).
tff(c_14903,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_14509,c_14873]) ).
tff(c_28,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_14418,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_14393,c_28]) ).
tff(c_14918,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14418,c_14873]) ).
tff(c_15275,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14903,c_14918]) ).
tff(c_32,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_14432,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14393,c_32]) ).
tff(c_14392,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_14397,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14392,c_4]) ).
tff(c_14478,plain,
! [Z_230] : ( multiply(sk_c7,multiply(sk_c3,Z_230)) = multiply(identity,Z_230) ),
inference(superposition,[status(thm),theory(equality)],[c_14397,c_14451]) ).
tff(c_14520,plain,
! [Z_232] : ( multiply(sk_c7,multiply(sk_c3,Z_232)) = Z_232 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14478]) ).
tff(c_14532,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_14432,c_14520]) ).
tff(c_14897,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14532,c_14873]) ).
tff(c_15410,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15275,c_15275,c_14897]) ).
tff(c_15421,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15410]) ).
tff(c_15430,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15421,c_15275]) ).
tff(c_15416,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15275,c_15275,c_14532]) ).
tff(c_15424,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14509,c_15416]) ).
tff(c_15444,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15421,c_15424]) ).
tff(c_14942,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_14873]) ).
tff(c_15287,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15275,c_15275,c_14897]) ).
tff(c_15298,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15287]) ).
tff(c_14921,plain,
multiply(inverse(sk_c6),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_14409,c_14873]) ).
tff(c_15309,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_15298,c_14921]) ).
tff(c_15315,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14942,c_15309]) ).
tff(c_15314,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15298,c_14405]) ).
tff(c_15354,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15315,c_15314]) ).
tff(c_15307,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15298,c_15275]) ).
tff(c_15085,plain,
! [Z_244] : ( multiply(sk_c6,multiply(sk_c7,Z_244)) = multiply(sk_c5,Z_244) ),
inference(superposition,[status(thm),theory(equality)],[c_14418,c_14451]) ).
tff(c_15106,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_14532,c_15085]) ).
tff(c_15113,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14509,c_15106]) ).
tff(c_15117,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_15113,c_14495]) ).
tff(c_15123,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15117]) ).
tff(c_14933,plain,
multiply(inverse(sk_c7),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_79,c_14873]) ).
tff(c_15129,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_15123,c_14933]) ).
tff(c_15139,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15129]) ).
tff(c_15137,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15123,c_75]) ).
tff(c_15238,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15139,c_15137]) ).
tff(c_15133,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15123,c_15123,c_14532]) ).
tff(c_15141,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15133]) ).
tff(c_14754,plain,
! [Z_238] : ( multiply(sk_c6,multiply(sk_c7,Z_238)) = multiply(sk_c5,Z_238) ),
inference(superposition,[status(thm),theory(equality)],[c_14418,c_14451]) ).
tff(c_14772,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_14532,c_14754]) ).
tff(c_14779,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14509,c_14772]) ).
tff(c_14783,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14779,c_14495]) ).
tff(c_14789,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_14783]) ).
tff(c_14798,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14789,c_14789,c_14532]) ).
tff(c_14806,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14798]) ).
tff(c_14838,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14806,c_14806,c_14509]) ).
tff(c_14845,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14838]) ).
tff(c_14557,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14418,c_58]) ).
tff(c_14558,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_14557]) ).
tff(c_14796,plain,
multiply(identity,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14789,c_14558]) ).
tff(c_14805,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14796]) ).
tff(c_14863,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14845,c_14806,c_14805]) ).
tff(c_14865,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_14557]) ).
tff(c_14891,plain,
multiply(inverse(sk_c7),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_14865,c_14873]) ).
tff(c_15130,plain,
multiply(inverse(identity),sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15123,c_14891]) ).
tff(c_15140,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14942,c_15130]) ).
tff(c_15161,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15141,c_15140]) ).
tff(c_14864,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_14557]) ).
tff(c_15081,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_14864]) ).
tff(c_15167,plain,
! [X2_245] :
( ( multiply(X2_245,sk_c5) != identity )
| ( inverse(X2_245) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15141,c_15141,c_15081]) ).
tff(c_15184,plain,
inverse(inverse(sk_c5)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_15167]) ).
tff(c_15260,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_15238,c_15238,c_15161,c_15184]) ).
tff(c_15261,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_14864]) ).
tff(c_15286,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_15261]) ).
tff(c_15389,plain,
! [X3_247] :
( ( inverse(X3_247) != identity )
| ( multiply(X3_247,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15307,c_15298,c_15307,c_15286]) ).
tff(c_15400,plain,
inverse(inverse(identity)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_15389]) ).
tff(c_15408,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_15354,c_15354,c_15400]) ).
tff(c_15409,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_15261]) ).
tff(c_15497,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( multiply(X4_7,identity) != identity )
| ( multiply(X1_8,identity) != identity )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15430,c_15430,c_15421,c_15430,c_15444,c_15430,c_15409]) ).
tff(c_15498,plain,
! [X1_8] :
( ( multiply(X1_8,identity) != identity )
| ( inverse(X1_8) != identity ) ),
inference(splitLeft,[status(thm)],[c_15497]) ).
tff(c_15860,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_15589,c_15498]) ).
tff(c_15432,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_15421,c_14921]) ).
tff(c_15438,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14942,c_15432]) ).
tff(c_15437,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15421,c_14405]) ).
tff(c_15478,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15438,c_15437]) ).
tff(c_15862,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15860,c_15478]) ).
tff(c_15863,plain,
! [X4_7] :
( ( inverse(X4_7) != identity )
| ( multiply(X4_7,identity) != identity ) ),
inference(splitRight,[status(thm)],[c_15497]) ).
tff(c_16293,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_15916,c_15863]) ).
tff(c_16295,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16293,c_15478]) ).
tff(c_16297,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_56,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_16335,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_16297,c_56]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_16322,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_16297,c_54]) ).
tff(c_16326,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16322,c_4]) ).
tff(c_16367,plain,
! [X_267,Y_268,Z_269] : ( multiply(multiply(X_267,Y_268),Z_269) = multiply(X_267,multiply(Y_268,Z_269)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16391,plain,
! [Z_269] : ( multiply(sk_c6,multiply(sk_c4,Z_269)) = multiply(identity,Z_269) ),
inference(superposition,[status(thm),theory(equality)],[c_16326,c_16367]) ).
tff(c_16413,plain,
! [Z_270] : ( multiply(sk_c6,multiply(sk_c4,Z_270)) = Z_270 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16391]) ).
tff(c_16425,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16335,c_16413]) ).
tff(c_52,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_16342,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16297,c_52]) ).
tff(c_16296,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_16301,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16296,c_4]) ).
tff(c_16397,plain,
! [Z_269] : ( multiply(sk_c7,multiply(sk_c3,Z_269)) = multiply(identity,Z_269) ),
inference(superposition,[status(thm),theory(equality)],[c_16301,c_16367]) ).
tff(c_16436,plain,
! [Z_271] : ( multiply(sk_c7,multiply(sk_c3,Z_271)) = Z_271 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16397]) ).
tff(c_16448,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16342,c_16436]) ).
tff(c_48,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_16353,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_16297,c_48]) ).
tff(c_16638,plain,
! [Z_277] : ( multiply(sk_c6,multiply(sk_c7,Z_277)) = multiply(sk_c5,Z_277) ),
inference(superposition,[status(thm),theory(equality)],[c_16353,c_16367]) ).
tff(c_16656,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_16448,c_16638]) ).
tff(c_16669,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16425,c_16656]) ).
tff(c_16400,plain,
! [X_2,Z_269] : ( multiply(inverse(X_2),multiply(X_2,Z_269)) = multiply(identity,Z_269) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16367]) ).
tff(c_16411,plain,
! [X_2,Z_269] : ( multiply(inverse(X_2),multiply(X_2,Z_269)) = Z_269 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16400]) ).
tff(c_16673,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16669,c_16411]) ).
tff(c_16682,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16673]) ).
tff(c_16690,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16682,c_16682,c_16448]) ).
tff(c_16702,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16690]) ).
tff(c_16388,plain,
! [Z_269] : ( multiply(sk_c4,multiply(sk_c5,Z_269)) = multiply(sk_c6,Z_269) ),
inference(superposition,[status(thm),theory(equality)],[c_16335,c_16367]) ).
tff(c_16676,plain,
multiply(sk_c6,sk_c7) = multiply(sk_c4,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16669,c_16388]) ).
tff(c_16683,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16353,c_16335,c_16676]) ).
tff(c_16739,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16702,c_16683]) ).
tff(c_16453,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16353,c_58]) ).
tff(c_16454,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_16453]) ).
tff(c_16691,plain,
multiply(identity,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16682,c_16454]) ).
tff(c_16703,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16691]) ).
tff(c_16749,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16739,c_16702,c_16703]) ).
tff(c_16751,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_16453]) ).
tff(c_16801,plain,
! [Z_281] : ( multiply(sk_c3,multiply(sk_c6,Z_281)) = multiply(sk_c7,Z_281) ),
inference(superposition,[status(thm),theory(equality)],[c_16342,c_16367]) ).
tff(c_16816,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16425,c_16801]) ).
tff(c_16829,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16751,c_16816]) ).
tff(c_16822,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16353,c_16801]) ).
tff(c_16854,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16829,c_16448,c_16822]) ).
tff(c_16858,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16854,c_16854,c_16425]) ).
tff(c_17454,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16858,c_16411]) ).
tff(c_17460,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17454]) ).
tff(c_17403,plain,
! [X_292,Z_293] : ( multiply(inverse(X_292),multiply(X_292,Z_293)) = Z_293 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16400]) ).
tff(c_17627,plain,
! [X_297,Z_298] : ( multiply(inverse(inverse(X_297)),Z_298) = multiply(X_297,Z_298) ),
inference(superposition,[status(thm),theory(equality)],[c_17403,c_16411]) ).
tff(c_17433,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17403]) ).
tff(c_17638,plain,
! [X_297] : ( multiply(X_297,identity) = X_297 ),
inference(superposition,[status(thm),theory(equality)],[c_17627,c_17433]) ).
tff(c_16923,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_16400]) ).
tff(c_17125,plain,
! [X_285,Z_286] : ( multiply(inverse(inverse(X_285)),Z_286) = multiply(X_285,Z_286) ),
inference(superposition,[status(thm),theory(equality)],[c_16923,c_16411]) ).
tff(c_16962,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16923]) ).
tff(c_17132,plain,
! [X_285] : ( multiply(X_285,identity) = X_285 ),
inference(superposition,[status(thm),theory(equality)],[c_17125,c_16962]) ).
tff(c_16941,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16858,c_16923]) ).
tff(c_16969,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16941]) ).
tff(c_16861,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16854,c_16342]) ).
tff(c_16866,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16829,c_16861]) ).
tff(c_16750,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_16453]) ).
tff(c_16780,plain,
! [X2_280] :
( ( multiply(X2_280,sk_c5) != sk_c6 )
| ( inverse(X2_280) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_16750]) ).
tff(c_16787,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16335,c_16780]) ).
tff(c_16799,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16322,c_16787]) ).
tff(c_16800,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(X4_7,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_16750]) ).
tff(c_16882,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c5) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16866,c_16854,c_16866,c_16866,c_16866,c_16866,c_16866,c_16854,c_16800]) ).
tff(c_16883,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_16882]) ).
tff(c_17385,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_17132,c_16969,c_16969,c_16969,c_16883]) ).
tff(c_16877,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16866,c_16296]) ).
tff(c_16894,plain,
multiply(sk_c5,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16877,c_4]) ).
tff(c_16993,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16969,c_16894]) ).
tff(c_16975,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16969,c_16877]) ).
tff(c_17008,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16993,c_16975]) ).
tff(c_17387,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17385,c_17008]) ).
tff(c_17388,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c5 )
| ( inverse(X1_8) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_16882]) ).
tff(c_27820,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17460,c_17638,c_17460,c_17460,c_17638,c_17460,c_17460,c_17460,c_17388]) ).
tff(c_27822,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_27820]) ).
tff(c_17399,plain,
multiply(sk_c5,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16877,c_4]) ).
tff(c_17475,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17460,c_17399]) ).
tff(c_17465,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17460,c_16877]) ).
tff(c_17498,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17475,c_17465]) ).
tff(c_27824,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27822,c_17498]) ).
tff(c_27826,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_27820]) ).
tff(c_27828,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27826,c_17498]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : GRP284-1 : TPTP v9.0.0. Released v2.5.0.
% 0.08/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.13/0.35 % Computer : n003.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Mon Apr 7 21:40:33 EDT 2025
% 0.13/0.35 % CPUTime :
% 12.70/4.17 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.03/4.27
% 13.03/4.27 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------