%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP277-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 : n029.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:47 PM UTC 2025
% Result : Unsatisfiable 20.66s 7.24s
% Output : CNFRefutation 21.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 27
% Syntax : Number of formulae : 404 ( 341 unt; 0 typ; 0 def)
% Number of atoms : 521 ( 507 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 236 ( 119 ~; 117 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 201 ( 201 !; 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_77,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
! [X2,X1,X3,X4] :
( ( multiply(X2,sk_c7) != sk_c6 )
| ( inverse(X2) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(sk_c5,sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( multiply(X3,X4) != sk_c6 )
| ( inverse(X3) != X4 )
| ( multiply(X4,sk_c7) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c5,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,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_27168,plain,
! [X_294,Y_295,Z_296] : ( multiply(multiply(X_294,Y_295),Z_296) = multiply(X_294,multiply(Y_295,Z_296)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_27201,plain,
! [X_2,Z_296] : ( multiply(inverse(X_2),multiply(X_2,Z_296)) = multiply(identity,Z_296) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_27168]) ).
tff(c_27211,plain,
! [X_2,Z_296] : ( multiply(inverse(X_2),multiply(X_2,Z_296)) = Z_296 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27201]) ).
tff(c_27875,plain,
! [X_308,Z_309] : ( multiply(inverse(X_308),multiply(X_308,Z_309)) = Z_309 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27201]) ).
tff(c_29554,plain,
! [X_334,Z_335] : ( multiply(inverse(inverse(X_334)),Z_335) = multiply(X_334,Z_335) ),
inference(superposition,[status(thm),theory(equality)],[c_27211,c_27875]) ).
tff(c_27938,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_27875]) ).
tff(c_29598,plain,
! [X_336] : ( multiply(X_336,identity) = X_336 ),
inference(superposition,[status(thm),theory(equality)],[c_29554,c_27938]) ).
tff(c_27941,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_27875]) ).
tff(c_29616,plain,
inverse(identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_29598,c_27941]) ).
tff(c_29575,plain,
! [X_334] : ( multiply(X_334,inverse(X_334)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_29554,c_4]) ).
tff(c_24978,plain,
! [X_251,Y_252,Z_253] : ( multiply(multiply(X_251,Y_252),Z_253) = multiply(X_251,multiply(Y_252,Z_253)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_25020,plain,
! [X_2,Z_253] : ( multiply(inverse(X_2),multiply(X_2,Z_253)) = multiply(identity,Z_253) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_24978]) ).
tff(c_25104,plain,
! [X_257,Z_258] : ( multiply(inverse(X_257),multiply(X_257,Z_258)) = Z_258 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25020]) ).
tff(c_25182,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_25104]) ).
tff(c_23445,plain,
! [X_224,Y_225,Z_226] : ( multiply(multiply(X_224,Y_225),Z_226) = multiply(X_224,multiply(Y_225,Z_226)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_23487,plain,
! [X_2,Z_226] : ( multiply(inverse(X_2),multiply(X_2,Z_226)) = multiply(identity,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_23445]) ).
tff(c_24125,plain,
! [X_242,Z_243] : ( multiply(inverse(X_242),multiply(X_242,Z_243)) = Z_243 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23487]) ).
tff(c_24206,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_24125]) ).
tff(c_16,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_99,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_22,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_73,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_77,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_73,c_4]) ).
tff(c_120,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_144,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_77,c_120]) ).
tff(c_158,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_144]) ).
tff(c_170,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_99,c_158]) ).
tff(c_147,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_120]) ).
tff(c_181,plain,
! [X_16,Z_17] : ( multiply(inverse(X_16),multiply(X_16,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_147]) ).
tff(c_199,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_170,c_181]) ).
tff(c_230,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_199]) ).
tff(c_217,plain,
multiply(inverse(sk_c7),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_77,c_181]) ).
tff(c_34,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_91,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_211,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_91,c_181]) ).
tff(c_418,plain,
multiply(inverse(sk_c7),identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_230,c_211]) ).
tff(c_430,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_217,c_418]) ).
tff(c_46,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_86,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_56,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( multiply(sk_c5,sk_c6) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_234,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_91,c_86,c_56]) ).
tff(c_235,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_234]) ).
tff(c_244,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_230,c_235]) ).
tff(c_447,plain,
sk_c7 != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_430,c_244]) ).
tff(c_236,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_230,c_170]) ).
tff(c_141,plain,
! [Z_14] : ( multiply(sk_c5,multiply(sk_c6,Z_14)) = multiply(sk_c7,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_86,c_120]) ).
tff(c_333,plain,
! [Z_19] : ( multiply(sk_c7,Z_19) = multiply(sk_c5,Z_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_230,c_141]) ).
tff(c_354,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_333,c_77]) ).
tff(c_443,plain,
multiply(sk_c1,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_430,c_354]) ).
tff(c_156,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_147]) ).
tff(c_472,plain,
multiply(inverse(sk_c1),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_443,c_156]) ).
tff(c_481,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_236,c_73,c_472]) ).
tff(c_483,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_447,c_481]) ).
tff(c_485,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_234]) ).
tff(c_530,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_230,c_485]) ).
tff(c_4876,plain,
multiply(inverse(sk_c5),identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_230,c_530,c_211]) ).
tff(c_4888,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_4876,c_530,c_217]) ).
tff(c_533,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_530,c_73]) ).
tff(c_4894,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_4888,c_533]) ).
tff(c_488,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_230,c_91]) ).
tff(c_4862,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_530,c_488]) ).
tff(c_4890,plain,
multiply(sk_c1,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4888,c_4888,c_4862]) ).
tff(c_5126,plain,
! [X_84,Z_85] : ( multiply(inverse(inverse(X_84)),Z_85) = multiply(X_84,Z_85) ),
inference(superposition,[status(thm),theory(equality)],[c_156,c_181]) ).
tff(c_223,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_181]) ).
tff(c_5137,plain,
! [X_84] : ( multiply(X_84,identity) = X_84 ),
inference(superposition,[status(thm),theory(equality)],[c_5126,c_223]) ).
tff(c_494,plain,
! [X_21] : ( multiply(inverse(identity),X_21) = X_21 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_181]) ).
tff(c_727,plain,
! [X_24] : ( multiply(inverse(inverse(identity)),X_24) = X_24 ),
inference(superposition,[status(thm),theory(equality)],[c_494,c_156]) ).
tff(c_748,plain,
inverse(identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_727,c_4]) ).
tff(c_836,plain,
! [X_26,Z_27] : ( multiply(inverse(inverse(X_26)),Z_27) = multiply(X_26,Z_27) ),
inference(superposition,[status(thm),theory(equality)],[c_156,c_181]) ).
tff(c_884,plain,
! [X_26] : ( multiply(X_26,inverse(X_26)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_836]) ).
tff(c_603,plain,
multiply(inverse(sk_c5),identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_530,c_230,c_211]) ).
tff(c_615,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_603,c_530,c_217]) ).
tff(c_622,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_615,c_530]) ).
tff(c_138,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c5,Z_14)) = multiply(sk_c6,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_120]) ).
tff(c_641,plain,
! [Z_14] : ( multiply(sk_c1,multiply(sk_c1,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_622,c_615,c_2,c_230,c_138]) ).
tff(c_873,plain,
! [X_2] : ( multiply(X_2,identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_223,c_836]) ).
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_1064,plain,
! [X_31,Y_32,Z_33] : ( multiply(inverse(multiply(X_31,Y_32)),multiply(X_31,multiply(Y_32,Z_33))) = Z_33 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_181]) ).
tff(c_1100,plain,
! [X_31,X_26] : ( multiply(inverse(multiply(X_31,X_26)),multiply(X_31,identity)) = inverse(X_26) ),
inference(superposition,[status(thm),theory(equality)],[c_884,c_1064]) ).
tff(c_1997,plain,
! [X_47,X_48] : ( multiply(inverse(multiply(X_47,X_48)),X_47) = inverse(X_48) ),
inference(demodulation,[status(thm),theory(equality)],[c_873,c_1100]) ).
tff(c_2111,plain,
! [Z_14] : ( multiply(inverse(Z_14),sk_c1) = inverse(multiply(sk_c1,Z_14)) ),
inference(superposition,[status(thm),theory(equality)],[c_641,c_1997]) ).
tff(c_484,plain,
! [X2_6,X1_7,X3_8] :
( ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_234]) ).
tff(c_575,plain,
! [X2_6,X1_7,X3_8] :
( ( inverse(X2_6) != sk_c5 )
| ( multiply(X2_6,sk_c5) != identity )
| ( multiply(X1_7,identity) != sk_c5 )
| ( inverse(X1_7) != sk_c5 )
| ( multiply(inverse(X3_8),sk_c5) != identity )
| ( multiply(X3_8,inverse(X3_8)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_230,c_530,c_230,c_530,c_530,c_230,c_530,c_230,c_530,c_484]) ).
tff(c_576,plain,
! [X3_8] :
( ( multiply(inverse(X3_8),sk_c5) != identity )
| ( multiply(X3_8,inverse(X3_8)) != identity ) ),
inference(splitLeft,[status(thm)],[c_575]) ).
tff(c_4816,plain,
! [X3_78] : ( inverse(multiply(sk_c1,X3_78)) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_884,c_2111,c_615,c_576]) ).
tff(c_4834,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_884,c_4816]) ).
tff(c_4849,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_748,c_4834]) ).
tff(c_4850,plain,
! [X1_7,X2_6] :
( ( multiply(X1_7,identity) != sk_c5 )
| ( inverse(X1_7) != sk_c5 )
| ( inverse(X2_6) != sk_c5 )
| ( multiply(X2_6,sk_c5) != identity ) ),
inference(splitRight,[status(thm)],[c_575]) ).
tff(c_23305,plain,
! [X1_7,X2_6] :
( ( sk_c1 != X1_7 )
| ( inverse(X1_7) != sk_c1 )
| ( inverse(X2_6) != sk_c1 )
| ( multiply(X2_6,sk_c1) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4888,c_4888,c_4888,c_5137,c_4888,c_4850]) ).
tff(c_23307,plain,
! [X2_223] :
( ( inverse(X2_223) != sk_c1 )
| ( multiply(X2_223,sk_c1) != identity ) ),
inference(splitLeft,[status(thm)],[c_23305]) ).
tff(c_23358,plain,
inverse(sk_c1) != sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_4890,c_23307]) ).
tff(c_23384,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4894,c_23358]) ).
tff(c_23386,plain,
inverse(sk_c1) != sk_c1,
inference(splitRight,[status(thm)],[c_23305]) ).
tff(c_23388,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23386,c_4894]) ).
tff(c_23390,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_14,plain,
( ( multiply(sk_c3,sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_23431,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_23390,c_14]) ).
tff(c_23389,plain,
inverse(sk_c3) = sk_c4,
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_23394,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23389,c_4]) ).
tff(c_23475,plain,
! [Z_226] : ( multiply(sk_c4,multiply(sk_c3,Z_226)) = multiply(identity,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_23394,c_23445]) ).
tff(c_24102,plain,
! [Z_241] : ( multiply(sk_c4,multiply(sk_c3,Z_241)) = Z_241 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23475]) ).
tff(c_24114,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_23431,c_24102]) ).
tff(c_24143,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_24114,c_24125]) ).
tff(c_24210,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24143]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_23437,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_23390,c_8]) ).
tff(c_24221,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24210,c_23437]) ).
tff(c_23498,plain,
! [X_2,Z_226] : ( multiply(inverse(X_2),multiply(X_2,Z_226)) = Z_226 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23487]) ).
tff(c_24349,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_24221,c_23498]) ).
tff(c_24361,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24206,c_24349]) ).
tff(c_24227,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_24210,c_86]) ).
tff(c_24419,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24361,c_24227]) ).
tff(c_10,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_23404,plain,
inverse(sk_c2) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_23390,c_10]) ).
tff(c_24427,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24361,c_23404]) ).
tff(c_12,plain,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_23426,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_23390,c_12]) ).
tff(c_23466,plain,
! [Z_226] : ( multiply(sk_c2,multiply(sk_c6,Z_226)) = multiply(sk_c7,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_23426,c_23445]) ).
tff(c_24540,plain,
! [Z_247] : ( multiply(sk_c5,Z_247) = multiply(sk_c2,Z_247) ),
inference(demodulation,[status(thm),theory(equality)],[c_24361,c_2,c_24210,c_23466]) ).
tff(c_23408,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23404,c_4]) ).
tff(c_23481,plain,
! [Z_226] : ( multiply(sk_c5,multiply(sk_c6,Z_226)) = multiply(sk_c7,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_86,c_23445]) ).
tff(c_24364,plain,
! [Z_246] : ( multiply(sk_c7,Z_246) = multiply(sk_c5,Z_246) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24210,c_23481]) ).
tff(c_24409,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23408,c_24364]) ).
tff(c_24552,plain,
multiply(sk_c2,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24540,c_24409]) ).
tff(c_24614,plain,
multiply(inverse(sk_c2),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_24552,c_23498]) ).
tff(c_24620,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_24419,c_24427,c_24614]) ).
tff(c_24660,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_24620,c_24427]) ).
tff(c_24412,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_77,c_24364]) ).
tff(c_24570,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24412,c_24540]) ).
tff(c_24773,plain,
multiply(inverse(sk_c2),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_24570,c_23498]) ).
tff(c_24779,plain,
multiply(sk_c2,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_24660,c_24773]) ).
tff(c_24217,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_24210,c_24114]) ).
tff(c_24226,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24210,c_91]) ).
tff(c_24422,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24361,c_24226]) ).
tff(c_24555,plain,
multiply(sk_c2,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24540,c_24422]) ).
tff(c_24538,plain,
! [Z_226] : ( multiply(sk_c5,Z_226) = multiply(sk_c2,Z_226) ),
inference(demodulation,[status(thm),theory(equality)],[c_24361,c_2,c_24210,c_23466]) ).
tff(c_18,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_23419,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_23390,c_18]) ).
tff(c_23469,plain,
! [Z_226] : ( multiply(sk_c4,multiply(sk_c7,Z_226)) = multiply(sk_c6,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_23419,c_23445]) ).
tff(c_24624,plain,
! [Z_248] : ( multiply(sk_c4,multiply(sk_c2,Z_248)) = Z_248 ),
inference(demodulation,[status(thm),theory(equality)],[c_24538,c_24361,c_2,c_24210,c_23469]) ).
tff(c_24642,plain,
multiply(sk_c4,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_24555,c_24624]) ).
tff(c_24649,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_24217,c_24642]) ).
tff(c_24670,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_24620,c_24649]) ).
tff(c_24673,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_24670,c_24670,c_24217]) ).
tff(c_24815,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_24779,c_24673]) ).
tff(c_24429,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24361,c_73]) ).
tff(c_24661,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_24620,c_24429]) ).
tff(c_24725,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24661,c_4]) ).
tff(c_24871,plain,
multiply(sk_c1,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24815,c_24725]) ).
tff(c_24225,plain,
multiply(sk_c1,sk_c7) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_24210,c_23390]) ).
tff(c_24421,plain,
multiply(sk_c1,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_24361,c_24225]) ).
tff(c_24654,plain,
multiply(sk_c1,sk_c2) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_24620,c_24421]) ).
tff(c_24913,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24871,c_24815,c_24654]) ).
tff(c_24915,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_38,plain,
( ( multiply(sk_c3,sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_24952,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_24915,c_38]) ).
tff(c_40,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_24927,plain,
inverse(sk_c3) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_24915,c_40]) ).
tff(c_24931,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24927,c_4]) ).
tff(c_25008,plain,
! [Z_253] : ( multiply(sk_c4,multiply(sk_c3,Z_253)) = multiply(identity,Z_253) ),
inference(superposition,[status(thm),theory(equality)],[c_24931,c_24978]) ).
tff(c_25056,plain,
! [Z_255] : ( multiply(sk_c4,multiply(sk_c3,Z_255)) = Z_255 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25008]) ).
tff(c_25068,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_24952,c_25056]) ).
tff(c_25128,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_25068,c_25104]) ).
tff(c_25186,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25128]) ).
tff(c_32,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_24972,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_24915,c_32]) ).
tff(c_25197,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_25186,c_24972]) ).
tff(c_25031,plain,
! [X_2,Z_253] : ( multiply(inverse(X_2),multiply(X_2,Z_253)) = Z_253 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25020]) ).
tff(c_25386,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_25197,c_25031]) ).
tff(c_25398,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_25182,c_25386]) ).
tff(c_24914,plain,
inverse(sk_c2) = sk_c7,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_36,plain,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_24963,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_24915,c_36]) ).
tff(c_25198,plain,
multiply(sk_c2,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_25186,c_24963]) ).
tff(c_25274,plain,
multiply(inverse(sk_c2),sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25198,c_25031]) ).
tff(c_25283,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24914,c_25274]) ).
tff(c_25496,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25398,c_25398,c_25283]) ).
tff(c_25202,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_25186,c_24915]) ).
tff(c_25405,plain,
multiply(sk_c5,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_25398,c_25202]) ).
tff(c_25566,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_25496,c_25405]) ).
tff(c_25568,plain,
multiply(sk_c5,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_50,plain,
( ( multiply(sk_c3,sk_c4) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_26100,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_25568,c_50]) ).
tff(c_52,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_25588,plain,
inverse(sk_c3) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_25568,c_52]) ).
tff(c_25592,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25588,c_4]) ).
tff(c_26121,plain,
! [X_273,Y_274,Z_275] : ( multiply(multiply(X_273,Y_274),Z_275) = multiply(X_273,multiply(Y_274,Z_275)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_26148,plain,
! [Z_275] : ( multiply(sk_c4,multiply(sk_c3,Z_275)) = multiply(identity,Z_275) ),
inference(superposition,[status(thm),theory(equality)],[c_25592,c_26121]) ).
tff(c_26211,plain,
! [Z_278] : ( multiply(sk_c4,multiply(sk_c3,Z_278)) = Z_278 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26148]) ).
tff(c_26223,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_26100,c_26211]) ).
tff(c_26160,plain,
! [X_2,Z_275] : ( multiply(inverse(X_2),multiply(X_2,Z_275)) = multiply(identity,Z_275) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_26121]) ).
tff(c_26234,plain,
! [X_279,Z_280] : ( multiply(inverse(X_279),multiply(X_279,Z_280)) = Z_280 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26160]) ).
tff(c_26252,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_26223,c_26234]) ).
tff(c_26310,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26252]) ).
tff(c_26316,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_26310,c_26223]) ).
tff(c_26306,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_26234]) ).
tff(c_25636,plain,
! [X_263,Y_264,Z_265] : ( multiply(multiply(X_263,Y_264),Z_265) = multiply(X_263,multiply(Y_264,Z_265)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_25678,plain,
! [X_2,Z_265] : ( multiply(inverse(X_2),multiply(X_2,Z_265)) = multiply(identity,Z_265) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_25636]) ).
tff(c_25755,plain,
! [X_269,Z_270] : ( multiply(inverse(X_269),multiply(X_269,Z_270)) = Z_270 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25678]) ).
tff(c_25830,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_25755]) ).
tff(c_25604,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_25675,plain,
! [Z_265] : ( multiply(sk_c7,multiply(sk_c1,Z_265)) = multiply(identity,Z_265) ),
inference(superposition,[status(thm),theory(equality)],[c_77,c_25636]) ).
tff(c_25693,plain,
! [Z_266] : ( multiply(sk_c7,multiply(sk_c1,Z_266)) = Z_266 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25675]) ).
tff(c_25705,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_25604,c_25693]) ).
tff(c_25782,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_25705,c_25755]) ).
tff(c_25834,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25782]) ).
tff(c_44,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_25631,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_25568,c_44]) ).
tff(c_25843,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_25834,c_25631]) ).
tff(c_25689,plain,
! [X_2,Z_265] : ( multiply(inverse(X_2),multiply(X_2,Z_265)) = Z_265 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25678]) ).
tff(c_25953,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_25843,c_25689]) ).
tff(c_25965,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_25830,c_25953]) ).
tff(c_25842,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_25834,c_25705]) ).
tff(c_26042,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_25965,c_25965,c_25842]) ).
tff(c_25849,plain,
multiply(sk_c5,identity) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_25834,c_25568]) ).
tff(c_26087,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26042,c_25965,c_25849]) ).
tff(c_26088,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_26322,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26310,c_26088]) ).
tff(c_26171,plain,
! [X_2,Z_275] : ( multiply(inverse(X_2),multiply(X_2,Z_275)) = Z_275 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26160]) ).
tff(c_26407,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_26322,c_26171]) ).
tff(c_26419,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26306,c_26407]) ).
tff(c_25582,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_26323,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26310,c_25582]) ).
tff(c_26499,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26419,c_26323]) ).
tff(c_54,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_26095,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_25568,c_54]) ).
tff(c_26142,plain,
! [Z_275] : ( multiply(sk_c4,multiply(sk_c7,Z_275)) = multiply(sk_c6,Z_275) ),
inference(superposition,[status(thm),theory(equality)],[c_26095,c_26121]) ).
tff(c_26512,plain,
! [Z_282] : ( multiply(sk_c4,multiply(sk_c5,Z_282)) = Z_282 ),
inference(demodulation,[status(thm),theory(equality)],[c_26419,c_2,c_26310,c_26142]) ).
tff(c_26527,plain,
multiply(sk_c4,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_26499,c_26512]) ).
tff(c_26534,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_26316,c_26527]) ).
tff(c_26324,plain,
multiply(sk_c5,identity) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_26310,c_25568]) ).
tff(c_26422,plain,
multiply(sk_c5,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26419,c_26324]) ).
tff(c_26536,plain,
multiply(sk_c4,identity) != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_26534,c_26534,c_26422]) ).
tff(c_26546,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26316,c_26536]) ).
tff(c_26548,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_26574,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_26548,c_38]) ).
tff(c_26547,plain,
inverse(sk_c3) = sk_c4,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_26552,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_26547,c_4]) ).
tff(c_26603,plain,
! [X_283,Y_284,Z_285] : ( multiply(multiply(X_283,Y_284),Z_285) = multiply(X_283,multiply(Y_284,Z_285)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_26633,plain,
! [Z_285] : ( multiply(sk_c4,multiply(sk_c3,Z_285)) = multiply(identity,Z_285) ),
inference(superposition,[status(thm),theory(equality)],[c_26552,c_26603]) ).
tff(c_26655,plain,
! [Z_286] : ( multiply(sk_c4,multiply(sk_c3,Z_286)) = Z_286 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26633]) ).
tff(c_26667,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_26574,c_26655]) ).
tff(c_26642,plain,
! [X_2,Z_285] : ( multiply(inverse(X_2),multiply(X_2,Z_285)) = multiply(identity,Z_285) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_26603]) ).
tff(c_26726,plain,
! [X_289,Z_290] : ( multiply(inverse(X_289),multiply(X_289,Z_290)) = Z_290 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26642]) ).
tff(c_26756,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_26667,c_26726]) ).
tff(c_26806,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_26756]) ).
tff(c_48,plain,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_26583,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_25568,c_48]) ).
tff(c_26621,plain,
! [Z_285] : ( multiply(sk_c2,multiply(sk_c6,Z_285)) = multiply(sk_c7,Z_285) ),
inference(superposition,[status(thm),theory(equality)],[c_26583,c_26603]) ).
tff(c_26894,plain,
! [Z_285] : ( multiply(sk_c7,Z_285) = multiply(sk_c2,Z_285) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26806,c_26621]) ).
tff(c_26821,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_26806,c_26548]) ).
tff(c_26895,plain,
multiply(sk_c2,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_26894,c_26821]) ).
tff(c_26801,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_26726]) ).
tff(c_26567,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_25568,c_44]) ).
tff(c_26820,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26806,c_26567]) ).
tff(c_26653,plain,
! [X_2,Z_285] : ( multiply(inverse(X_2),multiply(X_2,Z_285)) = Z_285 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26642]) ).
tff(c_26993,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_26820,c_26653]) ).
tff(c_27005,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_26801,c_26993]) ).
tff(c_25567,plain,
inverse(sk_c2) = sk_c7,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_25572,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25567,c_4]) ).
tff(c_26636,plain,
! [Z_285] : ( multiply(sk_c7,multiply(sk_c2,Z_285)) = multiply(identity,Z_285) ),
inference(superposition,[status(thm),theory(equality)],[c_25572,c_26603]) ).
tff(c_26678,plain,
! [Z_287] : ( multiply(sk_c7,multiply(sk_c2,Z_287)) = Z_287 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_26636]) ).
tff(c_26690,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_26583,c_26678]) ).
tff(c_26814,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_26806,c_26690]) ).
tff(c_26949,plain,
multiply(sk_c2,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_26894,c_26814]) ).
tff(c_27103,plain,
multiply(sk_c2,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27005,c_26949]) ).
tff(c_27104,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26895,c_27103]) ).
tff(c_27106,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_26,plain,
( ( multiply(sk_c3,sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_27133,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_27106,c_26]) ).
tff(c_28,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_27114,plain,
inverse(sk_c3) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_27106,c_28]) ).
tff(c_27118,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27114,c_4]) ).
tff(c_27195,plain,
! [Z_296] : ( multiply(sk_c4,multiply(sk_c3,Z_296)) = multiply(identity,Z_296) ),
inference(superposition,[status(thm),theory(equality)],[c_27118,c_27168]) ).
tff(c_27213,plain,
! [Z_297] : ( multiply(sk_c4,multiply(sk_c3,Z_297)) = Z_297 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27195]) ).
tff(c_27225,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_27133,c_27213]) ).
tff(c_27905,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_27225,c_27875]) ).
tff(c_27945,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_27905]) ).
tff(c_27953,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27945,c_27225]) ).
tff(c_20,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_27138,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_27106,c_20]) ).
tff(c_27956,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_27945,c_27138]) ).
tff(c_29071,plain,
sk_c7 = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_27956,c_2]) ).
tff(c_24,plain,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_27146,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_27106,c_24]) ).
tff(c_27186,plain,
! [Z_296] : ( multiply(sk_c2,multiply(sk_c6,Z_296)) = multiply(sk_c7,Z_296) ),
inference(superposition,[status(thm),theory(equality)],[c_27146,c_27168]) ).
tff(c_29089,plain,
! [Z_296] : ( multiply(sk_c5,Z_296) = multiply(sk_c2,Z_296) ),
inference(demodulation,[status(thm),theory(equality)],[c_29071,c_2,c_27945,c_27186]) ).
tff(c_27262,plain,
! [X_299,Z_300] : ( multiply(inverse(X_299),multiply(X_299,Z_300)) = Z_300 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27201]) ).
tff(c_27322,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_27262]) ).
tff(c_27286,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_27225,c_27262]) ).
tff(c_27326,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_27286]) ).
tff(c_27336,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_27326,c_27138]) ).
tff(c_27407,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_27336,c_27211]) ).
tff(c_27419,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_27322,c_27407]) ).
tff(c_27433,plain,
! [Z_296] : ( multiply(sk_c5,Z_296) = multiply(sk_c2,Z_296) ),
inference(demodulation,[status(thm),theory(equality)],[c_27419,c_2,c_27326,c_27186]) ).
tff(c_27105,plain,
inverse(sk_c2) = sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_27110,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27105,c_4]) ).
tff(c_27198,plain,
! [Z_296] : ( multiply(sk_c7,multiply(sk_c2,Z_296)) = multiply(identity,Z_296) ),
inference(superposition,[status(thm),theory(equality)],[c_27110,c_27168]) ).
tff(c_27236,plain,
! [Z_298] : ( multiply(sk_c7,multiply(sk_c2,Z_298)) = Z_298 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27198]) ).
tff(c_27248,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_27146,c_27236]) ).
tff(c_27332,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27326,c_27248]) ).
tff(c_27478,plain,
multiply(sk_c2,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27433,c_27419,c_27419,c_27332]) ).
tff(c_27260,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(sk_c5,sk_c6) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_27138,c_56]) ).
tff(c_27261,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitLeft,[status(thm)],[c_27260]) ).
tff(c_27331,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_27326,c_27261]) ).
tff(c_27517,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_27478,c_27433,c_27419,c_27331]) ).
tff(c_27519,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_27260]) ).
tff(c_27951,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27945,c_27519]) ).
tff(c_29147,plain,
multiply(sk_c2,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29089,c_29071,c_27951]) ).
tff(c_30,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_27151,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_27106,c_30]) ).
tff(c_27183,plain,
! [Z_296] : ( multiply(sk_c4,multiply(sk_c7,Z_296)) = multiply(sk_c6,Z_296) ),
inference(superposition,[status(thm),theory(equality)],[c_27151,c_27168]) ).
tff(c_29186,plain,
! [Z_329] : ( multiply(sk_c4,multiply(sk_c2,Z_329)) = Z_329 ),
inference(demodulation,[status(thm),theory(equality)],[c_29089,c_29071,c_2,c_27945,c_27183]) ).
tff(c_29201,plain,
multiply(sk_c4,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_29147,c_29186]) ).
tff(c_29208,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27953,c_29201]) ).
tff(c_29083,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_29071,c_27105]) ).
tff(c_29215,plain,
inverse(sk_c2) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_29208,c_29083]) ).
tff(c_29113,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_29083,c_4]) ).
tff(c_29120,plain,
multiply(sk_c2,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_29113,c_29089]) ).
tff(c_29341,plain,
multiply(inverse(sk_c2),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_29120,c_27211]) ).
tff(c_29347,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_27953,c_29215,c_29341]) ).
tff(c_29357,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_29347,c_29208]) ).
tff(c_29217,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_29208,c_29071]) ).
tff(c_29356,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_29347,c_29217]) ).
tff(c_27523,plain,
! [Z_5] : ( multiply(sk_c7,multiply(sk_c5,Z_5)) = multiply(sk_c6,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_27519,c_6]) ).
tff(c_29464,plain,
! [Z_5] : ( multiply(sk_c2,multiply(sk_c2,Z_5)) = Z_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_29357,c_29356,c_2,c_27945,c_27523]) ).
tff(c_29561,plain,
! [X_334] : ( multiply(X_334,identity) = X_334 ),
inference(superposition,[status(thm),theory(equality)],[c_29554,c_27938]) ).
tff(c_29793,plain,
! [X_339,Y_340,Z_341] : ( multiply(inverse(multiply(X_339,Y_340)),multiply(X_339,multiply(Y_340,Z_341))) = Z_341 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_27875]) ).
tff(c_29829,plain,
! [X_339,X_334] : ( multiply(inverse(multiply(X_339,X_334)),multiply(X_339,identity)) = inverse(X_334) ),
inference(superposition,[status(thm),theory(equality)],[c_29575,c_29793]) ).
tff(c_30922,plain,
! [X_357,X_358] : ( multiply(inverse(multiply(X_357,X_358)),X_357) = inverse(X_358) ),
inference(demodulation,[status(thm),theory(equality)],[c_29561,c_29829]) ).
tff(c_31033,plain,
! [Z_5] : ( multiply(inverse(Z_5),sk_c2) = inverse(multiply(sk_c2,Z_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_29464,c_30922]) ).
tff(c_27999,plain,
sk_c7 = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_27956,c_2]) ).
tff(c_28011,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_27999,c_27105]) ).
tff(c_28024,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28011,c_4]) ).
tff(c_28053,plain,
! [Z_5] : ( multiply(sk_c5,multiply(sk_c5,Z_5)) = Z_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_27999,c_2,c_27945,c_27523]) ).
tff(c_28125,plain,
multiply(sk_c5,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_28024,c_28053]) ).
tff(c_27528,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_27201]) ).
tff(c_27555,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_27225,c_27528]) ).
tff(c_27595,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_27555]) ).
tff(c_27603,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27595,c_27225]) ).
tff(c_27591,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_27528]) ).
tff(c_27606,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_27595,c_27138]) ).
tff(c_27651,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_27606,c_27211]) ).
tff(c_27663,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_27591,c_27651]) ).
tff(c_27601,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27595,c_27519]) ).
tff(c_27758,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_27663,c_27601]) ).
tff(c_27677,plain,
! [Z_296] : ( multiply(sk_c4,multiply(sk_c5,Z_296)) = Z_296 ),
inference(demodulation,[status(thm),theory(equality)],[c_27663,c_2,c_27595,c_27183]) ).
tff(c_27762,plain,
multiply(sk_c4,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_27758,c_27677]) ).
tff(c_27771,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27603,c_27762]) ).
tff(c_27780,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_27771,c_27663]) ).
tff(c_27518,plain,
! [X2_6,X1_7,X3_8] :
( ( multiply(sk_c5,sk_c6) != sk_c7 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_27260]) ).
tff(c_27527,plain,
multiply(sk_c5,sk_c6) != sk_c7,
inference(splitLeft,[status(thm)],[c_27518]) ).
tff(c_27600,plain,
multiply(sk_c5,identity) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_27595,c_27527]) ).
tff(c_27865,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_27780,c_27603,c_27771,c_27600]) ).
tff(c_27867,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(splitRight,[status(thm)],[c_27518]) ).
tff(c_27950,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_27945,c_27867]) ).
tff(c_28007,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_27999,c_27950]) ).
tff(c_28140,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28125,c_28007]) ).
tff(c_28164,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28140,c_28011]) ).
tff(c_28158,plain,
multiply(sk_c2,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28140,c_28024]) ).
tff(c_28165,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28140,c_27999]) ).
tff(c_27866,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_27518]) ).
tff(c_27973,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c7) != identity )
| ( multiply(X3_8,inverse(X3_8)) != identity )
| ( multiply(X1_7,identity) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_27945,c_27945,c_27945,c_27945,c_27866]) ).
tff(c_27974,plain,
! [X2_6] :
( ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != identity ) ),
inference(splitLeft,[status(thm)],[c_27973]) ).
tff(c_29026,plain,
! [X2_327] :
( ( inverse(X2_327) != sk_c2 )
| ( multiply(X2_327,sk_c2) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28165,c_28165,c_27974]) ).
tff(c_29029,plain,
inverse(sk_c2) != sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_28158,c_29026]) ).
tff(c_29045,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28164,c_29029]) ).
tff(c_29046,plain,
! [X1_7,X3_8] :
( ( multiply(X1_7,identity) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(inverse(X3_8),sk_c7) != identity )
| ( multiply(X3_8,inverse(X3_8)) != identity ) ),
inference(splitRight,[status(thm)],[c_27973]) ).
tff(c_54984,plain,
! [X1_7,X3_8] :
( ( sk_c2 != X1_7 )
| ( inverse(X1_7) != sk_c2 )
| ( inverse(multiply(sk_c2,X3_8)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29575,c_31033,c_29356,c_29356,c_29561,c_29356,c_29046]) ).
tff(c_54986,plain,
! [X3_502] : ( inverse(multiply(sk_c2,X3_502)) != identity ),
inference(splitLeft,[status(thm)],[c_54984]) ).
tff(c_55019,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_29575,c_54986]) ).
tff(c_55037,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_29616,c_55019]) ).
tff(c_55039,plain,
inverse(sk_c2) != sk_c2,
inference(splitRight,[status(thm)],[c_54984]) ).
tff(c_29354,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_29347,c_29215]) ).
tff(c_55041,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_55039,c_29354]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP277-1 : TPTP v9.0.0. Released v2.5.0.
% 0.07/0.14 % 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.35 % Computer : n029.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Mon Apr 7 21:40:19 EDT 2025
% 0.14/0.36 % CPUTime :
% 20.66/7.24 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.66/7.27
% 20.66/7.27 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------