%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP272-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 : n016.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:46 PM UTC 2025
% Result : Unsatisfiable 17.79s 7.03s
% Output : CNFRefutation 18.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 27
% Syntax : Number of formulae : 615 ( 528 unt; 0 typ; 0 def)
% Number of atoms : 808 ( 782 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 428 ( 235 ~; 193 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 287 ( 287 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_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_74,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
! [X3,X4,X1,X2] :
( ( multiply(X3,sk_c7) != sk_c6 )
| ( inverse(X3) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(X4,sk_c6) != sk_c5 )
| ( inverse(X4) != sk_c6 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( inverse(X2) != sk_c6 )
| ( multiply(X2,sk_c5) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = 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_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
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_16667,plain,
! [X_243,Y_244,Z_245] : ( multiply(multiply(X_243,Y_244),Z_245) = multiply(X_243,multiply(Y_244,Z_245)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16700,plain,
! [X_2,Z_245] : ( multiply(inverse(X_2),multiply(X_2,Z_245)) = multiply(identity,Z_245) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16667]) ).
tff(c_18155,plain,
! [X_274,Z_275] : ( multiply(inverse(X_274),multiply(X_274,Z_275)) = Z_275 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16700]) ).
tff(c_16711,plain,
! [X_2,Z_245] : ( multiply(inverse(X_2),multiply(X_2,Z_245)) = Z_245 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16700]) ).
tff(c_18381,plain,
! [X_277,Z_278] : ( multiply(inverse(inverse(X_277)),Z_278) = multiply(X_277,Z_278) ),
inference(superposition,[status(thm),theory(equality)],[c_18155,c_16711]) ).
tff(c_18203,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18155]) ).
tff(c_18388,plain,
! [X_277] : ( multiply(X_277,identity) = X_277 ),
inference(superposition,[status(thm),theory(equality)],[c_18381,c_18203]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_102,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_20,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_87,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_91,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_87,c_4]) ).
tff(c_12302,plain,
! [X_161,Y_162,Z_163] : ( multiply(multiply(X_161,Y_162),Z_163) = multiply(X_161,multiply(Y_162,Z_163)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_12335,plain,
! [Z_163] : ( multiply(sk_c7,multiply(sk_c1,Z_163)) = multiply(identity,Z_163) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_12302]) ).
tff(c_12370,plain,
! [Z_165] : ( multiply(sk_c7,multiply(sk_c1,Z_165)) = Z_165 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12335]) ).
tff(c_12382,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_102,c_12370]) ).
tff(c_12341,plain,
! [X_2,Z_163] : ( multiply(inverse(X_2),multiply(X_2,Z_163)) = multiply(identity,Z_163) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12302]) ).
tff(c_12416,plain,
! [X_167,Z_168] : ( multiply(inverse(X_167),multiply(X_167,Z_168)) = Z_168 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12341]) ).
tff(c_12440,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12382,c_12416]) ).
tff(c_12495,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12440]) ).
tff(c_50,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_75,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_12514,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12495,c_75]) ).
tff(c_12535,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12514,c_4]) ).
tff(c_12353,plain,
! [X_2,Z_163] : ( multiply(inverse(X_2),multiply(X_2,Z_163)) = Z_163 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12341]) ).
tff(c_12653,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_12535,c_12353]) ).
tff(c_12665,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12653]) ).
tff(c_134,plain,
! [X_12,Y_13,Z_14] : ( multiply(multiply(X_12,Y_13),Z_14) = multiply(X_12,multiply(Y_13,Z_14)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_158,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_134]) ).
tff(c_489,plain,
! [Z_23] : ( multiply(sk_c7,multiply(sk_c1,Z_23)) = Z_23 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_507,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_102,c_489]) ).
tff(c_155,plain,
! [Z_14] : ( multiply(sk_c1,multiply(sk_c7,Z_14)) = multiply(sk_c6,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_134]) ).
tff(c_514,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c1,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_507,c_155]) ).
tff(c_520,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_514]) ).
tff(c_164,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_134]) ).
tff(c_1025,plain,
! [X_32,Z_33] : ( multiply(inverse(X_32),multiply(X_32,Z_33)) = Z_33 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_1058,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_520,c_1025]) ).
tff(c_1082,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1058]) ).
tff(c_174,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_1216,plain,
! [X_35,Z_36] : ( multiply(inverse(inverse(X_35)),Z_36) = multiply(X_35,Z_36) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_1025]) ).
tff(c_1073,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1025]) ).
tff(c_1223,plain,
! [X_35] : ( multiply(X_35,identity) = X_35 ),
inference(superposition,[status(thm),theory(equality)],[c_1216,c_1073]) ).
tff(c_40,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_112,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_79,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_75,c_4]) ).
tff(c_161,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_134]) ).
tff(c_529,plain,
! [Z_24] : ( multiply(sk_c6,multiply(sk_c2,Z_24)) = Z_24 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_541,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_112,c_529]) ).
tff(c_1052,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_541,c_1025]) ).
tff(c_1081,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1052]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_107,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_470,plain,
! [Z_22] : ( multiply(sk_c1,multiply(sk_c7,Z_22)) = multiply(sk_c6,Z_22) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_134]) ).
tff(c_482,plain,
multiply(sk_c6,sk_c5) = multiply(sk_c1,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_107,c_470]) ).
tff(c_725,plain,
multiply(sk_c1,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_541,c_482]) ).
tff(c_172,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_729,plain,
multiply(sk_c7,sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_725,c_172]) ).
tff(c_736,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_729,c_507]) ).
tff(c_179,plain,
! [Z_15] : ( multiply(sk_c6,multiply(sk_c2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_191,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_112,c_179]) ).
tff(c_238,plain,
! [X_18,Z_19] : ( multiply(inverse(X_18),multiply(X_18,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_265,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_191,c_238]) ).
tff(c_303,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_265]) ).
tff(c_215,plain,
! [Z_17] : ( multiply(sk_c7,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_227,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_102,c_215]) ).
tff(c_256,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_227,c_238]) ).
tff(c_302,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_256]) ).
tff(c_58,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_177,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_107,c_58]) ).
tff(c_178,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_177]) ).
tff(c_312,plain,
multiply(identity,sk_c7) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_302,c_178]) ).
tff(c_319,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_312]) ).
tff(c_345,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_303,c_319]) ).
tff(c_308,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_302,c_227]) ).
tff(c_314,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_302,c_107]) ).
tff(c_459,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_308,c_303,c_314]) ).
tff(c_460,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_345,c_459]) ).
tff(c_462,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_751,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_736,c_462]) ).
tff(c_780,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_751,c_520]) ).
tff(c_789,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_780,c_780,c_751]) ).
tff(c_828,plain,
! [X_27,Z_28] : ( multiply(inverse(X_27),multiply(X_27,Z_28)) = Z_28 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_846,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_789,c_828]) ).
tff(c_865,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_846]) ).
tff(c_755,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_736,c_87]) ).
tff(c_791,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_780,c_755]) ).
tff(c_810,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_791,c_4]) ).
tff(c_884,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_865,c_810]) ).
tff(c_868,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_865,c_791]) ).
tff(c_899,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_884,c_868]) ).
tff(c_927,plain,
! [X_29] : ( multiply(inverse(inverse(X_29)),identity) = X_29 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_828]) ).
tff(c_933,plain,
! [X_29] : ( multiply(inverse(inverse(inverse(X_29))),X_29) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_927,c_174]) ).
tff(c_870,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_865,c_780]) ).
tff(c_553,plain,
multiply(sk_c1,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_541,c_482]) ).
tff(c_557,plain,
multiply(sk_c7,sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_553,c_172]) ).
tff(c_564,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_557,c_507]) ).
tff(c_579,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_564,c_462]) ).
tff(c_646,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_579,c_520]) ).
tff(c_583,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_564,c_87]) ).
tff(c_659,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_646,c_583]) ).
tff(c_662,plain,
multiply(sk_c1,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_646,c_646,c_553]) ).
tff(c_461,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_552,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_461]) ).
tff(c_674,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_646,c_646,c_552]) ).
tff(c_714,plain,
inverse(sk_c1) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_662,c_674]) ).
tff(c_723,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_659,c_714]) ).
tff(c_724,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_461]) ).
tff(c_763,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_736,c_736,c_736,c_736,c_724]) ).
tff(c_764,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_763]) ).
tff(c_985,plain,
! [X3_31] :
( ( inverse(X3_31) != identity )
| ( multiply(X3_31,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_870,c_870,c_870,c_764]) ).
tff(c_989,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_933,c_985]) ).
tff(c_1008,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_899,c_899,c_899,c_899,c_989]) ).
tff(c_1009,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c6 )
| ( inverse(X1_8) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_763]) ).
tff(c_10963,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1082,c_1223,c_1082,c_1082,c_1223,c_1082,c_1081,c_1082,c_1009]) ).
tff(c_10965,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_10963]) ).
tff(c_1013,plain,
multiply(sk_c6,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_755,c_4]) ).
tff(c_1108,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1082,c_1013]) ).
tff(c_1092,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1082,c_755]) ).
tff(c_1123,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1108,c_1092]) ).
tff(c_10967,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10965,c_1123]) ).
tff(c_10969,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_10963]) ).
tff(c_10971,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10969,c_1123]) ).
tff(c_10973,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_11019,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10973,c_46]) ).
tff(c_44,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_10988,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10973,c_44]) ).
tff(c_10992,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10988,c_4]) ).
tff(c_11025,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_11049,plain,
! [Z_139] : ( multiply(sk_c6,multiply(sk_c4,Z_139)) = multiply(identity,Z_139) ),
inference(superposition,[status(thm),theory(equality)],[c_10992,c_11025]) ).
tff(c_11117,plain,
! [Z_142] : ( multiply(sk_c6,multiply(sk_c4,Z_142)) = Z_142 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11049]) ).
tff(c_11129,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11019,c_11117]) ).
tff(c_11061,plain,
! [Z_139] : ( multiply(sk_c7,multiply(sk_c1,Z_139)) = multiply(identity,Z_139) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_11025]) ).
tff(c_11081,plain,
! [Z_140] : ( multiply(sk_c7,multiply(sk_c1,Z_140)) = Z_140 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11061]) ).
tff(c_11093,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_102,c_11081]) ).
tff(c_11194,plain,
! [Z_145] : ( multiply(sk_c1,multiply(sk_c7,Z_145)) = multiply(sk_c6,Z_145) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_11025]) ).
tff(c_11209,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c1,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_11093,c_11194]) ).
tff(c_11225,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_11129,c_11209]) ).
tff(c_11227,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11225,c_11225,c_11129]) ).
tff(c_11067,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_11025]) ).
tff(c_11332,plain,
! [X_146,Z_147] : ( multiply(inverse(X_146),multiply(X_146,Z_147)) = Z_147 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11067]) ).
tff(c_11362,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11227,c_11332]) ).
tff(c_11407,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11362]) ).
tff(c_11239,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11225,c_79]) ).
tff(c_11431,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11407,c_11239]) ).
tff(c_11079,plain,
! [X_2,Z_139] : ( multiply(inverse(X_2),multiply(X_2,Z_139)) = Z_139 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11067]) ).
tff(c_11522,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_11431,c_11079]) ).
tff(c_11534,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11522]) ).
tff(c_11236,plain,
multiply(sk_c2,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11225,c_10973]) ).
tff(c_11428,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_11407,c_11407,c_11236]) ).
tff(c_11550,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11534,c_11428]) ).
tff(c_11551,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_11552,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_12292,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_11552,c_36]) ).
tff(c_12452,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_12292,c_12416]) ).
tff(c_12496,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11551,c_12452]) ).
tff(c_12578,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12495,c_2,c_12495,c_12496]) ).
tff(c_11564,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_11609,plain,
! [X_148,Y_149,Z_150] : ( multiply(multiply(X_148,Y_149),Z_150) = multiply(X_148,multiply(Y_149,Z_150)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11648,plain,
! [Z_150] : ( multiply(sk_c6,multiply(sk_c2,Z_150)) = multiply(identity,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_11609]) ).
tff(c_11667,plain,
! [Z_151] : ( multiply(sk_c6,multiply(sk_c2,Z_151)) = Z_151 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11648]) ).
tff(c_11679,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11564,c_11667]) ).
tff(c_11651,plain,
! [X_2,Z_150] : ( multiply(inverse(X_2),multiply(X_2,Z_150)) = multiply(identity,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11609]) ).
tff(c_11783,plain,
! [X_155,Z_156] : ( multiply(inverse(X_155),multiply(X_155,Z_156)) = Z_156 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11651]) ).
tff(c_11822,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11679,c_11783]) ).
tff(c_11880,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11822]) ).
tff(c_11645,plain,
! [Z_150] : ( multiply(sk_c7,multiply(sk_c1,Z_150)) = multiply(identity,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_11609]) ).
tff(c_11690,plain,
! [Z_152] : ( multiply(sk_c7,multiply(sk_c1,Z_152)) = Z_152 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11645]) ).
tff(c_11702,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_102,c_11690]) ).
tff(c_11813,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11702,c_11783]) ).
tff(c_11878,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11813]) ).
tff(c_28,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_11589,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_11552,c_28]) ).
tff(c_11895,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11878,c_11589]) ).
tff(c_12125,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11880,c_11895]) ).
tff(c_11663,plain,
! [X_2,Z_150] : ( multiply(inverse(X_2),multiply(X_2,Z_150)) = Z_150 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11651]) ).
tff(c_12129,plain,
multiply(inverse(identity),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_12125,c_11663]) ).
tff(c_12141,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12129]) ).
tff(c_11898,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_11878,c_11552]) ).
tff(c_12254,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12141,c_11880,c_11898]) ).
tff(c_12256,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_12508,plain,
multiply(sk_c2,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12495,c_12256]) ).
tff(c_12679,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12665,c_12578,c_12508]) ).
tff(c_12681,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_15960,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12681,c_16]) ).
tff(c_12680,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_12685,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12680,c_4]) ).
tff(c_15973,plain,
! [X_229,Y_230,Z_231] : ( multiply(multiply(X_229,Y_230),Z_231) = multiply(X_229,multiply(Y_230,Z_231)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16000,plain,
! [Z_231] : ( multiply(sk_c6,multiply(sk_c4,Z_231)) = multiply(identity,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_12685,c_15973]) ).
tff(c_16074,plain,
! [Z_235] : ( multiply(sk_c6,multiply(sk_c4,Z_235)) = Z_235 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16000]) ).
tff(c_16086,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_15960,c_16074]) ).
tff(c_12694,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_12743,plain,
! [X_170,Y_171,Z_172] : ( multiply(multiply(X_170,Y_171),Z_172) = multiply(X_170,multiply(Y_171,Z_172)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_12782,plain,
! [Z_172] : ( multiply(sk_c6,multiply(sk_c2,Z_172)) = multiply(identity,Z_172) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_12743]) ).
tff(c_12812,plain,
! [Z_174] : ( multiply(sk_c6,multiply(sk_c2,Z_174)) = Z_174 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12782]) ).
tff(c_12824,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12694,c_12812]) ).
tff(c_12785,plain,
! [X_2,Z_172] : ( multiply(inverse(X_2),multiply(X_2,Z_172)) = multiply(identity,Z_172) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12743]) ).
tff(c_13894,plain,
! [X_191,Z_192] : ( multiply(inverse(X_191),multiply(X_191,Z_192)) = Z_192 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12785]) ).
tff(c_13927,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_12824,c_13894]) ).
tff(c_13985,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13927]) ).
tff(c_12773,plain,
! [Z_172] : ( multiply(sk_c2,multiply(sk_c6,Z_172)) = multiply(sk_c5,Z_172) ),
inference(superposition,[status(thm),theory(equality)],[c_12694,c_12743]) ).
tff(c_14134,plain,
! [Z_194] : ( multiply(sk_c2,multiply(sk_c6,Z_194)) = Z_194 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13985,c_12773]) ).
tff(c_14170,plain,
multiply(sk_c2,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_79,c_14134]) ).
tff(c_12728,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12681,c_16]) ).
tff(c_12776,plain,
! [Z_172] : ( multiply(sk_c6,multiply(sk_c4,Z_172)) = multiply(identity,Z_172) ),
inference(superposition,[status(thm),theory(equality)],[c_12685,c_12743]) ).
tff(c_12835,plain,
! [Z_175] : ( multiply(sk_c6,multiply(sk_c4,Z_175)) = Z_175 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12776]) ).
tff(c_12847,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_12728,c_12835]) ).
tff(c_13994,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13985,c_12847]) ).
tff(c_14152,plain,
multiply(sk_c2,identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_13994,c_14134]) ).
tff(c_14194,plain,
sk_c6 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14170,c_14152]) ).
tff(c_14210,plain,
multiply(sk_c2,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14194,c_79]) ).
tff(c_14211,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14194,c_75]) ).
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_12723,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_12681,c_8]) ).
tff(c_13997,plain,
multiply(sk_c6,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13985,c_12723]) ).
tff(c_14155,plain,
multiply(sk_c2,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13997,c_14134]) ).
tff(c_14315,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14170,c_14155]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_12704,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_12681,c_10]) ).
tff(c_14322,plain,
inverse(sk_c3) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14315,c_12704]) ).
tff(c_14335,plain,
multiply(sk_c2,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14322,c_4]) ).
tff(c_12797,plain,
! [X_2,Z_172] : ( multiply(inverse(X_2),multiply(X_2,Z_172)) = Z_172 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12785]) ).
tff(c_14342,plain,
multiply(inverse(sk_c2),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_14335,c_12797]) ).
tff(c_14348,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14170,c_14211,c_14342]) ).
tff(c_12,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_12734,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_12681,c_12]) ).
tff(c_14206,plain,
multiply(sk_c3,sk_c2) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_14194,c_12734]) ).
tff(c_14318,plain,
multiply(sk_c3,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14315,c_14206]) ).
tff(c_14406,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14210,c_14348,c_14318]) ).
tff(c_14323,plain,
multiply(sk_c2,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14315,c_91]) ).
tff(c_14467,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14406,c_14323]) ).
tff(c_14208,plain,
multiply(sk_c1,sk_c7) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14194,c_12681]) ).
tff(c_14317,plain,
multiply(sk_c1,sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14315,c_14208]) ).
tff(c_14407,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_14406,c_14406,c_14317]) ).
tff(c_14483,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14467,c_14407]) ).
tff(c_14485,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_42,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_15951,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14485,c_42]) ).
tff(c_14484,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_14489,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14484,c_4]) ).
tff(c_15997,plain,
! [Z_231] : ( multiply(sk_c7,multiply(sk_c3,Z_231)) = multiply(identity,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_14489,c_15973]) ).
tff(c_16051,plain,
! [Z_234] : ( multiply(sk_c7,multiply(sk_c3,Z_234)) = Z_234 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15997]) ).
tff(c_16063,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_15951,c_16051]) ).
tff(c_14517,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12681,c_16]) ).
tff(c_14534,plain,
! [X_197,Y_198,Z_199] : ( multiply(multiply(X_197,Y_198),Z_199) = multiply(X_197,multiply(Y_198,Z_199)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14564,plain,
! [Z_199] : ( multiply(sk_c6,multiply(sk_c4,Z_199)) = multiply(identity,Z_199) ),
inference(superposition,[status(thm),theory(equality)],[c_12685,c_14534]) ).
tff(c_15503,plain,
! [Z_224] : ( multiply(sk_c6,multiply(sk_c4,Z_224)) = Z_224 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14564]) ).
tff(c_15515,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_14517,c_15503]) ).
tff(c_14507,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14485,c_42]) ).
tff(c_14561,plain,
! [Z_199] : ( multiply(sk_c7,multiply(sk_c3,Z_199)) = multiply(identity,Z_199) ),
inference(superposition,[status(thm),theory(equality)],[c_14489,c_14534]) ).
tff(c_15480,plain,
! [Z_223] : ( multiply(sk_c7,multiply(sk_c3,Z_223)) = Z_223 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14561]) ).
tff(c_15492,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_14507,c_15480]) ).
tff(c_38,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_14524,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_14485,c_38]) ).
tff(c_15558,plain,
! [Z_226] : ( multiply(sk_c6,multiply(sk_c7,Z_226)) = multiply(sk_c5,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_14524,c_14534]) ).
tff(c_15570,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_15492,c_15558]) ).
tff(c_15592,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_15515,c_15570]) ).
tff(c_14573,plain,
! [X_2,Z_199] : ( multiply(inverse(X_2),multiply(X_2,Z_199)) = multiply(identity,Z_199) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14534]) ).
tff(c_15696,plain,
! [X_227,Z_228] : ( multiply(inverse(X_227),multiply(X_227,Z_228)) = Z_228 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14573]) ).
tff(c_15735,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_15592,c_15696]) ).
tff(c_15771,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15735]) ).
tff(c_15796,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15771,c_91]) ).
tff(c_14585,plain,
! [X_2,Z_199] : ( multiply(inverse(X_2),multiply(X_2,Z_199)) = Z_199 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14573]) ).
tff(c_15887,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_15796,c_14585]) ).
tff(c_15899,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15887]) ).
tff(c_14506,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_15582,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_14506,c_15558]) ).
tff(c_15593,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_15515,c_15582]) ).
tff(c_15738,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_15593,c_15696]) ).
tff(c_15772,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15738]) ).
tff(c_14555,plain,
! [Z_199] : ( multiply(sk_c7,multiply(sk_c5,Z_199)) = multiply(sk_c6,Z_199) ),
inference(superposition,[status(thm),theory(equality)],[c_14506,c_14534]) ).
tff(c_15608,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c6,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_15592,c_14555]) ).
tff(c_15614,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_14506,c_14524,c_15608]) ).
tff(c_15628,plain,
multiply(sk_c1,sk_c7) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_15614,c_12681]) ).
tff(c_15779,plain,
multiply(sk_c1,sk_c7) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_15772,c_15628]) ).
tff(c_15944,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15899,c_15771,c_15779]) ).
tff(c_15945,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_16461,plain,
! [Z_242] : ( multiply(sk_c6,multiply(sk_c7,Z_242)) = multiply(sk_c5,Z_242) ),
inference(superposition,[status(thm),theory(equality)],[c_15945,c_15973]) ).
tff(c_16479,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_16063,c_16461]) ).
tff(c_16489,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16086,c_16479]) ).
tff(c_16009,plain,
! [X_2,Z_231] : ( multiply(inverse(X_2),multiply(X_2,Z_231)) = multiply(identity,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_15973]) ).
tff(c_16021,plain,
! [X_2,Z_231] : ( multiply(inverse(X_2),multiply(X_2,Z_231)) = Z_231 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16009]) ).
tff(c_16496,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16489,c_16021]) ).
tff(c_16503,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16496]) ).
tff(c_16165,plain,
! [X_237,Z_238] : ( multiply(inverse(X_237),multiply(X_237,Z_238)) = Z_238 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16009]) ).
tff(c_16240,plain,
multiply(inverse(sk_c7),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_91,c_16165]) ).
tff(c_16529,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_16503,c_16240]) ).
tff(c_16533,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16529]) ).
tff(c_16246,plain,
multiply(inverse(sk_c6),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_79,c_16165]) ).
tff(c_16325,plain,
! [X_240] : ( multiply(inverse(inverse(X_240)),identity) = X_240 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16165]) ).
tff(c_16343,plain,
multiply(inverse(sk_c6),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_12680,c_16325]) ).
tff(c_16354,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_16246,c_16343]) ).
tff(c_16373,plain,
multiply(sk_c2,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16354,c_15960]) ).
tff(c_15988,plain,
! [Z_231] : ( multiply(sk_c4,multiply(sk_c5,Z_231)) = multiply(sk_c6,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_15960,c_15973]) ).
tff(c_16428,plain,
! [Z_231] : ( multiply(sk_c2,multiply(sk_c5,Z_231)) = multiply(sk_c6,Z_231) ),
inference(demodulation,[status(thm),theory(equality)],[c_16354,c_15988]) ).
tff(c_16493,plain,
multiply(sk_c6,sk_c7) = multiply(sk_c2,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16489,c_16428]) ).
tff(c_16502,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16373,c_15945,c_16493]) ).
tff(c_16519,plain,
multiply(sk_c1,sk_c7) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16502,c_12681]) ).
tff(c_16593,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16533,c_16503,c_16519]) ).
tff(c_16514,plain,
multiply(sk_c7,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16502,c_16063]) ).
tff(c_16606,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16503,c_2,c_16503,c_16514]) ).
tff(c_16607,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16593,c_16606]) ).
tff(c_16609,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_16642,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16609,c_22]) ).
tff(c_16608,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_16613,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16608,c_4]) ).
tff(c_16694,plain,
! [Z_245] : ( multiply(sk_c7,multiply(sk_c3,Z_245)) = multiply(identity,Z_245) ),
inference(superposition,[status(thm),theory(equality)],[c_16613,c_16667]) ).
tff(c_16736,plain,
! [Z_247] : ( multiply(sk_c7,multiply(sk_c3,Z_247)) = Z_247 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16694]) ).
tff(c_16748,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16642,c_16736]) ).
tff(c_18,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_16647,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_16609,c_18]) ).
tff(c_17099,plain,
! [Z_257] : ( multiply(sk_c3,multiply(sk_c6,Z_257)) = multiply(sk_c7,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_16642,c_16667]) ).
tff(c_17120,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16647,c_17099]) ).
tff(c_17153,plain,
multiply(sk_c3,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16748,c_17120]) ).
tff(c_16709,plain,
! [Z_245] : ( multiply(sk_c7,multiply(sk_c3,Z_245)) = Z_245 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16694]) ).
tff(c_17157,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_17153,c_16709]) ).
tff(c_26,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_16635,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_16609,c_26]) ).
tff(c_24,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_16621,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_16609,c_24]) ).
tff(c_16625,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16621,c_4]) ).
tff(c_16691,plain,
! [Z_245] : ( multiply(sk_c6,multiply(sk_c4,Z_245)) = multiply(identity,Z_245) ),
inference(superposition,[status(thm),theory(equality)],[c_16625,c_16667]) ).
tff(c_16713,plain,
! [Z_246] : ( multiply(sk_c6,multiply(sk_c4,Z_246)) = Z_246 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16691]) ).
tff(c_16725,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16635,c_16713]) ).
tff(c_17114,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16725,c_17099]) ).
tff(c_17570,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17153,c_17157,c_17114]) ).
tff(c_17580,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17570,c_16647]) ).
tff(c_18215,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_17580,c_16711]) ).
tff(c_18221,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_18215]) ).
tff(c_17575,plain,
multiply(sk_c7,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17570,c_16748]) ).
tff(c_18224,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_18221,c_18221,c_17575]) ).
tff(c_18231,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18224]) ).
tff(c_17578,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17570,c_17570,c_16725]) ).
tff(c_17681,plain,
! [X_264,Z_265] : ( multiply(inverse(X_264),multiply(X_264,Z_265)) = Z_265 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16700]) ).
tff(c_17699,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_17578,c_17681]) ).
tff(c_17727,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17699]) ).
tff(c_17573,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17570,c_17153]) ).
tff(c_17581,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_17570,c_16642]) ).
tff(c_17662,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17573,c_17581]) ).
tff(c_17729,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17727,c_17662]) ).
tff(c_17882,plain,
! [X_267,Z_268] : ( multiply(inverse(inverse(X_267)),Z_268) = multiply(X_267,Z_268) ),
inference(superposition,[status(thm),theory(equality)],[c_16711,c_17681]) ).
tff(c_17720,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17681]) ).
tff(c_17889,plain,
! [X_267] : ( multiply(X_267,identity) = X_267 ),
inference(superposition,[status(thm),theory(equality)],[c_17882,c_17720]) ).
tff(c_17188,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17157,c_17153,c_17114]) ).
tff(c_17190,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17188,c_17153]) ).
tff(c_17198,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_17188,c_16642]) ).
tff(c_17277,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17190,c_17198]) ).
tff(c_17197,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17188,c_16647]) ).
tff(c_17311,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17277,c_17197]) ).
tff(c_17328,plain,
! [X_260,Z_261] : ( multiply(inverse(X_260),multiply(X_260,Z_261)) = Z_261 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16700]) ).
tff(c_17349,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_17311,c_17328]) ).
tff(c_17384,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17349]) ).
tff(c_17390,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17384,c_17277]) ).
tff(c_17296,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17277,c_16608]) ).
tff(c_17307,plain,
multiply(sk_c5,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_17296,c_4]) ).
tff(c_17412,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17384,c_17307]) ).
tff(c_17389,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17384,c_17296]) ).
tff(c_17439,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17412,c_17389]) ).
tff(c_16938,plain,
! [Z_253] : ( multiply(sk_c6,multiply(sk_c7,Z_253)) = multiply(sk_c5,Z_253) ),
inference(superposition,[status(thm),theory(equality)],[c_16647,c_16667]) ).
tff(c_16953,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_16748,c_16938]) ).
tff(c_16963,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16725,c_16953]) ).
tff(c_16967,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16963,c_16711]) ).
tff(c_16976,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16967]) ).
tff(c_16983,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16976,c_16976,c_16748]) ).
tff(c_16993,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16983]) ).
tff(c_16688,plain,
! [Z_245] : ( multiply(sk_c4,multiply(sk_c5,Z_245)) = multiply(sk_c6,Z_245) ),
inference(superposition,[status(thm),theory(equality)],[c_16635,c_16667]) ).
tff(c_16970,plain,
multiply(sk_c6,sk_c7) = multiply(sk_c4,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_16963,c_16688]) ).
tff(c_16977,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16647,c_16635,c_16970]) ).
tff(c_17029,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16993,c_16977]) ).
tff(c_16753,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16647,c_58]) ).
tff(c_16754,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitLeft,[status(thm)],[c_16753]) ).
tff(c_16984,plain,
multiply(identity,sk_c5) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16976,c_16754]) ).
tff(c_16994,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16984]) ).
tff(c_17043,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_17029,c_16993,c_16994]) ).
tff(c_17044,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_16753]) ).
tff(c_17074,plain,
! [X2_256] :
( ( multiply(X2_256,sk_c5) != sk_c6 )
| ( inverse(X2_256) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_17044]) ).
tff(c_17084,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16635,c_17074]) ).
tff(c_17097,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16621,c_17084]) ).
tff(c_17098,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_17044]) ).
tff(c_17179,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_17098]) ).
tff(c_17254,plain,
! [X3_259] :
( ( inverse(X3_259) != sk_c7 )
| ( multiply(X3_259,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17188,c_17179]) ).
tff(c_17266,plain,
( ( inverse(identity) != sk_c7 )
| ( sk_c7 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_17254]) ).
tff(c_17544,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_17390,c_17384,c_17439,c_17390,c_17266]) ).
tff(c_17545,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_17098]) ).
tff(c_17615,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17570,c_17570,c_17570,c_17545]) ).
tff(c_17616,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_17615]) ).
tff(c_18144,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_17729,c_17889,c_17729,c_17727,c_17616]) ).
tff(c_17584,plain,
inverse(sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_17570,c_16621]) ).
tff(c_17594,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_17584,c_4]) ).
tff(c_17750,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17727,c_17594]) ).
tff(c_17735,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17727,c_17584]) ).
tff(c_17766,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17750,c_17735]) ).
tff(c_18146,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18144,c_17766]) ).
tff(c_18147,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_17615]) ).
tff(c_18766,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_18388,c_18231,c_18231,c_18231,c_18147]) ).
tff(c_18246,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18231,c_17594]) ).
tff(c_18240,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18231,c_17584]) ).
tff(c_18255,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18246,c_18240]) ).
tff(c_18768,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18766,c_18255]) ).
tff(c_18770,plain,
inverse(sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_52,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_18811,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_18770,c_52]) ).
tff(c_18769,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_18774,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18769,c_4]) ).
tff(c_18840,plain,
! [X_287,Y_288,Z_289] : ( multiply(multiply(X_287,Y_288),Z_289) = multiply(X_287,multiply(Y_288,Z_289)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_18870,plain,
! [Z_289] : ( multiply(sk_c7,multiply(sk_c3,Z_289)) = multiply(identity,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_18774,c_18840]) ).
tff(c_18912,plain,
! [Z_291] : ( multiply(sk_c7,multiply(sk_c3,Z_291)) = Z_291 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18870]) ).
tff(c_18924,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_18811,c_18912]) ).
tff(c_48,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_18825,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_18770,c_48]) ).
tff(c_18935,plain,
! [Z_292] : ( multiply(sk_c3,multiply(sk_c6,Z_292)) = multiply(sk_c7,Z_292) ),
inference(superposition,[status(thm),theory(equality)],[c_18811,c_18840]) ).
tff(c_18956,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_18825,c_18935]) ).
tff(c_18963,plain,
multiply(sk_c3,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_18924,c_18956]) ).
tff(c_18883,plain,
! [Z_289] : ( multiply(sk_c7,multiply(sk_c3,Z_289)) = Z_289 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18870]) ).
tff(c_18967,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_18963,c_18883]) ).
tff(c_56,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_18819,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_18770,c_56]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_18795,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_18770,c_54]) ).
tff(c_18799,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18795,c_4]) ).
tff(c_18864,plain,
! [Z_289] : ( multiply(sk_c6,multiply(sk_c4,Z_289)) = multiply(identity,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_18799,c_18840]) ).
tff(c_18886,plain,
! [Z_290] : ( multiply(sk_c6,multiply(sk_c4,Z_290)) = Z_290 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18864]) ).
tff(c_18898,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_18819,c_18886]) ).
tff(c_18950,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_18898,c_18935]) ).
tff(c_19002,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_18967,c_18963,c_18950]) ).
tff(c_19008,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19002,c_19002,c_18898]) ).
tff(c_18873,plain,
! [X_2,Z_289] : ( multiply(inverse(X_2),multiply(X_2,Z_289)) = multiply(identity,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18840]) ).
tff(c_18884,plain,
! [X_2,Z_289] : ( multiply(inverse(X_2),multiply(X_2,Z_289)) = Z_289 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18873]) ).
tff(c_19084,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_19008,c_18884]) ).
tff(c_19090,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19084]) ).
tff(c_19013,plain,
multiply(sk_c5,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19002,c_18799]) ).
tff(c_19127,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19090,c_19013]) ).
tff(c_19014,plain,
inverse(sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19002,c_18795]) ).
tff(c_19106,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19090,c_19014]) ).
tff(c_19128,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19127,c_19106]) ).
tff(c_19107,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19090,c_19002]) ).
tff(c_18855,plain,
! [Z_289] : ( multiply(sk_c6,multiply(sk_c7,Z_289)) = multiply(sk_c5,Z_289) ),
inference(superposition,[status(thm),theory(equality)],[c_18825,c_18840]) ).
tff(c_19135,plain,
! [Z_296] : ( multiply(sk_c7,Z_296) = Z_296 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19107,c_2,c_19090,c_18855]) ).
tff(c_19156,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_19135,c_18774]) ).
tff(c_19177,plain,
inverse(identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_19156,c_18769]) ).
tff(c_19208,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19128,c_19177]) ).
tff(c_18910,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18825,c_58]) ).
tff(c_18911,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitLeft,[status(thm)],[c_18910]) ).
tff(c_19007,plain,
multiply(sk_c7,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19002,c_18911]) ).
tff(c_19225,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19208,c_19090,c_19090,c_19007]) ).
tff(c_19227,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_18910]) ).
tff(c_19333,plain,
! [X_302,Z_303] : ( multiply(inverse(X_302),multiply(X_302,Z_303)) = Z_303 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18873]) ).
tff(c_19363,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_19227,c_19333]) ).
tff(c_19235,plain,
! [Z_297] : ( multiply(sk_c7,multiply(sk_c3,Z_297)) = Z_297 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18870]) ).
tff(c_19247,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_18811,c_19235]) ).
tff(c_19354,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_19247,c_19333]) ).
tff(c_19958,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19363,c_19354]) ).
tff(c_18783,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_19968,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19958,c_18783]) ).
tff(c_18787,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18783,c_4]) ).
tff(c_19390,plain,
multiply(inverse(sk_c7),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_18787,c_19333]) ).
tff(c_19396,plain,
multiply(inverse(sk_c7),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_18774,c_19333]) ).
tff(c_19919,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_19390,c_19396]) ).
tff(c_19932,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_19919,c_18811]) ).
tff(c_19959,plain,
multiply(sk_c1,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19958,c_19932]) ).
tff(c_19787,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19363,c_19354]) ).
tff(c_19797,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19787,c_18783]) ).
tff(c_19725,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_19390,c_19396]) ).
tff(c_19738,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_19725,c_18811]) ).
tff(c_19788,plain,
multiply(sk_c1,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19787,c_19738]) ).
tff(c_19366,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_18898,c_19333]) ).
tff(c_19375,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_18825,c_19333]) ).
tff(c_19560,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_19366,c_19375]) ).
tff(c_19598,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19560,c_19363]) ).
tff(c_19605,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19598]) ).
tff(c_19600,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_19560,c_19560,c_19247]) ).
tff(c_19606,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_18898,c_19600]) ).
tff(c_19622,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19605,c_19606]) ).
tff(c_19623,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19622,c_19560]) ).
tff(c_19226,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_18910]) ).
tff(c_19272,plain,
! [X2_299] :
( ( multiply(X2_299,sk_c5) != sk_c6 )
| ( inverse(X2_299) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_19226]) ).
tff(c_19282,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_18819,c_19272]) ).
tff(c_19295,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18795,c_19282]) ).
tff(c_19296,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_19226]) ).
tff(c_19571,plain,
! [X3_306] :
( ( inverse(X3_306) != sk_c7 )
| ( multiply(X3_306,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_19296]) ).
tff(c_19585,plain,
( ( inverse(sk_c6) != sk_c7 )
| ( sk_c6 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18825,c_19571]) ).
tff(c_19654,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_19605,c_19622,c_19623,c_19622,c_19585]) ).
tff(c_19384,plain,
multiply(inverse(sk_c6),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_18799,c_19333]) ).
tff(c_19624,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_19622,c_19384]) ).
tff(c_19629,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19624]) ).
tff(c_19627,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19622,c_18795]) ).
tff(c_19663,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19629,c_19627]) ).
tff(c_19664,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19654,c_19663]) ).
tff(c_19665,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_19296]) ).
tff(c_19724,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_19665]) ).
tff(c_19839,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_19787,c_19787,c_19724]) ).
tff(c_19878,plain,
inverse(sk_c1) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_19788,c_19839]) ).
tff(c_19890,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_19797,c_19878]) ).
tff(c_19891,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_19665]) ).
tff(c_20049,plain,
inverse(sk_c1) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_19959,c_19891]) ).
tff(c_20059,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19968,c_20049]) ).
tff(c_19961,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19958,c_19375]) ).
tff(c_20072,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19961,c_19366]) ).
tff(c_20073,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20059,c_20072]) ).
tff(c_20075,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_20089,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_20075,c_26]) ).
tff(c_20074,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_20079,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20074,c_4]) ).
tff(c_20125,plain,
! [X_312,Y_313,Z_314] : ( multiply(multiply(X_312,Y_313),Z_314) = multiply(X_312,multiply(Y_313,Z_314)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20149,plain,
! [Z_314] : ( multiply(sk_c6,multiply(sk_c4,Z_314)) = multiply(identity,Z_314) ),
inference(superposition,[status(thm),theory(equality)],[c_20079,c_20125]) ).
tff(c_20167,plain,
! [Z_315] : ( multiply(sk_c6,multiply(sk_c4,Z_315)) = Z_315 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20149]) ).
tff(c_20179,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_20089,c_20167]) ).
tff(c_20103,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_18770,c_52]) ).
tff(c_20152,plain,
! [Z_314] : ( multiply(sk_c7,multiply(sk_c3,Z_314)) = multiply(identity,Z_314) ),
inference(superposition,[status(thm),theory(equality)],[c_18774,c_20125]) ).
tff(c_20447,plain,
! [Z_322] : ( multiply(sk_c7,multiply(sk_c3,Z_322)) = Z_322 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20152]) ).
tff(c_20462,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20103,c_20447]) ).
tff(c_20096,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_20075,c_18]) ).
tff(c_20143,plain,
! [Z_314] : ( multiply(sk_c6,multiply(sk_c7,Z_314)) = multiply(sk_c5,Z_314) ),
inference(superposition,[status(thm),theory(equality)],[c_20096,c_20125]) ).
tff(c_20536,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_20462,c_20143]) ).
tff(c_20542,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20179,c_20536]) ).
tff(c_20155,plain,
! [X_2,Z_314] : ( multiply(inverse(X_2),multiply(X_2,Z_314)) = multiply(identity,Z_314) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20125]) ).
tff(c_21182,plain,
! [X_337,Z_338] : ( multiply(inverse(X_337),multiply(X_337,Z_338)) = Z_338 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20155]) ).
tff(c_21212,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20542,c_21182]) ).
tff(c_21237,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21212]) ).
tff(c_20165,plain,
! [X_2,Z_314] : ( multiply(inverse(X_2),multiply(X_2,Z_314)) = Z_314 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20155]) ).
tff(c_21357,plain,
! [X_340,Z_341] : ( multiply(inverse(inverse(X_340)),Z_341) = multiply(X_340,Z_341) ),
inference(superposition,[status(thm),theory(equality)],[c_21182,c_20165]) ).
tff(c_21230,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_21182]) ).
tff(c_21364,plain,
! [X_340] : ( multiply(X_340,identity) = X_340 ),
inference(superposition,[status(thm),theory(equality)],[c_21357,c_21230]) ).
tff(c_20193,plain,
! [Z_316] : ( multiply(sk_c7,multiply(sk_c3,Z_316)) = Z_316 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20152]) ).
tff(c_20205,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20103,c_20193]) ).
tff(c_20231,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_20205,c_20143]) ).
tff(c_20237,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20179,c_20231]) ).
tff(c_20254,plain,
! [X_318,Z_319] : ( multiply(inverse(X_318),multiply(X_318,Z_319)) = Z_319 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20155]) ).
tff(c_20275,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20237,c_20254]) ).
tff(c_20324,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20275]) ).
tff(c_20330,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20324,c_20324,c_20205]) ).
tff(c_20339,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20330]) ).
tff(c_20377,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20339,c_20339,c_20179]) ).
tff(c_20385,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20377]) ).
tff(c_20184,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_20096,c_58]) ).
tff(c_20185,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitLeft,[status(thm)],[c_20184]) ).
tff(c_20333,plain,
multiply(identity,sk_c5) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_20324,c_20185]) ).
tff(c_20341,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20333]) ).
tff(c_20395,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20385,c_20339,c_20341]) ).
tff(c_20397,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_20184]) ).
tff(c_20417,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_20397,c_20143]) ).
tff(c_20439,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20179,c_20417]) ).
tff(c_21218,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_20439,c_21182]) ).
tff(c_21238,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21218]) ).
tff(c_20641,plain,
! [X_325,Z_326] : ( multiply(inverse(X_325),multiply(X_325,Z_326)) = Z_326 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20155]) ).
tff(c_20887,plain,
! [X_330,Z_331] : ( multiply(inverse(inverse(X_330)),Z_331) = multiply(X_330,Z_331) ),
inference(superposition,[status(thm),theory(equality)],[c_20641,c_20165]) ).
tff(c_20698,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20641]) ).
tff(c_20894,plain,
! [X_330] : ( multiply(X_330,identity) = X_330 ),
inference(superposition,[status(thm),theory(equality)],[c_20887,c_20698]) ).
tff(c_20680,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20542,c_20641]) ).
tff(c_20708,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20680]) ).
tff(c_20686,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_20439,c_20641]) ).
tff(c_20709,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20686]) ).
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_20420,plain,
! [Z_5] : ( multiply(sk_c7,multiply(sk_c5,Z_5)) = multiply(sk_c6,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_20397,c_6]) ).
tff(c_20554,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c6,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_20542,c_20420]) ).
tff(c_20560,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20096,c_20397,c_20554]) ).
tff(c_20396,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_20184]) ).
tff(c_20485,plain,
! [X2_323] :
( ( multiply(X2_323,sk_c5) != sk_c6 )
| ( inverse(X2_323) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_20396]) ).
tff(c_20498,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20089,c_20485]) ).
tff(c_20511,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20074,c_20498]) ).
tff(c_20512,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_20396]) ).
tff(c_20590,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_20560,c_20560,c_20560,c_20560,c_20512]) ).
tff(c_20591,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_20590]) ).
tff(c_21156,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20894,c_20708,c_20709,c_20708,c_20591]) ).
tff(c_20398,plain,
! [Z_321] : ( multiply(sk_c6,multiply(sk_c7,Z_321)) = multiply(sk_c5,Z_321) ),
inference(superposition,[status(thm),theory(equality)],[c_20096,c_20125]) ).
tff(c_20410,plain,
multiply(sk_c6,identity) = multiply(sk_c5,sk_c3),
inference(superposition,[status(thm),theory(equality)],[c_18774,c_20398]) ).
tff(c_20565,plain,
multiply(sk_c5,sk_c3) = multiply(sk_c5,identity),
inference(demodulation,[status(thm),theory(equality)],[c_20560,c_20410]) ).
tff(c_20711,plain,
multiply(identity,sk_c3) = multiply(identity,identity),
inference(demodulation,[status(thm),theory(equality)],[c_20709,c_20709,c_20565]) ).
tff(c_20722,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_20711]) ).
tff(c_20731,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_20708,c_18769]) ).
tff(c_20781,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_20722,c_20731]) ).
tff(c_21158,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21156,c_20781]) ).
tff(c_21159,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_20590]) ).
tff(c_44552,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21237,c_21364,c_21237,c_21238,c_21364,c_21238,c_21238,c_21238,c_21159]) ).
tff(c_44554,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_44552]) ).
tff(c_20574,plain,
inverse(sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20560,c_20074]) ).
tff(c_20586,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20574,c_4]) ).
tff(c_21265,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21238,c_20586]) ).
tff(c_21244,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21238,c_20574]) ).
tff(c_21280,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21265,c_21244]) ).
tff(c_44556,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44554,c_21280]) ).
tff(c_44558,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_44552]) ).
tff(c_44560,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44558,c_21280]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP272-1 : TPTP v9.0.0. Released v2.5.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:39:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 17.79/7.03 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.93/7.12
% 17.93/7.12 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------