%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP224-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 : n028.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:36 PM UTC 2025
% Result : Unsatisfiable 21.92s 7.77s
% Output : CNFRefutation 22.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 37
% Syntax : Number of formulae : 445 ( 335 unt; 0 typ; 0 def)
% Number of atoms : 680 ( 651 equ)
% Maximal formula atoms : 15 ( 1 avg)
% Number of connectives : 480 ( 245 ~; 235 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 257 ( 257 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c11 > sk_c10 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c10,type,
sk_c10: $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c11,type,
sk_c11: $i ).
tff(sk_c9,type,
sk_c9: $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( multiply(sk_c11,sk_c3) = sk_c10 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_203,axiom,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_257,axiom,
! [X5,X6,X3,X9,X7,X1,X2,X8,X4] :
( ( inverse(X4) != sk_c11 )
| ( multiply(X4,sk_c10) != sk_c11 )
| ( multiply(sk_c11,X5) != sk_c10 )
| ( multiply(X6,sk_c11) != X5 )
| ( inverse(X6) != sk_c11 )
| ( multiply(X2,X1) != sk_c11 )
| ( inverse(X2) != X1 )
| ( multiply(X1,sk_c10) != sk_c11 )
| ( inverse(X3) != sk_c11 )
| ( multiply(X3,sk_c10) != sk_c11 )
| ( multiply(X7,X8) != sk_c10 )
| ( inverse(X7) != X8 )
| ( multiply(X8,sk_c11) != sk_c10 )
| ( inverse(X9) != sk_c10 )
| ( multiply(X9,sk_c11) != sk_c10 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_173,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( inverse(sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c11,sk_c3) = sk_c10 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( inverse(sk_c6) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c5,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c11,sk_c3) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_176,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c8,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_182,axiom,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c11,sk_c3) = sk_c10 )
| ( inverse(sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( inverse(sk_c6) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_188,axiom,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_200,axiom,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_194,axiom,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c6) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_197,axiom,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
file(unknown,unknown) ).
tff(f_209,axiom,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c9) = sk_c10 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_42110,plain,
! [X_476,Y_477,Z_478] : ( multiply(multiply(X_476,Y_477),Z_478) = multiply(X_476,multiply(Y_477,Z_478)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_42158,plain,
! [X_2,Z_478] : ( multiply(inverse(X_2),multiply(X_2,Z_478)) = multiply(identity,Z_478) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42110]) ).
tff(c_42171,plain,
! [X_2,Z_478] : ( multiply(inverse(X_2),multiply(X_2,Z_478)) = Z_478 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42158]) ).
tff(c_42341,plain,
! [X_486,Z_487] : ( multiply(inverse(X_486),multiply(X_486,Z_487)) = Z_487 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42158]) ).
tff(c_43890,plain,
! [X_511,Z_512] : ( multiply(inverse(inverse(X_511)),Z_512) = multiply(X_511,Z_512) ),
inference(superposition,[status(thm),theory(equality)],[c_42171,c_42341]) ).
tff(c_43928,plain,
! [X_511] : ( multiply(X_511,inverse(X_511)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_43890]) ).
tff(c_42437,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42341]) ).
tff(c_43897,plain,
! [X_511] : ( multiply(X_511,identity) = X_511 ),
inference(superposition,[status(thm),theory(equality)],[c_43890,c_42437]) ).
tff(c_42905,plain,
! [X_493,Z_494] : ( multiply(inverse(inverse(X_493)),Z_494) = multiply(X_493,Z_494) ),
inference(superposition,[status(thm),theory(equality)],[c_42171,c_42341]) ).
tff(c_42912,plain,
! [X_493] : ( multiply(X_493,identity) = X_493 ),
inference(superposition,[status(thm),theory(equality)],[c_42905,c_42437]) ).
tff(c_24374,plain,
! [X_286,Y_287,Z_288] : ( multiply(multiply(X_286,Y_287),Z_288) = multiply(X_286,multiply(Y_287,Z_288)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_24422,plain,
! [X_2,Z_288] : ( multiply(inverse(X_2),multiply(X_2,Z_288)) = multiply(identity,Z_288) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_24374]) ).
tff(c_24435,plain,
! [X_2,Z_288] : ( multiply(inverse(X_2),multiply(X_2,Z_288)) = Z_288 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24422]) ).
tff(c_25194,plain,
! [X_307,Z_308] : ( multiply(inverse(X_307),multiply(X_307,Z_308)) = Z_308 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24422]) ).
tff(c_27757,plain,
! [X_349,Z_350] : ( multiply(inverse(inverse(X_349)),Z_350) = multiply(X_349,Z_350) ),
inference(superposition,[status(thm),theory(equality)],[c_24435,c_25194]) ).
tff(c_27795,plain,
! [X_349] : ( multiply(X_349,inverse(X_349)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_27757]) ).
tff(c_50,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_161,plain,
multiply(sk_c11,sk_c3) = sk_c10,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_70,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_172,plain,
multiply(sk_c2,sk_c11) = sk_c3,
inference(splitLeft,[status(thm)],[c_70]) ).
tff(c_100,plain,
( ( inverse(sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_203]) ).
tff(c_125,plain,
inverse(sk_c2) = sk_c11,
inference(splitLeft,[status(thm)],[c_100]) ).
tff(c_129,plain,
multiply(sk_c11,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_125,c_4]) ).
tff(c_209,plain,
! [X_17,Y_18,Z_19] : ( multiply(multiply(X_17,Y_18),Z_19) = multiply(X_17,multiply(Y_18,Z_19)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_236,plain,
! [Z_19] : ( multiply(sk_c11,multiply(sk_c2,Z_19)) = multiply(identity,Z_19) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_209]) ).
tff(c_274,plain,
! [Z_21] : ( multiply(sk_c11,multiply(sk_c2,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_236]) ).
tff(c_286,plain,
multiply(sk_c11,sk_c3) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_172,c_274]) ).
tff(c_290,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_161,c_286]) ).
tff(c_40,plain,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_155,plain,
multiply(sk_c1,sk_c10) = sk_c11,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_10,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_137,plain,
inverse(sk_c1) = sk_c11,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_141,plain,
multiply(sk_c11,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_137,c_4]) ).
tff(c_233,plain,
! [Z_19] : ( multiply(sk_c11,multiply(sk_c1,Z_19)) = multiply(identity,Z_19) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_209]) ).
tff(c_251,plain,
! [Z_20] : ( multiply(sk_c11,multiply(sk_c1,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_233]) ).
tff(c_263,plain,
multiply(sk_c11,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_155,c_251]) ).
tff(c_292,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_290,c_290,c_263]) ).
tff(c_239,plain,
! [X_2,Z_19] : ( multiply(inverse(X_2),multiply(X_2,Z_19)) = multiply(identity,Z_19) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_209]) ).
tff(c_249,plain,
! [X_2,Z_19] : ( multiply(inverse(X_2),multiply(X_2,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_239]) ).
tff(c_1013,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_292,c_249]) ).
tff(c_1019,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1013]) ).
tff(c_936,plain,
! [X_34,Z_35] : ( multiply(inverse(X_34),multiply(X_34,Z_35)) = Z_35 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_239]) ).
tff(c_1178,plain,
! [X_38,Z_39] : ( multiply(inverse(inverse(X_38)),Z_39) = multiply(X_38,Z_39) ),
inference(superposition,[status(thm),theory(equality)],[c_249,c_936]) ).
tff(c_972,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_936]) ).
tff(c_1185,plain,
! [X_38] : ( multiply(X_38,identity) = X_38 ),
inference(superposition,[status(thm),theory(equality)],[c_1178,c_972]) ).
tff(c_1216,plain,
! [X_38] : ( multiply(X_38,inverse(X_38)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1178]) ).
tff(c_367,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_239]) ).
tff(c_385,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_292,c_367]) ).
tff(c_419,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_385]) ).
tff(c_644,plain,
! [X_27,Z_28] : ( multiply(inverse(inverse(X_27)),Z_28) = multiply(X_27,Z_28) ),
inference(superposition,[status(thm),theory(equality)],[c_249,c_367]) ).
tff(c_412,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_367]) ).
tff(c_651,plain,
! [X_27] : ( multiply(X_27,identity) = X_27 ),
inference(superposition,[status(thm),theory(equality)],[c_644,c_412]) ).
tff(c_108,plain,
! [X2_12,X7_10,X3_8,X9_9,X4_14,X6_7] :
( ( multiply(X9_9,sk_c11) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X6_7) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_7,sk_c11)) != sk_c10 )
| ( multiply(X4_14,sk_c10) != sk_c11 )
| ( inverse(X4_14) != sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_257]) ).
tff(c_312,plain,
! [X2_12,X7_10,X3_8,X9_9,X4_14,X6_7] :
( ( multiply(X9_9,sk_c10) != sk_c10 )
| ( inverse(X9_9) != sk_c10 )
| ( multiply(inverse(X7_10),sk_c10) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c10 )
| ( inverse(X3_8) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c10 )
| ( multiply(X4_14,sk_c10) != sk_c10 )
| ( inverse(X4_14) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_290,c_290,c_290,c_290,c_290,c_290,c_290,c_290,c_290,c_290,c_290,c_108]) ).
tff(c_313,plain,
! [X4_14] :
( ( multiply(X4_14,sk_c10) != sk_c10 )
| ( inverse(X4_14) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_312]) ).
tff(c_903,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_419,c_651,c_419,c_419,c_313]) ).
tff(c_297,plain,
multiply(sk_c10,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_290,c_141]) ).
tff(c_431,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_419,c_297]) ).
tff(c_524,plain,
sk_c1 = identity,
inference(superposition,[status(thm),theory(equality)],[c_431,c_2]) ).
tff(c_298,plain,
inverse(sk_c1) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_290,c_137]) ).
tff(c_433,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_419,c_298]) ).
tff(c_553,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_433]) ).
tff(c_905,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_903,c_553]) ).
tff(c_906,plain,
! [X2_12,X7_10,X3_8,X9_9,X6_7] :
( ( inverse(X6_7) != sk_c10 )
| ( multiply(sk_c10,multiply(X6_7,sk_c10)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c10 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c10 )
| ( inverse(X3_8) != sk_c10 )
| ( multiply(inverse(X7_10),sk_c10) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X9_9,sk_c10) != sk_c10 )
| ( inverse(X9_9) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_312]) ).
tff(c_9045,plain,
! [X2_12,X7_10,X3_8,X9_9,X6_7] :
( ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X2_12) != identity )
| ( identity != X3_8 )
| ( inverse(X3_8) != identity )
| ( inverse(X7_10) != identity )
| ( identity != X9_9 )
| ( inverse(X9_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1019,c_1185,c_1019,c_1019,c_1216,c_1019,c_1185,c_1019,c_1019,c_1019,c_1185,c_1019,c_1019,c_1216,c_1019,c_1185,c_1019,c_1019,c_1185,c_1019,c_1019,c_2,c_1019,c_1019,c_906]) ).
tff(c_9047,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9045]) ).
tff(c_910,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_298,c_4]) ).
tff(c_1089,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1019,c_910]) ).
tff(c_1025,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1019,c_298]) ).
tff(c_1091,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1089,c_1025]) ).
tff(c_9049,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9047,c_1091]) ).
tff(c_9050,plain,
! [X7_10,X6_7,X2_12,X3_8] :
( ( inverse(X7_10) != identity )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 )
| ( inverse(X2_12) != identity )
| ( identity != X3_8 )
| ( inverse(X3_8) != identity ) ),
inference(splitRight,[status(thm)],[c_9045]) ).
tff(c_18694,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9050]) ).
tff(c_18696,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18694,c_1091]) ).
tff(c_18697,plain,
! [X2_12,X7_10,X6_7] :
( ( inverse(X2_12) != identity )
| ( inverse(X7_10) != identity )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(splitRight,[status(thm)],[c_9050]) ).
tff(c_18699,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_18697]) ).
tff(c_18701,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18699,c_1091]) ).
tff(c_18702,plain,
! [X7_10,X2_12] :
( ( inverse(X7_10) != identity )
| ( inverse(X2_12) != identity ) ),
inference(splitRight,[status(thm)],[c_18697]) ).
tff(c_18704,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitLeft,[status(thm)],[c_18702]) ).
tff(c_18706,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18704,c_1091]) ).
tff(c_18707,plain,
! [X7_10] : ( inverse(X7_10) != identity ),
inference(splitRight,[status(thm)],[c_18702]) ).
tff(c_18709,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18707,c_1091]) ).
tff(c_18711,plain,
multiply(sk_c2,sk_c11) != sk_c3,
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_78,plain,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_18776,plain,
multiply(sk_c7,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_18711,c_78]) ).
tff(c_80,plain,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_18748,plain,
inverse(sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_18711,c_80]) ).
tff(c_18752,plain,
multiply(sk_c8,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18748,c_4]) ).
tff(c_18812,plain,
! [X_182,Y_183,Z_184] : ( multiply(multiply(X_182,Y_183),Z_184) = multiply(X_182,multiply(Y_183,Z_184)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_18845,plain,
! [Z_184] : ( multiply(sk_c8,multiply(sk_c7,Z_184)) = multiply(identity,Z_184) ),
inference(superposition,[status(thm),theory(equality)],[c_18752,c_18812]) ).
tff(c_19010,plain,
! [Z_191] : ( multiply(sk_c8,multiply(sk_c7,Z_191)) = Z_191 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18845]) ).
tff(c_19022,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_18776,c_19010]) ).
tff(c_18869,plain,
! [X_2,Z_184] : ( multiply(inverse(X_2),multiply(X_2,Z_184)) = multiply(identity,Z_184) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18812]) ).
tff(c_19176,plain,
! [X_197,Z_198] : ( multiply(inverse(X_197),multiply(X_197,Z_198)) = Z_198 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18869]) ).
tff(c_19215,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_19022,c_19176]) ).
tff(c_19305,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19215]) ).
tff(c_68,plain,
( ( multiply(sk_c4,sk_c5) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_18771,plain,
multiply(sk_c4,sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_18711,c_68]) ).
tff(c_18710,plain,
inverse(sk_c4) = sk_c5,
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_18715,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18710,c_4]) ).
tff(c_18854,plain,
! [Z_184] : ( multiply(sk_c5,multiply(sk_c4,Z_184)) = multiply(identity,Z_184) ),
inference(superposition,[status(thm),theory(equality)],[c_18715,c_18812]) ).
tff(c_19033,plain,
! [Z_192] : ( multiply(sk_c5,multiply(sk_c4,Z_192)) = Z_192 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18854]) ).
tff(c_19045,plain,
multiply(sk_c5,sk_c11) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_18771,c_19033]) ).
tff(c_19209,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_19045,c_19176]) ).
tff(c_19304,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19209]) ).
tff(c_19491,plain,
multiply(identity,sk_c3) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_19304,c_161]) ).
tff(c_19893,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19305,c_19491]) ).
tff(c_18883,plain,
! [X_2,Z_184] : ( multiply(inverse(X_2),multiply(X_2,Z_184)) = Z_184 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18869]) ).
tff(c_19897,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_19893,c_18883]) ).
tff(c_19909,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19897]) ).
tff(c_19496,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19304,c_125]) ).
tff(c_19587,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_19496,c_4]) ).
tff(c_19646,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_19587,c_18883]) ).
tff(c_19658,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19646]) ).
tff(c_19490,plain,
multiply(sk_c2,identity) != sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_19304,c_18711]) ).
tff(c_19926,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_19909,c_2,c_19658,c_19490]) ).
tff(c_19928,plain,
multiply(sk_c11,sk_c3) != sk_c10,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_48,plain,
( ( multiply(sk_c4,sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_20014,plain,
multiply(sk_c4,sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_19928,c_48]) ).
tff(c_19927,plain,
inverse(sk_c4) = sk_c5,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_19948,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_19927,c_4]) ).
tff(c_20055,plain,
! [X_204,Y_205,Z_206] : ( multiply(multiply(X_204,Y_205),Z_206) = multiply(X_204,multiply(Y_205,Z_206)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20097,plain,
! [Z_206] : ( multiply(sk_c5,multiply(sk_c4,Z_206)) = multiply(identity,Z_206) ),
inference(superposition,[status(thm),theory(equality)],[c_19948,c_20055]) ).
tff(c_20451,plain,
! [Z_218] : ( multiply(sk_c5,multiply(sk_c4,Z_218)) = Z_218 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20097]) ).
tff(c_20463,plain,
multiply(sk_c5,sk_c11) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_20014,c_20451]) ).
tff(c_20112,plain,
! [X_2,Z_206] : ( multiply(inverse(X_2),multiply(X_2,Z_206)) = multiply(identity,Z_206) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20055]) ).
tff(c_20515,plain,
! [X_220,Z_221] : ( multiply(inverse(X_220),multiply(X_220,Z_221)) = Z_221 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20112]) ).
tff(c_20542,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_20463,c_20515]) ).
tff(c_20646,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20542]) ).
tff(c_20106,plain,
! [Z_206] : ( multiply(sk_c11,multiply(sk_c1,Z_206)) = multiply(identity,Z_206) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_20055]) ).
tff(c_20128,plain,
! [Z_207] : ( multiply(sk_c11,multiply(sk_c1,Z_207)) = Z_207 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20106]) ).
tff(c_20140,plain,
multiply(sk_c11,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_155,c_20128]) ).
tff(c_20675,plain,
multiply(identity,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20646,c_20646,c_20140]) ).
tff(c_20692,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20675]) ).
tff(c_74,plain,
( ( inverse(sk_c6) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_19969,plain,
multiply(sk_c2,sk_c11) = sk_c3,
inference(splitLeft,[status(thm)],[c_74]) ).
tff(c_20109,plain,
! [Z_206] : ( multiply(sk_c11,multiply(sk_c2,Z_206)) = multiply(identity,Z_206) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_20055]) ).
tff(c_20151,plain,
! [Z_208] : ( multiply(sk_c11,multiply(sk_c2,Z_208)) = Z_208 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20109]) ).
tff(c_20163,plain,
multiply(sk_c11,sk_c3) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_19969,c_20151]) ).
tff(c_20167,plain,
sk_c11 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20163,c_19928]) ).
tff(c_20673,plain,
sk_c10 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20646,c_20167]) ).
tff(c_20710,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20692,c_20673]) ).
tff(c_20711,plain,
inverse(sk_c6) = sk_c11,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_20712,plain,
multiply(sk_c2,sk_c11) != sk_c3,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_76,plain,
( ( multiply(sk_c6,sk_c10) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_20796,plain,
multiply(sk_c6,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_20712,c_76]) ).
tff(c_20803,plain,
! [X_222,Y_223,Z_224] : ( multiply(multiply(X_222,Y_223),Z_224) = multiply(X_222,multiply(Y_223,Z_224)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20851,plain,
! [Z_224] : ( multiply(sk_c11,multiply(sk_c1,Z_224)) = multiply(identity,Z_224) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_20803]) ).
tff(c_20963,plain,
! [Z_229] : ( multiply(sk_c11,multiply(sk_c1,Z_229)) = Z_229 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20851]) ).
tff(c_20975,plain,
multiply(sk_c11,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_155,c_20963]) ).
tff(c_72,plain,
( ( multiply(sk_c5,sk_c10) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_20765,plain,
multiply(sk_c5,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_20712,c_72]) ).
tff(c_20760,plain,
multiply(sk_c4,sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_20712,c_68]) ).
tff(c_20842,plain,
! [Z_224] : ( multiply(sk_c5,multiply(sk_c4,Z_224)) = multiply(identity,Z_224) ),
inference(superposition,[status(thm),theory(equality)],[c_19948,c_20803]) ).
tff(c_21049,plain,
! [Z_233] : ( multiply(sk_c5,multiply(sk_c4,Z_233)) = Z_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20842]) ).
tff(c_21061,plain,
multiply(sk_c5,sk_c11) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_20760,c_21049]) ).
tff(c_58,plain,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_20773,plain,
multiply(sk_c7,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_19928,c_58]) ).
tff(c_20732,plain,
inverse(sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20712,c_80]) ).
tff(c_20736,plain,
multiply(sk_c8,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20732,c_4]) ).
tff(c_20836,plain,
! [Z_224] : ( multiply(sk_c8,multiply(sk_c7,Z_224)) = multiply(identity,Z_224) ),
inference(superposition,[status(thm),theory(equality)],[c_20736,c_20803]) ).
tff(c_21018,plain,
! [Z_232] : ( multiply(sk_c8,multiply(sk_c7,Z_232)) = Z_232 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20836]) ).
tff(c_21030,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_20773,c_21018]) ).
tff(c_82,plain,
( ( multiply(sk_c8,sk_c11) = sk_c10 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_20780,plain,
multiply(sk_c8,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_20712,c_82]) ).
tff(c_21286,plain,
! [Z_240] : ( multiply(sk_c8,multiply(sk_c11,Z_240)) = multiply(sk_c10,Z_240) ),
inference(superposition,[status(thm),theory(equality)],[c_20780,c_20803]) ).
tff(c_21307,plain,
multiply(sk_c8,sk_c10) = multiply(sk_c10,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_20975,c_21286]) ).
tff(c_21324,plain,
multiply(sk_c10,sk_c11) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_21030,c_21307]) ).
tff(c_20848,plain,
! [Z_224] : ( multiply(sk_c1,multiply(sk_c10,Z_224)) = multiply(sk_c11,Z_224) ),
inference(superposition,[status(thm),theory(equality)],[c_155,c_20803]) ).
tff(c_21328,plain,
multiply(sk_c11,sk_c11) = multiply(sk_c1,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_21324,c_20848]) ).
tff(c_21334,plain,
multiply(sk_c1,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20975,c_21328]) ).
tff(c_20869,plain,
! [Z_224] : ( multiply(sk_c11,multiply(sk_c1,Z_224)) = Z_224 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20851]) ).
tff(c_21339,plain,
multiply(sk_c11,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_21334,c_20869]) ).
tff(c_86,plain,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_20755,plain,
multiply(sk_c9,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_20712,c_86]) ).
tff(c_64,plain,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_19929,plain,
multiply(sk_c11,sk_c3) = sk_c10,
inference(splitLeft,[status(thm)],[c_64]) ).
tff(c_19942,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_19929,c_19928]) ).
tff(c_19943,plain,
inverse(sk_c9) = sk_c10,
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_19955,plain,
multiply(sk_c10,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_19943,c_4]) ).
tff(c_20845,plain,
! [Z_224] : ( multiply(sk_c10,multiply(sk_c9,Z_224)) = multiply(identity,Z_224) ),
inference(superposition,[status(thm),theory(equality)],[c_19955,c_20803]) ).
tff(c_21240,plain,
! [Z_238] : ( multiply(sk_c10,multiply(sk_c9,Z_238)) = Z_238 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20845]) ).
tff(c_21255,plain,
multiply(sk_c10,sk_c10) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_20755,c_21240]) ).
tff(c_22301,plain,
! [Z_252] : ( multiply(sk_c5,multiply(sk_c10,Z_252)) = multiply(sk_c11,Z_252) ),
inference(superposition,[status(thm),theory(equality)],[c_20765,c_20803]) ).
tff(c_22331,plain,
multiply(sk_c5,sk_c11) = multiply(sk_c11,sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_21255,c_22301]) ).
tff(c_22345,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_21061,c_21339,c_22331]) ).
tff(c_22359,plain,
multiply(sk_c5,sk_c10) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22345,c_22345,c_21030]) ).
tff(c_22365,plain,
sk_c5 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_20765,c_22359]) ).
tff(c_22372,plain,
multiply(sk_c11,sk_c11) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_22365,c_22365,c_21061]) ).
tff(c_22378,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20975,c_22372]) ).
tff(c_22388,plain,
sk_c5 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22378,c_22365]) ).
tff(c_22370,plain,
sk_c8 = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_22365,c_22345]) ).
tff(c_22387,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22378,c_22370]) ).
tff(c_22328,plain,
multiply(sk_c5,sk_c8) = multiply(sk_c11,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_21324,c_22301]) ).
tff(c_22344,plain,
multiply(sk_c5,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20975,c_22328]) ).
tff(c_22489,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22388,c_22387,c_22344]) ).
tff(c_20857,plain,
! [X_2,Z_224] : ( multiply(inverse(X_2),multiply(X_2,Z_224)) = multiply(identity,Z_224) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20803]) ).
tff(c_22498,plain,
! [X_254,Z_255] : ( multiply(inverse(X_254),multiply(X_254,Z_255)) = Z_255 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20857]) ).
tff(c_22516,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_22489,c_22498]) ).
tff(c_22574,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22516]) ).
tff(c_22405,plain,
inverse(sk_c1) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_22378,c_137]) ).
tff(c_22484,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22405,c_4]) ).
tff(c_22617,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22574,c_22484]) ).
tff(c_22595,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22574,c_22405]) ).
tff(c_22696,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22617,c_22595]) ).
tff(c_20854,plain,
! [Z_224] : ( multiply(sk_c11,multiply(sk_c2,Z_224)) = multiply(identity,Z_224) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_20803]) ).
tff(c_20870,plain,
! [Z_224] : ( multiply(sk_c11,multiply(sk_c2,Z_224)) = Z_224 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20854]) ).
tff(c_20933,plain,
! [X4_228] :
( ( multiply(X4_228,sk_c10) != sk_c11 )
| ( inverse(X4_228) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_108]) ).
tff(c_20943,plain,
inverse(sk_c6) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_20796,c_20933]) ).
tff(c_20961,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20711,c_20943]) ).
tff(c_20962,plain,
! [X2_12,X7_10,X3_8,X9_9,X6_7] :
( ( inverse(X6_7) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_7,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X9_9,sk_c11) != sk_c10 )
| ( inverse(X9_9) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_108]) ).
tff(c_21205,plain,
! [X9_237] :
( ( multiply(X9_237,sk_c11) != sk_c10 )
| ( inverse(X9_237) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_20962]) ).
tff(c_21224,plain,
inverse(sk_c9) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_20755,c_21205]) ).
tff(c_21238,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_19943,c_21224]) ).
tff(c_21239,plain,
! [X7_10,X3_8,X2_12,X6_7] :
( ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X6_7) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_7,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_20962]) ).
tff(c_21505,plain,
! [X6_242] :
( ( inverse(X6_242) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_242,sk_c11)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_21239]) ).
tff(c_21522,plain,
( ( inverse(sk_c2) != sk_c11 )
| ( sk_c11 != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_20870,c_21505]) ).
tff(c_21554,plain,
sk_c11 != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_125,c_21522]) ).
tff(c_21883,plain,
! [Z_246] : ( multiply(sk_c4,multiply(sk_c5,Z_246)) = multiply(sk_c11,Z_246) ),
inference(superposition,[status(thm),theory(equality)],[c_20760,c_20803]) ).
tff(c_21898,plain,
multiply(sk_c4,sk_c5) = multiply(sk_c11,sk_c11),
inference(superposition,[status(thm),theory(equality)],[c_21061,c_21883]) ).
tff(c_21911,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_20760,c_20975,c_21898]) ).
tff(c_21913,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21554,c_21911]) ).
tff(c_21914,plain,
! [X2_12,X3_8,X7_10] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_21239]) ).
tff(c_22108,plain,
! [X7_249] :
( ( multiply(inverse(X7_249),sk_c11) != sk_c10 )
| ( multiply(X7_249,inverse(X7_249)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_21914]) ).
tff(c_22110,plain,
( ( multiply(sk_c8,sk_c11) != sk_c10 )
| ( multiply(sk_c7,inverse(sk_c7)) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_20732,c_22108]) ).
tff(c_22126,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20773,c_20732,c_20780,c_22110]) ).
tff(c_22127,plain,
! [X3_8,X2_12] :
( ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_21914]) ).
tff(c_22267,plain,
! [X2_12] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_22127]) ).
tff(c_22418,plain,
! [X2_253] :
( ( multiply(inverse(X2_253),sk_c10) != sk_c10 )
| ( multiply(X2_253,inverse(X2_253)) != sk_c10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_22378,c_22378,c_22267]) ).
tff(c_22423,plain,
( ( sk_c10 != identity )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_22418]) ).
tff(c_22847,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_22696,c_22574,c_22574,c_2,c_22574,c_22574,c_22423]) ).
tff(c_22973,plain,
! [X3_261] :
( ( multiply(X3_261,sk_c10) != sk_c11 )
| ( inverse(X3_261) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_22127]) ).
tff(c_22996,plain,
inverse(sk_c6) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_20796,c_22973]) ).
tff(c_23018,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20711,c_22996]) ).
tff(c_23020,plain,
multiply(sk_c1,sk_c10) != sk_c11,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_28,plain,
( ( multiply(sk_c4,sk_c5) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_23601,plain,
multiply(sk_c4,sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_23020,c_28]) ).
tff(c_30,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_23551,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_23020,c_30]) ).
tff(c_23555,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23551,c_4]) ).
tff(c_23643,plain,
! [X_270,Y_271,Z_272] : ( multiply(multiply(X_270,Y_271),Z_272) = multiply(X_270,multiply(Y_271,Z_272)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_23679,plain,
! [Z_272] : ( multiply(sk_c5,multiply(sk_c4,Z_272)) = multiply(identity,Z_272) ),
inference(superposition,[status(thm),theory(equality)],[c_23555,c_23643]) ).
tff(c_23739,plain,
! [Z_275] : ( multiply(sk_c5,multiply(sk_c4,Z_275)) = Z_275 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23679]) ).
tff(c_23751,plain,
multiply(sk_c5,sk_c11) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_23601,c_23739]) ).
tff(c_23697,plain,
! [X_2,Z_272] : ( multiply(inverse(X_2),multiply(X_2,Z_272)) = multiply(identity,Z_272) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_23643]) ).
tff(c_23950,plain,
! [X_284,Z_285] : ( multiply(inverse(X_284),multiply(X_284,Z_285)) = Z_285 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23697]) ).
tff(c_23989,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_23751,c_23950]) ).
tff(c_24069,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_23989]) ).
tff(c_24098,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24069,c_137]) ).
tff(c_24134,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24098,c_4]) ).
tff(c_23711,plain,
! [X_2,Z_272] : ( multiply(inverse(X_2),multiply(X_2,Z_272)) = Z_272 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23697]) ).
tff(c_24229,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_24134,c_23711]) ).
tff(c_24241,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24229]) ).
tff(c_36,plain,
( ( multiply(sk_c6,sk_c10) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_23633,plain,
multiply(sk_c6,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_23020,c_36]) ).
tff(c_34,plain,
( ( inverse(sk_c6) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_23566,plain,
inverse(sk_c6) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_23020,c_34]) ).
tff(c_23570,plain,
multiply(sk_c11,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23566,c_4]) ).
tff(c_23676,plain,
! [Z_272] : ( multiply(sk_c11,multiply(sk_c6,Z_272)) = multiply(identity,Z_272) ),
inference(superposition,[status(thm),theory(equality)],[c_23570,c_23643]) ).
tff(c_23852,plain,
! [Z_280] : ( multiply(sk_c11,multiply(sk_c6,Z_280)) = Z_280 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23676]) ).
tff(c_23864,plain,
multiply(sk_c11,sk_c11) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_23633,c_23852]) ).
tff(c_24082,plain,
multiply(identity,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_24069,c_24069,c_23864]) ).
tff(c_24101,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24082]) ).
tff(c_24096,plain,
multiply(sk_c1,sk_c10) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_24069,c_23020]) ).
tff(c_24255,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24241,c_24101,c_24096]) ).
tff(c_24257,plain,
inverse(sk_c1) != sk_c11,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_8,plain,
( ( multiply(sk_c4,sk_c5) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_24324,plain,
multiply(sk_c4,sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_24257,c_8]) ).
tff(c_24256,plain,
inverse(sk_c4) = sk_c5,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_24261,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24256,c_4]) ).
tff(c_24416,plain,
! [Z_288] : ( multiply(sk_c5,multiply(sk_c4,Z_288)) = multiply(identity,Z_288) ),
inference(superposition,[status(thm),theory(equality)],[c_24261,c_24374]) ).
tff(c_24537,plain,
! [Z_294] : ( multiply(sk_c5,multiply(sk_c4,Z_294)) = Z_294 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24416]) ).
tff(c_24549,plain,
multiply(sk_c5,sk_c11) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_24324,c_24537]) ).
tff(c_25257,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_24549,c_25194]) ).
tff(c_25330,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25257]) ).
tff(c_25317,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_25194]) ).
tff(c_27764,plain,
! [X_349] : ( multiply(X_349,identity) = X_349 ),
inference(superposition,[status(thm),theory(equality)],[c_27757,c_25317]) ).
tff(c_25710,plain,
! [X_313,Z_314] : ( multiply(inverse(inverse(X_313)),Z_314) = multiply(X_313,Z_314) ),
inference(superposition,[status(thm),theory(equality)],[c_24435,c_25194]) ).
tff(c_25731,plain,
! [X_313] : ( multiply(X_313,inverse(X_313)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_25710,c_4]) ).
tff(c_25717,plain,
! [X_313] : ( multiply(X_313,identity) = X_313 ),
inference(superposition,[status(thm),theory(equality)],[c_25710,c_25317]) ).
tff(c_18,plain,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_24310,plain,
multiply(sk_c7,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_24257,c_18]) ).
tff(c_20,plain,
( ( inverse(sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_24270,plain,
inverse(sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_24257,c_20]) ).
tff(c_24274,plain,
multiply(sk_c8,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24270,c_4]) ).
tff(c_24413,plain,
! [Z_288] : ( multiply(sk_c8,multiply(sk_c7,Z_288)) = multiply(identity,Z_288) ),
inference(superposition,[status(thm),theory(equality)],[c_24274,c_24374]) ).
tff(c_24582,plain,
! [Z_296] : ( multiply(sk_c8,multiply(sk_c7,Z_296)) = Z_296 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24413]) ).
tff(c_24594,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_24310,c_24582]) ).
tff(c_25248,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_24594,c_25194]) ).
tff(c_25328,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25248]) ).
tff(c_24901,plain,
! [X_303,Z_304] : ( multiply(inverse(X_303),multiply(X_303,Z_304)) = Z_304 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24422]) ).
tff(c_24964,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_24549,c_24901]) ).
tff(c_25037,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24964]) ).
tff(c_24955,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_24594,c_24901]) ).
tff(c_25035,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24955]) ).
tff(c_24,plain,
( ( inverse(sk_c9) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_24278,plain,
inverse(sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_24257,c_24]) ).
tff(c_26,plain,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_24318,plain,
multiply(sk_c9,sk_c11) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_24257,c_26]) ).
tff(c_14,plain,
( ( inverse(sk_c6) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_24296,plain,
inverse(sk_c6) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_24257,c_14]) ).
tff(c_16,plain,
( ( multiply(sk_c6,sk_c10) = sk_c11 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_24350,plain,
multiply(sk_c6,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_24257,c_16]) ).
tff(c_24497,plain,
! [X4_292] :
( ( multiply(X4_292,sk_c10) != sk_c11 )
| ( inverse(X4_292) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_108]) ).
tff(c_24507,plain,
inverse(sk_c6) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_24350,c_24497]) ).
tff(c_24522,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24296,c_24507]) ).
tff(c_24523,plain,
! [X2_12,X7_10,X3_8,X9_9,X6_7] :
( ( inverse(X6_7) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_7,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X9_9,sk_c11) != sk_c10 )
| ( inverse(X9_9) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_108]) ).
tff(c_24755,plain,
! [X9_300] :
( ( multiply(X9_300,sk_c11) != sk_c10 )
| ( inverse(X9_300) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_24523]) ).
tff(c_24774,plain,
inverse(sk_c9) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_24318,c_24755]) ).
tff(c_24788,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24278,c_24774]) ).
tff(c_24789,plain,
! [X7_10,X3_8,X2_12,X6_7] :
( ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X6_7) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_7,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_24523]) ).
tff(c_24893,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_7,sk_c11)) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_24789]) ).
tff(c_25152,plain,
! [X6_306] :
( ( inverse(X6_306) != identity )
| ( multiply(X6_306,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_25037,c_2,c_25037,c_25035,c_25037,c_24893]) ).
tff(c_25171,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_25152]) ).
tff(c_24560,plain,
! [Z_295] : ( multiply(sk_c9,multiply(sk_c11,Z_295)) = multiply(sk_c10,Z_295) ),
inference(superposition,[status(thm),theory(equality)],[c_24318,c_24374]) ).
tff(c_24578,plain,
multiply(sk_c9,identity) = multiply(sk_c10,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_129,c_24560]) ).
tff(c_24282,plain,
multiply(sk_c10,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24278,c_4]) ).
tff(c_24410,plain,
! [Z_288] : ( multiply(sk_c10,multiply(sk_c9,Z_288)) = multiply(identity,Z_288) ),
inference(superposition,[status(thm),theory(equality)],[c_24282,c_24374]) ).
tff(c_24613,plain,
! [Z_297] : ( multiply(sk_c10,multiply(sk_c9,Z_297)) = Z_297 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24410]) ).
tff(c_24625,plain,
multiply(sk_c10,multiply(sk_c10,sk_c2)) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24578,c_24613]) ).
tff(c_25097,plain,
multiply(identity,multiply(identity,sk_c2)) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25035,c_25035,c_24625]) ).
tff(c_25113,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_25097]) ).
tff(c_25129,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25037,c_125]) ).
tff(c_25184,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25113,c_25129]) ).
tff(c_25185,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25171,c_25184]) ).
tff(c_25186,plain,
! [X2_12,X3_8,X7_10] :
( ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_24789]) ).
tff(c_25381,plain,
! [X2_12,X3_8,X7_10] :
( ( multiply(inverse(X2_12),identity) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( multiply(X3_8,identity) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X7_10),sk_c11) != identity )
| ( multiply(X7_10,inverse(X7_10)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_25328,c_25328,c_25328,c_25328,c_25186]) ).
tff(c_25382,plain,
! [X7_10] :
( ( multiply(inverse(X7_10),sk_c11) != identity )
| ( multiply(X7_10,inverse(X7_10)) != identity ) ),
inference(splitLeft,[status(thm)],[c_25381]) ).
tff(c_27441,plain,
! [X7_10] : ( inverse(X7_10) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_25731,c_25717,c_25330,c_25382]) ).
tff(c_25354,plain,
multiply(identity,multiply(identity,sk_c2)) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25328,c_25328,c_24625]) ).
tff(c_25370,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_25354]) ).
tff(c_25393,plain,
inverse(identity) = sk_c11,
inference(demodulation,[status(thm),theory(equality)],[c_25370,c_125]) ).
tff(c_25475,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25330,c_25393]) ).
tff(c_27443,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27441,c_25475]) ).
tff(c_27444,plain,
! [X3_8,X2_12] :
( ( multiply(X3_8,identity) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X2_12),identity) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 ) ),
inference(splitRight,[status(thm)],[c_25381]) ).
tff(c_41969,plain,
! [X3_8,X2_12] :
( ( identity != X3_8 )
| ( inverse(X3_8) != identity )
| ( inverse(X2_12) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_27795,c_25330,c_27764,c_25330,c_25330,c_27764,c_25330,c_27444]) ).
tff(c_41970,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitLeft,[status(thm)],[c_41969]) ).
tff(c_27494,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25330,c_125]) ).
tff(c_27552,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25370,c_27494]) ).
tff(c_41972,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41970,c_27552]) ).
tff(c_41974,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_41969]) ).
tff(c_41976,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41974,c_27552]) ).
tff(c_41978,plain,
inverse(sk_c2) != sk_c11,
inference(splitRight,[status(thm)],[c_100]) ).
tff(c_88,plain,
( ( multiply(sk_c4,sk_c5) = sk_c11 )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_42075,plain,
multiply(sk_c4,sk_c5) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_41978,c_88]) ).
tff(c_90,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_41986,plain,
inverse(sk_c2) = sk_c11,
inference(splitLeft,[status(thm)],[c_90]) ).
tff(c_41987,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41978,c_41986]) ).
tff(c_41988,plain,
inverse(sk_c4) = sk_c5,
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_41993,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_41988,c_4]) ).
tff(c_42152,plain,
! [Z_478] : ( multiply(sk_c5,multiply(sk_c4,Z_478)) = multiply(identity,Z_478) ),
inference(superposition,[status(thm),theory(equality)],[c_41993,c_42110]) ).
tff(c_42196,plain,
! [Z_480] : ( multiply(sk_c5,multiply(sk_c4,Z_480)) = Z_480 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42152]) ).
tff(c_42208,plain,
multiply(sk_c5,sk_c11) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_42075,c_42196]) ).
tff(c_42374,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_42208,c_42341]) ).
tff(c_42445,plain,
sk_c11 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42374]) ).
tff(c_98,plain,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_42087,plain,
multiply(sk_c7,sk_c8) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_41978,c_98]) ).
tff(c_41977,plain,
inverse(sk_c7) = sk_c8,
inference(splitRight,[status(thm)],[c_100]) ).
tff(c_41982,plain,
multiply(sk_c8,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_41977,c_4]) ).
tff(c_42155,plain,
! [Z_478] : ( multiply(sk_c8,multiply(sk_c7,Z_478)) = multiply(identity,Z_478) ),
inference(superposition,[status(thm),theory(equality)],[c_41982,c_42110]) ).
tff(c_42305,plain,
! [Z_484] : ( multiply(sk_c8,multiply(sk_c7,Z_484)) = Z_484 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42155]) ).
tff(c_42317,plain,
multiply(sk_c8,sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_42087,c_42305]) ).
tff(c_42362,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_42317,c_42341]) ).
tff(c_42444,plain,
sk_c10 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42362]) ).
tff(c_94,plain,
( ( inverse(sk_c6) = sk_c11 )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_42030,plain,
inverse(sk_c6) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_41978,c_94]) ).
tff(c_96,plain,
( ( multiply(sk_c6,sk_c10) = sk_c11 )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_42061,plain,
multiply(sk_c6,sk_c10) = sk_c11,
inference(negUnitSimplification,[status(thm)],[c_41978,c_96]) ).
tff(c_42266,plain,
! [X4_483] :
( ( multiply(X4_483,sk_c10) != sk_c11 )
| ( inverse(X4_483) != sk_c11 ) ),
inference(splitLeft,[status(thm)],[c_108]) ).
tff(c_42282,plain,
inverse(sk_c6) != sk_c11,
inference(superposition,[status(thm),theory(equality)],[c_42061,c_42266]) ).
tff(c_42296,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_42030,c_42282]) ).
tff(c_42297,plain,
! [X2_12,X7_10,X3_8,X9_9,X6_7] :
( ( inverse(X6_7) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_7,sk_c11)) != sk_c10 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X9_9,sk_c11) != sk_c10 )
| ( inverse(X9_9) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_108]) ).
tff(c_42455,plain,
! [X9_9] :
( ( multiply(X9_9,sk_c11) != sk_c10 )
| ( inverse(X9_9) != sk_c10 ) ),
inference(splitLeft,[status(thm)],[c_42297]) ).
tff(c_42571,plain,
! [X9_489] :
( ( multiply(X9_489,identity) != identity )
| ( inverse(X9_489) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42444,c_42445,c_42444,c_42455]) ).
tff(c_42590,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_42571]) ).
tff(c_42034,plain,
multiply(sk_c11,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42030,c_4]) ).
tff(c_42476,plain,
multiply(identity,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42445,c_42034]) ).
tff(c_42555,plain,
multiply(inverse(identity),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_42476,c_42171]) ).
tff(c_42567,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42555]) ).
tff(c_42477,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42445,c_42030]) ).
tff(c_42592,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42567,c_42477]) ).
tff(c_42600,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_42590,c_42592]) ).
tff(c_42601,plain,
! [X7_10,X3_8,X2_12,X6_7] :
( ( multiply(inverse(X7_10),sk_c11) != sk_c10 )
| ( multiply(X7_10,inverse(X7_10)) != sk_c10 )
| ( multiply(X3_8,sk_c10) != sk_c11 )
| ( inverse(X3_8) != sk_c11 )
| ( multiply(inverse(X2_12),sk_c10) != sk_c11 )
| ( multiply(X2_12,inverse(X2_12)) != sk_c11 )
| ( inverse(X6_7) != sk_c11 )
| ( multiply(sk_c11,multiply(X6_7,sk_c11)) != sk_c10 ) ),
inference(splitRight,[status(thm)],[c_42297]) ).
tff(c_42642,plain,
! [X7_10,X3_8,X2_12,X6_7] :
( ( multiply(inverse(X7_10),identity) != identity )
| ( multiply(X7_10,inverse(X7_10)) != identity )
| ( multiply(X3_8,identity) != identity )
| ( inverse(X3_8) != identity )
| ( multiply(inverse(X2_12),identity) != identity )
| ( multiply(X2_12,inverse(X2_12)) != identity )
| ( inverse(X6_7) != identity )
| ( multiply(X6_7,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42445,c_2,c_42445,c_42444,c_42445,c_42445,c_42445,c_42444,c_42445,c_42445,c_42444,c_42444,c_42445,c_42444,c_42601]) ).
tff(c_42643,plain,
! [X6_7] :
( ( inverse(X6_7) != identity )
| ( multiply(X6_7,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_42642]) ).
tff(c_43458,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_42912,c_42643]) ).
tff(c_104,plain,
( ( inverse(sk_c9) = sk_c10 )
| ( inverse(sk_c2) = sk_c11 ) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_41997,plain,
inverse(sk_c9) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_41978,c_104]) ).
tff(c_42612,plain,
inverse(sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42444,c_41997]) ).
tff(c_42638,plain,
multiply(identity,sk_c9) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42612,c_4]) ).
tff(c_42667,plain,
multiply(inverse(identity),identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_42638,c_42171]) ).
tff(c_42679,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42667]) ).
tff(c_42683,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42679,c_42612]) ).
tff(c_43460,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43458,c_42683]) ).
tff(c_43461,plain,
! [X2_12,X3_8,X7_10] :
( ( multiply(inverse(X2_12),identity) != identity )
| ( multiply(X2_12,inverse(X2_12)) != identity )
| ( multiply(X3_8,identity) != identity )
| ( inverse(X3_8) != identity )
| ( multiply(inverse(X7_10),identity) != identity )
| ( multiply(X7_10,inverse(X7_10)) != identity ) ),
inference(splitRight,[status(thm)],[c_42642]) ).
tff(c_69317,plain,
! [X2_12,X3_8,X7_10] :
( ( inverse(X2_12) != identity )
| ( identity != X3_8 )
| ( inverse(X3_8) != identity )
| ( inverse(X7_10) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_43928,c_43897,c_43897,c_43928,c_43897,c_43461]) ).
tff(c_69318,plain,
! [X7_10] : ( inverse(X7_10) != identity ),
inference(splitLeft,[status(thm)],[c_69317]) ).
tff(c_43475,plain,
multiply(inverse(identity),identity) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_42638,c_42171]) ).
tff(c_43487,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_43475]) ).
tff(c_43491,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43487,c_42612]) ).
tff(c_69320,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_69318,c_43491]) ).
tff(c_69321,plain,
! [X2_12,X3_8] :
( ( inverse(X2_12) != identity )
| ( identity != X3_8 )
| ( inverse(X3_8) != identity ) ),
inference(splitRight,[status(thm)],[c_69317]) ).
tff(c_69323,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_69321]) ).
tff(c_69325,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_69323,c_43491]) ).
tff(c_69326,plain,
! [X2_12] : ( inverse(X2_12) != identity ),
inference(splitRight,[status(thm)],[c_69321]) ).
tff(c_69329,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_69326,c_43491]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP224-1 : TPTP v9.0.0. Released v2.5.0.
% 0.06/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 : n028.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:37:35 EDT 2025
% 0.13/0.34 % CPUTime :
% 21.92/7.77 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.11/7.80
% 22.11/7.80 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------