%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP310-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:25:53 PM UTC 2025
% Result : Unsatisfiable 11.52s 3.82s
% Output : CNFRefutation 11.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 28
% Syntax : Number of formulae : 459 ( 383 unt; 0 typ; 0 def)
% Number of atoms : 592 ( 572 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 285 ( 152 ~; 133 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 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 : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 178 ( 178 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > 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(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_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_114,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_129,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_78,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_108,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_93,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_63,axiom,
multiply(sk_c8,sk_c7) = sk_c6,
file(unknown,unknown) ).
tff(f_171,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(sk_c8,sk_c7) != sk_c6 )
| ( inverse(sk_c8) != sk_c6 )
| ( multiply(sk_c6,sk_c7) != sk_c8 )
| ( multiply(sk_c8,X3) != sk_c7 )
| ( multiply(X4,sk_c8) != X3 )
| ( inverse(X4) != sk_c8 )
| ( multiply(X1,sk_c8) != sk_c7 )
| ( inverse(X1) != sk_c8 )
| ( multiply(sk_c8,X2) != sk_c7 )
| ( multiply(X5,sk_c8) != X2 )
| ( inverse(X5) != sk_c8 ) ),
file(unknown,unknown) ).
tff(f_123,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_117,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_120,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_84,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_81,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_105,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_102,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_99,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_96,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_87,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_72,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_75,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_69,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_66,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_132,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_135,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_138,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_126,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
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_11757,plain,
! [X_194,Y_195,Z_196] : ( multiply(multiply(X_194,Y_195),Z_196) = multiply(X_194,multiply(Y_195,Z_196)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11790,plain,
! [X_2,Z_196] : ( multiply(inverse(X_2),multiply(X_2,Z_196)) = multiply(identity,Z_196) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11757]) ).
tff(c_12217,plain,
! [X_203,Z_204] : ( multiply(inverse(X_203),multiply(X_203,Z_204)) = Z_204 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11790]) ).
tff(c_11804,plain,
! [X_2,Z_196] : ( multiply(inverse(X_2),multiply(X_2,Z_196)) = Z_196 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11790]) ).
tff(c_12574,plain,
! [X_208,Z_209] : ( multiply(inverse(inverse(X_208)),Z_209) = multiply(X_208,Z_209) ),
inference(superposition,[status(thm),theory(equality)],[c_12217,c_11804]) ).
tff(c_12259,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12217]) ).
tff(c_12581,plain,
! [X_208] : ( multiply(X_208,identity) = X_208 ),
inference(superposition,[status(thm),theory(equality)],[c_12574,c_12259]) ).
tff(c_42,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_9293,plain,
multiply(sk_c1,sk_c8) = sk_c2,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_52,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_83,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_87,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_83,c_4]) ).
tff(c_18,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_91,plain,
inverse(sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_95,plain,
multiply(sk_c6,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_91,c_4]) ).
tff(c_9892,plain,
! [X_157,Y_158,Z_159] : ( multiply(multiply(X_157,Y_158),Z_159) = multiply(X_157,multiply(Y_158,Z_159)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9925,plain,
! [Z_159] : ( multiply(sk_c6,multiply(sk_c8,Z_159)) = multiply(identity,Z_159) ),
inference(superposition,[status(thm),theory(equality)],[c_95,c_9892]) ).
tff(c_9948,plain,
! [Z_160] : ( multiply(sk_c6,multiply(sk_c8,Z_160)) = Z_160 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9925]) ).
tff(c_9969,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_87,c_9948]) ).
tff(c_38,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_110,plain,
multiply(sk_c8,sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_8834,plain,
! [X_137,Y_138,Z_139] : ( multiply(multiply(X_137,Y_138),Z_139) = multiply(X_137,multiply(Y_138,Z_139)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_8870,plain,
! [Z_139] : ( multiply(sk_c6,multiply(sk_c8,Z_139)) = multiply(identity,Z_139) ),
inference(superposition,[status(thm),theory(equality)],[c_95,c_8834]) ).
tff(c_8893,plain,
! [Z_140] : ( multiply(sk_c6,multiply(sk_c8,Z_140)) = Z_140 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8870]) ).
tff(c_8914,plain,
multiply(sk_c6,sk_c7) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_110,c_8893]) ).
tff(c_8441,plain,
! [X_131,Y_132,Z_133] : ( multiply(multiply(X_131,Y_132),Z_133) = multiply(X_131,multiply(Y_132,Z_133)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_8477,plain,
! [Z_133] : ( multiply(sk_c6,multiply(sk_c8,Z_133)) = multiply(identity,Z_133) ),
inference(superposition,[status(thm),theory(equality)],[c_95,c_8441]) ).
tff(c_8500,plain,
! [Z_134] : ( multiply(sk_c6,multiply(sk_c8,Z_134)) = Z_134 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8477]) ).
tff(c_8524,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_87,c_8500]) ).
tff(c_8521,plain,
multiply(sk_c6,sk_c7) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_110,c_8500]) ).
tff(c_28,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c6,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_115,plain,
multiply(sk_c6,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_8538,plain,
sk_c8 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8521,c_115]) ).
tff(c_8558,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8538,c_91]) ).
tff(c_142,plain,
! [X_13,Y_14,Z_15] : ( multiply(multiply(X_13,Y_14),Z_15) = multiply(X_13,multiply(Y_14,Z_15)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_172,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_142]) ).
tff(c_1549,plain,
! [X_45,Z_46] : ( multiply(inverse(X_45),multiply(X_45,Z_46)) = Z_46 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_172]) ).
tff(c_185,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_172]) ).
tff(c_1790,plain,
! [X_49,Z_50] : ( multiply(inverse(inverse(X_49)),Z_50) = multiply(X_49,Z_50) ),
inference(superposition,[status(thm),theory(equality)],[c_1549,c_185]) ).
tff(c_1588,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1549]) ).
tff(c_1797,plain,
! [X_49] : ( multiply(X_49,identity) = X_49 ),
inference(superposition,[status(thm),theory(equality)],[c_1790,c_1588]) ).
tff(c_166,plain,
! [Z_15] : ( multiply(sk_c6,multiply(sk_c8,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_95,c_142]) ).
tff(c_187,plain,
! [Z_16] : ( multiply(sk_c6,multiply(sk_c8,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_166]) ).
tff(c_199,plain,
multiply(sk_c6,sk_c7) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_110,c_187]) ).
tff(c_216,plain,
sk_c8 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_199,c_115]) ).
tff(c_244,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_216,c_95]) ).
tff(c_243,plain,
multiply(sk_c2,sk_c2) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_216,c_110]) ).
tff(c_247,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_216,c_83]) ).
tff(c_122,plain,
multiply(sk_c1,sk_c8) = sk_c2,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_242,plain,
multiply(sk_c1,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_216,c_122]) ).
tff(c_1634,plain,
multiply(inverse(sk_c1),sk_c2) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_242,c_185]) ).
tff(c_1640,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_243,c_247,c_1634]) ).
tff(c_1644,plain,
multiply(sk_c6,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_1640,c_199]) ).
tff(c_1646,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_244,c_1644]) ).
tff(c_1651,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1646,c_1640]) ).
tff(c_351,plain,
! [X_19,Z_20] : ( multiply(inverse(X_19),multiply(X_19,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_172]) ).
tff(c_547,plain,
! [X_23,Z_24] : ( multiply(inverse(inverse(X_23)),Z_24) = multiply(X_23,Z_24) ),
inference(superposition,[status(thm),theory(equality)],[c_351,c_185]) ).
tff(c_396,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_351]) ).
tff(c_554,plain,
! [X_23] : ( multiply(X_23,identity) = X_23 ),
inference(superposition,[status(thm),theory(equality)],[c_547,c_396]) ).
tff(c_169,plain,
! [Z_15] : ( multiply(sk_c8,multiply(sk_c1,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_87,c_142]) ).
tff(c_184,plain,
! [Z_15] : ( multiply(sk_c8,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_169]) ).
tff(c_318,plain,
! [Z_18] : ( multiply(sk_c2,multiply(sk_c1,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_216,c_184]) ).
tff(c_330,plain,
multiply(sk_c2,sk_c2) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_242,c_318]) ).
tff(c_334,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_330,c_243]) ).
tff(c_343,plain,
multiply(sk_c6,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_334,c_199]) ).
tff(c_346,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_244,c_343]) ).
tff(c_416,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_346,c_334]) ).
tff(c_246,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216,c_91]) ).
tff(c_8,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_60,plain,
! [X5_6,X1_8,X4_10] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c8 )
| ( inverse(sk_c8) != sk_c6 )
| ( multiply(sk_c8,sk_c7) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_171]) ).
tff(c_62,plain,
! [X5_6,X1_8,X4_10] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c8 )
| ( inverse(sk_c8) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_60]) ).
tff(c_283,plain,
! [X5_6,X1_8,X4_10] :
( ( inverse(X5_6) != sk_c2 )
| ( multiply(sk_c2,multiply(X5_6,sk_c2)) != sk_c7 )
| ( inverse(X1_8) != sk_c2 )
| ( multiply(X1_8,sk_c2) != sk_c7 )
| ( inverse(X4_10) != sk_c2 )
| ( multiply(sk_c2,multiply(X4_10,sk_c2)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_246,c_216,c_216,c_199,c_216,c_216,c_216,c_216,c_216,c_216,c_216,c_216,c_62]) ).
tff(c_284,plain,
! [X4_10] :
( ( inverse(X4_10) != sk_c2 )
| ( multiply(sk_c2,multiply(X4_10,sk_c2)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_283]) ).
tff(c_1545,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_554,c_416,c_346,c_2,c_346,c_346,c_284]) ).
tff(c_248,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_216,c_8]) ).
tff(c_342,plain,
multiply(sk_c2,sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_334,c_248]) ).
tff(c_345,plain,
sk_c6 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_330,c_342]) ).
tff(c_410,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_246]) ).
tff(c_477,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_346,c_346,c_410]) ).
tff(c_1547,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1545,c_477]) ).
tff(c_1548,plain,
! [X1_8,X5_6] :
( ( inverse(X1_8) != sk_c2 )
| ( multiply(X1_8,sk_c2) != sk_c7 )
| ( inverse(X5_6) != sk_c2 )
| ( multiply(sk_c2,multiply(X5_6,sk_c2)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_283]) ).
tff(c_8381,plain,
! [X1_8,X5_6] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1797,c_1651,c_1646,c_2,c_1646,c_1646,c_1797,c_1651,c_1646,c_1646,c_1548]) ).
tff(c_8383,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8381]) ).
tff(c_263,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_247,c_4]) ).
tff(c_1709,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1646,c_263]) ).
tff(c_1655,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1646,c_247]) ).
tff(c_1710,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1709,c_1655]) ).
tff(c_8385,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8383,c_1710]) ).
tff(c_8387,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_8381]) ).
tff(c_8389,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8387,c_1710]) ).
tff(c_8391,plain,
multiply(sk_c1,sk_c8) != sk_c2,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_48,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_8405,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_8391,c_48]) ).
tff(c_8409,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8405,c_4]) ).
tff(c_8550,plain,
multiply(sk_c2,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8538,c_8409]) ).
tff(c_8483,plain,
! [X_2,Z_133] : ( multiply(inverse(X_2),multiply(X_2,Z_133)) = multiply(identity,Z_133) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_8441]) ).
tff(c_8647,plain,
! [X_135,Z_136] : ( multiply(inverse(X_135),multiply(X_135,Z_136)) = Z_136 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8483]) ).
tff(c_8665,plain,
multiply(inverse(sk_c2),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_8550,c_8647]) ).
tff(c_8711,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8524,c_8558,c_8665]) ).
tff(c_44,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_8420,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_8391,c_44]) ).
tff(c_8512,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_8420,c_8500]) ).
tff(c_8626,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8521,c_8512]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_8434,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_8391,c_46]) ).
tff(c_8547,plain,
multiply(sk_c4,sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8538,c_8434]) ).
tff(c_8762,plain,
multiply(sk_c1,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8711,c_8626,c_8547]) ).
tff(c_8553,plain,
multiply(sk_c1,sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8538,c_8391]) ).
tff(c_8775,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8762,c_8553]) ).
tff(c_8777,plain,
multiply(sk_c6,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_8947,plain,
sk_c8 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8914,c_8777]) ).
tff(c_8809,plain,
multiply(sk_c1,sk_c8) = sk_c2,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_8917,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_87,c_8893]) ).
tff(c_22,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c6,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_8791,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_8777,c_22]) ).
tff(c_8795,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8791,c_4]) ).
tff(c_8908,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_8795,c_8893]) ).
tff(c_8982,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8917,c_8908]) ).
tff(c_20,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_8824,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_8777,c_20]) ).
tff(c_8983,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_8982,c_8824]) ).
tff(c_8986,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8809,c_8983]) ).
tff(c_8996,plain,
multiply(sk_c8,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8986,c_110]) ).
tff(c_8876,plain,
! [X_2,Z_139] : ( multiply(inverse(X_2),multiply(X_2,Z_139)) = multiply(identity,Z_139) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_8834]) ).
tff(c_9057,plain,
! [X_142,Z_143] : ( multiply(inverse(X_142),multiply(X_142,Z_143)) = Z_143 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8876]) ).
tff(c_9084,plain,
multiply(inverse(sk_c1),sk_c2) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_8809,c_9057]) ).
tff(c_9101,plain,
sk_c8 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8996,c_83,c_9084]) ).
tff(c_9103,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8947,c_9101]) ).
tff(c_9105,plain,
multiply(sk_c1,sk_c8) != sk_c2,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_9129,plain,
! [X_144,Y_145,Z_146] : ( multiply(multiply(X_144,Y_145),Z_146) = multiply(X_144,multiply(Y_145,Z_146)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9162,plain,
! [Z_146] : ( multiply(sk_c6,multiply(sk_c8,Z_146)) = multiply(identity,Z_146) ),
inference(superposition,[status(thm),theory(equality)],[c_95,c_9129]) ).
tff(c_9185,plain,
! [Z_147] : ( multiply(sk_c6,multiply(sk_c8,Z_147)) = Z_147 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9162]) ).
tff(c_9209,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_87,c_9185]) ).
tff(c_8776,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_8781,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8776,c_4]) ).
tff(c_9203,plain,
multiply(sk_c6,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_8781,c_9185]) ).
tff(c_9263,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9209,c_9203]) ).
tff(c_9206,plain,
multiply(sk_c6,sk_c7) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_110,c_9185]) ).
tff(c_9104,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_9197,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9104,c_9185]) ).
tff(c_9255,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_9206,c_9197]) ).
tff(c_9117,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_9105,c_46]) ).
tff(c_9256,plain,
multiply(sk_c4,sk_c8) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_9255,c_9117]) ).
tff(c_9274,plain,
multiply(sk_c1,sk_c8) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_9263,c_9256]) ).
tff(c_9275,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9105,c_9274]) ).
tff(c_9276,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_9281,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9276,c_4]) ).
tff(c_9966,plain,
multiply(sk_c6,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_9281,c_9948]) ).
tff(c_10038,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9969,c_9966]) ).
tff(c_9277,plain,
multiply(sk_c8,sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_9880,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_9277,c_36]) ).
tff(c_10039,plain,
multiply(sk_c1,sk_c8) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10038,c_9880]) ).
tff(c_10042,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_9293,c_10039]) ).
tff(c_34,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_102]) ).
tff(c_9327,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9277,c_34]) ).
tff(c_9339,plain,
! [X_149,Y_150,Z_151] : ( multiply(multiply(X_149,Y_150),Z_151) = multiply(X_149,multiply(Y_150,Z_151)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9375,plain,
! [Z_151] : ( multiply(sk_c6,multiply(sk_c8,Z_151)) = multiply(identity,Z_151) ),
inference(superposition,[status(thm),theory(equality)],[c_95,c_9339]) ).
tff(c_9398,plain,
! [Z_152] : ( multiply(sk_c6,multiply(sk_c8,Z_152)) = Z_152 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9375]) ).
tff(c_9410,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9327,c_9398]) ).
tff(c_9298,plain,
multiply(sk_c6,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_9733,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9410,c_9298]) ).
tff(c_9755,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9733,c_83]) ).
tff(c_9419,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_87,c_9398]) ).
tff(c_9416,plain,
multiply(sk_c6,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_9281,c_9398]) ).
tff(c_9817,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9419,c_9416]) ).
tff(c_9334,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_9277,c_36]) ).
tff(c_9743,plain,
multiply(sk_c4,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9733,c_9334]) ).
tff(c_9835,plain,
multiply(sk_c1,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9817,c_9743]) ).
tff(c_9585,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9410,c_9298]) ).
tff(c_9595,plain,
multiply(sk_c5,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_9585,c_9327]) ).
tff(c_9606,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9585,c_83]) ).
tff(c_9655,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9419,c_9416]) ).
tff(c_9594,plain,
multiply(sk_c4,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9585,c_9334]) ).
tff(c_9695,plain,
multiply(sk_c1,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9655,c_9594]) ).
tff(c_9436,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9410,c_9298]) ).
tff(c_9446,plain,
multiply(sk_c5,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_9436,c_9327]) ).
tff(c_9457,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9436,c_83]) ).
tff(c_32,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_9305,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_9277,c_32]) ).
tff(c_9309,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9305,c_4]) ).
tff(c_9413,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_9309,c_9398]) ).
tff(c_9528,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9419,c_9413]) ).
tff(c_9506,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_9413,c_9416]) ).
tff(c_9537,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9528,c_9506]) ).
tff(c_9445,plain,
multiply(sk_c4,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9436,c_9334]) ).
tff(c_9570,plain,
multiply(sk_c1,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9537,c_9445]) ).
tff(c_9434,plain,
! [X5_6,X1_8,X4_10] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_91,c_9298,c_62]) ).
tff(c_9435,plain,
! [X4_10] :
( ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_9434]) ).
tff(c_9513,plain,
! [X4_10] :
( ( inverse(X4_10) != sk_c5 )
| ( multiply(sk_c5,multiply(X4_10,sk_c5)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_9436,c_9436,c_9436,c_9435]) ).
tff(c_9574,plain,
( ( inverse(sk_c1) != sk_c5 )
| ( multiply(sk_c5,sk_c5) != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_9570,c_9513]) ).
tff(c_9582,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9446,c_9457,c_9574]) ).
tff(c_9583,plain,
! [X1_8,X5_6] :
( ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_9434]) ).
tff(c_9584,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_9583]) ).
tff(c_9662,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c5 )
| ( multiply(sk_c5,multiply(X5_6,sk_c5)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_9585,c_9585,c_9585,c_9584]) ).
tff(c_9699,plain,
( ( inverse(sk_c1) != sk_c5 )
| ( multiply(sk_c5,sk_c5) != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_9695,c_9662]) ).
tff(c_9707,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9595,c_9606,c_9699]) ).
tff(c_9708,plain,
! [X1_8] :
( ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_9583]) ).
tff(c_9775,plain,
! [X1_8] :
( ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_9733,c_9733,c_9708]) ).
tff(c_9839,plain,
( ( inverse(sk_c1) != sk_c5 )
| ( sk_c7 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_9835,c_9775]) ).
tff(c_9846,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9755,c_9839]) ).
tff(c_9803,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9419,c_9413]) ).
tff(c_30,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_9321,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9277,c_30]) ).
tff(c_9745,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_9733,c_9321]) ).
tff(c_9848,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9835,c_9803,c_9745]) ).
tff(c_9849,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9846,c_9848]) ).
tff(c_9851,plain,
multiply(sk_c6,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_24,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_9874,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9851,c_24]) ).
tff(c_9960,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9874,c_9948]) ).
tff(c_9993,plain,
sk_c8 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9960,c_9851]) ).
tff(c_10049,plain,
sk_c8 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_10042,c_9993]) ).
tff(c_9850,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_9855,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9850,c_4]) ).
tff(c_9963,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_9855,c_9948]) ).
tff(c_10001,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9969,c_9963]) ).
tff(c_9868,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9277,c_30]) ).
tff(c_10002,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10001,c_9868]) ).
tff(c_10005,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_9293,c_10002]) ).
tff(c_10031,plain,
multiply(sk_c8,sk_c5) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_10005,c_9874]) ).
tff(c_10054,plain,
multiply(sk_c8,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_10042,c_10031]) ).
tff(c_9931,plain,
! [X_2,Z_159] : ( multiply(inverse(X_2),multiply(X_2,Z_159)) = multiply(identity,Z_159) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9892]) ).
tff(c_10065,plain,
! [X_162,Z_163] : ( multiply(inverse(X_162),multiply(X_162,Z_163)) = Z_163 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9931]) ).
tff(c_10095,plain,
multiply(inverse(sk_c1),sk_c2) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_9293,c_10065]) ).
tff(c_10118,plain,
sk_c8 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_10054,c_83,c_10095]) ).
tff(c_10120,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10049,c_10118]) ).
tff(c_10121,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_10151,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9277,c_30]) ).
tff(c_10122,plain,
multiply(sk_c1,sk_c8) != sk_c2,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_10156,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_10122,c_44]) ).
tff(c_10169,plain,
! [X_164,Y_165,Z_166] : ( multiply(multiply(X_164,Y_165),Z_166) = multiply(X_164,multiply(Y_165,Z_166)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_10202,plain,
! [Z_166] : ( multiply(sk_c6,multiply(sk_c8,Z_166)) = multiply(identity,Z_166) ),
inference(superposition,[status(thm),theory(equality)],[c_95,c_10169]) ).
tff(c_10422,plain,
! [Z_171] : ( multiply(sk_c6,multiply(sk_c8,Z_171)) = Z_171 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10202]) ).
tff(c_10434,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10156,c_10422]) ).
tff(c_10146,plain,
multiply(sk_c6,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_10491,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10434,c_10146]) ).
tff(c_10443,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_87,c_10422]) ).
tff(c_10126,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10121,c_4]) ).
tff(c_10437,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_10126,c_10422]) ).
tff(c_10481,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_10443,c_10437]) ).
tff(c_10482,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10481,c_10151]) ).
tff(c_10552,plain,
multiply(sk_c1,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10491,c_10482]) ).
tff(c_10440,plain,
multiply(sk_c6,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_9281,c_10422]) ).
tff(c_10565,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_10443,c_10440]) ).
tff(c_10141,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_10122,c_46]) ).
tff(c_10502,plain,
multiply(sk_c4,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10491,c_10141]) ).
tff(c_10579,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10552,c_10565,c_10502]) ).
tff(c_10501,plain,
multiply(sk_c5,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10491,c_10156]) ).
tff(c_10589,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10579,c_10501]) ).
tff(c_10208,plain,
! [X_2,Z_166] : ( multiply(inverse(X_2),multiply(X_2,Z_166)) = multiply(identity,Z_166) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_10169]) ).
tff(c_10620,plain,
! [X_174,Z_175] : ( multiply(inverse(X_174),multiply(X_174,Z_175)) = Z_175 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10208]) ).
tff(c_10647,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10589,c_10620]) ).
tff(c_10670,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10647]) ).
tff(c_10510,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10491,c_83]) ).
tff(c_10241,plain,
! [Z_168] : ( multiply(sk_c6,multiply(sk_c8,Z_168)) = Z_168 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10202]) ).
tff(c_10256,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10156,c_10241]) ).
tff(c_10364,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10256,c_10146]) ).
tff(c_10205,plain,
! [Z_166] : ( multiply(sk_c8,multiply(sk_c1,Z_166)) = multiply(identity,Z_166) ),
inference(superposition,[status(thm),theory(equality)],[c_87,c_10169]) ).
tff(c_10222,plain,
! [Z_166] : ( multiply(sk_c8,multiply(sk_c1,Z_166)) = Z_166 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10205]) ).
tff(c_10226,plain,
! [X5_6,X1_8,X4_10] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_91,c_10146,c_62]) ).
tff(c_10336,plain,
! [X4_170] :
( ( inverse(X4_170) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_170,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_10226]) ).
tff(c_10344,plain,
( ( inverse(sk_c1) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10222,c_10336]) ).
tff(c_10362,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_83,c_10344]) ).
tff(c_10372,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10364,c_10362]) ).
tff(c_10265,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_87,c_10241]) ).
tff(c_10259,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_10126,c_10241]) ).
tff(c_10313,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_10265,c_10259]) ).
tff(c_10323,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10313,c_10151]) ).
tff(c_10410,plain,
multiply(sk_c1,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10364,c_10323]) ).
tff(c_10262,plain,
multiply(sk_c6,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_9281,c_10241]) ).
tff(c_10303,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_10259,c_10262]) ).
tff(c_10304,plain,
multiply(sk_c3,sk_c8) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10303,c_10141]) ).
tff(c_10418,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10410,c_10364,c_10313,c_10304]) ).
tff(c_10419,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10372,c_10418]) ).
tff(c_10420,plain,
! [X1_8,X5_6] :
( ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_10226]) ).
tff(c_10421,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_10420]) ).
tff(c_10530,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c5 )
| ( multiply(sk_c5,multiply(X5_6,sk_c5)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10491,c_10491,c_10491,c_10421]) ).
tff(c_10556,plain,
( ( inverse(sk_c1) != sk_c5 )
| ( multiply(sk_c5,sk_c7) != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10552,c_10530]) ).
tff(c_10563,plain,
multiply(sk_c5,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10510,c_10556]) ).
tff(c_10753,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10670,c_10563]) ).
tff(c_10806,plain,
! [X1_177] :
( ( inverse(X1_177) != sk_c8 )
| ( multiply(X1_177,sk_c8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_10420]) ).
tff(c_10813,plain,
inverse(sk_c3) != sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_10151,c_10806]) ).
tff(c_10831,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10121,c_10813]) ).
tff(c_10833,plain,
multiply(sk_c6,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_10840,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_10833,c_24]) ).
tff(c_10855,plain,
! [X_178,Y_179,Z_180] : ( multiply(multiply(X_178,Y_179),Z_180) = multiply(X_178,multiply(Y_179,Z_180)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_10885,plain,
! [Z_180] : ( multiply(sk_c6,multiply(sk_c8,Z_180)) = multiply(identity,Z_180) ),
inference(superposition,[status(thm),theory(equality)],[c_95,c_10855]) ).
tff(c_10908,plain,
! [Z_181] : ( multiply(sk_c6,multiply(sk_c8,Z_181)) = Z_181 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10885]) ).
tff(c_10920,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10840,c_10908]) ).
tff(c_10967,plain,
sk_c8 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10920,c_10833]) ).
tff(c_10929,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_87,c_10908]) ).
tff(c_10923,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_10126,c_10908]) ).
tff(c_10985,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_10929,c_10923]) ).
tff(c_10926,plain,
multiply(sk_c6,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_9281,c_10908]) ).
tff(c_10975,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_10923,c_10926]) ).
tff(c_10976,plain,
multiply(sk_c3,sk_c8) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10975,c_10141]) ).
tff(c_11010,plain,
multiply(sk_c1,sk_c8) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10985,c_10976]) ).
tff(c_10832,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_10995,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10985,c_10832]) ).
tff(c_11045,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11010,c_10995]) ).
tff(c_11050,plain,
multiply(sk_c8,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11045,c_10840]) ).
tff(c_10891,plain,
! [X_2,Z_180] : ( multiply(inverse(X_2),multiply(X_2,Z_180)) = multiply(identity,Z_180) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_10855]) ).
tff(c_11093,plain,
! [X_184,Z_185] : ( multiply(inverse(X_184),multiply(X_184,Z_185)) = Z_185 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10891]) ).
tff(c_11120,plain,
multiply(inverse(sk_c1),sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_11010,c_11093]) ).
tff(c_11152,plain,
sk_c8 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11050,c_83,c_11120]) ).
tff(c_11154,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10967,c_11152]) ).
tff(c_11156,plain,
inverse(sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_14,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_11192,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11156,c_14]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_11185,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_11156,c_16]) ).
tff(c_11155,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_11160,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11155,c_4]) ).
tff(c_11218,plain,
! [X_186,Y_187,Z_188] : ( multiply(multiply(X_186,Y_187),Z_188) = multiply(X_186,multiply(Y_187,Z_188)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11245,plain,
! [Z_188] : ( multiply(sk_c8,multiply(sk_c4,Z_188)) = multiply(identity,Z_188) ),
inference(superposition,[status(thm),theory(equality)],[c_11160,c_11218]) ).
tff(c_11267,plain,
! [Z_189] : ( multiply(sk_c8,multiply(sk_c4,Z_189)) = Z_189 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11245]) ).
tff(c_11279,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_11185,c_11267]) ).
tff(c_11283,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11192,c_11279]) ).
tff(c_11295,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11283,c_8]) ).
tff(c_12,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_11173,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_11156,c_12]) ).
tff(c_11289,plain,
inverse(sk_c3) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11283,c_11173]) ).
tff(c_10,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_11203,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11156,c_10]) ).
tff(c_11285,plain,
multiply(sk_c3,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11283,c_11203]) ).
tff(c_11251,plain,
! [X_2,Z_188] : ( multiply(inverse(X_2),multiply(X_2,Z_188)) = multiply(identity,Z_188) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11218]) ).
tff(c_11265,plain,
! [X_2,Z_188] : ( multiply(inverse(X_2),multiply(X_2,Z_188)) = Z_188 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11251]) ).
tff(c_11411,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11285,c_11265]) ).
tff(c_11417,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11295,c_11289,c_11411]) ).
tff(c_11426,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11417,c_11417,c_11295]) ).
tff(c_11571,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11426,c_11265]) ).
tff(c_11578,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11571]) ).
tff(c_11294,plain,
inverse(sk_c1) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11283,c_83]) ).
tff(c_11425,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11417,c_11294]) ).
tff(c_11453,plain,
multiply(sk_c6,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11425,c_4]) ).
tff(c_11642,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11578,c_11453]) ).
tff(c_11625,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11578,c_11425]) ).
tff(c_11651,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11642,c_11625]) ).
tff(c_11292,plain,
inverse(sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11283,c_11156]) ).
tff(c_11423,plain,
inverse(sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11417,c_11292]) ).
tff(c_11627,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_11578,c_11578,c_11423]) ).
tff(c_11685,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_11651,c_11627]) ).
tff(c_11687,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_54,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_11729,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11687,c_54]) ).
tff(c_56,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_11742,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_11687,c_56]) ).
tff(c_58,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_138]) ).
tff(c_11712,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_11687,c_58]) ).
tff(c_11716,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11712,c_4]) ).
tff(c_11781,plain,
! [Z_196] : ( multiply(sk_c8,multiply(sk_c4,Z_196)) = multiply(identity,Z_196) ),
inference(superposition,[status(thm),theory(equality)],[c_11716,c_11757]) ).
tff(c_11806,plain,
! [Z_197] : ( multiply(sk_c8,multiply(sk_c4,Z_197)) = Z_197 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11781]) ).
tff(c_11818,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_11742,c_11806]) ).
tff(c_11822,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11729,c_11818]) ).
tff(c_11834,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11822,c_8]) ).
tff(c_11686,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_11833,plain,
inverse(sk_c3) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11822,c_11686]) ).
tff(c_50,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_11737,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11687,c_50]) ).
tff(c_11825,plain,
multiply(sk_c3,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11822,c_11737]) ).
tff(c_12241,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11825,c_12217]) ).
tff(c_12268,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11834,c_11833,c_12241]) ).
tff(c_11699,plain,
inverse(sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_11704,plain,
multiply(sk_c6,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11699,c_4]) ).
tff(c_11829,plain,
multiply(sk_c6,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11822,c_11704]) ).
tff(c_12374,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12268,c_11829]) ).
tff(c_11691,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11686,c_4]) ).
tff(c_11787,plain,
! [Z_196] : ( multiply(sk_c8,multiply(sk_c3,Z_196)) = multiply(identity,Z_196) ),
inference(superposition,[status(thm),theory(equality)],[c_11691,c_11757]) ).
tff(c_11803,plain,
! [Z_196] : ( multiply(sk_c8,multiply(sk_c3,Z_196)) = Z_196 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11787]) ).
tff(c_11920,plain,
! [Z_198] : ( multiply(sk_c7,multiply(sk_c3,Z_198)) = Z_198 ),
inference(demodulation,[status(thm),theory(equality)],[c_11822,c_11803]) ).
tff(c_11932,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11825,c_11920]) ).
tff(c_11936,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11834,c_11932]) ).
tff(c_11830,plain,
inverse(sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11822,c_11699]) ).
tff(c_11883,plain,
! [X5_6,X1_8,X4_10] :
( ( inverse(X5_6) != sk_c7 )
| ( multiply(sk_c7,multiply(X5_6,sk_c7)) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_10,sk_c7)) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11830,c_11822,c_11822,c_11822,c_11822,c_11822,c_11822,c_11822,c_11822,c_11822,c_11822,c_62]) ).
tff(c_11884,plain,
multiply(sk_c6,sk_c7) != sk_c7,
inference(splitLeft,[status(thm)],[c_11883]) ).
tff(c_11916,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_11829,c_11884]) ).
tff(c_12007,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_11936,c_11916]) ).
tff(c_12017,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11936,c_11936,c_11834]) ).
tff(c_12198,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12017,c_11804]) ).
tff(c_12205,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12198]) ).
tff(c_12207,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12007,c_12205]) ).
tff(c_12209,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(splitRight,[status(thm)],[c_11883]) ).
tff(c_12387,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12374,c_12268,c_12268,c_12209]) ).
tff(c_12395,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12387,c_12268]) ).
tff(c_12208,plain,
! [X4_10,X1_8,X5_6] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_10,sk_c7)) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c7 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(sk_c7,multiply(X5_6,sk_c7)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_11883]) ).
tff(c_21176,plain,
! [X4_10,X1_8,X5_6] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_12581,c_12395,c_12395,c_2,c_12395,c_12395,c_12581,c_12395,c_12395,c_12395,c_12581,c_12395,c_12395,c_2,c_12395,c_12395,c_12208]) ).
tff(c_21178,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_21176]) ).
tff(c_12273,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12268,c_11830]) ).
tff(c_12389,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12387,c_12387,c_12273]) ).
tff(c_21180,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21178,c_12389]) ).
tff(c_21181,plain,
! [X1_8,X4_10] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 ) ),
inference(splitRight,[status(thm)],[c_21176]) ).
tff(c_21183,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_21181]) ).
tff(c_21185,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21183,c_12389]) ).
tff(c_21514,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_21181]) ).
tff(c_21516,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21514,c_12389]) ).
tff(c_21518,plain,
inverse(sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_21534,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_21518,c_14]) ).
tff(c_21540,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_21518,c_16]) ).
tff(c_21517,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_21522,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21517,c_4]) ).
tff(c_21570,plain,
! [X_304,Y_305,Z_306] : ( multiply(multiply(X_304,Y_305),Z_306) = multiply(X_304,multiply(Y_305,Z_306)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_21594,plain,
! [Z_306] : ( multiply(sk_c8,multiply(sk_c4,Z_306)) = multiply(identity,Z_306) ),
inference(superposition,[status(thm),theory(equality)],[c_21522,c_21570]) ).
tff(c_21615,plain,
! [Z_307] : ( multiply(sk_c8,multiply(sk_c4,Z_307)) = Z_307 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21594]) ).
tff(c_21627,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_21540,c_21615]) ).
tff(c_21631,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21534,c_21627]) ).
tff(c_21656,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21631,c_8]) ).
tff(c_21551,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11687,c_50]) ).
tff(c_21647,plain,
multiply(sk_c3,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21631,c_21551]) ).
tff(c_21597,plain,
! [Z_306] : ( multiply(sk_c8,multiply(sk_c3,Z_306)) = multiply(identity,Z_306) ),
inference(superposition,[status(thm),theory(equality)],[c_11691,c_21570]) ).
tff(c_21612,plain,
! [Z_306] : ( multiply(sk_c8,multiply(sk_c3,Z_306)) = Z_306 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21597]) ).
tff(c_21723,plain,
! [Z_309] : ( multiply(sk_c7,multiply(sk_c3,Z_309)) = Z_309 ),
inference(demodulation,[status(thm),theory(equality)],[c_21631,c_21612]) ).
tff(c_21735,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_21647,c_21723]) ).
tff(c_21739,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21656,c_21735]) ).
tff(c_21804,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21739,c_21739,c_21656]) ).
tff(c_21600,plain,
! [X_2,Z_306] : ( multiply(inverse(X_2),multiply(X_2,Z_306)) = multiply(identity,Z_306) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_21570]) ).
tff(c_21613,plain,
! [X_2,Z_306] : ( multiply(inverse(X_2),multiply(X_2,Z_306)) = Z_306 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21600]) ).
tff(c_21944,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_21804,c_21613]) ).
tff(c_21950,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21944]) ).
tff(c_21651,plain,
inverse(sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21631,c_21518]) ).
tff(c_21809,plain,
inverse(sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21739,c_21651]) ).
tff(c_21961,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_21950,c_21950,c_21809]) ).
tff(c_21652,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21631,c_21517]) ).
tff(c_21806,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21739,c_21652]) ).
tff(c_21866,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21806,c_4]) ).
tff(c_22007,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21950,c_21866]) ).
tff(c_21960,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21950,c_21806]) ).
tff(c_22008,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22007,c_21960]) ).
tff(c_22023,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21961,c_22008]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : GRP310-1 : TPTP v9.0.0. Released v2.5.0.
% 0.08/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.14/0.34 % Computer : n018.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Apr 7 21:41:47 EDT 2025
% 0.14/0.34 % CPUTime :
% 11.52/3.82 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.52/3.88
% 11.52/3.88 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------