%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP333-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n011.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:57 PM UTC 2025
% Result : Unsatisfiable 12.43s 4.47s
% Output : CNFRefutation 12.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 19
% Syntax : Number of formulae : 404 ( 333 unt; 0 typ; 0 def)
% Number of atoms : 547 ( 519 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 342 ( 199 ~; 143 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 188 ( 188 !; 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_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_63,axiom,
multiply(sk_c6,sk_c7) = sk_c5,
file(unknown,unknown) ).
tff(f_69,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_87,axiom,
( ( inverse(sk_c1) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_105,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_93,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_138,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( multiply(X3,sk_c6) != sk_c7 )
| ( inverse(X3) != sk_c6 )
| ( inverse(X4) != sk_c6 )
| ( multiply(X4,sk_c5) != sk_c6 )
| ( multiply(X1,sk_c7) != sk_c6 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X2,sk_c6) != sk_c5 )
| ( inverse(X2) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_66,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_75,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_72,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_102,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_78,axiom,
( ( inverse(sk_c1) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_81,axiom,
( ( inverse(sk_c1) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_84,axiom,
( ( inverse(sk_c1) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_96,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_99,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_90,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_25968,plain,
! [X_336,Y_337,Z_338] : ( multiply(multiply(X_336,Y_337),Z_338) = multiply(X_336,multiply(Y_337,Z_338)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_25998,plain,
! [X_2,Z_338] : ( multiply(inverse(X_2),multiply(X_2,Z_338)) = multiply(identity,Z_338) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_25968]) ).
tff(c_26359,plain,
! [X_346,Z_347] : ( multiply(inverse(X_346),multiply(X_346,Z_347)) = Z_347 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25998]) ).
tff(c_26012,plain,
! [X_2,Z_338] : ( multiply(inverse(X_2),multiply(X_2,Z_338)) = Z_338 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25998]) ).
tff(c_27339,plain,
! [X_364,Z_365] : ( multiply(inverse(inverse(X_364)),Z_365) = multiply(X_364,Z_365) ),
inference(superposition,[status(thm),theory(equality)],[c_26359,c_26012]) ).
tff(c_26419,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_26359]) ).
tff(c_27346,plain,
! [X_364] : ( multiply(X_364,identity) = X_364 ),
inference(superposition,[status(thm),theory(equality)],[c_27339,c_26419]) ).
tff(c_12716,plain,
! [X_196,Y_197,Z_198] : ( multiply(multiply(X_196,Y_197),Z_198) = multiply(X_196,multiply(Y_197,Z_198)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_12746,plain,
! [X_2,Z_198] : ( multiply(inverse(X_2),multiply(X_2,Z_198)) = multiply(identity,Z_198) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12716]) ).
tff(c_12859,plain,
! [X_203,Z_204] : ( multiply(inverse(X_203),multiply(X_203,Z_204)) = Z_204 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12746]) ).
tff(c_12760,plain,
! [X_2,Z_198] : ( multiply(inverse(X_2),multiply(X_2,Z_198)) = Z_198 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12746]) ).
tff(c_13919,plain,
! [X_221,Z_222] : ( multiply(inverse(inverse(X_221)),Z_222) = multiply(X_221,Z_222) ),
inference(superposition,[status(thm),theory(equality)],[c_12859,c_12760]) ).
tff(c_12928,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12859]) ).
tff(c_13926,plain,
! [X_221] : ( multiply(X_221,identity) = X_221 ),
inference(superposition,[status(thm),theory(equality)],[c_13919,c_12928]) ).
tff(c_111,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_138,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_111]) ).
tff(c_1041,plain,
! [X_36,Z_37] : ( multiply(inverse(X_36),multiply(X_36,Z_37)) = Z_37 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_138]) ).
tff(c_151,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_138]) ).
tff(c_1305,plain,
! [X_40,Z_41] : ( multiply(inverse(inverse(X_40)),Z_41) = multiply(X_40,Z_41) ),
inference(superposition,[status(thm),theory(equality)],[c_1041,c_151]) ).
tff(c_1089,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1041]) ).
tff(c_1312,plain,
! [X_40] : ( multiply(X_40,identity) = X_40 ),
inference(superposition,[status(thm),theory(equality)],[c_1305,c_1089]) ).
tff(c_8,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_12,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_97,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_24,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_73,plain,
inverse(sk_c1) = sk_c6,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_77,plain,
multiply(sk_c6,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_73,c_4]) ).
tff(c_132,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_77,c_111]) ).
tff(c_153,plain,
! [Z_15] : ( multiply(sk_c6,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_132]) ).
tff(c_165,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_97,c_153]) ).
tff(c_169,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_165]) ).
tff(c_36,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_91,plain,
multiply(sk_c2,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_172,plain,
multiply(sk_c2,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_169,c_91]) ).
tff(c_28,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_65,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_69,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_65,c_4]) ).
tff(c_135,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_69,c_111]) ).
tff(c_150,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_135]) ).
tff(c_1018,plain,
! [Z_35] : ( multiply(sk_c5,multiply(sk_c2,Z_35)) = Z_35 ),
inference(demodulation,[status(thm),theory(equality)],[c_169,c_150]) ).
tff(c_1030,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_172,c_1018]) ).
tff(c_1059,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_1030,c_1041]) ).
tff(c_1096,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1059]) ).
tff(c_177,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_169,c_8]) ).
tff(c_1080,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_177,c_1041]) ).
tff(c_1100,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1080]) ).
tff(c_294,plain,
! [X_19,Z_20] : ( multiply(inverse(X_19),multiply(X_19,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_138]) ).
tff(c_627,plain,
! [X_25,Z_26] : ( multiply(inverse(inverse(X_25)),Z_26) = multiply(X_25,Z_26) ),
inference(superposition,[status(thm),theory(equality)],[c_294,c_151]) ).
tff(c_348,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_294]) ).
tff(c_634,plain,
! [X_25] : ( multiply(X_25,identity) = X_25 ),
inference(superposition,[status(thm),theory(equality)],[c_627,c_348]) ).
tff(c_238,plain,
! [Z_16] : ( multiply(sk_c5,multiply(sk_c2,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_169,c_150]) ).
tff(c_250,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_172,c_238]) ).
tff(c_315,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_250,c_294]) ).
tff(c_355,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_315]) ).
tff(c_339,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_177,c_294]) ).
tff(c_360,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_339]) ).
tff(c_42,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_138]) ).
tff(c_44,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_42]) ).
tff(c_233,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_169,c_169,c_169,c_169,c_169,c_169,c_169,c_44]) ).
tff(c_234,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_233]) ).
tff(c_1011,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_634,c_355,c_360,c_355,c_234]) ).
tff(c_174,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_169,c_69]) ).
tff(c_422,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_355,c_174]) ).
tff(c_529,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_422,c_151]) ).
tff(c_541,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_529]) ).
tff(c_176,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_169,c_65]) ).
tff(c_424,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_355,c_176]) ).
tff(c_546,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_541,c_424]) ).
tff(c_1013,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1011,c_546]) ).
tff(c_1014,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c5 )
| ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_233]) ).
tff(c_9852,plain,
! [X4_7,X1_8,X2_9] :
( ( identity != X4_7 )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1312,c_1096,c_1096,c_1096,c_1312,c_1096,c_1100,c_1100,c_1096,c_1312,c_1096,c_1096,c_1014]) ).
tff(c_9854,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9852]) ).
tff(c_1110,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1096,c_174]) ).
tff(c_1197,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_1110,c_151]) ).
tff(c_1209,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1197]) ).
tff(c_1112,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1096,c_176]) ).
tff(c_1214,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1209,c_1112]) ).
tff(c_9856,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9854,c_1214]) ).
tff(c_9857,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X4_7 )
| ( inverse(X4_7) != identity ) ),
inference(splitRight,[status(thm)],[c_9852]) ).
tff(c_9859,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9857]) ).
tff(c_9861,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9859,c_1214]) ).
tff(c_10190,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_9857]) ).
tff(c_10192,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10190,c_1214]) ).
tff(c_10193,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_10194,plain,
multiply(sk_c1,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_10,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_10222,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10194,c_10]) ).
tff(c_16,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_10208,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10194,c_16]) ).
tff(c_14,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_10228,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_10194,c_14]) ).
tff(c_10400,plain,
! [X3_144] :
( ( inverse(X3_144) != sk_c6 )
| ( multiply(X3_144,sk_c6) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_10420,plain,
( ( inverse(inverse(sk_c6)) != sk_c6 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_10400]) ).
tff(c_10429,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_10420]) ).
tff(c_10212,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10208,c_4]) ).
tff(c_10234,plain,
! [X_136,Y_137,Z_138] : ( multiply(multiply(X_136,Y_137),Z_138) = multiply(X_136,multiply(Y_137,Z_138)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_10255,plain,
! [Z_138] : ( multiply(sk_c6,multiply(sk_c4,Z_138)) = multiply(identity,Z_138) ),
inference(superposition,[status(thm),theory(equality)],[c_10212,c_10234]) ).
tff(c_10340,plain,
! [Z_142] : ( multiply(sk_c6,multiply(sk_c4,Z_142)) = Z_142 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10255]) ).
tff(c_10352,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_10228,c_10340]) ).
tff(c_10270,plain,
! [X_2,Z_138] : ( multiply(inverse(X_2),multiply(X_2,Z_138)) = multiply(identity,Z_138) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_10234]) ).
tff(c_10438,plain,
! [X_145,Z_146] : ( multiply(inverse(X_145),multiply(X_145,Z_146)) = Z_146 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10270]) ).
tff(c_10468,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10352,c_10438]) ).
tff(c_10534,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10468]) ).
tff(c_10198,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10193,c_4]) ).
tff(c_10258,plain,
! [Z_138] : ( multiply(sk_c7,multiply(sk_c3,Z_138)) = multiply(identity,Z_138) ),
inference(superposition,[status(thm),theory(equality)],[c_10198,c_10234]) ).
tff(c_10363,plain,
! [Z_143] : ( multiply(sk_c7,multiply(sk_c3,Z_143)) = Z_143 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10258]) ).
tff(c_10378,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10222,c_10363]) ).
tff(c_10462,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_10378,c_10438]) ).
tff(c_10533,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10462]) ).
tff(c_10564,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10533,c_8]) ).
tff(c_10577,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10534,c_10564]) ).
tff(c_10285,plain,
! [X_2,Z_138] : ( multiply(inverse(X_2),multiply(X_2,Z_138)) = Z_138 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10270]) ).
tff(c_10581,plain,
multiply(inverse(identity),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10577,c_10285]) ).
tff(c_10593,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10581]) ).
tff(c_10595,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10429,c_10593]) ).
tff(c_10597,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_10420]) ).
tff(c_10424,plain,
( ( inverse(identity) != sk_c6 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_10400]) ).
tff(c_10428,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_10424]) ).
tff(c_10598,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_10597,c_10428]) ).
tff(c_10608,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10597,c_10193]) ).
tff(c_10618,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10608,c_4]) ).
tff(c_10644,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_10618,c_2]) ).
tff(c_10605,plain,
multiply(sk_c3,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10597,c_10222]) ).
tff(c_10653,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10644,c_10605]) ).
tff(c_10656,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10653]) ).
tff(c_10658,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10598,c_10656]) ).
tff(c_10660,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_10424]) ).
tff(c_10416,plain,
( ( inverse(sk_c4) != sk_c6 )
| ( sk_c7 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10228,c_10400]) ).
tff(c_10427,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10208,c_10416]) ).
tff(c_10662,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10660,c_10427]) ).
tff(c_10267,plain,
! [Z_138] : ( multiply(sk_c6,multiply(sk_c2,Z_138)) = multiply(identity,Z_138) ),
inference(superposition,[status(thm),theory(equality)],[c_69,c_10234]) ).
tff(c_10288,plain,
! [Z_139] : ( multiply(sk_c6,multiply(sk_c2,Z_139)) = Z_139 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10267]) ).
tff(c_10300,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_91,c_10288]) ).
tff(c_10664,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10660,c_10660,c_10378]) ).
tff(c_10672,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10300,c_10664]) ).
tff(c_10678,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10662,c_10672]) ).
tff(c_10679,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_10801,plain,
! [X2_152] :
( ( inverse(X2_152) != sk_c6 )
| ( multiply(X2_152,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_10679]) ).
tff(c_10817,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_10228,c_10801]) ).
tff(c_10831,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10208,c_10817]) ).
tff(c_10832,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_10679]) ).
tff(c_10938,plain,
! [X4_157] :
( ( multiply(X4_157,sk_c5) != sk_c6 )
| ( inverse(X4_157) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_10832]) ).
tff(c_10948,plain,
inverse(sk_c2) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_91,c_10938]) ).
tff(c_10961,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_65,c_10948]) ).
tff(c_10963,plain,
! [X1_158] :
( ( inverse(X1_158) != sk_c7 )
| ( multiply(X1_158,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_10832]) ).
tff(c_10970,plain,
inverse(sk_c3) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10222,c_10963]) ).
tff(c_10985,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10193,c_10970]) ).
tff(c_10986,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_11001,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_11033,plain,
! [X_159,Y_160,Z_161] : ( multiply(multiply(X_159,Y_160),Z_161) = multiply(X_159,multiply(Y_160,Z_161)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11063,plain,
! [Z_161] : ( multiply(sk_c6,multiply(sk_c1,Z_161)) = multiply(identity,Z_161) ),
inference(superposition,[status(thm),theory(equality)],[c_77,c_11033]) ).
tff(c_11212,plain,
! [Z_166] : ( multiply(sk_c6,multiply(sk_c1,Z_166)) = Z_166 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11063]) ).
tff(c_11224,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11001,c_11212]) ).
tff(c_11228,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_11224]) ).
tff(c_11241,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11228,c_8]) ).
tff(c_11069,plain,
! [X_2,Z_161] : ( multiply(inverse(X_2),multiply(X_2,Z_161)) = multiply(identity,Z_161) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11033]) ).
tff(c_11340,plain,
! [X_168,Z_169] : ( multiply(inverse(X_168),multiply(X_168,Z_169)) = Z_169 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11069]) ).
tff(c_11388,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11241,c_11340]) ).
tff(c_11410,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11388]) ).
tff(c_10987,plain,
multiply(sk_c2,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_34,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_102]) ).
tff(c_11017,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10987,c_34]) ).
tff(c_11233,plain,
multiply(sk_c3,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11228,c_11017]) ).
tff(c_11364,plain,
multiply(inverse(sk_c3),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11233,c_11340]) ).
tff(c_11408,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10986,c_11364]) ).
tff(c_11496,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11410,c_2,c_11410,c_11408]) ).
tff(c_11238,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11228,c_69]) ).
tff(c_11500,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11496,c_11238]) ).
tff(c_11604,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_11500,c_2]) ).
tff(c_11236,plain,
multiply(sk_c2,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11228,c_10987]) ).
tff(c_11502,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_11496,c_11496,c_11236]) ).
tff(c_11660,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11604,c_11502]) ).
tff(c_11662,plain,
multiply(sk_c1,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_11687,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_11662,c_10]) ).
tff(c_10991,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10986,c_4]) ).
tff(c_11694,plain,
! [X_171,Y_172,Z_173] : ( multiply(multiply(X_171,Y_172),Z_173) = multiply(X_171,multiply(Y_172,Z_173)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11718,plain,
! [Z_173] : ( multiply(sk_c7,multiply(sk_c3,Z_173)) = multiply(identity,Z_173) ),
inference(superposition,[status(thm),theory(equality)],[c_10991,c_11694]) ).
tff(c_12320,plain,
! [Z_189] : ( multiply(sk_c7,multiply(sk_c3,Z_189)) = Z_189 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11718]) ).
tff(c_12332,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11687,c_12320]) ).
tff(c_11727,plain,
! [X_2,Z_173] : ( multiply(inverse(X_2),multiply(X_2,Z_173)) = multiply(identity,Z_173) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11694]) ).
tff(c_12363,plain,
! [X_191,Z_192] : ( multiply(inverse(X_191),multiply(X_191,Z_192)) = Z_192 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11727]) ).
tff(c_12381,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12332,c_12363]) ).
tff(c_12442,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12381]) ).
tff(c_11661,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_11680,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_11662,c_14]) ).
tff(c_11855,plain,
! [X3_179] :
( ( inverse(X3_179) != sk_c6 )
| ( multiply(X3_179,sk_c6) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_11872,plain,
( ( inverse(inverse(sk_c6)) != sk_c6 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11855]) ).
tff(c_11881,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_11872]) ).
tff(c_11666,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11661,c_4]) ).
tff(c_11715,plain,
! [Z_173] : ( multiply(sk_c6,multiply(sk_c4,Z_173)) = multiply(identity,Z_173) ),
inference(superposition,[status(thm),theory(equality)],[c_11666,c_11694]) ).
tff(c_11771,plain,
! [Z_176] : ( multiply(sk_c6,multiply(sk_c4,Z_176)) = Z_176 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11715]) ).
tff(c_11783,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11680,c_11771]) ).
tff(c_11882,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_11727]) ).
tff(c_11912,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11783,c_11882]) ).
tff(c_11972,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11912]) ).
tff(c_11818,plain,
! [Z_178] : ( multiply(sk_c7,multiply(sk_c3,Z_178)) = Z_178 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11718]) ).
tff(c_11833,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11687,c_11818]) ).
tff(c_11903,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11833,c_11882]) ).
tff(c_11971,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11903]) ).
tff(c_12000,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11971,c_8]) ).
tff(c_12041,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11972,c_12000]) ).
tff(c_11742,plain,
! [X_2,Z_173] : ( multiply(inverse(X_2),multiply(X_2,Z_173)) = Z_173 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11727]) ).
tff(c_12045,plain,
multiply(inverse(identity),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_12041,c_11742]) ).
tff(c_12057,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12045]) ).
tff(c_12059,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11881,c_12057]) ).
tff(c_12061,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_11872]) ).
tff(c_11876,plain,
( ( inverse(identity) != sk_c6 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_11855]) ).
tff(c_11880,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_11876]) ).
tff(c_12062,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_12061,c_11880]) ).
tff(c_12072,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12061,c_10986]) ).
tff(c_12082,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12072,c_4]) ).
tff(c_12109,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_12082,c_2]) ).
tff(c_12069,plain,
multiply(sk_c3,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12061,c_11687]) ).
tff(c_12118,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12109,c_12069]) ).
tff(c_12121,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12118]) ).
tff(c_12123,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12062,c_12121]) ).
tff(c_12125,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_11876]) ).
tff(c_11868,plain,
( ( inverse(sk_c4) != sk_c6 )
| ( sk_c7 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11680,c_11855]) ).
tff(c_11879,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11661,c_11868]) ).
tff(c_12127,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12125,c_11879]) ).
tff(c_12136,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12125,c_8]) ).
tff(c_12129,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12125,c_12125,c_11833]) ).
tff(c_12171,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12136,c_12129]) ).
tff(c_12172,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12127,c_12171]) ).
tff(c_12173,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_12285,plain,
! [X2_188] :
( ( inverse(X2_188) != sk_c6 )
| ( multiply(X2_188,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_12173]) ).
tff(c_12298,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11680,c_12285]) ).
tff(c_12311,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_11661,c_12298]) ).
tff(c_12312,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_12173]) ).
tff(c_12344,plain,
! [X4_190] :
( ( multiply(X4_190,sk_c5) != sk_c6 )
| ( inverse(X4_190) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_12312]) ).
tff(c_12359,plain,
( ( sk_c6 != sk_c5 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_12344]) ).
tff(c_12361,plain,
inverse(identity) != sk_c6,
inference(splitLeft,[status(thm)],[c_12359]) ).
tff(c_12451,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_12442,c_12361]) ).
tff(c_12468,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12442,c_65]) ).
tff(c_12515,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12468,c_4]) ).
tff(c_12601,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_12515,c_11742]) ).
tff(c_12613,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12601]) ).
tff(c_12617,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12613,c_12468]) ).
tff(c_12620,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12451,c_12617]) ).
tff(c_12621,plain,
sk_c6 != sk_c5,
inference(splitRight,[status(thm)],[c_12359]) ).
tff(c_12622,plain,
inverse(identity) = sk_c6,
inference(splitRight,[status(thm)],[c_12359]) ).
tff(c_12626,plain,
multiply(sk_c6,identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12622,c_4]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_12633,plain,
! [Z_5] : ( multiply(sk_c6,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_12626,c_6]) ).
tff(c_12636,plain,
! [Z_5] : ( multiply(sk_c6,Z_5) = Z_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_12633]) ).
tff(c_12200,plain,
! [Z_185] : ( multiply(sk_c6,multiply(sk_c4,Z_185)) = Z_185 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11715]) ).
tff(c_12212,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11680,c_12200]) ).
tff(c_12639,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12636,c_12212]) ).
tff(c_12641,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12621,c_12639]) ).
tff(c_12643,plain,
! [X1_195] :
( ( inverse(X1_195) != sk_c7 )
| ( multiply(X1_195,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_12312]) ).
tff(c_12650,plain,
inverse(sk_c3) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11687,c_12643]) ).
tff(c_12665,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10986,c_12650]) ).
tff(c_12667,plain,
inverse(sk_c1) != sk_c6,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_18,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_12707,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12667,c_18]) ).
tff(c_20,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_12684,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_12667,c_20]) ).
tff(c_12688,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12684,c_4]) ).
tff(c_12737,plain,
! [Z_198] : ( multiply(sk_c7,multiply(sk_c3,Z_198)) = multiply(identity,Z_198) ),
inference(superposition,[status(thm),theory(equality)],[c_12688,c_12716]) ).
tff(c_12762,plain,
! [Z_199] : ( multiply(sk_c7,multiply(sk_c3,Z_199)) = Z_199 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12737]) ).
tff(c_12774,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_12707,c_12762]) ).
tff(c_12895,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12774,c_12859]) ).
tff(c_12940,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12895]) ).
tff(c_22,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( inverse(sk_c1) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_12702,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_12667,c_22]) ).
tff(c_12666,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_12671,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12666,c_4]) ).
tff(c_12740,plain,
! [Z_198] : ( multiply(sk_c6,multiply(sk_c4,Z_198)) = multiply(identity,Z_198) ),
inference(superposition,[status(thm),theory(equality)],[c_12671,c_12716]) ).
tff(c_12785,plain,
! [Z_200] : ( multiply(sk_c6,multiply(sk_c4,Z_200)) = Z_200 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12740]) ).
tff(c_12797,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12702,c_12785]) ).
tff(c_12886,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_12797,c_12859]) ).
tff(c_12939,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12886]) ).
tff(c_13061,plain,
multiply(sk_c6,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12939,c_8]) ).
tff(c_13738,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12940,c_13061]) ).
tff(c_13324,plain,
! [X_209,Z_210] : ( multiply(inverse(inverse(X_209)),Z_210) = multiply(X_209,Z_210) ),
inference(superposition,[status(thm),theory(equality)],[c_12760,c_12859]) ).
tff(c_13331,plain,
! [X_209] : ( multiply(X_209,identity) = X_209 ),
inference(superposition,[status(thm),theory(equality)],[c_13324,c_12928]) ).
tff(c_12952,plain,
multiply(sk_c6,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12939,c_8]) ).
tff(c_12973,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12940,c_12952]) ).
tff(c_12946,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_13030,plain,
! [X3_205] :
( ( inverse(X3_205) != identity )
| ( multiply(X3_205,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_12973,c_12940,c_12940,c_12946]) ).
tff(c_13044,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_13030]) ).
tff(c_12964,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12940,c_69]) ).
tff(c_13014,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_12964,c_12760]) ).
tff(c_13026,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13014]) ).
tff(c_12967,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12940,c_65]) ).
tff(c_13046,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13026,c_12967]) ).
tff(c_13054,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13044,c_13046]) ).
tff(c_13055,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_13082,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,identity) != identity )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != identity )
| ( inverse(X2_9) != identity )
| ( multiply(X2_9,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_12940,c_12939,c_12940,c_12940,c_12940,c_12940,c_12939,c_13055]) ).
tff(c_13083,plain,
! [X2_9] :
( ( inverse(X2_9) != identity )
| ( multiply(X2_9,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_13082]) ).
tff(c_13714,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_13331,c_13083]) ).
tff(c_13119,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12940,c_13061]) ).
tff(c_13122,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13119,c_12688]) ).
tff(c_13175,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_13122,c_12760]) ).
tff(c_13187,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13175]) ).
tff(c_13123,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13119,c_12684]) ).
tff(c_13192,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13187,c_13123]) ).
tff(c_13716,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13714,c_13192]) ).
tff(c_13717,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != identity )
| ( multiply(X4_7,identity) != identity )
| ( inverse(X4_7) != identity ) ),
inference(splitRight,[status(thm)],[c_13082]) ).
tff(c_25901,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X4_7 )
| ( inverse(X4_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13926,c_13926,c_13738,c_13738,c_13717]) ).
tff(c_25903,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25901]) ).
tff(c_13072,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12940,c_12671]) ).
tff(c_13786,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_13072,c_12760]) ).
tff(c_13798,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13786]) ).
tff(c_13075,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12940,c_12666]) ).
tff(c_13822,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13798,c_13075]) ).
tff(c_25905,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25903,c_13822]) ).
tff(c_25907,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_25901]) ).
tff(c_25909,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25907,c_13822]) ).
tff(c_25911,plain,
inverse(sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_30,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_25959,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_25911,c_30]) ).
tff(c_32,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_25935,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_25911,c_32]) ).
tff(c_25939,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25935,c_4]) ).
tff(c_25989,plain,
! [Z_338] : ( multiply(sk_c6,multiply(sk_c4,Z_338)) = multiply(identity,Z_338) ),
inference(superposition,[status(thm),theory(equality)],[c_25939,c_25968]) ).
tff(c_26014,plain,
! [Z_339] : ( multiply(sk_c6,multiply(sk_c4,Z_339)) = Z_339 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25989]) ).
tff(c_26026,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_25959,c_26014]) ).
tff(c_26386,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_26026,c_26359]) ).
tff(c_26430,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26386]) ).
tff(c_26,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_25948,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_25911,c_26]) ).
tff(c_25910,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_25915,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25910,c_4]) ).
tff(c_25995,plain,
! [Z_338] : ( multiply(sk_c7,multiply(sk_c3,Z_338)) = multiply(identity,Z_338) ),
inference(superposition,[status(thm),theory(equality)],[c_25915,c_25968]) ).
tff(c_26037,plain,
! [Z_340] : ( multiply(sk_c7,multiply(sk_c3,Z_340)) = Z_340 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25995]) ).
tff(c_26049,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_25948,c_26037]) ).
tff(c_26380,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_26049,c_26359]) ).
tff(c_26429,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26380]) ).
tff(c_26447,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26429,c_8]) ).
tff(c_27131,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26430,c_26447]) ).
tff(c_27135,plain,
multiply(inverse(identity),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_27131,c_26012]) ).
tff(c_27147,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_27135]) ).
tff(c_26702,plain,
! [X_351,Z_352] : ( multiply(inverse(inverse(X_351)),Z_352) = multiply(X_351,Z_352) ),
inference(superposition,[status(thm),theory(equality)],[c_26012,c_26359]) ).
tff(c_26709,plain,
! [X_351] : ( multiply(X_351,identity) = X_351 ),
inference(superposition,[status(thm),theory(equality)],[c_26702,c_26419]) ).
tff(c_26074,plain,
! [X3_342] :
( ( inverse(X3_342) != sk_c6 )
| ( multiply(X3_342,sk_c6) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_26088,plain,
( ( inverse(inverse(sk_c6)) != sk_c6 )
| ( sk_c7 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_26074]) ).
tff(c_26097,plain,
sk_c7 != identity,
inference(splitLeft,[status(thm)],[c_26088]) ).
tff(c_26098,plain,
! [X_343,Z_344] : ( multiply(inverse(X_343),multiply(X_343,Z_344)) = Z_344 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25998]) ).
tff(c_26125,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_26026,c_26098]) ).
tff(c_26169,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26125]) ).
tff(c_26119,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_26049,c_26098]) ).
tff(c_26168,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26119]) ).
tff(c_26189,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26168,c_8]) ).
tff(c_26228,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26169,c_26189]) ).
tff(c_26232,plain,
multiply(inverse(identity),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_26228,c_26012]) ).
tff(c_26244,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26232]) ).
tff(c_26246,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26097,c_26244]) ).
tff(c_26248,plain,
sk_c7 = identity,
inference(splitRight,[status(thm)],[c_26088]) ).
tff(c_26092,plain,
( ( inverse(identity) != sk_c6 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_26074]) ).
tff(c_26096,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_26092]) ).
tff(c_26249,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_26248,c_26096]) ).
tff(c_26256,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26248,c_25915]) ).
tff(c_26276,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_26256,c_2]) ).
tff(c_26255,plain,
multiply(sk_c3,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_26248,c_25948]) ).
tff(c_26309,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26276,c_26255]) ).
tff(c_26310,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26249,c_26309]) ).
tff(c_26312,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_26092]) ).
tff(c_26084,plain,
( ( inverse(sk_c4) != sk_c6 )
| ( sk_c7 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_25959,c_26074]) ).
tff(c_26095,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_25935,c_26084]) ).
tff(c_26314,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26312,c_26095]) ).
tff(c_26321,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26312,c_8]) ).
tff(c_26316,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_26312,c_26312,c_26049]) ).
tff(c_26356,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26321,c_26316]) ).
tff(c_26357,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26314,c_26356]) ).
tff(c_26358,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_26466,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,identity) != identity )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != identity )
| ( inverse(X2_9) != identity )
| ( multiply(X2_9,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26430,c_26429,c_26429,c_26429,c_26429,c_26430,c_26429,c_26358]) ).
tff(c_26467,plain,
! [X2_9] :
( ( inverse(X2_9) != identity )
| ( multiply(X2_9,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_26466]) ).
tff(c_27088,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_26709,c_26467]) ).
tff(c_26442,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26429,c_25939]) ).
tff(c_26561,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_26442,c_2]) ).
tff(c_26443,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26429,c_25935]) ).
tff(c_26572,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26561,c_26443]) ).
tff(c_27090,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27088,c_26572]) ).
tff(c_27091,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != identity )
| ( multiply(X4_7,identity) != identity )
| ( inverse(X4_7) != identity ) ),
inference(splitRight,[status(thm)],[c_26466]) ).
tff(c_37145,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X4_7 )
| ( inverse(X4_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_27346,c_27346,c_27147,c_27147,c_27091]) ).
tff(c_37147,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_37145]) ).
tff(c_27191,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_26442,c_26012]) ).
tff(c_27203,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_27191]) ).
tff(c_27208,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27203,c_26443]) ).
tff(c_37149,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37147,c_27208]) ).
tff(c_37151,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_37145]) ).
tff(c_37153,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37151,c_27208]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP333-1 : TPTP v9.0.0. Released v2.5.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n011.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Apr 7 21:43:03 EDT 2025
% 0.14/0.34 % CPUTime :
% 12.43/4.47 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.43/4.53
% 12.43/4.53 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------