%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP360-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 : n012.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:26:02 PM UTC 2025
% Result : Unsatisfiable 12.03s 4.00s
% Output : CNFRefutation 12.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 26
% Syntax : Number of formulae : 515 ( 449 unt; 0 typ; 0 def)
% Number of atoms : 632 ( 613 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 247 ( 130 ~; 117 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 220 ( 220 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c2 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(sk_c7,X3) != sk_c6 )
| ( multiply(X4,sk_c7) != X3 )
| ( inverse(X4) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( inverse(X2) != sk_c6 )
| ( multiply(X2,sk_c5) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c2 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c2 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c2 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c2 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_50,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_75,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_79,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_75,c_4]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_20,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_87,plain,
inverse(sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_91,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_87,c_4]) ).
tff(c_3641,plain,
! [X_82,Y_83,Z_84] : ( multiply(multiply(X_82,Y_83),Z_84) = multiply(X_82,multiply(Y_83,Z_84)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_3674,plain,
! [Z_84] : ( multiply(sk_c5,multiply(sk_c7,Z_84)) = multiply(identity,Z_84) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_3641]) ).
tff(c_3694,plain,
! [Z_85] : ( multiply(sk_c5,multiply(sk_c7,Z_85)) = Z_85 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3674]) ).
tff(c_3709,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_79,c_3694]) ).
tff(c_40,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_2971,plain,
multiply(sk_c1,sk_c7) = sk_c2,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_3020,plain,
! [X_69,Y_70,Z_71] : ( multiply(multiply(X_69,Y_70),Z_71) = multiply(X_69,multiply(Y_70,Z_71)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_3059,plain,
! [Z_71] : ( multiply(sk_c7,multiply(sk_c1,Z_71)) = multiply(identity,Z_71) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_3020]) ).
tff(c_3123,plain,
! [Z_73] : ( multiply(sk_c7,multiply(sk_c1,Z_73)) = Z_73 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3059]) ).
tff(c_3141,plain,
multiply(sk_c7,sk_c2) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_2971,c_3123]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_107,plain,
multiply(sk_c7,sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_2348,plain,
! [X_56,Y_57,Z_58] : ( multiply(multiply(X_56,Y_57),Z_58) = multiply(X_56,multiply(Y_57,Z_58)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_2384,plain,
! [Z_58] : ( multiply(sk_c5,multiply(sk_c7,Z_58)) = multiply(identity,Z_58) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_2348]) ).
tff(c_2404,plain,
! [Z_59] : ( multiply(sk_c5,multiply(sk_c7,Z_59)) = Z_59 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2384]) ).
tff(c_2419,plain,
multiply(sk_c5,sk_c6) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_107,c_2404]) ).
tff(c_2422,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_79,c_2404]) ).
tff(c_112,plain,
multiply(sk_c1,sk_c7) = sk_c2,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_134,plain,
! [X_12,Y_13,Z_14] : ( multiply(multiply(X_12,Y_13),Z_14) = multiply(X_12,multiply(Y_13,Z_14)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_161,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_134]) ).
tff(c_460,plain,
! [Z_20] : ( multiply(sk_c7,multiply(sk_c1,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_475,plain,
multiply(sk_c7,sk_c2) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_112,c_460]) ).
tff(c_479,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_107,c_475]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_102,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_760,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_479,c_102]) ).
tff(c_164,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_134]) ).
tff(c_2093,plain,
! [X_51,Z_52] : ( multiply(inverse(X_51),multiply(X_51,Z_52)) = Z_52 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_2114,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_760,c_2093]) ).
tff(c_2143,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2114]) ).
tff(c_762,plain,
inverse(sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_479,c_87]) ).
tff(c_2036,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_762,c_4]) ).
tff(c_2171,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2143,c_2036]) ).
tff(c_158,plain,
! [Z_14] : ( multiply(sk_c5,multiply(sk_c7,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_134]) ).
tff(c_426,plain,
! [Z_19] : ( multiply(sk_c5,multiply(sk_c7,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_441,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_79,c_426]) ).
tff(c_2148,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_2143,c_441]) ).
tff(c_2149,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2148]) ).
tff(c_764,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_479,c_75]) ).
tff(c_2156,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2149,c_764]) ).
tff(c_2182,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2171,c_2156]) ).
tff(c_2209,plain,
! [X_53] : ( multiply(inverse(inverse(X_53)),identity) = X_53 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2093]) ).
tff(c_174,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_2215,plain,
! [X_53] : ( multiply(inverse(inverse(inverse(X_53))),X_53) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_2209,c_174]) ).
tff(c_838,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_164]) ).
tff(c_1015,plain,
! [X_29,Z_30] : ( multiply(inverse(inverse(X_29)),Z_30) = multiply(X_29,Z_30) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_838]) ).
tff(c_880,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_838]) ).
tff(c_1026,plain,
! [X_29] : ( multiply(X_29,identity) = X_29 ),
inference(superposition,[status(thm),theory(equality)],[c_1015,c_880]) ).
tff(c_859,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_760,c_838]) ).
tff(c_888,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_859]) ).
tff(c_781,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_762,c_4]) ).
tff(c_916,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_888,c_781]) ).
tff(c_486,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_479,c_102]) ).
tff(c_597,plain,
! [X_22,Z_23] : ( multiply(inverse(X_22),multiply(X_22,Z_23)) = Z_23 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_624,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_486,c_597]) ).
tff(c_655,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_624]) ).
tff(c_488,plain,
inverse(sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_479,c_87]) ).
tff(c_179,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_191,plain,
multiply(sk_c7,sk_c2) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_112,c_179]) ).
tff(c_195,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_107,c_191]) ).
tff(c_200,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_195,c_102]) ).
tff(c_332,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_200,c_174]) ).
tff(c_338,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_332]) ).
tff(c_202,plain,
inverse(sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_195,c_87]) ).
tff(c_233,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_202,c_4]) ).
tff(c_407,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_338,c_233]) ).
tff(c_58,plain,
! [X2_9,X1_8,X4_7] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(sk_c6,sk_c5) != sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_177,plain,
! [X2_9,X1_8,X4_7] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_87,c_58]) ).
tff(c_178,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_177]) ).
tff(c_197,plain,
multiply(sk_c6,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_195,c_178]) ).
tff(c_361,plain,
multiply(sk_c6,sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_338,c_197]) ).
tff(c_410,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_407,c_407,c_361]) ).
tff(c_416,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_410]) ).
tff(c_417,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_480,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_417]) ).
tff(c_563,plain,
inverse(sk_c6) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_486,c_480]) ).
tff(c_570,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_488,c_563]) ).
tff(c_659,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_655,c_570]) ).
tff(c_664,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_655,c_441]) ).
tff(c_666,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_664]) ).
tff(c_487,plain,
multiply(sk_c5,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_479,c_91]) ).
tff(c_438,plain,
multiply(sk_c5,sk_c6) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_107,c_426]) ).
tff(c_532,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_487,c_438]) ).
tff(c_484,plain,
multiply(sk_c1,sk_c6) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_479,c_112]) ).
tff(c_541,plain,
multiply(sk_c1,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_532,c_484]) ).
tff(c_671,plain,
multiply(identity,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_541]) ).
tff(c_739,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_671,c_174]) ).
tff(c_751,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_739]) ).
tff(c_753,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_659,c_751]) ).
tff(c_754,plain,
! [X1_8,X4_7] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_417]) ).
tff(c_776,plain,
! [X1_8,X4_7] :
( ( multiply(X1_8,sk_c6) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(sk_c6,multiply(X4_7,sk_c6)) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_479,c_479,c_479,c_479,c_479,c_754]) ).
tff(c_777,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(sk_c6,multiply(X4_7,sk_c6)) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_776]) ).
tff(c_2029,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_1026,c_916,c_916,c_2,c_916,c_916,c_777]) ).
tff(c_893,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_888,c_441]) ).
tff(c_894,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_893]) ).
tff(c_901,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_894,c_764]) ).
tff(c_927,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_916,c_901]) ).
tff(c_2031,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2029,c_927]) ).
tff(c_2032,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c6) != sk_c6 )
| ( inverse(X1_8) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_776]) ).
tff(c_2271,plain,
! [X1_55] :
( ( multiply(X1_55,identity) != identity )
| ( inverse(X1_55) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2171,c_2171,c_2171,c_2032]) ).
tff(c_2275,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2215,c_2271]) ).
tff(c_2294,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2182,c_2182,c_2182,c_2182,c_2275]) ).
tff(c_2295,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_2300,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2295,c_4]) ).
tff(c_2416,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_2300,c_2404]) ).
tff(c_2444,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_2422,c_2416]) ).
tff(c_2296,plain,
multiply(sk_c1,sk_c7) != sk_c2,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_42,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_2329,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_2296,c_42]) ).
tff(c_2445,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_2444,c_2329]) ).
tff(c_2387,plain,
! [Z_58] : ( multiply(sk_c7,multiply(sk_c1,Z_58)) = multiply(identity,Z_58) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_2348]) ).
tff(c_2477,plain,
! [Z_61] : ( multiply(sk_c7,multiply(sk_c1,Z_61)) = Z_61 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2387]) ).
tff(c_2492,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_2445,c_2477]) ).
tff(c_2400,plain,
! [Z_58] : ( multiply(sk_c5,multiply(sk_c7,Z_58)) = Z_58 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2384]) ).
tff(c_2499,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_2492,c_2400]) ).
tff(c_2505,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_2419,c_2499]) ).
tff(c_2516,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2505,c_91]) ).
tff(c_2517,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2505,c_87]) ).
tff(c_38,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_2337,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_2296,c_38]) ).
tff(c_2512,plain,
multiply(sk_c6,sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2505,c_2337]) ).
tff(c_2381,plain,
! [Z_58] : ( multiply(sk_c6,multiply(sk_c5,Z_58)) = multiply(sk_c7,Z_58) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_2348]) ).
tff(c_2779,plain,
! [Z_66] : ( multiply(sk_c6,multiply(sk_c5,Z_66)) = multiply(sk_c2,Z_66) ),
inference(demodulation,[status(thm),theory(equality)],[c_2505,c_2381]) ).
tff(c_2800,plain,
multiply(sk_c6,sk_c2) = multiply(sk_c2,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_2419,c_2779]) ).
tff(c_2805,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2512,c_2800]) ).
tff(c_2390,plain,
! [X_2,Z_58] : ( multiply(inverse(X_2),multiply(X_2,Z_58)) = multiply(identity,Z_58) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2348]) ).
tff(c_2402,plain,
! [X_2,Z_58] : ( multiply(inverse(X_2),multiply(X_2,Z_58)) = Z_58 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2390]) ).
tff(c_2821,plain,
multiply(inverse(sk_c2),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_2805,c_2402]) ).
tff(c_2827,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2517,c_2821]) ).
tff(c_44,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_2311,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_2296,c_44]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_2342,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_2296,c_46]) ).
tff(c_2602,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_2390]) ).
tff(c_2650,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_2342,c_2602]) ).
tff(c_2669,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2311,c_2650]) ).
tff(c_2778,plain,
! [Z_58] : ( multiply(sk_c6,multiply(sk_c5,Z_58)) = multiply(sk_c2,Z_58) ),
inference(demodulation,[status(thm),theory(equality)],[c_2505,c_2381]) ).
tff(c_2832,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c2,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_2827,c_2778]) ).
tff(c_2841,plain,
multiply(sk_c2,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2669,c_2832]) ).
tff(c_2873,plain,
multiply(inverse(sk_c2),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_2841,c_2402]) ).
tff(c_2879,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2827,c_2517,c_2873]) ).
tff(c_2890,plain,
multiply(sk_c5,sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2879,c_2512]) ).
tff(c_2901,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2516,c_2890]) ).
tff(c_2507,plain,
multiply(sk_c2,sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2505,c_2505,c_2492]) ).
tff(c_2794,plain,
multiply(sk_c6,identity) = multiply(sk_c2,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_2516,c_2779]) ).
tff(c_2804,plain,
multiply(sk_c6,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2507,c_2794]) ).
tff(c_2883,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2879,c_2879,c_2804]) ).
tff(c_2899,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_2422,c_2883]) ).
tff(c_2918,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2901,c_2899]) ).
tff(c_2513,plain,
multiply(sk_c1,sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_2505,c_2296]) ).
tff(c_2954,plain,
multiply(identity,sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_2918,c_2513]) ).
tff(c_2961,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2954]) ).
tff(c_2963,plain,
multiply(sk_c7,sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_3145,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_3141,c_2963]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_3012,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_2963,c_36]) ).
tff(c_2962,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_2967,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2962,c_4]) ).
tff(c_3047,plain,
! [Z_71] : ( multiply(sk_c6,multiply(sk_c4,Z_71)) = multiply(identity,Z_71) ),
inference(superposition,[status(thm),theory(equality)],[c_2967,c_3020]) ).
tff(c_3285,plain,
! [Z_76] : ( multiply(sk_c6,multiply(sk_c4,Z_76)) = Z_76 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3047]) ).
tff(c_3297,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_3012,c_3285]) ).
tff(c_3062,plain,
! [X_2,Z_71] : ( multiply(inverse(X_2),multiply(X_2,Z_71)) = multiply(identity,Z_71) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_3020]) ).
tff(c_3357,plain,
! [X_78,Z_79] : ( multiply(inverse(X_78),multiply(X_78,Z_79)) = Z_79 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3062]) ).
tff(c_3378,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_3297,c_3357]) ).
tff(c_28,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_2999,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_2963,c_28]) ).
tff(c_3417,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_2999,c_3357]) ).
tff(c_3588,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_3378,c_3417]) ).
tff(c_3590,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3145,c_3588]) ).
tff(c_3591,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_3597,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_3591,c_4]) ).
tff(c_3706,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_3597,c_3694]) ).
tff(c_3721,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_3709,c_3706]) ).
tff(c_3592,plain,
multiply(sk_c1,sk_c7) != sk_c2,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_3617,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_3592,c_42]) ).
tff(c_3722,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_3721,c_3617]) ).
tff(c_3624,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_2963,c_36]) ).
tff(c_3677,plain,
! [Z_84] : ( multiply(sk_c7,multiply(sk_c1,Z_84)) = multiply(identity,Z_84) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_3641]) ).
tff(c_3691,plain,
! [Z_84] : ( multiply(sk_c7,multiply(sk_c1,Z_84)) = Z_84 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3677]) ).
tff(c_3632,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_2963,c_28]) ).
tff(c_3732,plain,
! [X2_9,X1_8,X4_7] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_87,c_3632,c_58]) ).
tff(c_3848,plain,
! [X4_89] :
( ( inverse(X4_89) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_89,sk_c7)) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_3732]) ).
tff(c_3855,plain,
( ( inverse(sk_c1) != sk_c7 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_3691,c_3848]) ).
tff(c_3876,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_3855]) ).
tff(c_3668,plain,
! [Z_84] : ( multiply(sk_c6,multiply(sk_c4,Z_84)) = multiply(identity,Z_84) ),
inference(superposition,[status(thm),theory(equality)],[c_2967,c_3641]) ).
tff(c_3832,plain,
! [Z_88] : ( multiply(sk_c6,multiply(sk_c4,Z_88)) = Z_88 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3668]) ).
tff(c_3844,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_3624,c_3832]) ).
tff(c_3741,plain,
! [Z_86] : ( multiply(sk_c7,multiply(sk_c1,Z_86)) = Z_86 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3677]) ).
tff(c_3756,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_3722,c_3741]) ).
tff(c_3887,plain,
! [Z_90] : ( multiply(sk_c6,multiply(sk_c7,Z_90)) = multiply(sk_c5,Z_90) ),
inference(superposition,[status(thm),theory(equality)],[c_3632,c_3641]) ).
tff(c_3902,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_3756,c_3887]) ).
tff(c_3913,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_3844,c_91,c_3902]) ).
tff(c_3690,plain,
! [Z_84] : ( multiply(sk_c5,multiply(sk_c7,Z_84)) = Z_84 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3674]) ).
tff(c_3763,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_3756,c_3690]) ).
tff(c_3919,plain,
multiply(identity,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_3913,c_3763]) ).
tff(c_3930,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3919]) ).
tff(c_3932,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3876,c_3930]) ).
tff(c_3933,plain,
! [X1_8,X2_9] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_3732]) ).
tff(c_4080,plain,
! [X2_94] :
( ( multiply(X2_94,sk_c5) != sk_c6 )
| ( inverse(X2_94) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_3933]) ).
tff(c_4093,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_3624,c_4080]) ).
tff(c_4109,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2962,c_4093]) ).
tff(c_4213,plain,
! [X1_97] :
( ( multiply(X1_97,sk_c6) != sk_c7 )
| ( inverse(X1_97) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_3933]) ).
tff(c_4225,plain,
inverse(sk_c1) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_3722,c_4213]) ).
tff(c_4243,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_4225]) ).
tff(c_4244,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_4245,plain,
multiply(sk_c6,sk_c5) != sk_c7,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_5713,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_4245,c_16]) ).
tff(c_5724,plain,
! [X_128,Y_129,Z_130] : ( multiply(multiply(X_128,Y_129),Z_130) = multiply(X_128,multiply(Y_129,Z_130)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_5760,plain,
! [X_2,Z_130] : ( multiply(inverse(X_2),multiply(X_2,Z_130)) = multiply(identity,Z_130) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_5724]) ).
tff(c_5828,plain,
! [X_132,Z_133] : ( multiply(inverse(X_132),multiply(X_132,Z_133)) = Z_133 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5760]) ).
tff(c_5858,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5713,c_5828]) ).
tff(c_5890,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4244,c_5858]) ).
tff(c_5772,plain,
! [X_2,Z_130] : ( multiply(inverse(X_2),multiply(X_2,Z_130)) = Z_130 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5760]) ).
tff(c_5896,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5890,c_5772]) ).
tff(c_5310,plain,
multiply(sk_c7,sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_5338,plain,
! [X_119,Y_120,Z_121] : ( multiply(multiply(X_119,Y_120),Z_121) = multiply(X_119,multiply(Y_120,Z_121)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_5371,plain,
! [Z_121] : ( multiply(sk_c5,multiply(sk_c7,Z_121)) = multiply(identity,Z_121) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_5338]) ).
tff(c_5391,plain,
! [Z_122] : ( multiply(sk_c5,multiply(sk_c7,Z_122)) = Z_122 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5371]) ).
tff(c_5403,plain,
multiply(sk_c5,sk_c6) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_5310,c_5391]) ).
tff(c_5409,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_79,c_5391]) ).
tff(c_4725,plain,
! [X_107,Y_108,Z_109] : ( multiply(multiply(X_107,Y_108),Z_109) = multiply(X_107,multiply(Y_108,Z_109)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_4758,plain,
! [Z_109] : ( multiply(sk_c5,multiply(sk_c7,Z_109)) = multiply(identity,Z_109) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_4725]) ).
tff(c_4778,plain,
! [Z_110] : ( multiply(sk_c5,multiply(sk_c7,Z_110)) = Z_110 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4758]) ).
tff(c_4793,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_79,c_4778]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_4268,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_4245,c_10]) ).
tff(c_4272,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4268,c_4]) ).
tff(c_4790,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_4272,c_4778]) ).
tff(c_4805,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_4793,c_4790]) ).
tff(c_12,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_4707,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_4245,c_12]) ).
tff(c_4816,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_4805,c_4707]) ).
tff(c_4761,plain,
! [Z_109] : ( multiply(sk_c7,multiply(sk_c1,Z_109)) = multiply(identity,Z_109) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_4725]) ).
tff(c_4832,plain,
! [Z_111] : ( multiply(sk_c7,multiply(sk_c1,Z_111)) = Z_111 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4761]) ).
tff(c_4847,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4816,c_4832]) ).
tff(c_4764,plain,
! [X_2,Z_109] : ( multiply(inverse(X_2),multiply(X_2,Z_109)) = multiply(identity,Z_109) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4725]) ).
tff(c_4776,plain,
! [X_2,Z_109] : ( multiply(inverse(X_2),multiply(X_2,Z_109)) = Z_109 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4764]) ).
tff(c_5000,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_4847,c_4776]) ).
tff(c_5009,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_87,c_5000]) ).
tff(c_4282,plain,
multiply(sk_c7,sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_4259,plain,
multiply(sk_c1,sk_c7) = sk_c2,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_4307,plain,
! [X_98,Y_99,Z_100] : ( multiply(multiply(X_98,Y_99),Z_100) = multiply(X_98,multiply(Y_99,Z_100)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_4346,plain,
! [Z_100] : ( multiply(sk_c7,multiply(sk_c1,Z_100)) = multiply(identity,Z_100) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_4307]) ).
tff(c_4454,plain,
! [Z_103] : ( multiply(sk_c7,multiply(sk_c1,Z_103)) = Z_103 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4346]) ).
tff(c_4478,plain,
multiply(sk_c7,sk_c2) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_4259,c_4454]) ).
tff(c_4482,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4282,c_4478]) ).
tff(c_4489,plain,
multiply(sk_c6,sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4482,c_4282]) ).
tff(c_4349,plain,
! [X_2,Z_100] : ( multiply(inverse(X_2),multiply(X_2,Z_100)) = multiply(identity,Z_100) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4307]) ).
tff(c_4361,plain,
! [X_2,Z_100] : ( multiply(inverse(X_2),multiply(X_2,Z_100)) = Z_100 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4349]) ).
tff(c_4587,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_4489,c_4361]) ).
tff(c_4593,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4587]) ).
tff(c_4490,plain,
multiply(sk_c1,sk_c6) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_4482,c_4259]) ).
tff(c_4613,plain,
multiply(sk_c1,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4593,c_4490]) ).
tff(c_4343,plain,
! [Z_100] : ( multiply(sk_c5,multiply(sk_c7,Z_100)) = multiply(identity,Z_100) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_4307]) ).
tff(c_4363,plain,
! [Z_101] : ( multiply(sk_c5,multiply(sk_c7,Z_101)) = Z_101 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4343]) ).
tff(c_4381,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_79,c_4363]) ).
tff(c_4378,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_4272,c_4363]) ).
tff(c_4402,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_4381,c_4378]) ).
tff(c_4294,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_4245,c_12]) ).
tff(c_4411,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_4402,c_4294]) ).
tff(c_4486,plain,
multiply(sk_c1,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4482,c_4411]) ).
tff(c_4627,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4613,c_4486]) ).
tff(c_4299,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_4245,c_16]) ).
tff(c_4514,plain,
! [X_104,Z_105] : ( multiply(inverse(X_104),multiply(X_104,Z_105)) = Z_105 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4349]) ).
tff(c_4547,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_4299,c_4514]) ).
tff(c_4563,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4244,c_4547]) ).
tff(c_4630,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4627,c_4627,c_4563]) ).
tff(c_4634,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4630]) ).
tff(c_4491,plain,
multiply(sk_c6,sk_c5) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4482,c_4245]) ).
tff(c_4699,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4634,c_4627,c_2,c_4627,c_4491]) ).
tff(c_4700,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_4743,plain,
! [Z_109] : ( multiply(sk_c3,multiply(sk_c6,Z_109)) = multiply(sk_c7,Z_109) ),
inference(superposition,[status(thm),theory(equality)],[c_4707,c_4725]) ).
tff(c_5169,plain,
! [Z_117] : ( multiply(sk_c1,multiply(sk_c6,Z_117)) = multiply(sk_c7,Z_117) ),
inference(demodulation,[status(thm),theory(equality)],[c_4805,c_4743]) ).
tff(c_5190,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c1,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_4700,c_5169]) ).
tff(c_5198,plain,
multiply(sk_c1,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4847,c_5190]) ).
tff(c_5203,plain,
multiply(inverse(sk_c1),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5198,c_4776]) ).
tff(c_5212,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_5203]) ).
tff(c_5249,plain,
! [Z_118] : ( multiply(sk_c6,multiply(sk_c7,Z_118)) = multiply(sk_c5,Z_118) ),
inference(superposition,[status(thm),theory(equality)],[c_4700,c_4725]) ).
tff(c_5267,plain,
multiply(sk_c6,sk_c5) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_5212,c_5249]) ).
tff(c_5286,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_5009,c_5267]) ).
tff(c_5288,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4245,c_5286]) ).
tff(c_5289,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_5294,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5289,c_4]) ).
tff(c_5406,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_5294,c_5391]) ).
tff(c_5428,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_5409,c_5406]) ).
tff(c_5290,plain,
multiply(sk_c1,sk_c7) != sk_c2,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_5315,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_5290,c_42]) ).
tff(c_5439,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_5428,c_5315]) ).
tff(c_5374,plain,
! [Z_121] : ( multiply(sk_c7,multiply(sk_c1,Z_121)) = multiply(identity,Z_121) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_5338]) ).
tff(c_5455,plain,
! [Z_123] : ( multiply(sk_c7,multiply(sk_c1,Z_123)) = Z_123 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5374]) ).
tff(c_5470,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5439,c_5455]) ).
tff(c_5387,plain,
! [Z_121] : ( multiply(sk_c5,multiply(sk_c7,Z_121)) = Z_121 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5371]) ).
tff(c_5493,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_5470,c_5387]) ).
tff(c_5499,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_5403,c_5493]) ).
tff(c_5511,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5499,c_87]) ).
tff(c_5521,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5511,c_4]) ).
tff(c_5327,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_4245,c_16]) ).
tff(c_5377,plain,
! [X_2,Z_121] : ( multiply(inverse(X_2),multiply(X_2,Z_121)) = multiply(identity,Z_121) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_5338]) ).
tff(c_5539,plain,
! [X_125,Z_126] : ( multiply(inverse(X_125),multiply(X_125,Z_126)) = Z_126 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5377]) ).
tff(c_5575,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5327,c_5539]) ).
tff(c_5592,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4244,c_5575]) ).
tff(c_5507,plain,
multiply(sk_c2,sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5499,c_5310]) ).
tff(c_5320,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_5290,c_38]) ).
tff(c_5356,plain,
! [Z_121] : ( multiply(sk_c6,multiply(sk_c7,Z_121)) = multiply(sk_c5,Z_121) ),
inference(superposition,[status(thm),theory(equality)],[c_5320,c_5338]) ).
tff(c_5650,plain,
! [Z_127] : ( multiply(sk_c6,multiply(sk_c2,Z_127)) = multiply(sk_c5,Z_127) ),
inference(demodulation,[status(thm),theory(equality)],[c_5499,c_5356]) ).
tff(c_5665,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_5507,c_5650]) ).
tff(c_5672,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5521,c_5592,c_5665]) ).
tff(c_5679,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_5672,c_5409]) ).
tff(c_5683,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5679]) ).
tff(c_5508,plain,
multiply(sk_c1,sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_5499,c_5290]) ).
tff(c_5688,plain,
multiply(identity,sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_5683,c_5508]) ).
tff(c_5695,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5688]) ).
tff(c_5696,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_5861,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_5696,c_5828]) ).
tff(c_5996,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5896,c_5861]) ).
tff(c_5754,plain,
! [Z_130] : ( multiply(sk_c5,multiply(sk_c7,Z_130)) = multiply(identity,Z_130) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_5724]) ).
tff(c_5776,plain,
! [Z_131] : ( multiply(sk_c5,multiply(sk_c7,Z_131)) = Z_131 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5754]) ).
tff(c_5791,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_79,c_5776]) ).
tff(c_5788,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_5294,c_5776]) ).
tff(c_5803,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_5791,c_5788]) ).
tff(c_5702,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_5290,c_42]) ).
tff(c_5812,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_5803,c_5702]) ).
tff(c_5846,plain,
multiply(inverse(sk_c1),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5812,c_5828]) ).
tff(c_5889,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_5846]) ).
tff(c_6038,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5996,c_5996,c_5889]) ).
tff(c_6049,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5890,c_6038]) ).
tff(c_6056,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6049,c_6049,c_5896]) ).
tff(c_6062,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_6056]) ).
tff(c_6088,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6062,c_6049]) ).
tff(c_6044,plain,
multiply(sk_c6,sk_c5) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5996,c_4245]) ).
tff(c_6204,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6088,c_2,c_6088,c_6062,c_6044]) ).
tff(c_6206,plain,
inverse(sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_26,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_6233,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_6206,c_26]) ).
tff(c_24,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_6219,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_6206,c_24]) ).
tff(c_6223,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6219,c_4]) ).
tff(c_6264,plain,
! [X_138,Y_139,Z_140] : ( multiply(multiply(X_138,Y_139),Z_140) = multiply(X_138,multiply(Y_139,Z_140)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_6288,plain,
! [Z_140] : ( multiply(sk_c6,multiply(sk_c4,Z_140)) = multiply(identity,Z_140) ),
inference(superposition,[status(thm),theory(equality)],[c_6223,c_6264]) ).
tff(c_6310,plain,
! [Z_141] : ( multiply(sk_c6,multiply(sk_c4,Z_141)) = Z_141 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6288]) ).
tff(c_6322,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_6233,c_6310]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_6241,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_6206,c_22]) ).
tff(c_6205,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_6210,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6205,c_4]) ).
tff(c_6291,plain,
! [Z_140] : ( multiply(sk_c7,multiply(sk_c3,Z_140)) = multiply(identity,Z_140) ),
inference(superposition,[status(thm),theory(equality)],[c_6210,c_6264]) ).
tff(c_6333,plain,
! [Z_142] : ( multiply(sk_c7,multiply(sk_c3,Z_142)) = Z_142 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6291]) ).
tff(c_6345,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_6241,c_6333]) ).
tff(c_18,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_6246,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_6206,c_18]) ).
tff(c_6567,plain,
! [Z_148] : ( multiply(sk_c6,multiply(sk_c7,Z_148)) = multiply(sk_c5,Z_148) ),
inference(superposition,[status(thm),theory(equality)],[c_6246,c_6264]) ).
tff(c_6585,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_6345,c_6567]) ).
tff(c_6592,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6322,c_6585]) ).
tff(c_6297,plain,
! [X_2,Z_140] : ( multiply(inverse(X_2),multiply(X_2,Z_140)) = multiply(identity,Z_140) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_6264]) ).
tff(c_6308,plain,
! [X_2,Z_140] : ( multiply(inverse(X_2),multiply(X_2,Z_140)) = Z_140 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6297]) ).
tff(c_6596,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_6592,c_6308]) ).
tff(c_6602,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_6596]) ).
tff(c_6371,plain,
! [X_144,Z_145] : ( multiply(inverse(X_144),multiply(X_144,Z_145)) = Z_145 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6297]) ).
tff(c_6428,plain,
multiply(inverse(sk_c7),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_79,c_6371]) ).
tff(c_6607,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_6602,c_6428]) ).
tff(c_6616,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_6607]) ).
tff(c_6614,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6602,c_75]) ).
tff(c_6679,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6616,c_6614]) ).
tff(c_6610,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6602,c_6602,c_6345]) ).
tff(c_6617,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6610]) ).
tff(c_6655,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6617,c_6617,c_6322]) ).
tff(c_6662,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6655]) ).
tff(c_6612,plain,
inverse(identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6602,c_6206]) ).
tff(c_6700,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6679,c_6662,c_6612]) ).
tff(c_6702,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_52,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_22480,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_6702,c_52]) ).
tff(c_6701,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_6706,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6701,c_4]) ).
tff(c_22502,plain,
! [X_311,Y_312,Z_313] : ( multiply(multiply(X_311,Y_312),Z_313) = multiply(X_311,multiply(Y_312,Z_313)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_22529,plain,
! [Z_313] : ( multiply(sk_c7,multiply(sk_c3,Z_313)) = multiply(identity,Z_313) ),
inference(superposition,[status(thm),theory(equality)],[c_6706,c_22502]) ).
tff(c_22569,plain,
! [Z_315] : ( multiply(sk_c7,multiply(sk_c3,Z_315)) = Z_315 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22529]) ).
tff(c_22581,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_22480,c_22569]) ).
tff(c_6772,plain,
! [X_150,Y_151,Z_152] : ( multiply(multiply(X_150,Y_151),Z_152) = multiply(X_150,multiply(Y_151,Z_152)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_6805,plain,
! [X_2,Z_152] : ( multiply(inverse(X_2),multiply(X_2,Z_152)) = multiply(identity,Z_152) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_6772]) ).
tff(c_8117,plain,
! [X_180,Z_181] : ( multiply(inverse(X_180),multiply(X_180,Z_181)) = Z_181 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6805]) ).
tff(c_6816,plain,
! [X_2,Z_152] : ( multiply(inverse(X_2),multiply(X_2,Z_152)) = Z_152 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6805]) ).
tff(c_8341,plain,
! [X_184,Z_185] : ( multiply(inverse(inverse(X_184)),Z_185) = multiply(X_184,Z_185) ),
inference(superposition,[status(thm),theory(equality)],[c_8117,c_6816]) ).
tff(c_8168,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_8117]) ).
tff(c_8348,plain,
! [X_184] : ( multiply(X_184,identity) = X_184 ),
inference(superposition,[status(thm),theory(equality)],[c_8341,c_8168]) ).
tff(c_56,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_6751,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_6702,c_56]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_6727,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_6702,c_54]) ).
tff(c_6731,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6727,c_4]) ).
tff(c_6796,plain,
! [Z_152] : ( multiply(sk_c6,multiply(sk_c4,Z_152)) = multiply(identity,Z_152) ),
inference(superposition,[status(thm),theory(equality)],[c_6731,c_6772]) ).
tff(c_6818,plain,
! [Z_153] : ( multiply(sk_c6,multiply(sk_c4,Z_153)) = Z_153 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6796]) ).
tff(c_6830,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_6751,c_6818]) ).
tff(c_6715,plain,
inverse(sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_6719,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6715,c_4]) ).
tff(c_6744,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_6702,c_52]) ).
tff(c_6802,plain,
! [Z_152] : ( multiply(sk_c7,multiply(sk_c3,Z_152)) = multiply(identity,Z_152) ),
inference(superposition,[status(thm),theory(equality)],[c_6706,c_6772]) ).
tff(c_7564,plain,
! [Z_169] : ( multiply(sk_c7,multiply(sk_c3,Z_169)) = Z_169 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6802]) ).
tff(c_7579,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_6744,c_7564]) ).
tff(c_48,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_6758,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_6702,c_48]) ).
tff(c_6787,plain,
! [Z_152] : ( multiply(sk_c6,multiply(sk_c7,Z_152)) = multiply(sk_c5,Z_152) ),
inference(superposition,[status(thm),theory(equality)],[c_6758,c_6772]) ).
tff(c_7586,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_7579,c_6787]) ).
tff(c_7592,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6830,c_6719,c_7586]) ).
tff(c_7599,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7592,c_6719]) ).
tff(c_8109,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_7599,c_2]) ).
tff(c_7600,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7592,c_6715]) ).
tff(c_8141,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_7579,c_8117]) ).
tff(c_8176,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7600,c_8141]) ).
tff(c_8198,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8109,c_8176]) ).
tff(c_7621,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_7599,c_2]) ).
tff(c_7631,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_7621,c_7621,c_7579]) ).
tff(c_7638,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7631]) ).
tff(c_7674,plain,
! [X_170,Z_171] : ( multiply(inverse(X_170),multiply(X_170,Z_171)) = Z_171 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6805]) ).
tff(c_7837,plain,
! [X_173,Z_174] : ( multiply(inverse(inverse(X_173)),Z_174) = multiply(X_173,Z_174) ),
inference(superposition,[status(thm),theory(equality)],[c_7674,c_6816]) ).
tff(c_7704,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_7674]) ).
tff(c_7844,plain,
! [X_173] : ( multiply(X_173,identity) = X_173 ),
inference(superposition,[status(thm),theory(equality)],[c_7837,c_7704]) ).
tff(c_6889,plain,
! [X_156,Z_157] : ( multiply(inverse(X_156),multiply(X_156,Z_157)) = Z_157 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6805]) ).
tff(c_6916,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_6830,c_6889]) ).
tff(c_6925,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_6758,c_6889]) ).
tff(c_7170,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6916,c_6925]) ).
tff(c_6844,plain,
! [Z_154] : ( multiply(sk_c7,multiply(sk_c3,Z_154)) = Z_154 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6802]) ).
tff(c_6856,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_6744,c_6844]) ).
tff(c_7186,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_7170,c_7170,c_6856]) ).
tff(c_7197,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6830,c_7186]) ).
tff(c_7204,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_7197,c_7197,c_6916]) ).
tff(c_7213,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_7204]) ).
tff(c_7245,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7213,c_7197]) ).
tff(c_6835,plain,
! [X2_9,X1_8,X4_7] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6715,c_6758,c_58]) ).
tff(c_6836,plain,
multiply(sk_c6,sk_c5) != sk_c7,
inference(splitLeft,[status(thm)],[c_6835]) ).
tff(c_7188,plain,
multiply(sk_c6,sk_c5) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_7170,c_6836]) ).
tff(c_7531,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7245,c_2,c_7245,c_7213,c_7188]) ).
tff(c_7532,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_6835]) ).
tff(c_7613,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,identity) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7592,c_7532]) ).
tff(c_7614,plain,
! [X2_9] :
( ( multiply(X2_9,identity) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_7613]) ).
tff(c_8099,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_7638,c_7844,c_7638,c_7614]) ).
tff(c_7630,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7621,c_7600]) ).
tff(c_8101,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8099,c_7630]) ).
tff(c_8102,plain,
! [X1_8,X4_7] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_7613]) ).
tff(c_22442,plain,
! [X1_8,X4_7] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8348,c_8198,c_8109,c_2,c_8109,c_8109,c_8109,c_8348,c_8198,c_8109,c_8102]) ).
tff(c_22444,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_22442]) ).
tff(c_8162,plain,
multiply(inverse(sk_c7),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_6706,c_8117]) ).
tff(c_8180,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7600,c_8162]) ).
tff(c_8189,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8176,c_6701]) ).
tff(c_8212,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8198,c_8180,c_8189]) ).
tff(c_22446,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22444,c_8212]) ).
tff(c_22448,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_22442]) ).
tff(c_22450,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22448,c_8212]) ).
tff(c_22452,plain,
inverse(sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_22473,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_22452,c_18]) ).
tff(c_22592,plain,
! [Z_316] : ( multiply(sk_c3,multiply(sk_c6,Z_316)) = multiply(sk_c7,Z_316) ),
inference(superposition,[status(thm),theory(equality)],[c_22480,c_22502]) ).
tff(c_22613,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_22473,c_22592]) ).
tff(c_22620,plain,
multiply(sk_c3,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_22581,c_22613]) ).
tff(c_22541,plain,
! [Z_313] : ( multiply(sk_c7,multiply(sk_c3,Z_313)) = Z_313 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22529]) ).
tff(c_22624,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_22620,c_22541]) ).
tff(c_22466,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_22452,c_26]) ).
tff(c_22451,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_22456,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22451,c_4]) ).
tff(c_22526,plain,
! [Z_313] : ( multiply(sk_c6,multiply(sk_c4,Z_313)) = multiply(identity,Z_313) ),
inference(superposition,[status(thm),theory(equality)],[c_22456,c_22502]) ).
tff(c_22544,plain,
! [Z_314] : ( multiply(sk_c6,multiply(sk_c4,Z_314)) = Z_314 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22526]) ).
tff(c_22556,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_22466,c_22544]) ).
tff(c_22607,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_22556,c_22592]) ).
tff(c_22646,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22624,c_22620,c_22607]) ).
tff(c_22648,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22646,c_22620]) ).
tff(c_22653,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_22646,c_22480]) ).
tff(c_22738,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22648,c_22653]) ).
tff(c_22654,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22646,c_22473]) ).
tff(c_22817,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22738,c_22654]) ).
tff(c_22532,plain,
! [X_2,Z_313] : ( multiply(inverse(X_2),multiply(X_2,Z_313)) = multiply(identity,Z_313) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_22502]) ).
tff(c_22542,plain,
! [X_2,Z_313] : ( multiply(inverse(X_2),multiply(X_2,Z_313)) = Z_313 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22532]) ).
tff(c_22824,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_22817,c_22542]) ).
tff(c_22831,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22824]) ).
tff(c_22741,plain,
inverse(sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22738,c_22452]) ).
tff(c_22838,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_22831,c_22831,c_22741]) ).
tff(c_22744,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22738,c_6701]) ).
tff(c_22757,plain,
multiply(sk_c5,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22744,c_4]) ).
tff(c_22856,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22831,c_22757]) ).
tff(c_22840,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22831,c_22744]) ).
tff(c_22875,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22856,c_22840]) ).
tff(c_22876,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22838,c_22875]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP360-1 : TPTP v9.0.0. Released v2.5.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n012.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:43:30 EDT 2025
% 0.13/0.34 % CPUTime :
% 12.03/4.00 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.28/4.05
% 12.28/4.05 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------