%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP301-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n014.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:51 PM UTC 2025
% Result : Unsatisfiable 21.02s 8.55s
% Output : CNFRefutation 21.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 31
% Syntax : Number of formulae : 549 ( 462 unt; 0 typ; 0 def)
% Number of atoms : 758 ( 732 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 433 ( 224 ~; 209 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 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 : 262 ( 262 !; 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_113,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
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_185,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c7,sk_c6) != sk_c5 )
| ( multiply(X3,sk_c7) != sk_c6 )
| ( inverse(X3) != sk_c7 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(X4,sk_c6) != sk_c5 )
| ( inverse(X4) != sk_c6 )
| ( 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_149,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
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_86,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
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_131,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
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_74,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
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_98,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = 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_122,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_40,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_98,plain,
inverse(sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_102,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_111,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_115,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_111,c_4]) ).
tff(c_16421,plain,
! [X_202,Y_203,Z_204] : ( multiply(multiply(X_202,Y_203),Z_204) = multiply(X_202,multiply(Y_203,Z_204)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16454,plain,
! [Z_204] : ( multiply(sk_c5,multiply(sk_c7,Z_204)) = multiply(identity,Z_204) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_16421]) ).
tff(c_16488,plain,
! [Z_206] : ( multiply(sk_c5,multiply(sk_c7,Z_206)) = Z_206 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16454]) ).
tff(c_16506,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_16488]) ).
tff(c_14560,plain,
! [X_167,Y_168,Z_169] : ( multiply(multiply(X_167,Y_168),Z_169) = multiply(X_167,multiply(Y_168,Z_169)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14596,plain,
! [Z_169] : ( multiply(sk_c5,multiply(sk_c7,Z_169)) = multiply(identity,Z_169) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_14560]) ).
tff(c_15385,plain,
! [Z_185] : ( multiply(sk_c5,multiply(sk_c7,Z_185)) = Z_185 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14596]) ).
tff(c_15406,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_15385]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_124,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_129,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_13058,plain,
! [X_139,Y_140,Z_141] : ( multiply(multiply(X_139,Y_140),Z_141) = multiply(X_139,multiply(Y_140,Z_141)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13094,plain,
! [Z_141] : ( multiply(sk_c7,multiply(sk_c1,Z_141)) = multiply(identity,Z_141) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_13058]) ).
tff(c_13118,plain,
! [Z_142] : ( multiply(sk_c7,multiply(sk_c1,Z_142)) = Z_142 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13094]) ).
tff(c_13130,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_129,c_13118]) ).
tff(c_13134,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_124,c_13130]) ).
tff(c_68,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_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(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_185]) ).
tff(c_13157,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_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(sk_c6,sk_c5) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 )
| ( multiply(sk_c5,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13134,c_13134,c_13134,c_13134,c_13134,c_13134,c_13134,c_68]) ).
tff(c_13158,plain,
multiply(sk_c5,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_13157]) ).
tff(c_13143,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_13134,c_111]) ).
tff(c_13140,plain,
multiply(sk_c1,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13134,c_129]) ).
tff(c_13103,plain,
! [X_2,Z_141] : ( multiply(inverse(X_2),multiply(X_2,Z_141)) = multiply(identity,Z_141) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13058]) ).
tff(c_13188,plain,
! [X_143,Z_144] : ( multiply(inverse(X_143),multiply(X_143,Z_144)) = Z_144 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13103]) ).
tff(c_13206,plain,
multiply(inverse(sk_c1),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_13140,c_13188]) ).
tff(c_13246,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_13143,c_13206]) ).
tff(c_13248,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13158,c_13246]) ).
tff(c_13250,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_13157]) ).
tff(c_13304,plain,
! [X_145,Z_146] : ( multiply(inverse(X_145),multiply(X_145,Z_146)) = Z_146 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13103]) ).
tff(c_13328,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_13250,c_13304]) ).
tff(c_13372,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13328]) ).
tff(c_64,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_85,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_64]) ).
tff(c_89,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_13383,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13372,c_89]) ).
tff(c_13116,plain,
! [X_2,Z_141] : ( multiply(inverse(X_2),multiply(X_2,Z_141)) = Z_141 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13103]) ).
tff(c_13491,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_13383,c_13116]) ).
tff(c_13503,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13491]) ).
tff(c_160,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_184,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_160]) ).
tff(c_206,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_184]) ).
tff(c_218,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_129,c_206]) ).
tff(c_222,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_124,c_218]) ).
tff(c_225,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_222,c_124]) ).
tff(c_193,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_160]) ).
tff(c_297,plain,
! [X_16,Z_17] : ( multiply(inverse(X_16),multiply(X_16,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_315,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_225,c_297]) ).
tff(c_349,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_315]) ).
tff(c_204,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_193]) ).
tff(c_522,plain,
! [X_21,Z_22] : ( multiply(inverse(inverse(X_21)),Z_22) = multiply(X_21,Z_22) ),
inference(superposition,[status(thm),theory(equality)],[c_297,c_204]) ).
tff(c_342,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_297]) ).
tff(c_533,plain,
! [X_21] : ( multiply(X_21,identity) = X_21 ),
inference(superposition,[status(thm),theory(equality)],[c_522,c_342]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_135,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_333,plain,
multiply(inverse(sk_c2),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_135,c_297]) ).
tff(c_352,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_85,c_333]) ).
tff(c_372,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_349,c_2,c_349,c_352]) ).
tff(c_227,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_222,c_111]) ).
tff(c_237,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_227,c_4]) ).
tff(c_381,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_372,c_237]) ).
tff(c_375,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_372,c_227]) ).
tff(c_390,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_381,c_375]) ).
tff(c_241,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_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(sk_c6,sk_c5) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 )
| ( multiply(sk_c5,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_222,c_222,c_222,c_222,c_222,c_222,c_222,c_68]) ).
tff(c_242,plain,
multiply(sk_c5,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_241]) ).
tff(c_265,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_242,c_225]) ).
tff(c_266,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(sk_c5) != sk_c5 )
| ( multiply(sk_c6,sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != 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(splitRight,[status(thm)],[c_241]) ).
tff(c_7595,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != identity )
| ( identity != X3_6 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( identity != X2_9 )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_349,c_533,c_372,c_349,c_372,c_533,c_372,c_349,c_533,c_372,c_349,c_349,c_533,c_372,c_349,c_372,c_2,c_349,c_390,c_372,c_372,c_266]) ).
tff(c_7597,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_7595]) ).
tff(c_7599,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7597,c_390]) ).
tff(c_7600,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(splitRight,[status(thm)],[c_7595]) ).
tff(c_12206,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_7600]) ).
tff(c_12208,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12206,c_390]) ).
tff(c_12209,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_7600]) ).
tff(c_12211,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_12209]) ).
tff(c_12213,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12211,c_390]) ).
tff(c_12999,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_12209]) ).
tff(c_13001,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12999,c_390]) ).
tff(c_13002,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_13003,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_56,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_13050,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_13003,c_56]) ).
tff(c_13349,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_13050,c_13304]) ).
tff(c_13375,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_13002,c_13349]) ).
tff(c_13411,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13372,c_2,c_13372,c_13375]) ).
tff(c_13381,plain,
multiply(sk_c2,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_13372,c_13003]) ).
tff(c_13536,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13503,c_13411,c_13381]) ).
tff(c_13538,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_20]) ).
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_14541,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_13538,c_18]) ).
tff(c_15446,plain,
! [Z_186] : ( multiply(sk_c7,multiply(sk_c6,Z_186)) = multiply(sk_c5,Z_186) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_14560]) ).
tff(c_15464,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_14541,c_15446]) ).
tff(c_15474,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_15464]) ).
tff(c_14613,plain,
! [Z_169] : ( multiply(sk_c5,multiply(sk_c7,Z_169)) = Z_169 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14596]) ).
tff(c_15478,plain,
multiply(sk_c5,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_15474,c_14613]) ).
tff(c_15484,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_15406,c_15478]) ).
tff(c_15496,plain,
multiply(sk_c1,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15484,c_102]) ).
tff(c_15510,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_15496,c_13538]) ).
tff(c_13599,plain,
! [X_148,Y_149,Z_150] : ( multiply(multiply(X_148,Y_149),Z_150) = multiply(X_148,multiply(Y_149,Z_150)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13638,plain,
! [Z_150] : ( multiply(sk_c5,multiply(sk_c7,Z_150)) = multiply(identity,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_13599]) ).
tff(c_14039,plain,
! [Z_159] : ( multiply(sk_c5,multiply(sk_c7,Z_159)) = Z_159 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13638]) ).
tff(c_14057,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_14039]) ).
tff(c_13537,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_13542,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13537,c_4]) ).
tff(c_14051,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_13542,c_14039]) ).
tff(c_14076,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_14057,c_14051]) ).
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_13589,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_13538,c_22]) ).
tff(c_14077,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_14076,c_13589]) ).
tff(c_13579,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_13538,c_18]) ).
tff(c_14311,plain,
! [Z_164] : ( multiply(sk_c7,multiply(sk_c6,Z_164)) = multiply(sk_c5,Z_164) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_13599]) ).
tff(c_14326,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_13579,c_14311]) ).
tff(c_14336,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_14326]) ).
tff(c_13655,plain,
! [Z_150] : ( multiply(sk_c5,multiply(sk_c7,Z_150)) = Z_150 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13638]) ).
tff(c_14340,plain,
multiply(sk_c5,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_14336,c_13655]) ).
tff(c_14346,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_14057,c_14340]) ).
tff(c_13552,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_14358,plain,
multiply(sk_c2,sk_c6) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_14346,c_13552]) ).
tff(c_14054,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_124,c_14039]) ).
tff(c_13641,plain,
! [Z_150] : ( multiply(sk_c6,multiply(sk_c2,Z_150)) = multiply(identity,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_13599]) ).
tff(c_14094,plain,
! [Z_160] : ( multiply(sk_c6,multiply(sk_c2,Z_160)) = Z_160 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13641]) ).
tff(c_14115,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_13552,c_14094]) ).
tff(c_13626,plain,
! [Z_150] : ( multiply(sk_c2,multiply(sk_c6,Z_150)) = multiply(sk_c5,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_13552,c_13599]) ).
tff(c_14122,plain,
multiply(sk_c5,sk_c5) = multiply(sk_c2,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_14115,c_13626]) ).
tff(c_14128,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14054,c_13552,c_14122]) ).
tff(c_14170,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14128,c_13579]) ).
tff(c_14178,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_14170]) ).
tff(c_14190,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14178,c_98]) ).
tff(c_14130,plain,
! [Z_161] : ( multiply(sk_c7,multiply(sk_c6,Z_161)) = multiply(sk_c5,Z_161) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_13599]) ).
tff(c_14151,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_13579,c_14130]) ).
tff(c_14162,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_14151]) ).
tff(c_14259,plain,
multiply(sk_c7,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14178,c_14162]) ).
tff(c_14185,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14178,c_14128]) ).
tff(c_13685,plain,
! [Z_152] : ( multiply(sk_c5,multiply(sk_c7,Z_152)) = Z_152 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13638]) ).
tff(c_13703,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_13685]) ).
tff(c_13707,plain,
! [Z_153] : ( multiply(sk_c7,multiply(sk_c6,Z_153)) = multiply(sk_c5,Z_153) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_13599]) ).
tff(c_13728,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_13579,c_13707]) ).
tff(c_13739,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_13728]) ).
tff(c_13743,plain,
multiply(sk_c5,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_13739,c_13655]) ).
tff(c_13766,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13703,c_13743]) ).
tff(c_13777,plain,
multiply(sk_c1,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13766,c_102]) ).
tff(c_13775,plain,
multiply(sk_c2,sk_c6) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13766,c_13552]) ).
tff(c_13700,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_124,c_13685]) ).
tff(c_13768,plain,
multiply(sk_c1,sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13766,c_13766,c_13700]) ).
tff(c_13662,plain,
! [Z_151] : ( multiply(sk_c6,multiply(sk_c2,Z_151)) = Z_151 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13641]) ).
tff(c_13674,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_13552,c_13662]) ).
tff(c_13772,plain,
multiply(sk_c6,sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13766,c_13674]) ).
tff(c_13888,plain,
! [Z_150] : ( multiply(sk_c2,multiply(sk_c6,Z_150)) = multiply(sk_c1,Z_150) ),
inference(demodulation,[status(thm),theory(equality)],[c_13766,c_13626]) ).
tff(c_13921,plain,
multiply(sk_c2,sk_c6) = multiply(sk_c1,sk_c1),
inference(superposition,[status(thm),theory(equality)],[c_13772,c_13888]) ).
tff(c_13927,plain,
sk_c6 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13775,c_13768,c_13921]) ).
tff(c_13774,plain,
multiply(sk_c6,sk_c7) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13766,c_13579]) ).
tff(c_13934,plain,
multiply(sk_c1,sk_c7) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13927,c_13774]) ).
tff(c_13945,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13777,c_13934]) ).
tff(c_13778,plain,
inverse(sk_c7) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13766,c_98]) ).
tff(c_13660,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_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_124,c_98,c_13579,c_68]) ).
tff(c_13791,plain,
! [X3_154] :
( ( inverse(X3_154) != sk_c7 )
| ( multiply(X3_154,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_13660]) ).
tff(c_13799,plain,
( ( inverse(inverse(sk_c7)) != sk_c7 )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13791]) ).
tff(c_13805,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_111,c_13778,c_13799]) ).
tff(c_13938,plain,
sk_c1 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_13927,c_13805]) ).
tff(c_14006,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_13945,c_13938]) ).
tff(c_14007,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != 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_13660]) ).
tff(c_14086,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_14007]) ).
tff(c_14201,plain,
! [X2_9] :
( ( multiply(X2_9,identity) != identity )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14185,c_14185,c_14178,c_14086]) ).
tff(c_14263,plain,
inverse(sk_c7) != identity,
inference(superposition,[status(thm),theory(equality)],[c_14259,c_14201]) ).
tff(c_14272,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14190,c_14263]) ).
tff(c_14273,plain,
! [X1_8,X4_7] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_14007]) ).
tff(c_14274,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_14273]) ).
tff(c_14398,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14346,c_14274]) ).
tff(c_14464,plain,
inverse(sk_c2) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_14358,c_14398]) ).
tff(c_14473,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_85,c_14464]) ).
tff(c_14474,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_14273]) ).
tff(c_14501,plain,
inverse(sk_c1) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14077,c_14474]) ).
tff(c_14510,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_111,c_14501]) ).
tff(c_14511,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_54]) ).
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_14546,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_13538,c_26]) ).
tff(c_15492,plain,
multiply(sk_c4,sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15484,c_14546]) ).
tff(c_14602,plain,
! [X_2,Z_169] : ( multiply(inverse(X_2),multiply(X_2,Z_169)) = multiply(identity,Z_169) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14560]) ).
tff(c_15597,plain,
! [X_188,Z_189] : ( multiply(inverse(X_188),multiply(X_188,Z_189)) = Z_189 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14602]) ).
tff(c_15630,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_15492,c_15597]) ).
tff(c_15680,plain,
multiply(sk_c6,sk_c6) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_14511,c_15630]) ).
tff(c_15400,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_13542,c_15385]) ).
tff(c_15426,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_15406,c_15400]) ).
tff(c_14512,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_52,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_14536,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14512,c_52]) ).
tff(c_15427,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_15426,c_14536]) ).
tff(c_14593,plain,
! [Z_169] : ( multiply(sk_c7,multiply(sk_c1,Z_169)) = multiply(identity,Z_169) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_14560]) ).
tff(c_14612,plain,
! [Z_169] : ( multiply(sk_c7,multiply(sk_c1,Z_169)) = Z_169 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14593]) ).
tff(c_15439,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_15427,c_14612]) ).
tff(c_14578,plain,
! [Z_169] : ( multiply(sk_c6,multiply(sk_c7,Z_169)) = multiply(sk_c5,Z_169) ),
inference(superposition,[status(thm),theory(equality)],[c_14541,c_14560]) ).
tff(c_15777,plain,
! [Z_191] : ( multiply(sk_c6,multiply(sk_c7,Z_191)) = multiply(sk_c1,Z_191) ),
inference(demodulation,[status(thm),theory(equality)],[c_15484,c_14578]) ).
tff(c_15795,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c1,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_15439,c_15777]) ).
tff(c_15809,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15680,c_15496,c_15795]) ).
tff(c_15403,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_124,c_15385]) ).
tff(c_15490,plain,
multiply(sk_c1,sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15484,c_15484,c_15403]) ).
tff(c_15815,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15809,c_15809,c_15490]) ).
tff(c_15831,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15815]) ).
tff(c_15833,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15510,c_15831]) ).
tff(c_15834,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_15839,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_15834,c_4]) ).
tff(c_16503,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_15839,c_16488]) ).
tff(c_16520,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_16506,c_16503]) ).
tff(c_15835,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_12,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_16402,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_15835,c_12]) ).
tff(c_16521,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16520,c_16402]) ).
tff(c_16451,plain,
! [Z_204] : ( multiply(sk_c7,multiply(sk_c1,Z_204)) = multiply(identity,Z_204) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_16421]) ).
tff(c_16470,plain,
! [Z_204] : ( multiply(sk_c7,multiply(sk_c1,Z_204)) = Z_204 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16451]) ).
tff(c_16533,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16521,c_16470]) ).
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_16408,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_15835,c_8]) ).
tff(c_16436,plain,
! [Z_204] : ( multiply(sk_c6,multiply(sk_c7,Z_204)) = multiply(sk_c5,Z_204) ),
inference(superposition,[status(thm),theory(equality)],[c_16408,c_16421]) ).
tff(c_16562,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_16533,c_16436]) ).
tff(c_16571,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_16562]) ).
tff(c_15851,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_15897,plain,
! [X_192,Y_193,Z_194] : ( multiply(multiply(X_192,Y_193),Z_194) = multiply(X_192,multiply(Y_193,Z_194)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_15939,plain,
! [X_2,Z_194] : ( multiply(inverse(X_2),multiply(X_2,Z_194)) = multiply(identity,Z_194) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_15897]) ).
tff(c_16052,plain,
! [X_198,Z_199] : ( multiply(inverse(X_198),multiply(X_198,Z_199)) = Z_199 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15939]) ).
tff(c_16106,plain,
multiply(inverse(sk_c2),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_15851,c_16052]) ).
tff(c_16138,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_85,c_16106]) ).
tff(c_15952,plain,
! [X_2,Z_194] : ( multiply(inverse(X_2),multiply(X_2,Z_194)) = Z_194 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15939]) ).
tff(c_16146,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16138,c_15952]) ).
tff(c_16152,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16146]) ).
tff(c_15933,plain,
! [Z_194] : ( multiply(sk_c5,multiply(sk_c7,Z_194)) = multiply(identity,Z_194) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_15897]) ).
tff(c_15967,plain,
! [Z_196] : ( multiply(sk_c5,multiply(sk_c7,Z_196)) = Z_196 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15933]) ).
tff(c_15985,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_15967]) ).
tff(c_16156,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_16152,c_15985]) ).
tff(c_16165,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16156]) ).
tff(c_15982,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_15839,c_15967]) ).
tff(c_15999,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_15985,c_15982]) ).
tff(c_15881,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_15835,c_12]) ).
tff(c_16000,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_15999,c_15881]) ).
tff(c_16170,plain,
multiply(identity,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16165,c_16000]) ).
tff(c_16175,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16170]) ).
tff(c_16163,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16152,c_98]) ).
tff(c_16227,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16175,c_16163]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_15856,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_15835,c_14]) ).
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_15890,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_15835,c_16]) ).
tff(c_16094,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_15890,c_16052]) ).
tff(c_16137,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_15856,c_16094]) ).
tff(c_16283,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16152,c_16137]) ).
tff(c_16290,plain,
multiply(inverse(sk_c6),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16283,c_15952]) ).
tff(c_16296,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16227,c_16290]) ).
tff(c_16303,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16296,c_16175]) ).
tff(c_16161,plain,
multiply(sk_c7,sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_16152,c_15835]) ).
tff(c_16372,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16303,c_16296,c_16161]) ).
tff(c_16373,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_16397,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_15835,c_16]) ).
tff(c_16460,plain,
! [X_2,Z_204] : ( multiply(inverse(X_2),multiply(X_2,Z_204)) = multiply(identity,Z_204) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16421]) ).
tff(c_16602,plain,
! [X_209,Z_210] : ( multiply(inverse(X_209),multiply(X_209,Z_210)) = Z_210 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16460]) ).
tff(c_16653,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16397,c_16602]) ).
tff(c_16690,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16571,c_16373,c_16653]) ).
tff(c_16471,plain,
! [Z_204] : ( multiply(sk_c5,multiply(sk_c7,Z_204)) = Z_204 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16454]) ).
tff(c_16565,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16533,c_16471]) ).
tff(c_16695,plain,
multiply(identity,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16690,c_16565]) ).
tff(c_16705,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16695]) ).
tff(c_16712,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16705,c_16705,c_16533]) ).
tff(c_16717,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16571,c_16712]) ).
tff(c_16767,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16717,c_16705]) ).
tff(c_16702,plain,
multiply(sk_c7,sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_16690,c_15835]) ).
tff(c_16853,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16767,c_16717,c_16702]) ).
tff(c_16855,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_30,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_16863,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16855,c_30]) ).
tff(c_16867,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16863,c_4]) ).
tff(c_16915,plain,
! [X_212,Y_213,Z_214] : ( multiply(multiply(X_212,Y_213),Z_214) = multiply(X_212,multiply(Y_213,Z_214)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16945,plain,
! [Z_214] : ( multiply(sk_c5,multiply(sk_c7,Z_214)) = multiply(identity,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_16915]) ).
tff(c_16965,plain,
! [Z_215] : ( multiply(sk_c5,multiply(sk_c7,Z_215)) = Z_215 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16945]) ).
tff(c_16977,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_16867,c_16965]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_16883,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_16855,c_36]) ).
tff(c_16854,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_16859,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16854,c_4]) ).
tff(c_16942,plain,
! [Z_214] : ( multiply(sk_c6,multiply(sk_c4,Z_214)) = multiply(identity,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_16859,c_16915]) ).
tff(c_17367,plain,
! [Z_225] : ( multiply(sk_c6,multiply(sk_c4,Z_225)) = Z_225 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16942]) ).
tff(c_17382,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16883,c_17367]) ).
tff(c_28,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_16896,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_16855,c_28]) ).
tff(c_16990,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_c6 )
| ( multiply(X4_7,sk_c6) != 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_98,c_16896,c_68]) ).
tff(c_16991,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_16990]) ).
tff(c_32,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_16891,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16855,c_32]) ).
tff(c_16939,plain,
! [Z_214] : ( multiply(sk_c7,multiply(sk_c3,Z_214)) = multiply(identity,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_16867,c_16915]) ).
tff(c_17005,plain,
! [Z_217] : ( multiply(sk_c7,multiply(sk_c3,Z_217)) = Z_217 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16939]) ).
tff(c_17020,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16891,c_17005]) ).
tff(c_17262,plain,
! [Z_222] : ( multiply(sk_c3,multiply(sk_c6,Z_222)) = multiply(sk_c7,Z_222) ),
inference(superposition,[status(thm),theory(equality)],[c_16891,c_16915]) ).
tff(c_17286,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16896,c_17262]) ).
tff(c_17294,plain,
multiply(sk_c3,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17020,c_17286]) ).
tff(c_16951,plain,
! [X_2,Z_214] : ( multiply(inverse(X_2),multiply(X_2,Z_214)) = multiply(identity,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16915]) ).
tff(c_16963,plain,
! [X_2,Z_214] : ( multiply(inverse(X_2),multiply(X_2,Z_214)) = Z_214 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16951]) ).
tff(c_17298,plain,
multiply(inverse(sk_c3),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_17294,c_16963]) ).
tff(c_17307,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16863,c_17298]) ).
tff(c_17309,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16991,c_17307]) ).
tff(c_17311,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_16990]) ).
tff(c_16961,plain,
! [Z_214] : ( multiply(sk_c5,multiply(sk_c7,Z_214)) = Z_214 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16945]) ).
tff(c_17315,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17311,c_16961]) ).
tff(c_16933,plain,
! [Z_214] : ( multiply(sk_c3,multiply(sk_c6,Z_214)) = multiply(sk_c7,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_16891,c_16915]) ).
tff(c_17389,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_17382,c_16933]) ).
tff(c_17395,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17311,c_17389]) ).
tff(c_17329,plain,
! [Z_223] : ( multiply(sk_c3,multiply(sk_c6,Z_223)) = multiply(sk_c7,Z_223) ),
inference(superposition,[status(thm),theory(equality)],[c_16891,c_16915]) ).
tff(c_17341,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16896,c_17329]) ).
tff(c_17404,plain,
multiply(sk_c7,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17395,c_17341]) ).
tff(c_17408,plain,
multiply(sk_c5,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_17404,c_16961]) ).
tff(c_17414,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17315,c_17408]) ).
tff(c_17513,plain,
multiply(sk_c5,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17414,c_102]) ).
tff(c_16930,plain,
! [Z_214] : ( multiply(sk_c6,multiply(sk_c7,Z_214)) = multiply(sk_c5,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_16896,c_16915]) ).
tff(c_18587,plain,
! [Z_249] : ( multiply(sk_c6,multiply(sk_c6,Z_249)) = multiply(sk_c5,Z_249) ),
inference(demodulation,[status(thm),theory(equality)],[c_17414,c_16930]) ).
tff(c_18608,plain,
multiply(sk_c6,sk_c5) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_17382,c_18587]) ).
tff(c_18624,plain,
multiply(sk_c6,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17513,c_18608]) ).
tff(c_18586,plain,
! [Z_214] : ( multiply(sk_c6,multiply(sk_c6,Z_214)) = multiply(sk_c5,Z_214) ),
inference(demodulation,[status(thm),theory(equality)],[c_17414,c_16930]) ).
tff(c_18628,plain,
multiply(sk_c6,identity) = multiply(sk_c5,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_18624,c_18586]) ).
tff(c_18634,plain,
multiply(sk_c6,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17315,c_18628]) ).
tff(c_18640,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,identity),
inference(superposition,[status(thm),theory(equality)],[c_18634,c_18586]) ).
tff(c_18646,plain,
sk_c5 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_16977,c_17382,c_18640]) ).
tff(c_18654,plain,
multiply(sk_c6,sk_c6) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_18646,c_17382]) ).
tff(c_17511,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17414,c_16863]) ).
tff(c_17509,plain,
multiply(sk_c3,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17414,c_16891]) ).
tff(c_18677,plain,
! [X_250,Z_251] : ( multiply(inverse(X_250),multiply(X_250,Z_251)) = Z_251 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16951]) ).
tff(c_18704,plain,
multiply(inverse(sk_c3),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17509,c_18677]) ).
tff(c_18743,plain,
sk_c6 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_18654,c_17511,c_18704]) ).
tff(c_17514,plain,
inverse(sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17414,c_98]) ).
tff(c_18652,plain,
inverse(sk_c6) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_18646,c_17514]) ).
tff(c_18666,plain,
multiply(sk_c3,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18652,c_4]) ).
tff(c_18783,plain,
multiply(sk_c3,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18743,c_18666]) ).
tff(c_18762,plain,
inverse(sk_c4) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_18743,c_16854]) ).
tff(c_18657,plain,
multiply(sk_c4,sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_18646,c_16883]) ).
tff(c_18879,plain,
multiply(sk_c4,sk_c3) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_18743,c_18657]) ).
tff(c_18883,plain,
multiply(inverse(sk_c4),sk_c3) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_18879,c_16963]) ).
tff(c_18889,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18783,c_18762,c_18883]) ).
tff(c_18901,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18889,c_18743]) ).
tff(c_19013,plain,
! [X_254,Z_255] : ( multiply(inverse(inverse(X_254)),Z_255) = multiply(X_254,Z_255) ),
inference(superposition,[status(thm),theory(equality)],[c_16963,c_18677]) ).
tff(c_18734,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18677]) ).
tff(c_19020,plain,
! [X_254] : ( multiply(X_254,identity) = X_254 ),
inference(superposition,[status(thm),theory(equality)],[c_19013,c_18734]) ).
tff(c_18902,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18889,c_18646]) ).
tff(c_17664,plain,
! [X_229,Z_230] : ( multiply(inverse(X_229),multiply(X_229,Z_230)) = Z_230 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16951]) ).
tff(c_17939,plain,
! [X_233,Z_234] : ( multiply(inverse(inverse(X_233)),Z_234) = multiply(X_233,Z_234) ),
inference(superposition,[status(thm),theory(equality)],[c_17664,c_16963]) ).
tff(c_17706,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17664]) ).
tff(c_17946,plain,
! [X_233] : ( multiply(X_233,identity) = X_233 ),
inference(superposition,[status(thm),theory(equality)],[c_17939,c_17706]) ).
tff(c_16959,plain,
! [Z_214] : ( multiply(sk_c7,multiply(sk_c3,Z_214)) = Z_214 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16939]) ).
tff(c_17564,plain,
! [Z_227] : ( multiply(sk_c6,multiply(sk_c3,Z_227)) = Z_227 ),
inference(demodulation,[status(thm),theory(equality)],[c_17414,c_16959]) ).
tff(c_17576,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17509,c_17564]) ).
tff(c_17583,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17382,c_17576]) ).
tff(c_17585,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17583,c_17513]) ).
tff(c_17579,plain,
multiply(sk_c6,sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_17395,c_17564]) ).
tff(c_17795,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17585,c_17583,c_17579]) ).
tff(c_17806,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17795,c_17583]) ).
tff(c_17310,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_c6 )
| ( multiply(X4_7,sk_c6) != 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_16990]) ).
tff(c_17474,plain,
! [X2_226] :
( ( multiply(X2_226,sk_c5) != sk_c6 )
| ( inverse(X2_226) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_17310]) ).
tff(c_17487,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16883,c_17474]) ).
tff(c_17502,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16854,c_17487]) ).
tff(c_17503,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_17310]) ).
tff(c_17561,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17414,c_17414,c_17414,c_17414,c_17503]) ).
tff(c_17562,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_17561]) ).
tff(c_18582,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_17946,c_17806,c_17806,c_17806,c_17562]) ).
tff(c_17587,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17583,c_17514]) ).
tff(c_17802,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17795,c_17795,c_17587]) ).
tff(c_18584,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18582,c_17802]) ).
tff(c_18585,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c6 )
| ( inverse(X1_8) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_17561]) ).
tff(c_39578,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_18901,c_19020,c_18901,c_18901,c_19020,c_18902,c_18901,c_18901,c_18585]) ).
tff(c_39580,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_39578]) ).
tff(c_18802,plain,
multiply(sk_c3,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18762,c_4]) ).
tff(c_18909,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18889,c_18802]) ).
tff(c_18897,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18889,c_18762]) ).
tff(c_18926,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18909,c_18897]) ).
tff(c_39582,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_39580,c_18926]) ).
tff(c_39584,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_39578]) ).
tff(c_39586,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_39584,c_18926]) ).
tff(c_39588,plain,
inverse(sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_39640,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_39588,c_46]) ).
tff(c_44,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_39600,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_39588,c_44]) ).
tff(c_39604,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39600,c_4]) ).
tff(c_39661,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_39688,plain,
! [Z_414] : ( multiply(sk_c6,multiply(sk_c4,Z_414)) = multiply(identity,Z_414) ),
inference(superposition,[status(thm),theory(equality)],[c_39604,c_39661]) ).
tff(c_39739,plain,
! [Z_417] : ( multiply(sk_c6,multiply(sk_c4,Z_417)) = Z_417 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39688]) ).
tff(c_39751,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_39640,c_39739]) ).
tff(c_42,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_39616,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_39588,c_42]) ).
tff(c_39587,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_39592,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39587,c_4]) ).
tff(c_39691,plain,
! [Z_414] : ( multiply(sk_c7,multiply(sk_c3,Z_414)) = multiply(identity,Z_414) ),
inference(superposition,[status(thm),theory(equality)],[c_39592,c_39661]) ).
tff(c_39762,plain,
! [Z_418] : ( multiply(sk_c7,multiply(sk_c3,Z_418)) = Z_418 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39691]) ).
tff(c_39774,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_39616,c_39762]) ).
tff(c_38,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_39645,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_39588,c_38]) ).
tff(c_40017,plain,
! [Z_423] : ( multiply(sk_c6,multiply(sk_c7,Z_423)) = multiply(sk_c5,Z_423) ),
inference(superposition,[status(thm),theory(equality)],[c_39645,c_39661]) ).
tff(c_40032,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_39774,c_40017]) ).
tff(c_40042,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_39751,c_40032]) ).
tff(c_39697,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_39661]) ).
tff(c_39709,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_39697]) ).
tff(c_40072,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40042,c_39709]) ).
tff(c_40078,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40072]) ).
tff(c_40123,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40078,c_40078,c_39774]) ).
tff(c_40132,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40123]) ).
tff(c_39785,plain,
! [X_419,Z_420] : ( multiply(inverse(X_419),multiply(X_419,Z_420)) = Z_420 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39697]) ).
tff(c_39851,plain,
multiply(inverse(sk_c6),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_39785]) ).
tff(c_40138,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_40132,c_39851]) ).
tff(c_40143,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40138]) ).
tff(c_40142,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40132,c_85]) ).
tff(c_40172,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40143,c_40142]) ).
tff(c_40139,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_40132,c_40132,c_39751]) ).
tff(c_40144,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40139]) ).
tff(c_40128,plain,
inverse(identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_40078,c_39588]) ).
tff(c_40193,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40172,c_40144,c_40128]) ).
tff(c_40195,plain,
inverse(sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_66,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_40235,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_40195,c_66]) ).
tff(c_40194,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_40199,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40194,c_4]) ).
tff(c_62915,plain,
! [X_615,Y_616,Z_617] : ( multiply(multiply(X_615,Y_616),Z_617) = multiply(X_615,multiply(Y_616,Z_617)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_62945,plain,
! [Z_617] : ( multiply(sk_c6,multiply(sk_c4,Z_617)) = multiply(identity,Z_617) ),
inference(superposition,[status(thm),theory(equality)],[c_40199,c_62915]) ).
tff(c_62984,plain,
! [Z_619] : ( multiply(sk_c6,multiply(sk_c4,Z_619)) = Z_619 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62945]) ).
tff(c_62996,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_40235,c_62984]) ).
tff(c_62948,plain,
! [X_2,Z_617] : ( multiply(inverse(X_2),multiply(X_2,Z_617)) = multiply(identity,Z_617) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_62915]) ).
tff(c_63022,plain,
! [X_621,Z_622] : ( multiply(inverse(X_621),multiply(X_621,Z_622)) = Z_622 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62948]) ).
tff(c_63043,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_62996,c_63022]) ).
tff(c_58,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_40242,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_40195,c_58]) ).
tff(c_63061,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40242,c_63022]) ).
tff(c_63297,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_63043,c_63061]) ).
tff(c_40281,plain,
! [X_425,Y_426,Z_427] : ( multiply(multiply(X_425,Y_426),Z_427) = multiply(X_425,multiply(Y_426,Z_427)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_40317,plain,
! [X_2,Z_427] : ( multiply(inverse(X_2),multiply(X_2,Z_427)) = multiply(identity,Z_427) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_40281]) ).
tff(c_40329,plain,
! [X_2,Z_427] : ( multiply(inverse(X_2),multiply(X_2,Z_427)) = Z_427 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40317]) ).
tff(c_41536,plain,
! [X_452,Z_453] : ( multiply(inverse(X_452),multiply(X_452,Z_453)) = Z_453 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40317]) ).
tff(c_41719,plain,
! [X_455,Z_456] : ( multiply(inverse(inverse(X_455)),Z_456) = multiply(X_455,Z_456) ),
inference(superposition,[status(thm),theory(equality)],[c_40329,c_41536]) ).
tff(c_41563,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_41536]) ).
tff(c_41726,plain,
! [X_455] : ( multiply(X_455,identity) = X_455 ),
inference(superposition,[status(thm),theory(equality)],[c_41719,c_41563]) ).
tff(c_40314,plain,
! [Z_427] : ( multiply(sk_c6,multiply(sk_c4,Z_427)) = multiply(identity,Z_427) ),
inference(superposition,[status(thm),theory(equality)],[c_40199,c_40281]) ).
tff(c_40739,plain,
! [Z_436] : ( multiply(sk_c6,multiply(sk_c4,Z_436)) = Z_436 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40314]) ).
tff(c_40751,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_40235,c_40739]) ).
tff(c_40247,plain,
inverse(sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_40251,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40247,c_4]) ).
tff(c_62,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_40263,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_40195,c_62]) ).
tff(c_60,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_40207,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_40195,c_60]) ).
tff(c_40211,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40207,c_4]) ).
tff(c_40311,plain,
! [Z_427] : ( multiply(sk_c7,multiply(sk_c3,Z_427)) = multiply(identity,Z_427) ),
inference(superposition,[status(thm),theory(equality)],[c_40211,c_40281]) ).
tff(c_40762,plain,
! [Z_437] : ( multiply(sk_c7,multiply(sk_c3,Z_437)) = Z_437 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40311]) ).
tff(c_40777,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_40263,c_40762]) ).
tff(c_40302,plain,
! [Z_427] : ( multiply(sk_c6,multiply(sk_c7,Z_427)) = multiply(sk_c5,Z_427) ),
inference(superposition,[status(thm),theory(equality)],[c_40242,c_40281]) ).
tff(c_40784,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_40777,c_40302]) ).
tff(c_40790,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40751,c_40251,c_40784]) ).
tff(c_40796,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40790,c_40247]) ).
tff(c_41479,plain,
multiply(identity,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40796,c_4]) ).
tff(c_41489,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_41479,c_2]) ).
tff(c_41499,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41489,c_41489,c_40777]) ).
tff(c_41507,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41499]) ).
tff(c_40795,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40790,c_40251]) ).
tff(c_40827,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_40795,c_2]) ).
tff(c_40838,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40827,c_40827,c_40777]) ).
tff(c_40846,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40838]) ).
tff(c_40882,plain,
! [X_438,Z_439] : ( multiply(inverse(X_438),multiply(X_438,Z_439)) = Z_439 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40317]) ).
tff(c_41091,plain,
! [X_442,Z_443] : ( multiply(inverse(inverse(X_442)),Z_443) = multiply(X_442,Z_443) ),
inference(superposition,[status(thm),theory(equality)],[c_40329,c_40882]) ).
tff(c_40912,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_40882]) ).
tff(c_41098,plain,
! [X_442] : ( multiply(X_442,identity) = X_442 ),
inference(superposition,[status(thm),theory(equality)],[c_41091,c_40912]) ).
tff(c_40357,plain,
! [Z_429] : ( multiply(sk_c6,multiply(sk_c4,Z_429)) = Z_429 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40314]) ).
tff(c_40369,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_40235,c_40357]) ).
tff(c_40334,plain,
! [Z_428] : ( multiply(sk_c7,multiply(sk_c3,Z_428)) = Z_428 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40311]) ).
tff(c_40346,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_40263,c_40334]) ).
tff(c_40583,plain,
! [Z_433] : ( multiply(sk_c6,multiply(sk_c7,Z_433)) = multiply(sk_c5,Z_433) ),
inference(superposition,[status(thm),theory(equality)],[c_40242,c_40281]) ).
tff(c_40598,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_40346,c_40583]) ).
tff(c_40605,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40369,c_40251,c_40598]) ).
tff(c_40380,plain,
! [X_430,Z_431] : ( multiply(inverse(X_430),multiply(X_430,Z_431)) = Z_431 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40317]) ).
tff(c_40416,plain,
multiply(inverse(sk_c5),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40251,c_40380]) ).
tff(c_40607,plain,
multiply(inverse(identity),identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_40605,c_40416]) ).
tff(c_40618,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40607]) ).
tff(c_40627,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_40618,c_40618,c_40346]) ).
tff(c_40630,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40627]) ).
tff(c_40332,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_c6 )
| ( multiply(X4_7,sk_c6) != 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_40247,c_40242,c_68]) ).
tff(c_40333,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_40332]) ).
tff(c_40612,plain,
multiply(sk_c7,sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_40605,c_40333]) ).
tff(c_40707,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40630,c_2,c_40618,c_40612]) ).
tff(c_40708,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_c6 )
| ( multiply(X4_7,sk_c6) != 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_40332]) ).
tff(c_40804,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_c6 )
| ( multiply(X4_7,sk_c6) != identity )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,identity) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_40790,c_40790,c_40708]) ).
tff(c_40805,plain,
! [X2_9] :
( ( multiply(X2_9,identity) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_40804]) ).
tff(c_41472,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_40846,c_41098,c_40846,c_40805]) ).
tff(c_40837,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40827,c_40796]) ).
tff(c_41474,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41472,c_40837]) ).
tff(c_41475,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != identity )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_40804]) ).
tff(c_62873,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_41726,c_41507,c_41489,c_41489,c_41726,c_41507,c_41507,c_41489,c_41726,c_41507,c_41489,c_41475]) ).
tff(c_62875,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_62873]) ).
tff(c_41498,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_41489,c_40796]) ).
tff(c_62877,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62875,c_41498]) ).
tff(c_62878,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_62873]) ).
tff(c_62880,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_62878]) ).
tff(c_62882,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62880,c_41498]) ).
tff(c_62885,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_62878]) ).
tff(c_62887,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62885,c_41498]) ).
tff(c_62888,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_62942,plain,
! [Z_617] : ( multiply(sk_c7,multiply(sk_c3,Z_617)) = multiply(identity,Z_617) ),
inference(superposition,[status(thm),theory(equality)],[c_40211,c_62915]) ).
tff(c_62961,plain,
! [Z_618] : ( multiply(sk_c7,multiply(sk_c3,Z_618)) = Z_618 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62942]) ).
tff(c_62973,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_62888,c_62961]) ).
tff(c_63049,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_62973,c_63022]) ).
tff(c_63308,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_63297,c_63297,c_63049]) ).
tff(c_63319,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_63308]) ).
tff(c_63079,plain,
multiply(inverse(sk_c6),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_40199,c_63022]) ).
tff(c_63330,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_63319,c_63079]) ).
tff(c_63337,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_63330]) ).
tff(c_63336,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63319,c_40194]) ).
tff(c_63395,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63337,c_63336]) ).
tff(c_63314,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_63297,c_63297,c_62973]) ).
tff(c_63321,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_62996,c_63314]) ).
tff(c_63360,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63319,c_63321]) ).
tff(c_62889,plain,
inverse(sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_63315,plain,
inverse(sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_63297,c_62889]) ).
tff(c_63415,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_63395,c_63360,c_63319,c_63315]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : GRP301-1 : TPTP v9.0.0. Released v2.5.0.
% 0.00/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.09/0.29 % Computer : n014.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Mon Apr 7 21:41:04 EDT 2025
% 0.09/0.29 % CPUTime :
% 21.02/8.55 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.19/8.60
% 21.19/8.60 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------