%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP266-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 : n018.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:44 PM UTC 2025
% Result : Unsatisfiable 61.19s 46.22s
% Output : CNFRefutation 61.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 38
% Syntax : Number of formulae : 663 ( 537 unt; 0 typ; 0 def)
% Number of atoms : 1015 ( 970 equ)
% Maximal formula atoms : 14 ( 1 avg)
% Number of connectives : 750 ( 398 ~; 352 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 417 ( 417 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c11 > sk_c10 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c10,type,
sk_c10: $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c11,type,
sk_c11: $i ).
tff(sk_c9,type,
sk_c9: $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
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_95,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_182,axiom,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_200,axiom,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_188,axiom,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( inverse(sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( multiply(sk_c10,sk_c4) = sk_c9 )
| ( inverse(sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( inverse(sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( inverse(sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_251,axiom,
! [X5,X6,X3,X7,X1,X2,X8,X4] :
( ( multiply(X5,sk_c11) != sk_c10 )
| ( inverse(X5) != sk_c11 )
| ( multiply(X6,sk_c9) != sk_c10 )
| ( inverse(X6) != sk_c9 )
| ( multiply(sk_c10,X7) != sk_c9 )
| ( multiply(X8,sk_c10) != X7 )
| ( inverse(X8) != sk_c10 )
| ( multiply(X1,sk_c11) != sk_c10 )
| ( inverse(X1) != sk_c11 )
| ( multiply(X2,sk_c9) != sk_c10 )
| ( inverse(X2) != sk_c9 )
| ( multiply(sk_c9,X3) != sk_c10 )
| ( multiply(X4,sk_c9) != X3 )
| ( inverse(X4) != sk_c9 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( inverse(sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_173,axiom,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( inverse(sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( multiply(sk_c10,sk_c4) = sk_c9 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( multiply(sk_c10,sk_c4) = sk_c9 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c10,sk_c4) = sk_c9 )
| ( inverse(sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c10,sk_c4) = sk_c9 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c1,sk_c11) = sk_c10 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( multiply(sk_c10,sk_c4) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_194,axiom,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_191,axiom,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_203,axiom,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_206,axiom,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c7,sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_209,axiom,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c7) = sk_c9 ) ),
file(unknown,unknown) ).
tff(c_24,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_171312,plain,
inverse(sk_c1) = sk_c11,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_171316,plain,
multiply(sk_c11,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_171312,c_4]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_171392,plain,
! [X_1050,Y_1051,Z_1052] : ( multiply(multiply(X_1050,Y_1051),Z_1052) = multiply(X_1050,multiply(Y_1051,Z_1052)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_171434,plain,
! [X_2,Z_1052] : ( multiply(inverse(X_2),multiply(X_2,Z_1052)) = multiply(identity,Z_1052) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_171392]) ).
tff(c_173849,plain,
! [X_1092,Z_1093] : ( multiply(inverse(X_1092),multiply(X_1092,Z_1093)) = Z_1093 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_171434]) ).
tff(c_173927,plain,
multiply(inverse(sk_c11),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_171316,c_173849]) ).
tff(c_28,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_135,plain,
inverse(sk_c1) = sk_c11,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_139,plain,
multiply(sk_c11,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_135,c_4]) ).
tff(c_86,plain,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( multiply(sk_c3,sk_c10) = sk_c4 ) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_95146,plain,
multiply(sk_c3,sk_c10) = sk_c4,
inference(splitLeft,[status(thm)],[c_86]) ).
tff(c_98,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_123,plain,
inverse(sk_c3) = sk_c10,
inference(splitLeft,[status(thm)],[c_98]) ).
tff(c_127,plain,
multiply(sk_c10,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_123,c_4]) ).
tff(c_95181,plain,
! [X_604,Y_605,Z_606] : ( multiply(multiply(X_604,Y_605),Z_606) = multiply(X_604,multiply(Y_605,Z_606)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_95226,plain,
! [Z_606] : ( multiply(sk_c10,multiply(sk_c3,Z_606)) = multiply(identity,Z_606) ),
inference(superposition,[status(thm),theory(equality)],[c_127,c_95181]) ).
tff(c_95340,plain,
! [Z_612] : ( multiply(sk_c10,multiply(sk_c3,Z_612)) = Z_612 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_95226]) ).
tff(c_95352,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_95146,c_95340]) ).
tff(c_8,plain,
( ( multiply(sk_c5,sk_c11) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_67088,plain,
multiply(sk_c1,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_67105,plain,
! [X_338,Y_339,Z_340] : ( multiply(multiply(X_338,Y_339),Z_340) = multiply(X_338,multiply(Y_339,Z_340)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_67153,plain,
! [Z_340] : ( multiply(sk_c11,multiply(sk_c1,Z_340)) = multiply(identity,Z_340) ),
inference(superposition,[status(thm),theory(equality)],[c_139,c_67105]) ).
tff(c_67293,plain,
! [Z_347] : ( multiply(sk_c11,multiply(sk_c1,Z_347)) = Z_347 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67153]) ).
tff(c_67305,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_67088,c_67293]) ).
tff(c_67159,plain,
! [X_2,Z_340] : ( multiply(inverse(X_2),multiply(X_2,Z_340)) = multiply(identity,Z_340) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_67105]) ).
tff(c_67477,plain,
! [X_352,Z_353] : ( multiply(inverse(X_352),multiply(X_352,Z_353)) = Z_353 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67159]) ).
tff(c_67534,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_67305,c_67477]) ).
tff(c_67579,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_67534]) ).
tff(c_67602,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67579,c_127]) ).
tff(c_67173,plain,
! [X_2,Z_340] : ( multiply(inverse(X_2),multiply(X_2,Z_340)) = Z_340 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67159]) ).
tff(c_67715,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_67602,c_67173]) ).
tff(c_67727,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_67715]) ).
tff(c_90,plain,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c3,sk_c10) = sk_c4 ) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_183,plain,
multiply(sk_c3,sk_c10) = sk_c4,
inference(splitLeft,[status(thm)],[c_90]) ).
tff(c_66176,plain,
! [X_323,Y_324,Z_325] : ( multiply(multiply(X_323,Y_324),Z_325) = multiply(X_323,multiply(Y_324,Z_325)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_66227,plain,
! [Z_325] : ( multiply(sk_c10,multiply(sk_c3,Z_325)) = multiply(identity,Z_325) ),
inference(superposition,[status(thm),theory(equality)],[c_127,c_66176]) ).
tff(c_66358,plain,
! [Z_330] : ( multiply(sk_c10,multiply(sk_c3,Z_330)) = Z_330 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66227]) ).
tff(c_66370,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_183,c_66358]) ).
tff(c_76,plain,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_165,plain,
multiply(sk_c10,sk_c4) = sk_c9,
inference(splitLeft,[status(thm)],[c_76]) ).
tff(c_66374,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_66370,c_165]) ).
tff(c_38,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_175,plain,
multiply(sk_c2,sk_c9) = sk_c10,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_62,plain,
( ( inverse(sk_c7) = sk_c9 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_150,plain,
inverse(sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_154,plain,
multiply(sk_c9,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_150,c_4]) ).
tff(c_66221,plain,
! [Z_325] : ( multiply(sk_c9,multiply(sk_c2,Z_325)) = multiply(identity,Z_325) ),
inference(superposition,[status(thm),theory(equality)],[c_154,c_66176]) ).
tff(c_66246,plain,
! [Z_326] : ( multiply(sk_c9,multiply(sk_c2,Z_326)) = Z_326 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66221]) ).
tff(c_66258,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_175,c_66246]) ).
tff(c_66382,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_66374,c_66374,c_66258]) ).
tff(c_66230,plain,
! [X_2,Z_325] : ( multiply(inverse(X_2),multiply(X_2,Z_325)) = multiply(identity,Z_325) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_66176]) ).
tff(c_66530,plain,
! [X_332,Z_333] : ( multiply(inverse(X_332),multiply(X_332,Z_333)) = Z_333 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66230]) ).
tff(c_66548,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_66382,c_66530]) ).
tff(c_66627,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_66548]) ).
tff(c_20,plain,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_197,plain,
multiply(sk_c1,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_221,plain,
! [X_16,Y_17,Z_18] : ( multiply(multiply(X_16,Y_17),Z_18) = multiply(X_16,multiply(Y_17,Z_18)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_251,plain,
! [Z_18] : ( multiply(sk_c11,multiply(sk_c1,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_139,c_221]) ).
tff(c_448,plain,
! [Z_23] : ( multiply(sk_c11,multiply(sk_c1,Z_23)) = Z_23 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_251]) ).
tff(c_460,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_197,c_448]) ).
tff(c_257,plain,
! [X_2,Z_18] : ( multiply(inverse(X_2),multiply(X_2,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_221]) ).
tff(c_3264,plain,
! [X_63,Z_64] : ( multiply(inverse(X_63),multiply(X_63,Z_64)) = Z_64 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_257]) ).
tff(c_3285,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_460,c_3264]) ).
tff(c_3337,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_3285]) ).
tff(c_3391,plain,
multiply(sk_c1,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_3337,c_197]) ).
tff(c_268,plain,
! [X_2,Z_18] : ( multiply(inverse(X_2),multiply(X_2,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_257]) ).
tff(c_3735,plain,
! [X_71,Z_72] : ( multiply(inverse(inverse(X_71)),Z_72) = multiply(X_71,Z_72) ),
inference(superposition,[status(thm),theory(equality)],[c_3264,c_268]) ).
tff(c_3330,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_3264]) ).
tff(c_3749,plain,
! [X_71] : ( multiply(X_71,identity) = X_71 ),
inference(superposition,[status(thm),theory(equality)],[c_3735,c_3330]) ).
tff(c_491,plain,
! [X_25,Z_26] : ( multiply(inverse(X_25),multiply(X_25,Z_26)) = Z_26 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_257]) ).
tff(c_962,plain,
! [X_33,Z_34] : ( multiply(inverse(inverse(X_33)),Z_34) = multiply(X_33,Z_34) ),
inference(superposition,[status(thm),theory(equality)],[c_491,c_268]) ).
tff(c_557,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_491]) ).
tff(c_976,plain,
! [X_33] : ( multiply(X_33,identity) = X_33 ),
inference(superposition,[status(thm),theory(equality)],[c_962,c_557]) ).
tff(c_512,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_460,c_491]) ).
tff(c_564,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_512]) ).
tff(c_254,plain,
! [Z_18] : ( multiply(sk_c10,multiply(sk_c3,Z_18)) = multiply(identity,Z_18) ),
inference(superposition,[status(thm),theory(equality)],[c_127,c_221]) ).
tff(c_293,plain,
! [Z_20] : ( multiply(sk_c10,multiply(sk_c3,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_254]) ).
tff(c_305,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_183,c_293]) ).
tff(c_401,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_305,c_165]) ).
tff(c_106,plain,
! [X5_6,X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X4_13) != sk_c9 )
| ( multiply(sk_c9,multiply(X4_13,sk_c9)) != sk_c10 )
| ( inverse(X2_11) != sk_c9 )
| ( multiply(X2_11,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( multiply(X6_7,sk_c9) != sk_c10 )
| ( inverse(X5_6) != sk_c11 )
| ( multiply(X5_6,sk_c11) != sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_251]) ).
tff(c_380,plain,
! [X5_22] :
( ( inverse(X5_22) != sk_c11 )
| ( multiply(X5_22,sk_c11) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_106]) ).
tff(c_387,plain,
inverse(sk_c1) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_197,c_380]) ).
tff(c_399,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_135,c_387]) ).
tff(c_400,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c9 )
| ( multiply(X6_7,sk_c9) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c9 )
| ( multiply(X2_11,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(sk_c9,multiply(X4_13,sk_c9)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_106]) ).
tff(c_471,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_401,c_401,c_401,c_401,c_401,c_401,c_401,c_401,c_400]) ).
tff(c_472,plain,
! [X4_13] :
( ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_471]) ).
tff(c_3242,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_976,c_564,c_564,c_2,c_564,c_564,c_472]) ).
tff(c_621,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_564,c_123]) ).
tff(c_642,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_621,c_4]) ).
tff(c_719,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_642,c_268]) ).
tff(c_731,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_719]) ).
tff(c_735,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_731,c_621]) ).
tff(c_3244,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3242,c_735]) ).
tff(c_3245,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_471]) ).
tff(c_10751,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3749,c_3337,c_3337,c_3337,c_3749,c_3337,c_3337,c_2,c_3337,c_3337,c_3337,c_3749,c_3337,c_3337,c_3337,c_3245]) ).
tff(c_10753,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_10751]) ).
tff(c_3394,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_3337,c_123]) ).
tff(c_3415,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_3394,c_4]) ).
tff(c_3492,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_3415,c_268]) ).
tff(c_3504,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_3492]) ).
tff(c_3508,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_3504,c_3394]) ).
tff(c_10755,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10753,c_3508]) ).
tff(c_10756,plain,
! [X8_12,X1_10,X2_11] :
( ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_10751]) ).
tff(c_64288,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_10756]) ).
tff(c_64290,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64288,c_3508]) ).
tff(c_64291,plain,
! [X1_10,X8_12] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 ) ),
inference(splitRight,[status(thm)],[c_10756]) ).
tff(c_64293,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_64291]) ).
tff(c_64295,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64293,c_3508]) ).
tff(c_65995,plain,
! [X1_322] :
( ( inverse(X1_322) != sk_c11 )
| ( multiply(X1_322,sk_c11) != identity ) ),
inference(splitRight,[status(thm)],[c_64291]) ).
tff(c_66073,plain,
inverse(sk_c1) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_3391,c_65995]) ).
tff(c_66105,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_135,c_66073]) ).
tff(c_66107,plain,
multiply(sk_c1,sk_c11) != sk_c10,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_66663,plain,
multiply(sk_c1,sk_c11) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_66627,c_66107]) ).
tff(c_66608,plain,
multiply(inverse(sk_c11),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_139,c_66530]) ).
tff(c_10,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_66119,plain,
inverse(sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_66107,c_10]) ).
tff(c_66988,plain,
! [X_337] : ( multiply(inverse(inverse(X_337)),identity) = X_337 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_66530]) ).
tff(c_67006,plain,
multiply(inverse(sk_c11),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_66119,c_66988]) ).
tff(c_67014,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_66608,c_67006]) ).
tff(c_66153,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_66107,c_8]) ).
tff(c_66662,plain,
multiply(sk_c5,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66627,c_66153]) ).
tff(c_67016,plain,
multiply(sk_c1,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_67014,c_66662]) ).
tff(c_67020,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_66663,c_67016]) ).
tff(c_67022,plain,
multiply(sk_c3,sk_c10) != sk_c4,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_67093,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_67022,c_86]) ).
tff(c_88,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( multiply(sk_c3,sk_c10) = sk_c4 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_67077,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_67022,c_88]) ).
tff(c_67021,plain,
inverse(sk_c7) = sk_c9,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_67026,plain,
multiply(sk_c9,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_67021,c_4]) ).
tff(c_67141,plain,
! [Z_340] : ( multiply(sk_c9,multiply(sk_c7,Z_340)) = multiply(identity,Z_340) ),
inference(superposition,[status(thm),theory(equality)],[c_67026,c_67105]) ).
tff(c_67359,plain,
! [Z_351] : ( multiply(sk_c9,multiply(sk_c7,Z_351)) = Z_351 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67141]) ).
tff(c_67371,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_67077,c_67359]) ).
tff(c_67375,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_67093,c_67371]) ).
tff(c_67388,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_67375,c_165]) ).
tff(c_67513,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_67388,c_67477]) ).
tff(c_67578,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_67513]) ).
tff(c_67601,plain,
multiply(sk_c3,identity) != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_67579,c_67022]) ).
tff(c_67799,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67727,c_67578,c_67601]) ).
tff(c_67800,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_80,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c3,sk_c10) = sk_c4 ) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_67047,plain,
inverse(sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_67022,c_80]) ).
tff(c_67051,plain,
multiply(sk_c11,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_67047,c_4]) ).
tff(c_67817,plain,
! [X_355,Y_356,Z_357] : ( multiply(multiply(X_355,Y_356),Z_357) = multiply(X_355,multiply(Y_356,Z_357)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_67844,plain,
! [Z_357] : ( multiply(sk_c11,multiply(sk_c5,Z_357)) = multiply(identity,Z_357) ),
inference(superposition,[status(thm),theory(equality)],[c_67051,c_67817]) ).
tff(c_68052,plain,
! [Z_368] : ( multiply(sk_c11,multiply(sk_c5,Z_368)) = Z_368 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67844]) ).
tff(c_68064,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_67800,c_68052]) ).
tff(c_67868,plain,
! [X_2,Z_357] : ( multiply(inverse(X_2),multiply(X_2,Z_357)) = multiply(identity,Z_357) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_67817]) ).
tff(c_68179,plain,
! [X_370,Z_371] : ( multiply(inverse(X_370),multiply(X_370,Z_371)) = Z_371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67868]) ).
tff(c_68224,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_68064,c_68179]) ).
tff(c_68271,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_68224]) ).
tff(c_68295,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68271,c_127]) ).
tff(c_67882,plain,
! [X_2,Z_357] : ( multiply(inverse(X_2),multiply(X_2,Z_357)) = Z_357 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67868]) ).
tff(c_68410,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_68295,c_67882]) ).
tff(c_68422,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_68410]) ).
tff(c_67806,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_67022,c_86]) ).
tff(c_67850,plain,
! [Z_357] : ( multiply(sk_c9,multiply(sk_c7,Z_357)) = multiply(identity,Z_357) ),
inference(superposition,[status(thm),theory(equality)],[c_67026,c_67817]) ).
tff(c_68075,plain,
! [Z_369] : ( multiply(sk_c9,multiply(sk_c7,Z_369)) = Z_369 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_67850]) ).
tff(c_68087,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_67077,c_68075]) ).
tff(c_68091,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_67806,c_68087]) ).
tff(c_68105,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_68091,c_165]) ).
tff(c_68200,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_68105,c_68179]) ).
tff(c_68268,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_68200]) ).
tff(c_68277,plain,
multiply(sk_c3,sk_c10) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_68268,c_67022]) ).
tff(c_68438,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68422,c_68271,c_68277]) ).
tff(c_68439,plain,
inverse(sk_c5) = sk_c11,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_68440,plain,
multiply(sk_c2,sk_c9) != sk_c10,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_36,plain,
( ( multiply(sk_c5,sk_c11) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_70009,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_68440,c_36]) ).
tff(c_70640,plain,
! [X_413,Y_414,Z_415] : ( multiply(multiply(X_413,Y_414),Z_415) = multiply(X_413,multiply(Y_414,Z_415)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_70688,plain,
! [X_2,Z_415] : ( multiply(inverse(X_2),multiply(X_2,Z_415)) = multiply(identity,Z_415) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_70640]) ).
tff(c_70899,plain,
! [X_424,Z_425] : ( multiply(inverse(X_424),multiply(X_424,Z_425)) = Z_425 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70688]) ).
tff(c_70950,plain,
multiply(inverse(sk_c5),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_70009,c_70899]) ).
tff(c_70981,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_68439,c_70950]) ).
tff(c_70702,plain,
! [X_2,Z_415] : ( multiply(inverse(X_2),multiply(X_2,Z_415)) = Z_415 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70688]) ).
tff(c_70993,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_70981,c_70702]) ).
tff(c_70999,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_70993]) ).
tff(c_16,plain,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_70014,plain,
multiply(sk_c1,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_70049,plain,
! [X_398,Y_399,Z_400] : ( multiply(multiply(X_398,Y_399),Z_400) = multiply(X_398,multiply(Y_399,Z_400)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_70094,plain,
! [Z_400] : ( multiply(sk_c11,multiply(sk_c1,Z_400)) = multiply(identity,Z_400) ),
inference(superposition,[status(thm),theory(equality)],[c_139,c_70049]) ).
tff(c_70236,plain,
! [Z_408] : ( multiply(sk_c11,multiply(sk_c1,Z_408)) = Z_408 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70094]) ).
tff(c_70248,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_70014,c_70236]) ).
tff(c_70100,plain,
! [X_2,Z_400] : ( multiply(inverse(X_2),multiply(X_2,Z_400)) = multiply(identity,Z_400) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_70049]) ).
tff(c_70405,plain,
! [X_411,Z_412] : ( multiply(inverse(X_411),multiply(X_411,Z_412)) = Z_412 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70100]) ).
tff(c_70459,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_70248,c_70405]) ).
tff(c_70508,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_70459]) ).
tff(c_69194,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_68440,c_36]) ).
tff(c_68444,plain,
multiply(sk_c11,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68439,c_4]) ).
tff(c_69220,plain,
! [X_384,Y_385,Z_386] : ( multiply(multiply(X_384,Y_385),Z_386) = multiply(X_384,multiply(Y_385,Z_386)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_69256,plain,
! [Z_386] : ( multiply(sk_c11,multiply(sk_c5,Z_386)) = multiply(identity,Z_386) ),
inference(superposition,[status(thm),theory(equality)],[c_68444,c_69220]) ).
tff(c_69489,plain,
! [Z_391] : ( multiply(sk_c11,multiply(sk_c5,Z_391)) = Z_391 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69256]) ).
tff(c_69501,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_69194,c_69489]) ).
tff(c_69271,plain,
! [X_2,Z_386] : ( multiply(inverse(X_2),multiply(X_2,Z_386)) = multiply(identity,Z_386) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_69220]) ).
tff(c_69529,plain,
! [X_393,Z_394] : ( multiply(inverse(X_393),multiply(X_393,Z_394)) = Z_394 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69271]) ).
tff(c_69550,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_69501,c_69529]) ).
tff(c_69626,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_69550]) ).
tff(c_68455,plain,
multiply(sk_c3,sk_c10) = sk_c4,
inference(splitLeft,[status(thm)],[c_90]) ).
tff(c_69268,plain,
! [Z_386] : ( multiply(sk_c10,multiply(sk_c3,Z_386)) = multiply(identity,Z_386) ),
inference(superposition,[status(thm),theory(equality)],[c_127,c_69220]) ).
tff(c_69313,plain,
! [Z_389] : ( multiply(sk_c10,multiply(sk_c3,Z_389)) = Z_389 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69268]) ).
tff(c_69325,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_68455,c_69313]) ).
tff(c_69395,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69325,c_165]) ).
tff(c_69413,plain,
inverse(sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69395,c_150]) ).
tff(c_69654,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69626,c_69413]) ).
tff(c_69735,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69654,c_4]) ).
tff(c_69285,plain,
! [X_2,Z_386] : ( multiply(inverse(X_2),multiply(X_2,Z_386)) = Z_386 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69271]) ).
tff(c_69858,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_69735,c_69285]) ).
tff(c_69870,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_69858]) ).
tff(c_69411,plain,
multiply(sk_c2,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_69395,c_68440]) ).
tff(c_69649,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_69626,c_69626,c_69411]) ).
tff(c_69968,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69870,c_69649]) ).
tff(c_69970,plain,
multiply(sk_c3,sk_c10) != sk_c4,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_70028,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_69970,c_86]) ).
tff(c_70019,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_69970,c_88]) ).
tff(c_69969,plain,
inverse(sk_c7) = sk_c9,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_69974,plain,
multiply(sk_c9,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_69969,c_4]) ).
tff(c_70082,plain,
! [Z_400] : ( multiply(sk_c9,multiply(sk_c7,Z_400)) = multiply(identity,Z_400) ),
inference(superposition,[status(thm),theory(equality)],[c_69974,c_70049]) ).
tff(c_70303,plain,
! [Z_410] : ( multiply(sk_c9,multiply(sk_c7,Z_410)) = Z_410 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70082]) ).
tff(c_70315,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_70019,c_70303]) ).
tff(c_70319,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_70028,c_70315]) ).
tff(c_70332,plain,
inverse(sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_70319,c_150]) ).
tff(c_70356,plain,
multiply(sk_c10,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_70332,c_4]) ).
tff(c_70548,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70508,c_70356]) ).
tff(c_70329,plain,
multiply(sk_c2,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_70319,c_68440]) ).
tff(c_70603,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70548,c_70508,c_70508,c_70329]) ).
tff(c_70604,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_70613,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_69970,c_88]) ).
tff(c_70670,plain,
! [Z_415] : ( multiply(sk_c9,multiply(sk_c7,Z_415)) = multiply(identity,Z_415) ),
inference(superposition,[status(thm),theory(equality)],[c_69974,c_70640]) ).
tff(c_70804,plain,
! [Z_423] : ( multiply(sk_c9,multiply(sk_c7,Z_423)) = Z_423 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70670]) ).
tff(c_70816,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_70613,c_70804]) ).
tff(c_70820,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_70604,c_70816]) ).
tff(c_70833,plain,
inverse(sk_c2) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_70820,c_150]) ).
tff(c_70843,plain,
multiply(sk_c10,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_70833,c_4]) ).
tff(c_71019,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70999,c_70843]) ).
tff(c_70830,plain,
multiply(sk_c2,sk_c10) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_70820,c_68440]) ).
tff(c_71129,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71019,c_70999,c_70999,c_70830]) ).
tff(c_71131,plain,
multiply(sk_c10,sk_c4) != sk_c9,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_95356,plain,
sk_c9 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_95352,c_71131]) ).
tff(c_71188,plain,
multiply(sk_c1,sk_c11) = sk_c10,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_71515,plain,
! [X_438,Y_439,Z_440] : ( multiply(multiply(X_438,Y_439),Z_440) = multiply(X_438,multiply(Y_439,Z_440)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_71560,plain,
! [Z_440] : ( multiply(sk_c11,multiply(sk_c1,Z_440)) = multiply(identity,Z_440) ),
inference(superposition,[status(thm),theory(equality)],[c_139,c_71515]) ).
tff(c_71679,plain,
! [Z_446] : ( multiply(sk_c11,multiply(sk_c1,Z_446)) = Z_446 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71560]) ).
tff(c_71691,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_71188,c_71679]) ).
tff(c_71566,plain,
! [X_2,Z_440] : ( multiply(inverse(X_2),multiply(X_2,Z_440)) = multiply(identity,Z_440) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_71515]) ).
tff(c_72880,plain,
! [X_466,Z_467] : ( multiply(inverse(X_466),multiply(X_466,Z_467)) = Z_467 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71566]) ).
tff(c_72919,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_71691,c_72880]) ).
tff(c_72964,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_72919]) ).
tff(c_72981,plain,
multiply(sk_c1,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_72964,c_71188]) ).
tff(c_71580,plain,
! [X_2,Z_440] : ( multiply(inverse(X_2),multiply(X_2,Z_440)) = Z_440 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71566]) ).
tff(c_73284,plain,
! [X_471,Z_472] : ( multiply(inverse(inverse(X_471)),Z_472) = multiply(X_471,Z_472) ),
inference(superposition,[status(thm),theory(equality)],[c_72880,c_71580]) ).
tff(c_72955,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_72880]) ).
tff(c_73294,plain,
! [X_471] : ( multiply(X_471,identity) = X_471 ),
inference(superposition,[status(thm),theory(equality)],[c_73284,c_72955]) ).
tff(c_72022,plain,
! [X_454,Z_455] : ( multiply(inverse(X_454),multiply(X_454,Z_455)) = Z_455 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71566]) ).
tff(c_72498,plain,
! [X_459,Z_460] : ( multiply(inverse(inverse(X_459)),Z_460) = multiply(X_459,Z_460) ),
inference(superposition,[status(thm),theory(equality)],[c_72022,c_71580]) ).
tff(c_72115,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_72022]) ).
tff(c_72508,plain,
! [X_459] : ( multiply(X_459,identity) = X_459 ),
inference(superposition,[status(thm),theory(equality)],[c_72498,c_72115]) ).
tff(c_72079,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_71691,c_72022]) ).
tff(c_72128,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_72079]) ).
tff(c_71193,plain,
multiply(sk_c3,sk_c10) = sk_c4,
inference(splitLeft,[status(thm)],[c_86]) ).
tff(c_71232,plain,
! [X_427,Y_428,Z_429] : ( multiply(multiply(X_427,Y_428),Z_429) = multiply(X_427,multiply(Y_428,Z_429)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_71283,plain,
! [Z_429] : ( multiply(sk_c10,multiply(sk_c3,Z_429)) = multiply(identity,Z_429) ),
inference(superposition,[status(thm),theory(equality)],[c_127,c_71232]) ).
tff(c_71397,plain,
! [Z_434] : ( multiply(sk_c10,multiply(sk_c3,Z_434)) = Z_434 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71283]) ).
tff(c_71409,plain,
multiply(sk_c10,sk_c4) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_71193,c_71397]) ).
tff(c_71413,plain,
sk_c9 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_71409,c_71131]) ).
tff(c_72,plain,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_71198,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_71131,c_72]) ).
tff(c_74,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_71221,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_71131,c_74]) ).
tff(c_71130,plain,
inverse(sk_c7) = sk_c9,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_71135,plain,
multiply(sk_c9,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_71130,c_4]) ).
tff(c_71274,plain,
! [Z_429] : ( multiply(sk_c9,multiply(sk_c7,Z_429)) = multiply(identity,Z_429) ),
inference(superposition,[status(thm),theory(equality)],[c_71135,c_71232]) ).
tff(c_71456,plain,
! [Z_437] : ( multiply(sk_c9,multiply(sk_c7,Z_437)) = Z_437 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71274]) ).
tff(c_71468,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_71221,c_71456]) ).
tff(c_71472,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_71198,c_71468]) ).
tff(c_71474,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_71413,c_71472]) ).
tff(c_71475,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(splitRight,[status(thm)],[c_86]) ).
tff(c_71506,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_71131,c_74]) ).
tff(c_71554,plain,
! [Z_440] : ( multiply(sk_c9,multiply(sk_c7,Z_440)) = multiply(identity,Z_440) ),
inference(superposition,[status(thm),theory(equality)],[c_71135,c_71515]) ).
tff(c_71871,plain,
! [Z_452] : ( multiply(sk_c9,multiply(sk_c7,Z_452)) = Z_452 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71554]) ).
tff(c_71883,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_71506,c_71871]) ).
tff(c_71887,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_71475,c_71883]) ).
tff(c_71563,plain,
! [Z_440] : ( multiply(sk_c10,multiply(sk_c3,Z_440)) = multiply(identity,Z_440) ),
inference(superposition,[status(thm),theory(equality)],[c_127,c_71515]) ).
tff(c_71579,plain,
! [Z_440] : ( multiply(sk_c10,multiply(sk_c3,Z_440)) = Z_440 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71563]) ).
tff(c_71720,plain,
! [Z_448] : ( multiply(sk_c9,multiply(sk_c7,Z_448)) = Z_448 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_71554]) ).
tff(c_71732,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_71506,c_71720]) ).
tff(c_71736,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_71475,c_71732]) ).
tff(c_66,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_71145,plain,
inverse(sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_71131,c_66]) ).
tff(c_64,plain,
( ( multiply(sk_c5,sk_c11) = sk_c10 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_71481,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_71131,c_64]) ).
tff(c_71619,plain,
! [X5_443] :
( ( inverse(X5_443) != sk_c11 )
| ( multiply(X5_443,sk_c11) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_106]) ).
tff(c_71626,plain,
inverse(sk_c5) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_71481,c_71619]) ).
tff(c_71641,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_71145,c_71626]) ).
tff(c_71642,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c9 )
| ( multiply(X6_7,sk_c9) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c9 )
| ( multiply(X2_11,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(sk_c9,multiply(X4_13,sk_c9)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_106]) ).
tff(c_71702,plain,
! [X4_13] :
( ( inverse(X4_13) != sk_c9 )
| ( multiply(sk_c9,multiply(X4_13,sk_c9)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_71642]) ).
tff(c_71824,plain,
! [X4_450] :
( ( inverse(X4_450) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_450,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_71736,c_71736,c_71736,c_71702]) ).
tff(c_71834,plain,
inverse(sk_c3) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_71579,c_71824]) ).
tff(c_71852,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_123,c_71834]) ).
tff(c_71853,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != sk_c9 )
| ( multiply(X2_11,sk_c9) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( multiply(X6_7,sk_c9) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_71642]) ).
tff(c_71974,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_71887,c_71887,c_71887,c_71887,c_71887,c_71853]) ).
tff(c_71975,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_71974]) ).
tff(c_72876,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_72508,c_72128,c_72128,c_72128,c_71975]) ).
tff(c_71899,plain,
inverse(sk_c7) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_71887,c_71130]) ).
tff(c_71955,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_71899,c_4]) ).
tff(c_72167,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72128,c_71955]) ).
tff(c_72143,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_72128,c_71899]) ).
tff(c_72224,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_72167,c_72143]) ).
tff(c_72878,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72876,c_72224]) ).
tff(c_72879,plain,
! [X8_12,X1_10,X2_11] :
( ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_71974]) ).
tff(c_80730,plain,
! [X8_12,X1_10,X2_11] :
( ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_73294,c_72964,c_72964,c_72964,c_72964,c_73294,c_72964,c_72964,c_2,c_72964,c_72964,c_72879]) ).
tff(c_80732,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_80730]) ).
tff(c_73003,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_72964,c_71955]) ).
tff(c_72972,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_72964,c_71899]) ).
tff(c_73018,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_73003,c_72972]) ).
tff(c_80734,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_80732,c_73018]) ).
tff(c_80735,plain,
! [X1_10,X8_12] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 ) ),
inference(splitRight,[status(thm)],[c_80730]) ).
tff(c_95056,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_80735]) ).
tff(c_95058,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_95056,c_73018]) ).
tff(c_95060,plain,
! [X1_603] :
( ( inverse(X1_603) != sk_c11 )
| ( multiply(X1_603,sk_c11) != identity ) ),
inference(splitRight,[status(thm)],[c_80735]) ).
tff(c_95112,plain,
inverse(sk_c1) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_72981,c_95060]) ).
tff(c_95139,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_135,c_95112]) ).
tff(c_95141,plain,
multiply(sk_c1,sk_c11) != sk_c10,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_95156,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_95141,c_16]) ).
tff(c_95151,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_71131,c_74]) ).
tff(c_95217,plain,
! [Z_606] : ( multiply(sk_c9,multiply(sk_c7,Z_606)) = multiply(identity,Z_606) ),
inference(superposition,[status(thm),theory(equality)],[c_71135,c_95181]) ).
tff(c_95452,plain,
! [Z_616] : ( multiply(sk_c9,multiply(sk_c7,Z_616)) = Z_616 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_95217]) ).
tff(c_95464,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_95151,c_95452]) ).
tff(c_95468,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_95156,c_95464]) ).
tff(c_95470,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_95356,c_95468]) ).
tff(c_95471,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(splitRight,[status(thm)],[c_86]) ).
tff(c_95473,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_71131,c_74]) ).
tff(c_95507,plain,
! [X_617,Y_618,Z_619] : ( multiply(multiply(X_617,Y_618),Z_619) = multiply(X_617,multiply(Y_618,Z_619)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_95540,plain,
! [Z_619] : ( multiply(sk_c9,multiply(sk_c7,Z_619)) = multiply(identity,Z_619) ),
inference(superposition,[status(thm),theory(equality)],[c_71135,c_95507]) ).
tff(c_95717,plain,
! [Z_627] : ( multiply(sk_c9,multiply(sk_c7,Z_627)) = Z_627 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_95540]) ).
tff(c_95729,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_95473,c_95717]) ).
tff(c_95733,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_95471,c_95729]) ).
tff(c_12,plain,
( ( multiply(sk_c6,sk_c9) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_95487,plain,
multiply(sk_c6,sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_95141,c_12]) ).
tff(c_70,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_71158,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_71131,c_70]) ).
tff(c_71162,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_71158,c_4]) ).
tff(c_95534,plain,
! [Z_619] : ( multiply(sk_c9,multiply(sk_c6,Z_619)) = multiply(identity,Z_619) ),
inference(superposition,[status(thm),theory(equality)],[c_71162,c_95507]) ).
tff(c_95694,plain,
! [Z_626] : ( multiply(sk_c9,multiply(sk_c6,Z_626)) = Z_626 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_95534]) ).
tff(c_95706,plain,
multiply(sk_c9,sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_95487,c_95694]) ).
tff(c_95777,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_95733,c_95733,c_95706]) ).
tff(c_95552,plain,
! [X_2,Z_619] : ( multiply(inverse(X_2),multiply(X_2,Z_619)) = multiply(identity,Z_619) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_95507]) ).
tff(c_95871,plain,
! [X_629,Z_630] : ( multiply(inverse(X_629),multiply(X_629,Z_630)) = Z_630 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_95552]) ).
tff(c_95901,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_95777,c_95871]) ).
tff(c_95957,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_95901]) ).
tff(c_95977,plain,
multiply(sk_c1,sk_c11) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_95957,c_95141]) ).
tff(c_95140,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_95531,plain,
! [Z_619] : ( multiply(sk_c5,multiply(sk_c11,Z_619)) = multiply(sk_c10,Z_619) ),
inference(superposition,[status(thm),theory(equality)],[c_95140,c_95507]) ).
tff(c_96044,plain,
! [Z_631] : ( multiply(sk_c5,multiply(sk_c11,Z_631)) = Z_631 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_95957,c_95531]) ).
tff(c_96065,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_139,c_96044]) ).
tff(c_71149,plain,
multiply(sk_c11,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_71145,c_4]) ).
tff(c_96062,plain,
multiply(sk_c5,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_71149,c_96044]) ).
tff(c_96207,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_96065,c_96062]) ).
tff(c_95978,plain,
multiply(sk_c5,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_95957,c_95140]) ).
tff(c_96222,plain,
multiply(sk_c1,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_96207,c_95978]) ).
tff(c_96227,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_95977,c_96222]) ).
tff(c_96229,plain,
inverse(sk_c2) != sk_c9,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_50,plain,
( ( multiply(sk_c5,sk_c11) = sk_c10 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_96266,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_96229,c_50]) ).
tff(c_52,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_96237,plain,
inverse(sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_96229,c_52]) ).
tff(c_96241,plain,
multiply(sk_c11,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_96237,c_4]) ).
tff(c_96322,plain,
! [X_632,Y_633,Z_634] : ( multiply(multiply(X_632,Y_633),Z_634) = multiply(X_632,multiply(Y_633,Z_634)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_96352,plain,
! [Z_634] : ( multiply(sk_c11,multiply(sk_c5,Z_634)) = multiply(identity,Z_634) ),
inference(superposition,[status(thm),theory(equality)],[c_96241,c_96322]) ).
tff(c_99475,plain,
! [Z_679] : ( multiply(sk_c11,multiply(sk_c5,Z_679)) = Z_679 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_96352]) ).
tff(c_99487,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_96266,c_99475]) ).
tff(c_96364,plain,
! [X_2,Z_634] : ( multiply(inverse(X_2),multiply(X_2,Z_634)) = multiply(identity,Z_634) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_96322]) ).
tff(c_99554,plain,
! [X_683,Z_684] : ( multiply(inverse(X_683),multiply(X_683,Z_684)) = Z_684 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_96364]) ).
tff(c_99581,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_99487,c_99554]) ).
tff(c_99649,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_99581]) ).
tff(c_96346,plain,
! [Z_634] : ( multiply(sk_c5,multiply(sk_c11,Z_634)) = multiply(sk_c10,Z_634) ),
inference(superposition,[status(thm),theory(equality)],[c_96266,c_96322]) ).
tff(c_99760,plain,
! [Z_686] : ( multiply(sk_c5,multiply(sk_c11,Z_686)) = Z_686 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_99649,c_96346]) ).
tff(c_99787,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_139,c_99760]) ).
tff(c_99784,plain,
multiply(sk_c5,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_96241,c_99760]) ).
tff(c_99966,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_99787,c_99784]) ).
tff(c_99675,plain,
multiply(sk_c5,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_99649,c_96266]) ).
tff(c_99984,plain,
multiply(sk_c1,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_99966,c_99675]) ).
tff(c_96377,plain,
! [X_2,Z_634] : ( multiply(inverse(X_2),multiply(X_2,Z_634)) = Z_634 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_96364]) ).
tff(c_100081,plain,
! [X_689,Z_690] : ( multiply(inverse(inverse(X_689)),Z_690) = multiply(X_689,Z_690) ),
inference(superposition,[status(thm),theory(equality)],[c_99554,c_96377]) ).
tff(c_99641,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_99554]) ).
tff(c_100091,plain,
! [X_689] : ( multiply(X_689,identity) = X_689 ),
inference(superposition,[status(thm),theory(equality)],[c_100081,c_99641]) ).
tff(c_96625,plain,
! [X_643,Z_644] : ( multiply(inverse(X_643),multiply(X_643,Z_644)) = Z_644 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_96364]) ).
tff(c_97152,plain,
! [X_649,Z_650] : ( multiply(inverse(inverse(X_649)),Z_650) = multiply(X_649,Z_650) ),
inference(superposition,[status(thm),theory(equality)],[c_96625,c_96377]) ).
tff(c_96712,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_96625]) ).
tff(c_97162,plain,
! [X_649] : ( multiply(X_649,identity) = X_649 ),
inference(superposition,[status(thm),theory(equality)],[c_97152,c_96712]) ).
tff(c_96546,plain,
! [Z_639] : ( multiply(sk_c11,multiply(sk_c5,Z_639)) = Z_639 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_96352]) ).
tff(c_96558,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_96266,c_96546]) ).
tff(c_96652,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_96558,c_96625]) ).
tff(c_96720,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_96652]) ).
tff(c_58,plain,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_96275,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_96229,c_58]) ).
tff(c_60,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_96293,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_96229,c_60]) ).
tff(c_96228,plain,
inverse(sk_c7) = sk_c9,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_96233,plain,
multiply(sk_c9,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_96228,c_4]) ).
tff(c_96355,plain,
! [Z_634] : ( multiply(sk_c9,multiply(sk_c7,Z_634)) = multiply(identity,Z_634) ),
inference(superposition,[status(thm),theory(equality)],[c_96233,c_96322]) ).
tff(c_96405,plain,
! [Z_637] : ( multiply(sk_c9,multiply(sk_c7,Z_637)) = Z_637 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_96355]) ).
tff(c_96417,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_96293,c_96405]) ).
tff(c_96421,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_96275,c_96417]) ).
tff(c_96457,plain,
! [X5_638] :
( ( inverse(X5_638) != sk_c11 )
| ( multiply(X5_638,sk_c11) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_106]) ).
tff(c_96464,plain,
inverse(sk_c5) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_96266,c_96457]) ).
tff(c_96476,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_96237,c_96464]) ).
tff(c_96477,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c9 )
| ( multiply(X6_7,sk_c9) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c9 )
| ( multiply(X2_11,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(sk_c9,multiply(X4_13,sk_c9)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_106]) ).
tff(c_96536,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_96421,c_96421,c_96421,c_96421,c_96421,c_96421,c_96421,c_96421,c_96477]) ).
tff(c_96537,plain,
! [X4_13] :
( ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_96536]) ).
tff(c_99463,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_97162,c_96720,c_96720,c_2,c_96720,c_96720,c_96537]) ).
tff(c_96747,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_96720,c_127]) ).
tff(c_96883,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_96747,c_96377]) ).
tff(c_96895,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_96883]) ).
tff(c_96748,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_96720,c_123]) ).
tff(c_96899,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_96895,c_96748]) ).
tff(c_99465,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_99463,c_96899]) ).
tff(c_99466,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_96536]) ).
tff(c_106942,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_100091,c_99649,c_99649,c_99649,c_100091,c_99649,c_99649,c_2,c_99649,c_99649,c_99649,c_100091,c_99649,c_99649,c_99649,c_99466]) ).
tff(c_106944,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_106942]) ).
tff(c_99676,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_99649,c_127]) ).
tff(c_99812,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_99676,c_96377]) ).
tff(c_99824,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_99812]) ).
tff(c_99677,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_99649,c_123]) ).
tff(c_99828,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_99824,c_99677]) ).
tff(c_106946,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_106944,c_99828]) ).
tff(c_106947,plain,
! [X8_12,X1_10,X2_11] :
( ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_106942]) ).
tff(c_159209,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_106947]) ).
tff(c_159211,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_159209,c_99828]) ).
tff(c_159212,plain,
! [X1_10,X8_12] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 ) ),
inference(splitRight,[status(thm)],[c_106947]) ).
tff(c_159214,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_159212]) ).
tff(c_159216,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_159214,c_99828]) ).
tff(c_160834,plain,
! [X1_939] :
( ( inverse(X1_939) != sk_c11 )
| ( multiply(X1_939,sk_c11) != identity ) ),
inference(splitRight,[status(thm)],[c_159212]) ).
tff(c_160912,plain,
inverse(sk_c1) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_99984,c_160834]) ).
tff(c_160944,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_135,c_160912]) ).
tff(c_160946,plain,
inverse(sk_c1) != sk_c11,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_160960,plain,
inverse(sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_160946,c_24]) ).
tff(c_22,plain,
( ( multiply(sk_c5,sk_c11) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_161025,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_160946,c_22]) ).
tff(c_161054,plain,
! [X_940,Y_941,Z_942] : ( multiply(multiply(X_940,Y_941),Z_942) = multiply(X_940,multiply(Y_941,Z_942)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_161096,plain,
! [X_2,Z_942] : ( multiply(inverse(X_2),multiply(X_2,Z_942)) = multiply(identity,Z_942) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_161054]) ).
tff(c_162288,plain,
! [X_963,Z_964] : ( multiply(inverse(X_963),multiply(X_963,Z_964)) = Z_964 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161096]) ).
tff(c_162333,plain,
multiply(inverse(sk_c5),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_161025,c_162288]) ).
tff(c_162358,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_160960,c_162333]) ).
tff(c_161109,plain,
! [X_2,Z_942] : ( multiply(inverse(X_2),multiply(X_2,Z_942)) = Z_942 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161096]) ).
tff(c_162368,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_162358,c_161109]) ).
tff(c_162374,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_162368]) ).
tff(c_162384,plain,
multiply(sk_c5,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_162374,c_161025]) ).
tff(c_162688,plain,
! [X_969,Z_970] : ( multiply(inverse(inverse(X_969)),Z_970) = multiply(X_969,Z_970) ),
inference(superposition,[status(thm),theory(equality)],[c_162288,c_161109]) ).
tff(c_162348,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_162288]) ).
tff(c_162695,plain,
! [X_969] : ( multiply(X_969,identity) = X_969 ),
inference(superposition,[status(thm),theory(equality)],[c_162688,c_162348]) ).
tff(c_161187,plain,
! [X_944,Z_945] : ( multiply(inverse(X_944),multiply(X_944,Z_945)) = Z_945 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161096]) ).
tff(c_161226,plain,
multiply(inverse(sk_c5),sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_161025,c_161187]) ).
tff(c_161250,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_160960,c_161226]) ).
tff(c_161254,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_161250,c_161109]) ).
tff(c_161260,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_161254]) ).
tff(c_161270,plain,
multiply(sk_c5,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_161260,c_161025]) ).
tff(c_30,plain,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_161002,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_160946,c_30]) ).
tff(c_32,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_161013,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_160946,c_32]) ).
tff(c_34,plain,
( ( inverse(sk_c7) = sk_c9 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_160986,plain,
inverse(sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_160946,c_34]) ).
tff(c_160990,plain,
multiply(sk_c9,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_160986,c_4]) ).
tff(c_161081,plain,
! [Z_942] : ( multiply(sk_c9,multiply(sk_c7,Z_942)) = multiply(identity,Z_942) ),
inference(superposition,[status(thm),theory(equality)],[c_160990,c_161054]) ).
tff(c_161111,plain,
! [Z_943] : ( multiply(sk_c9,multiply(sk_c7,Z_943)) = Z_943 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161081]) ).
tff(c_161123,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_161013,c_161111]) ).
tff(c_161127,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_161002,c_161123]) ).
tff(c_161149,plain,
! [X5_6,X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 )
| ( inverse(X5_6) != sk_c11 )
| ( multiply(X5_6,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_161127,c_161127,c_161127,c_161127,c_161127,c_161127,c_161127,c_161127,c_106]) ).
tff(c_161150,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c11 )
| ( multiply(X5_6,sk_c11) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_161149]) ).
tff(c_162210,plain,
! [X5_962] :
( ( inverse(X5_962) != sk_c11 )
| ( multiply(X5_962,sk_c11) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_161260,c_161150]) ).
tff(c_162217,plain,
inverse(sk_c5) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_161270,c_162210]) ).
tff(c_162234,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_160960,c_162217]) ).
tff(c_162235,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_161149]) ).
tff(c_169886,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X4_13) != identity )
| ( identity != X4_13 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_162695,c_162374,c_162374,c_2,c_162374,c_162374,c_162695,c_162374,c_162374,c_162374,c_162374,c_162695,c_162374,c_162374,c_2,c_162374,c_162374,c_162695,c_162374,c_162374,c_162374,c_162235]) ).
tff(c_169888,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_169886]) ).
tff(c_161133,plain,
inverse(sk_c7) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_161127,c_160986]) ).
tff(c_161145,plain,
multiply(sk_c10,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_161133,c_4]) ).
tff(c_162391,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_162374,c_161145]) ).
tff(c_162382,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_162374,c_161133]) ).
tff(c_162420,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_162391,c_162382]) ).
tff(c_169890,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_169888,c_162420]) ).
tff(c_169891,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(splitRight,[status(thm)],[c_169886]) ).
tff(c_170213,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_169891]) ).
tff(c_170215,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_170213,c_162420]) ).
tff(c_170216,plain,
! [X8_12,X1_10,X2_11] :
( ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_169891]) ).
tff(c_170937,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_170216]) ).
tff(c_170939,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_170937,c_162420]) ).
tff(c_170940,plain,
! [X1_10,X8_12] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 ) ),
inference(splitRight,[status(thm)],[c_170216]) ).
tff(c_171217,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_170940]) ).
tff(c_171219,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_171217,c_162420]) ).
tff(c_171221,plain,
! [X1_1049] :
( ( inverse(X1_1049) != sk_c11 )
| ( multiply(X1_1049,sk_c11) != identity ) ),
inference(splitRight,[status(thm)],[c_170940]) ).
tff(c_171249,plain,
inverse(sk_c5) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_162384,c_171221]) ).
tff(c_171270,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_160960,c_171249]) ).
tff(c_171272,plain,
inverse(sk_c3) != sk_c10,
inference(splitRight,[status(thm)],[c_98]) ).
tff(c_94,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_171324,plain,
inverse(sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_171272,c_94]) ).
tff(c_171328,plain,
multiply(sk_c11,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_171324,c_4]) ).
tff(c_173921,plain,
multiply(inverse(sk_c11),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_171328,c_173849]) ).
tff(c_174228,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_173927,c_173921]) ).
tff(c_92,plain,
( ( multiply(sk_c5,sk_c11) = sk_c10 )
| ( inverse(sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_171346,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_171272,c_92]) ).
tff(c_171419,plain,
! [Z_1052] : ( multiply(sk_c11,multiply(sk_c5,Z_1052)) = multiply(identity,Z_1052) ),
inference(superposition,[status(thm),theory(equality)],[c_171328,c_171392]) ).
tff(c_171449,plain,
! [Z_1053] : ( multiply(sk_c11,multiply(sk_c5,Z_1053)) = Z_1053 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_171419]) ).
tff(c_171461,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_171346,c_171449]) ).
tff(c_173909,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_171461,c_173849]) ).
tff(c_173947,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_173909]) ).
tff(c_173970,plain,
multiply(sk_c5,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_173947,c_171346]) ).
tff(c_174240,plain,
multiply(sk_c1,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_174228,c_173970]) ).
tff(c_171447,plain,
! [X_2,Z_1052] : ( multiply(inverse(X_2),multiply(X_2,Z_1052)) = Z_1052 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_171434]) ).
tff(c_174356,plain,
! [X_1098,Z_1099] : ( multiply(inverse(inverse(X_1098)),Z_1099) = multiply(X_1098,Z_1099) ),
inference(superposition,[status(thm),theory(equality)],[c_171447,c_173849]) ).
tff(c_173933,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_173849]) ).
tff(c_174366,plain,
! [X_1098] : ( multiply(X_1098,identity) = X_1098 ),
inference(superposition,[status(thm),theory(equality)],[c_174356,c_173933]) ).
tff(c_171706,plain,
! [X_1060,Z_1061] : ( multiply(inverse(X_1060),multiply(X_1060,Z_1061)) = Z_1061 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_171434]) ).
tff(c_172213,plain,
! [X_1066,Z_1067] : ( multiply(inverse(inverse(X_1066)),Z_1067) = multiply(X_1066,Z_1067) ),
inference(superposition,[status(thm),theory(equality)],[c_171447,c_171706]) ).
tff(c_171790,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_171706]) ).
tff(c_172223,plain,
! [X_1066] : ( multiply(X_1066,identity) = X_1066 ),
inference(superposition,[status(thm),theory(equality)],[c_172213,c_171790]) ).
tff(c_171766,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_171461,c_171706]) ).
tff(c_171804,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_171766]) ).
tff(c_100,plain,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( inverse(sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_203]) ).
tff(c_171362,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_171272,c_100]) ).
tff(c_102,plain,
( ( multiply(sk_c7,sk_c9) = sk_c8 )
| ( inverse(sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_206]) ).
tff(c_171354,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_171272,c_102]) ).
tff(c_104,plain,
( ( inverse(sk_c7) = sk_c9 )
| ( inverse(sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_171297,plain,
inverse(sk_c7) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_171272,c_104]) ).
tff(c_171301,plain,
multiply(sk_c9,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_171297,c_4]) ).
tff(c_171425,plain,
! [Z_1052] : ( multiply(sk_c9,multiply(sk_c7,Z_1052)) = multiply(identity,Z_1052) ),
inference(superposition,[status(thm),theory(equality)],[c_171301,c_171392]) ).
tff(c_171472,plain,
! [Z_1054] : ( multiply(sk_c9,multiply(sk_c7,Z_1054)) = Z_1054 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_171425]) ).
tff(c_171484,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_171354,c_171472]) ).
tff(c_171488,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_171362,c_171484]) ).
tff(c_171532,plain,
! [X5_1055] :
( ( inverse(X5_1055) != sk_c11 )
| ( multiply(X5_1055,sk_c11) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_106]) ).
tff(c_171539,plain,
inverse(sk_c5) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_171346,c_171532]) ).
tff(c_171551,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_171324,c_171539]) ).
tff(c_171552,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c9 )
| ( multiply(X6_7,sk_c9) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c9 )
| ( multiply(X2_11,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(sk_c9,multiply(X4_13,sk_c9)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_106]) ).
tff(c_171625,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_171488,c_171488,c_171488,c_171488,c_171488,c_171488,c_171488,c_171488,c_171552]) ).
tff(c_171626,plain,
! [X4_13] :
( ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_171625]) ).
tff(c_173766,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_172223,c_171804,c_171804,c_2,c_171804,c_171804,c_171626]) ).
tff(c_171558,plain,
inverse(sk_c7) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_171488,c_171297]) ).
tff(c_171824,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_171804,c_171558]) ).
tff(c_171891,plain,
multiply(identity,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_171824,c_4]) ).
tff(c_171941,plain,
multiply(inverse(identity),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_171891,c_171447]) ).
tff(c_171953,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_171941]) ).
tff(c_171958,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_171953,c_171824]) ).
tff(c_173768,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_173766,c_171958]) ).
tff(c_173769,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_171625]) ).
tff(c_180128,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_174366,c_173947,c_173947,c_173947,c_174366,c_173947,c_173947,c_2,c_173947,c_173947,c_173947,c_174366,c_173947,c_173947,c_173947,c_173769]) ).
tff(c_180130,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_180128]) ).
tff(c_173967,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_173947,c_171558]) ).
tff(c_174034,plain,
multiply(identity,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_173967,c_4]) ).
tff(c_174084,plain,
multiply(inverse(identity),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_174034,c_171447]) ).
tff(c_174096,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_174084]) ).
tff(c_174101,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_174096,c_173967]) ).
tff(c_180132,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_180130,c_174101]) ).
tff(c_180133,plain,
! [X8_12,X1_10,X2_11] :
( ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_180128]) ).
tff(c_243474,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_180133]) ).
tff(c_243476,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_243474,c_174101]) ).
tff(c_243477,plain,
! [X1_10,X8_12] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 ) ),
inference(splitRight,[status(thm)],[c_180133]) ).
tff(c_243479,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_243477]) ).
tff(c_243481,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_243479,c_174101]) ).
tff(c_244862,plain,
! [X1_1369] :
( ( inverse(X1_1369) != sk_c11 )
| ( multiply(X1_1369,sk_c11) != identity ) ),
inference(splitRight,[status(thm)],[c_243477]) ).
tff(c_244944,plain,
inverse(sk_c1) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_174240,c_244862]) ).
tff(c_244977,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_171312,c_244944]) ).
tff(c_244978,plain,
inverse(sk_c5) = sk_c11,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_245011,plain,
multiply(sk_c5,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_171272,c_92]) ).
tff(c_244983,plain,
multiply(sk_c11,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_244978,c_4]) ).
tff(c_245053,plain,
! [X_1370,Y_1371,Z_1372] : ( multiply(multiply(X_1370,Y_1371),Z_1372) = multiply(X_1370,multiply(Y_1371,Z_1372)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_245080,plain,
! [Z_1372] : ( multiply(sk_c11,multiply(sk_c5,Z_1372)) = multiply(identity,Z_1372) ),
inference(superposition,[status(thm),theory(equality)],[c_244983,c_245053]) ).
tff(c_245106,plain,
! [Z_1373] : ( multiply(sk_c11,multiply(sk_c5,Z_1373)) = Z_1373 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_245080]) ).
tff(c_245118,plain,
multiply(sk_c11,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_245011,c_245106]) ).
tff(c_245092,plain,
! [X_2,Z_1372] : ( multiply(inverse(X_2),multiply(X_2,Z_1372)) = multiply(identity,Z_1372) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_245053]) ).
tff(c_247532,plain,
! [X_1409,Z_1410] : ( multiply(inverse(X_1409),multiply(X_1409,Z_1410)) = Z_1410 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_245092]) ).
tff(c_247586,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_245118,c_247532]) ).
tff(c_247617,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_247586]) ).
tff(c_247639,plain,
multiply(sk_c5,sk_c11) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_247617,c_245011]) ).
tff(c_245104,plain,
! [X_2,Z_1372] : ( multiply(inverse(X_2),multiply(X_2,Z_1372)) = Z_1372 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_245092]) ).
tff(c_247989,plain,
! [X_1415,Z_1416] : ( multiply(inverse(inverse(X_1415)),Z_1416) = multiply(X_1415,Z_1416) ),
inference(superposition,[status(thm),theory(equality)],[c_245104,c_247532]) ).
tff(c_247604,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_247532]) ).
tff(c_247999,plain,
! [X_1415] : ( multiply(X_1415,identity) = X_1415 ),
inference(superposition,[status(thm),theory(equality)],[c_247989,c_247604]) ).
tff(c_245386,plain,
! [X_1380,Z_1381] : ( multiply(inverse(X_1380),multiply(X_1380,Z_1381)) = Z_1381 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_245092]) ).
tff(c_245843,plain,
! [X_1386,Z_1387] : ( multiply(inverse(inverse(X_1386)),Z_1387) = multiply(X_1386,Z_1387) ),
inference(superposition,[status(thm),theory(equality)],[c_245104,c_245386]) ).
tff(c_245458,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_245386]) ).
tff(c_245853,plain,
! [X_1386] : ( multiply(X_1386,identity) = X_1386 ),
inference(superposition,[status(thm),theory(equality)],[c_245843,c_245458]) ).
tff(c_245440,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_245118,c_245386]) ).
tff(c_245471,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_245440]) ).
tff(c_244979,plain,
inverse(sk_c1) != sk_c11,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_245022,plain,
multiply(sk_c9,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_244979,c_30]) ).
tff(c_244996,plain,
multiply(sk_c7,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_244979,c_32]) ).
tff(c_245083,plain,
! [Z_1372] : ( multiply(sk_c9,multiply(sk_c7,Z_1372)) = multiply(identity,Z_1372) ),
inference(superposition,[status(thm),theory(equality)],[c_171301,c_245053]) ).
tff(c_245228,plain,
! [Z_1377] : ( multiply(sk_c9,multiply(sk_c7,Z_1377)) = Z_1377 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_245083]) ).
tff(c_245240,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_244996,c_245228]) ).
tff(c_245244,plain,
sk_c9 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_245022,c_245240]) ).
tff(c_245200,plain,
! [X5_1376] :
( ( inverse(X5_1376) != sk_c11 )
| ( multiply(X5_1376,sk_c11) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_106]) ).
tff(c_245207,plain,
inverse(sk_c5) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_245011,c_245200]) ).
tff(c_245219,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_244978,c_245207]) ).
tff(c_245220,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c9 )
| ( multiply(X6_7,sk_c9) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c9 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c9 )
| ( multiply(X2_11,sk_c9) != sk_c10 )
| ( inverse(X4_13) != sk_c9 )
| ( multiply(sk_c9,multiply(X4_13,sk_c9)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_106]) ).
tff(c_245317,plain,
! [X4_13,X8_12,X1_10,X6_7,X2_11] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_245244,c_245244,c_245244,c_245244,c_245244,c_245244,c_245244,c_245244,c_245220]) ).
tff(c_245318,plain,
! [X4_13] :
( ( inverse(X4_13) != sk_c10 )
| ( multiply(sk_c10,multiply(X4_13,sk_c10)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_245317]) ).
tff(c_247461,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_245853,c_245471,c_245471,c_2,c_245471,c_245471,c_245318]) ).
tff(c_171271,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_98]) ).
tff(c_245256,plain,
inverse(sk_c6) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_245244,c_171271]) ).
tff(c_245490,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_245471,c_245256]) ).
tff(c_245557,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_245490,c_4]) ).
tff(c_245609,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_245557,c_245104]) ).
tff(c_245621,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_245609]) ).
tff(c_245626,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_245621,c_245490]) ).
tff(c_247463,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_247461,c_245626]) ).
tff(c_247464,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != sk_c10 )
| ( multiply(X2_11,sk_c10) != sk_c10 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != sk_c10 )
| ( inverse(X8_12) != sk_c10 )
| ( multiply(sk_c10,multiply(X8_12,sk_c10)) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(X6_7,sk_c10) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_245317]) ).
tff(c_254317,plain,
! [X2_11,X1_10,X8_12,X6_7] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_247999,c_247617,c_247617,c_247617,c_247999,c_247617,c_247617,c_2,c_247617,c_247617,c_247617,c_247999,c_247617,c_247617,c_247617,c_247464]) ).
tff(c_254319,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_254317]) ).
tff(c_247636,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_247617,c_245256]) ).
tff(c_247703,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_247636,c_4]) ).
tff(c_247755,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_247703,c_245104]) ).
tff(c_247767,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_247755]) ).
tff(c_247772,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_247767,c_247636]) ).
tff(c_254321,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_254319,c_247772]) ).
tff(c_254322,plain,
! [X8_12,X1_10,X2_11] :
( ( inverse(X8_12) != identity )
| ( identity != X8_12 )
| ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_254317]) ).
tff(c_320703,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_254322]) ).
tff(c_320705,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_320703,c_247772]) ).
tff(c_320706,plain,
! [X1_10,X8_12] :
( ( inverse(X1_10) != sk_c11 )
| ( multiply(X1_10,sk_c11) != identity )
| ( inverse(X8_12) != identity )
| ( identity != X8_12 ) ),
inference(splitRight,[status(thm)],[c_254322]) ).
tff(c_320708,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_320706]) ).
tff(c_320710,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_320708,c_247772]) ).
tff(c_320713,plain,
! [X1_1699] :
( ( inverse(X1_1699) != sk_c11 )
| ( multiply(X1_1699,sk_c11) != identity ) ),
inference(splitRight,[status(thm)],[c_320706]) ).
tff(c_320795,plain,
inverse(sk_c5) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_247639,c_320713]) ).
tff(c_320828,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_244978,c_320795]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP266-1 : TPTP v9.0.0. Released v2.5.0.
% 0.10/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 21:39:32 EDT 2025
% 0.12/0.34 % CPUTime :
% 61.19/46.22 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.47/46.31
% 61.47/46.31 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------