%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP212-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 : n021.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:34 PM UTC 2025
% Result : Unsatisfiable 18.42s 7.07s
% Output : CNFRefutation 18.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 27
% Syntax : Number of formulae : 422 ( 339 unt; 0 typ; 0 def)
% Number of atoms : 592 ( 571 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 357 ( 187 ~; 170 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 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 : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 224 ( 224 !; 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_140,axiom,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
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_68,axiom,
( ( multiply(sk_c1,sk_c2) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X5,X6,X3,X1,X2,X4] :
( ( multiply(X4,X5) != sk_c8 )
| ( inverse(X4) != X5 )
| ( multiply(X5,sk_c7) != sk_c8 )
| ( inverse(X6) != sk_c8 )
| ( multiply(X6,sk_c7) != sk_c8 )
| ( inverse(sk_c8) != sk_c7 )
| ( inverse(X1) != sk_c8 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( multiply(sk_c8,X2) != sk_c7 )
| ( multiply(X3,sk_c8) != X2 )
| ( inverse(X3) != sk_c8 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c1,sk_c2) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c1,sk_c2) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c1,sk_c2) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c1,sk_c2) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_58,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_28740,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_54,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_85,plain,
inverse(sk_c3) = sk_c8,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_89,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_28804,plain,
! [X_230,Y_231,Z_232] : ( multiply(multiply(X_230,Y_231),Z_232) = multiply(X_230,multiply(Y_231,Z_232)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_28846,plain,
! [Z_232] : ( multiply(sk_c8,multiply(sk_c3,Z_232)) = multiply(identity,Z_232) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_28804]) ).
tff(c_28887,plain,
! [Z_234] : ( multiply(sk_c8,multiply(sk_c3,Z_234)) = Z_234 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28846]) ).
tff(c_28899,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_28740,c_28887]) ).
tff(c_10,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_28745,plain,
multiply(sk_c1,sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_30,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_97,plain,
inverse(sk_c1) = sk_c2,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_101,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_97,c_4]) ).
tff(c_28843,plain,
! [Z_232] : ( multiply(sk_c2,multiply(sk_c1,Z_232)) = multiply(identity,Z_232) ),
inference(superposition,[status(thm),theory(equality)],[c_101,c_28804]) ).
tff(c_28864,plain,
! [Z_233] : ( multiply(sk_c2,multiply(sk_c1,Z_233)) = Z_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28843]) ).
tff(c_28876,plain,
multiply(sk_c2,sk_c8) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_28745,c_28864]) ).
tff(c_29809,plain,
! [Z_250] : ( multiply(sk_c1,multiply(sk_c2,Z_250)) = multiply(sk_c8,Z_250) ),
inference(superposition,[status(thm),theory(equality)],[c_28745,c_28804]) ).
tff(c_29824,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c1,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_28876,c_29809]) ).
tff(c_29834,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28899,c_28745,c_29824]) ).
tff(c_149,plain,
! [X_14,Y_15,Z_16] : ( multiply(multiply(X_14,Y_15),Z_16) = multiply(X_14,multiply(Y_15,Z_16)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_179,plain,
! [X_2,Z_16] : ( multiply(inverse(X_2),multiply(X_2,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_149]) ).
tff(c_237,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_179]) ).
tff(c_189,plain,
! [X_2,Z_16] : ( multiply(inverse(X_2),multiply(X_2,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_835,plain,
! [X_27,Z_28] : ( multiply(inverse(inverse(X_27)),Z_28) = multiply(X_27,Z_28) ),
inference(superposition,[status(thm),theory(equality)],[c_237,c_189]) ).
tff(c_873,plain,
! [X_27] : ( multiply(X_27,inverse(X_27)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_835]) ).
tff(c_291,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_237]) ).
tff(c_842,plain,
! [X_27] : ( multiply(X_27,identity) = X_27 ),
inference(superposition,[status(thm),theory(equality)],[c_835,c_291]) ).
tff(c_127,plain,
multiply(sk_c1,sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_173,plain,
! [Z_16] : ( multiply(sk_c2,multiply(sk_c1,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_101,c_149]) ).
tff(c_191,plain,
! [Z_17] : ( multiply(sk_c2,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_173]) ).
tff(c_203,plain,
multiply(sk_c2,sk_c8) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_127,c_191]) ).
tff(c_261,plain,
multiply(inverse(sk_c2),sk_c2) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_203,c_237]) ).
tff(c_298,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_261]) ).
tff(c_119,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_176,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c3,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_149]) ).
tff(c_214,plain,
! [Z_18] : ( multiply(sk_c8,multiply(sk_c3,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_176]) ).
tff(c_226,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_119,c_214]) ).
tff(c_431,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_298,c_226]) ).
tff(c_439,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_431]) ).
tff(c_304,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_298,c_226]) ).
tff(c_312,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_304]) ).
tff(c_68,plain,
! [X3_8,X1_9,X6_7,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(sk_c8) != sk_c7 )
| ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(inverse(X4_11),sk_c7) != sk_c8 )
| ( multiply(X4_11,inverse(X4_11)) != sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_303,plain,
inverse(sk_c8) != sk_c7,
inference(splitLeft,[status(thm)],[c_68]) ).
tff(c_321,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_312,c_298,c_303]) ).
tff(c_310,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_89]) ).
tff(c_398,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_310,c_189]) ).
tff(c_410,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_398]) ).
tff(c_311,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_85]) ).
tff(c_414,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_410,c_311]) ).
tff(c_417,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_321,c_414]) ).
tff(c_419,plain,
inverse(sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_430,plain,
inverse(identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_419]) ).
tff(c_459,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_439,c_430]) ).
tff(c_620,plain,
! [X_22] : ( multiply(inverse(inverse(X_22)),identity) = X_22 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_237]) ).
tff(c_626,plain,
! [X_22] : ( multiply(inverse(inverse(inverse(X_22))),X_22) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_620,c_189]) ).
tff(c_418,plain,
! [X4_11,X6_7,X1_9,X3_8] :
( ( multiply(inverse(X4_11),sk_c7) != sk_c8 )
| ( multiply(X4_11,inverse(X4_11)) != sk_c8 )
| ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_520,plain,
! [X4_11,X6_7,X1_9,X3_8] :
( ( multiply(inverse(X4_11),identity) != identity )
| ( multiply(X4_11,inverse(X4_11)) != identity )
| ( multiply(X6_7,identity) != identity )
| ( inverse(X6_7) != identity )
| ( multiply(X1_9,identity) != identity )
| ( inverse(X1_9) != identity )
| ( inverse(X3_8) != identity )
| ( multiply(X3_8,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_439,c_298,c_2,c_298,c_298,c_298,c_439,c_298,c_298,c_439,c_298,c_298,c_439,c_298,c_418]) ).
tff(c_680,plain,
! [X3_24] :
( ( inverse(X3_24) != identity )
| ( multiply(X3_24,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_520]) ).
tff(c_684,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_626,c_680]) ).
tff(c_703,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_459,c_459,c_459,c_459,c_684]) ).
tff(c_704,plain,
! [X1_9,X6_7,X4_11] :
( ( multiply(X1_9,identity) != identity )
| ( inverse(X1_9) != identity )
| ( multiply(X6_7,identity) != identity )
| ( inverse(X6_7) != identity )
| ( multiply(inverse(X4_11),identity) != identity )
| ( multiply(X4_11,inverse(X4_11)) != identity ) ),
inference(splitRight,[status(thm)],[c_520]) ).
tff(c_26859,plain,
! [X1_9,X6_7,X4_11] :
( ( identity != X1_9 )
| ( inverse(X1_9) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X4_11) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_873,c_842,c_842,c_842,c_704]) ).
tff(c_26860,plain,
! [X4_11] : ( inverse(X4_11) != identity ),
inference(splitLeft,[status(thm)],[c_26859]) ).
tff(c_26862,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26860,c_459]) ).
tff(c_26863,plain,
! [X1_9,X6_7] :
( ( identity != X1_9 )
| ( inverse(X1_9) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(splitRight,[status(thm)],[c_26859]) ).
tff(c_26865,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_26863]) ).
tff(c_26867,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26865,c_459]) ).
tff(c_27898,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_26863]) ).
tff(c_27900,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27898,c_459]) ).
tff(c_27902,plain,
multiply(sk_c1,sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_14,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_27945,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_27902,c_14]) ).
tff(c_16,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c1,sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_27954,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_27902,c_16]) ).
tff(c_18,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_27926,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_27902,c_18]) ).
tff(c_27930,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27926,c_4]) ).
tff(c_27965,plain,
! [X_212,Y_213,Z_214] : ( multiply(multiply(X_212,Y_213),Z_214) = multiply(X_212,multiply(Y_213,Z_214)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_27989,plain,
! [Z_214] : ( multiply(sk_c8,multiply(sk_c5,Z_214)) = multiply(identity,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_27930,c_27965]) ).
tff(c_28064,plain,
! [Z_217] : ( multiply(sk_c8,multiply(sk_c5,Z_217)) = Z_217 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_27989]) ).
tff(c_28076,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_27954,c_28064]) ).
tff(c_28080,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_27945,c_28076]) ).
tff(c_28007,plain,
! [Z_214] : ( multiply(sk_c8,multiply(sk_c3,Z_214)) = multiply(identity,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_27965]) ).
tff(c_28041,plain,
! [Z_216] : ( multiply(sk_c8,multiply(sk_c3,Z_216)) = Z_216 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28007]) ).
tff(c_28053,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_119,c_28041]) ).
tff(c_28103,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28080,c_28080,c_28053]) ).
tff(c_28118,plain,
inverse(sk_c3) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28080,c_85]) ).
tff(c_8,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_27918,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_27902,c_8]) ).
tff(c_27922,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_27918,c_4]) ).
tff(c_28081,plain,
! [Z_218] : ( multiply(sk_c3,multiply(sk_c7,Z_218)) = multiply(sk_c8,Z_218) ),
inference(superposition,[status(thm),theory(equality)],[c_119,c_27965]) ).
tff(c_28096,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c3,identity),
inference(superposition,[status(thm),theory(equality)],[c_27922,c_28081]) ).
tff(c_28100,plain,
multiply(sk_c3,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28053,c_28096]) ).
tff(c_28010,plain,
! [X_2,Z_214] : ( multiply(inverse(X_2),multiply(X_2,Z_214)) = multiply(identity,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_27965]) ).
tff(c_28226,plain,
! [X_220,Z_221] : ( multiply(inverse(X_220),multiply(X_220,Z_221)) = Z_221 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28010]) ).
tff(c_28244,plain,
multiply(inverse(sk_c3),sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28100,c_28226]) ).
tff(c_28296,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28103,c_28118,c_28244]) ).
tff(c_28147,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28118,c_4]) ).
tff(c_28328,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28296,c_28147]) ).
tff(c_28313,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28296,c_28118]) ).
tff(c_28337,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28328,c_28313]) ).
tff(c_28317,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28296,c_28080]) ).
tff(c_32,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_114,plain,
multiply(sk_c2,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_28001,plain,
! [Z_214] : ( multiply(sk_c2,multiply(sk_c7,Z_214)) = multiply(sk_c8,Z_214) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_27965]) ).
tff(c_28372,plain,
! [Z_222] : ( multiply(sk_c2,Z_222) = Z_222 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28317,c_2,c_28296,c_28001]) ).
tff(c_28387,plain,
sk_c1 = identity,
inference(superposition,[status(thm),theory(equality)],[c_28372,c_101]) ).
tff(c_28402,plain,
inverse(identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_28387,c_97]) ).
tff(c_28405,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_28337,c_28402]) ).
tff(c_28113,plain,
multiply(sk_c1,sk_c2) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28080,c_27902]) ).
tff(c_28309,plain,
multiply(sk_c1,sk_c2) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_28296,c_28113]) ).
tff(c_28477,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28405,c_2,c_28387,c_28309]) ).
tff(c_28479,plain,
multiply(sk_c3,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_56,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_28491,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_28479,c_56]) ).
tff(c_28495,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28491,c_4]) ).
tff(c_28550,plain,
! [X_223,Y_224,Z_225] : ( multiply(multiply(X_223,Y_224),Z_225) = multiply(X_223,multiply(Y_224,Z_225)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_28580,plain,
! [Z_225] : ( multiply(sk_c7,multiply(sk_c8,Z_225)) = multiply(identity,Z_225) ),
inference(superposition,[status(thm),theory(equality)],[c_28495,c_28550]) ).
tff(c_28649,plain,
! [Z_228] : ( multiply(sk_c7,multiply(sk_c8,Z_228)) = Z_228 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28580]) ).
tff(c_28673,plain,
multiply(sk_c7,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_89,c_28649]) ).
tff(c_28478,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_28483,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28478,c_4]) ).
tff(c_28670,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_28483,c_28649]) ).
tff(c_28721,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_28673,c_28670]) ).
tff(c_60,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_28543,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_28479,c_60]) ).
tff(c_28722,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_28721,c_28543]) ).
tff(c_28726,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28479,c_28722]) ).
tff(c_28727,plain,
inverse(sk_c8) = sk_c7,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_28732,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28727,c_4]) ).
tff(c_29848,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29834,c_28732]) ).
tff(c_29836,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_29834,c_29834,c_28899]) ).
tff(c_35324,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29848,c_29836]) ).
tff(c_28849,plain,
! [X_2,Z_232] : ( multiply(inverse(X_2),multiply(X_2,Z_232)) = multiply(identity,Z_232) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_28804]) ).
tff(c_35371,plain,
! [X_308,Z_309] : ( multiply(inverse(X_308),multiply(X_308,Z_309)) = Z_309 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28849]) ).
tff(c_28862,plain,
! [X_2,Z_232] : ( multiply(inverse(X_2),multiply(X_2,Z_232)) = Z_232 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28849]) ).
tff(c_35620,plain,
! [X_312,Z_313] : ( multiply(inverse(inverse(X_312)),Z_313) = multiply(X_312,Z_313) ),
inference(superposition,[status(thm),theory(equality)],[c_35371,c_28862]) ).
tff(c_35410,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_35371]) ).
tff(c_35630,plain,
! [X_312] : ( multiply(X_312,identity) = X_312 ),
inference(superposition,[status(thm),theory(equality)],[c_35620,c_35410]) ).
tff(c_29948,plain,
! [X_251,Z_252] : ( multiply(inverse(X_251),multiply(X_251,Z_252)) = Z_252 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28849]) ).
tff(c_30237,plain,
! [X_256,Z_257] : ( multiply(inverse(inverse(X_256)),Z_257) = multiply(X_256,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_29948,c_28862]) ).
tff(c_29990,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_29948]) ).
tff(c_30251,plain,
! [X_256] : ( multiply(X_256,identity) = X_256 ),
inference(superposition,[status(thm),theory(equality)],[c_30237,c_29990]) ).
tff(c_29894,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29848,c_29836]) ).
tff(c_28728,plain,
multiply(sk_c2,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_38,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_28784,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_28728,c_38]) ).
tff(c_28840,plain,
! [Z_232] : ( multiply(sk_c7,multiply(sk_c8,Z_232)) = multiply(identity,Z_232) ),
inference(superposition,[status(thm),theory(equality)],[c_28732,c_28804]) ).
tff(c_28913,plain,
! [Z_235] : ( multiply(sk_c7,multiply(sk_c8,Z_235)) = Z_235 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28840]) ).
tff(c_28931,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_28784,c_28913]) ).
tff(c_28951,plain,
! [Z_236] : ( multiply(sk_c1,multiply(sk_c2,Z_236)) = multiply(sk_c8,Z_236) ),
inference(superposition,[status(thm),theory(equality)],[c_28745,c_28804]) ).
tff(c_28966,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c1,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_28876,c_28951]) ).
tff(c_28976,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28899,c_28745,c_28966]) ).
tff(c_28979,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28976,c_28976,c_28899]) ).
tff(c_28996,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_28931,c_28979]) ).
tff(c_29001,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_28996,c_28976]) ).
tff(c_28925,plain,
multiply(sk_c7,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_28899,c_28913]) ).
tff(c_29098,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_29001,c_28996,c_28996,c_28925]) ).
tff(c_29116,plain,
! [X_238,Z_239] : ( multiply(inverse(X_238),multiply(X_238,Z_239)) = Z_239 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28849]) ).
tff(c_29137,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_29098,c_29116]) ).
tff(c_29175,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_29137]) ).
tff(c_28993,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_28976,c_28727]) ).
tff(c_29011,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_28996,c_28996,c_28993]) ).
tff(c_28904,plain,
! [X3_8,X1_9,X6_7,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(inverse(X4_11),sk_c7) != sk_c8 )
| ( multiply(X4_11,inverse(X4_11)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28727,c_68]) ).
tff(c_28905,plain,
! [X4_11] :
( ( multiply(inverse(X4_11),sk_c7) != sk_c8 )
| ( multiply(X4_11,inverse(X4_11)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_28904]) ).
tff(c_29028,plain,
! [X4_237] :
( ( multiply(inverse(X4_237),sk_c6) != sk_c6 )
| ( multiply(X4_237,inverse(X4_237)) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29001,c_29001,c_28996,c_28905]) ).
tff(c_29037,plain,
( ( sk_c6 != identity )
| ( multiply(sk_c6,inverse(sk_c6)) != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_29028]) ).
tff(c_29041,plain,
( ( sk_c6 != identity )
| ( multiply(sk_c6,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29011,c_29037]) ).
tff(c_29800,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_29175,c_29175,c_29041]) ).
tff(c_29801,plain,
! [X6_7,X1_9,X3_8] :
( ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_28904]) ).
tff(c_29885,plain,
! [X6_7,X1_9,X3_8] :
( ( multiply(X6_7,sk_c7) != sk_c7 )
| ( inverse(X6_7) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( inverse(X3_8) != sk_c7 )
| ( multiply(sk_c7,multiply(X3_8,sk_c7)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29834,c_29834,c_29834,c_29834,c_29834,c_29834,c_29834,c_29801]) ).
tff(c_29886,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c7 )
| ( multiply(sk_c7,multiply(X3_8,sk_c7)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_29885]) ).
tff(c_35313,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_30251,c_29894,c_29894,c_2,c_29894,c_29894,c_29886]) ).
tff(c_29850,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_29834,c_28727]) ).
tff(c_29904,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_29894,c_29894,c_29850]) ).
tff(c_35315,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35313,c_29904]) ).
tff(c_35316,plain,
! [X1_9,X6_7] :
( ( multiply(X1_9,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( multiply(X6_7,sk_c7) != sk_c7 )
| ( inverse(X6_7) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_29885]) ).
tff(c_62557,plain,
! [X1_9,X6_7] :
( ( identity != X1_9 )
| ( inverse(X1_9) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35324,c_35630,c_35324,c_35324,c_35324,c_35630,c_35324,c_35324,c_35316]) ).
tff(c_62559,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_62557]) ).
tff(c_35335,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35324,c_35324,c_29850]) ).
tff(c_62561,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62559,c_35335]) ).
tff(c_62563,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_62557]) ).
tff(c_62565,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62563,c_35335]) ).
tff(c_62567,plain,
multiply(sk_c1,sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_62604,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_62567,c_14]) ).
tff(c_62628,plain,
! [X_464,Y_465,Z_466] : ( multiply(multiply(X_464,Y_465),Z_466) = multiply(X_464,multiply(Y_465,Z_466)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_62661,plain,
! [Z_466] : ( multiply(sk_c7,multiply(sk_c8,Z_466)) = multiply(identity,Z_466) ),
inference(superposition,[status(thm),theory(equality)],[c_28732,c_62628]) ).
tff(c_63153,plain,
! [Z_477] : ( multiply(sk_c7,multiply(sk_c8,Z_477)) = Z_477 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62661]) ).
tff(c_63171,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_62604,c_63153]) ).
tff(c_63180,plain,
multiply(sk_c7,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_89,c_63153]) ).
tff(c_62580,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_62567,c_18]) ).
tff(c_62584,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_62580,c_4]) ).
tff(c_63174,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_62584,c_63153]) ).
tff(c_63240,plain,
sk_c5 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_63180,c_63174]) ).
tff(c_62619,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_62567,c_16]) ).
tff(c_63241,plain,
multiply(sk_c3,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_63240,c_62619]) ).
tff(c_62667,plain,
! [Z_466] : ( multiply(sk_c8,multiply(sk_c3,Z_466)) = multiply(identity,Z_466) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_62628]) ).
tff(c_62682,plain,
! [Z_466] : ( multiply(sk_c8,multiply(sk_c3,Z_466)) = Z_466 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62667]) ).
tff(c_63263,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_63241,c_62682]) ).
tff(c_63269,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_62604,c_63263]) ).
tff(c_62698,plain,
! [Z_468] : ( multiply(sk_c8,multiply(sk_c3,Z_468)) = Z_468 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62667]) ).
tff(c_62710,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_28740,c_62698]) ).
tff(c_63498,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_63269,c_63269,c_62710]) ).
tff(c_63508,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_63171,c_63498]) ).
tff(c_63514,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_63508,c_63508,c_63171]) ).
tff(c_63503,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63269,c_28732]) ).
tff(c_63569,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63514,c_63508,c_63508,c_63503]) ).
tff(c_63576,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_63569,c_63508]) ).
tff(c_63501,plain,
multiply(sk_c1,sk_c2) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_63269,c_62567]) ).
tff(c_63697,plain,
multiply(sk_c1,sk_c2) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_63576,c_63501]) ).
tff(c_62670,plain,
! [X_2,Z_466] : ( multiply(inverse(X_2),multiply(X_2,Z_466)) = multiply(identity,Z_466) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_62628]) ).
tff(c_62683,plain,
! [X_2,Z_466] : ( multiply(inverse(X_2),multiply(X_2,Z_466)) = Z_466 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62670]) ).
tff(c_63598,plain,
! [X_484,Z_485] : ( multiply(inverse(X_484),multiply(X_484,Z_485)) = Z_485 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_62670]) ).
tff(c_63754,plain,
! [X_487,Z_488] : ( multiply(inverse(inverse(X_487)),Z_488) = multiply(X_487,Z_488) ),
inference(superposition,[status(thm),theory(equality)],[c_62683,c_63598]) ).
tff(c_63631,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_63598]) ).
tff(c_63809,plain,
! [X_489] : ( multiply(X_489,identity) = X_489 ),
inference(superposition,[status(thm),theory(equality)],[c_63754,c_63631]) ).
tff(c_63625,plain,
multiply(inverse(sk_c2),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_101,c_63598]) ).
tff(c_63822,plain,
inverse(sk_c2) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_63809,c_63625]) ).
tff(c_63899,plain,
multiply(sk_c1,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_63822,c_4]) ).
tff(c_63905,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_63697,c_63899]) ).
tff(c_63907,plain,
multiply(sk_c3,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_63973,plain,
! [X_490,Y_491,Z_492] : ( multiply(multiply(X_490,Y_491),Z_492) = multiply(X_490,multiply(Y_491,Z_492)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_64006,plain,
! [Z_492] : ( multiply(sk_c7,multiply(sk_c8,Z_492)) = multiply(identity,Z_492) ),
inference(superposition,[status(thm),theory(equality)],[c_28732,c_63973]) ).
tff(c_64092,plain,
! [Z_496] : ( multiply(sk_c7,multiply(sk_c8,Z_496)) = Z_496 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_64006]) ).
tff(c_64122,plain,
multiply(sk_c7,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_89,c_64092]) ).
tff(c_63906,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_63912,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_63906,c_4]) ).
tff(c_64119,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_63912,c_64092]) ).
tff(c_64171,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_64122,c_64119]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_63965,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_28728,c_36]) ).
tff(c_64173,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_64171,c_63965]) ).
tff(c_64178,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_63907,c_64173]) ).
tff(c_64180,plain,
inverse(sk_c1) != sk_c2,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_26,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_64225,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_64180,c_26]) ).
tff(c_20,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_64206,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_64180,c_20]) ).
tff(c_64210,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_64206,c_4]) ).
tff(c_64254,plain,
! [X_498,Y_499,Z_500] : ( multiply(multiply(X_498,Y_499),Z_500) = multiply(X_498,multiply(Y_499,Z_500)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_64278,plain,
! [Z_500] : ( multiply(sk_c7,multiply(sk_c8,Z_500)) = multiply(identity,Z_500) ),
inference(superposition,[status(thm),theory(equality)],[c_64210,c_64254]) ).
tff(c_64304,plain,
! [Z_501] : ( multiply(sk_c7,multiply(sk_c8,Z_501)) = Z_501 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_64278]) ).
tff(c_64316,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_64225,c_64304]) ).
tff(c_64325,plain,
multiply(sk_c7,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_89,c_64304]) ).
tff(c_22,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_64194,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_64180,c_22]) ).
tff(c_64198,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_64194,c_4]) ).
tff(c_64319,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_64198,c_64304]) ).
tff(c_64649,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_64325,c_64319]) ).
tff(c_64179,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_64184,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_64179,c_4]) ).
tff(c_64322,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_64184,c_64304]) ).
tff(c_64639,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_64319,c_64322]) ).
tff(c_28,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_64236,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_64180,c_28]) ).
tff(c_64640,plain,
multiply(sk_c4,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64639,c_64236]) ).
tff(c_64692,plain,
multiply(sk_c3,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64649,c_64640]) ).
tff(c_64287,plain,
! [Z_500] : ( multiply(sk_c8,multiply(sk_c3,Z_500)) = multiply(identity,Z_500) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_64254]) ).
tff(c_64716,plain,
! [Z_508] : ( multiply(sk_c8,multiply(sk_c3,Z_508)) = Z_508 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_64287]) ).
tff(c_64734,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_64692,c_64716]) ).
tff(c_64738,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_64225,c_64734]) ).
tff(c_24,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_64231,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_64180,c_24]) ).
tff(c_64659,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_64649,c_64231]) ).
tff(c_64731,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_64659,c_64716]) ).
tff(c_64867,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64316,c_64738,c_64738,c_64731]) ).
tff(c_64844,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_64738,c_64225]) ).
tff(c_65393,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64867,c_64867,c_64844]) ).
tff(c_64290,plain,
! [X_2,Z_500] : ( multiply(inverse(X_2),multiply(X_2,Z_500)) = multiply(identity,Z_500) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_64254]) ).
tff(c_64302,plain,
! [X_2,Z_500] : ( multiply(inverse(X_2),multiply(X_2,Z_500)) = Z_500 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_64290]) ).
tff(c_65397,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_65393,c_64302]) ).
tff(c_65403,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_65397]) ).
tff(c_64870,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64867,c_64738]) ).
tff(c_65422,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_65403,c_64870]) ).
tff(c_65336,plain,
! [X_520,Z_521] : ( multiply(inverse(X_520),multiply(X_520,Z_521)) = Z_521 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_64290]) ).
tff(c_65543,plain,
! [X_524,Z_525] : ( multiply(inverse(inverse(X_524)),Z_525) = multiply(X_524,Z_525) ),
inference(superposition,[status(thm),theory(equality)],[c_64302,c_65336]) ).
tff(c_65363,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65336]) ).
tff(c_65550,plain,
! [X_524] : ( multiply(X_524,identity) = X_524 ),
inference(superposition,[status(thm),theory(equality)],[c_65543,c_65363]) ).
tff(c_64846,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_64738,c_64206]) ).
tff(c_64856,plain,
multiply(sk_c7,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_64846,c_4]) ).
tff(c_64897,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64867,c_64867,c_64856]) ).
tff(c_64924,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64897,c_64867,c_64867,c_64844]) ).
tff(c_64929,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64924,c_64870]) ).
tff(c_64945,plain,
! [X_510,Z_511] : ( multiply(inverse(X_510),multiply(X_510,Z_511)) = Z_511 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_64290]) ).
tff(c_65060,plain,
! [X_513,Z_514] : ( multiply(inverse(inverse(X_513)),Z_514) = multiply(X_513,Z_514) ),
inference(superposition,[status(thm),theory(equality)],[c_64302,c_64945]) ).
tff(c_64969,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_64945]) ).
tff(c_65067,plain,
! [X_513] : ( multiply(X_513,identity) = X_513 ),
inference(superposition,[status(thm),theory(equality)],[c_65060,c_64969]) ).
tff(c_64746,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_64738,c_64206]) ).
tff(c_64756,plain,
multiply(sk_c7,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_64746,c_4]) ).
tff(c_64791,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64756,c_64738,c_64738,c_64731]) ).
tff(c_64796,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64791,c_64738]) ).
tff(c_64357,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_64325,c_64319]) ).
tff(c_64347,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_64319,c_64322]) ).
tff(c_64348,plain,
multiply(sk_c4,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64347,c_64236]) ).
tff(c_64400,plain,
multiply(sk_c3,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64357,c_64348]) ).
tff(c_64424,plain,
! [Z_503] : ( multiply(sk_c8,multiply(sk_c3,Z_503)) = Z_503 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_64287]) ).
tff(c_64442,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_64400,c_64424]) ).
tff(c_64446,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_64225,c_64442]) ).
tff(c_64367,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_64357,c_64231]) ).
tff(c_64439,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_64367,c_64424]) ).
tff(c_64500,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64316,c_64446,c_64446,c_64439]) ).
tff(c_64507,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64500,c_64500,c_64316]) ).
tff(c_64571,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_64507,c_64302]) ).
tff(c_64577,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_64571]) ).
tff(c_64464,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_64446,c_64206]) ).
tff(c_64504,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64500,c_64500,c_64464]) ).
tff(c_64580,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64577,c_64577,c_64504]) ).
tff(c_64583,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64577,c_64500]) ).
tff(c_64505,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64500,c_64446]) ).
tff(c_64582,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64577,c_64505]) ).
tff(c_64345,plain,
! [X3_8,X1_9,X6_7,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(inverse(X4_11),sk_c7) != sk_c8 )
| ( multiply(X4_11,inverse(X4_11)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_64206,c_68]) ).
tff(c_64447,plain,
! [X4_504] :
( ( multiply(inverse(X4_504),sk_c7) != sk_c8 )
| ( multiply(X4_504,inverse(X4_504)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_64345]) ).
tff(c_64454,plain,
( ( sk_c8 != identity )
| ( multiply(sk_c7,inverse(sk_c7)) != sk_c8 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_64447]) ).
tff(c_64637,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_64580,c_64583,c_2,c_64583,c_64582,c_64582,c_64454]) ).
tff(c_64638,plain,
! [X6_7,X1_9,X3_8] :
( ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_64345]) ).
tff(c_64739,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_64638]) ).
tff(c_64809,plain,
! [X3_509] :
( ( inverse(X3_509) != identity )
| ( multiply(X3_509,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_64796,c_2,c_64796,c_64791,c_64796,c_64739]) ).
tff(c_64823,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_64809]) ).
tff(c_64795,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64791,c_64791,c_64746]) ).
tff(c_64838,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64823,c_64795]) ).
tff(c_64839,plain,
! [X1_9,X6_7] :
( ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_64638]) ).
tff(c_64877,plain,
! [X1_9,X6_7] :
( ( multiply(X1_9,sk_c6) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X6_7,sk_c6) != sk_c8 )
| ( inverse(X6_7) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_64867,c_64867,c_64839]) ).
tff(c_64878,plain,
! [X6_7] :
( ( multiply(X6_7,sk_c6) != sk_c8 )
| ( inverse(X6_7) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_64877]) ).
tff(c_65321,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_64929,c_65067,c_64929,c_64924,c_64878]) ).
tff(c_64869,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_64867,c_64867,c_64846]) ).
tff(c_64928,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_64924,c_64924,c_64869]) ).
tff(c_65323,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65321,c_64928]) ).
tff(c_65324,plain,
! [X1_9] :
( ( multiply(X1_9,sk_c6) != sk_c8 )
| ( inverse(X1_9) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_64877]) ).
tff(c_65923,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_65422,c_65550,c_65422,c_65403,c_65324]) ).
tff(c_65421,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_65403,c_65403,c_64869]) ).
tff(c_65925,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65923,c_65421]) ).
tff(c_65927,plain,
inverse(sk_c3) != sk_c8,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_50,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_65983,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_65927,c_50]) ).
tff(c_52,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_65989,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_65927,c_52]) ).
tff(c_65926,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_65931,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_65926,c_4]) ).
tff(c_66013,plain,
! [X_534,Y_535,Z_536] : ( multiply(multiply(X_534,Y_535),Z_536) = multiply(X_534,multiply(Y_535,Z_536)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_66046,plain,
! [Z_536] : ( multiply(sk_c8,multiply(sk_c5,Z_536)) = multiply(identity,Z_536) ),
inference(superposition,[status(thm),theory(equality)],[c_65931,c_66013]) ).
tff(c_66189,plain,
! [Z_541] : ( multiply(sk_c8,multiply(sk_c5,Z_541)) = Z_541 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66046]) ).
tff(c_66201,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_65989,c_66189]) ).
tff(c_66205,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_65983,c_66201]) ).
tff(c_44,plain,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_65953,plain,
inverse(sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_65927,c_44]) ).
tff(c_65957,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_65953,c_4]) ).
tff(c_66214,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66205,c_65957]) ).
tff(c_48,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_65994,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_65927,c_48]) ).
tff(c_46,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_65965,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_65927,c_46]) ).
tff(c_65969,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_65965,c_4]) ).
tff(c_66037,plain,
! [Z_536] : ( multiply(sk_c8,multiply(sk_c4,Z_536)) = multiply(identity,Z_536) ),
inference(superposition,[status(thm),theory(equality)],[c_65969,c_66013]) ).
tff(c_66063,plain,
! [Z_537] : ( multiply(sk_c8,multiply(sk_c4,Z_537)) = Z_537 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66037]) ).
tff(c_66075,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_65994,c_66063]) ).
tff(c_66207,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_66205,c_66205,c_66075]) ).
tff(c_68895,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66214,c_66207]) ).
tff(c_66049,plain,
! [X_2,Z_536] : ( multiply(inverse(X_2),multiply(X_2,Z_536)) = multiply(identity,Z_536) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_66013]) ).
tff(c_68934,plain,
! [X_578,Z_579] : ( multiply(inverse(X_578),multiply(X_578,Z_579)) = Z_579 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66049]) ).
tff(c_66061,plain,
! [X_2,Z_536] : ( multiply(inverse(X_2),multiply(X_2,Z_536)) = Z_536 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66049]) ).
tff(c_69150,plain,
! [X_583,Z_584] : ( multiply(inverse(inverse(X_583)),Z_584) = multiply(X_583,Z_584) ),
inference(superposition,[status(thm),theory(equality)],[c_68934,c_66061]) ).
tff(c_68964,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_68934]) ).
tff(c_69157,plain,
! [X_583] : ( multiply(X_583,identity) = X_583 ),
inference(superposition,[status(thm),theory(equality)],[c_69150,c_68964]) ).
tff(c_66344,plain,
! [X_543,Z_544] : ( multiply(inverse(X_543),multiply(X_543,Z_544)) = Z_544 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66049]) ).
tff(c_66560,plain,
! [X_548,Z_549] : ( multiply(inverse(inverse(X_548)),Z_549) = multiply(X_548,Z_549) ),
inference(superposition,[status(thm),theory(equality)],[c_66344,c_66061]) ).
tff(c_66374,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_66344]) ).
tff(c_66567,plain,
! [X_548] : ( multiply(X_548,identity) = X_548 ),
inference(superposition,[status(thm),theory(equality)],[c_66560,c_66374]) ).
tff(c_66305,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66214,c_66207]) ).
tff(c_66089,plain,
! [Z_538] : ( multiply(sk_c8,multiply(sk_c5,Z_538)) = Z_538 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_66046]) ).
tff(c_66101,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_65989,c_66089]) ).
tff(c_66105,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_65983,c_66101]) ).
tff(c_66107,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_66105,c_66105,c_66075]) ).
tff(c_66115,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_66105,c_65953]) ).
tff(c_66080,plain,
! [X3_8,X1_9,X6_7,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(inverse(X4_11),sk_c7) != sk_c8 )
| ( multiply(X4_11,inverse(X4_11)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_65953,c_68]) ).
tff(c_66081,plain,
! [X4_11] :
( ( multiply(inverse(X4_11),sk_c7) != sk_c8 )
| ( multiply(X4_11,inverse(X4_11)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_66080]) ).
tff(c_66166,plain,
! [X4_540] :
( ( multiply(inverse(X4_540),sk_c7) != sk_c7 )
| ( multiply(X4_540,inverse(X4_540)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_66105,c_66105,c_66081]) ).
tff(c_66168,plain,
( ( multiply(sk_c7,sk_c7) != sk_c7 )
| ( multiply(sk_c7,inverse(sk_c7)) != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_66115,c_66166]) ).
tff(c_66180,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_66107,c_66115,c_66107,c_66168]) ).
tff(c_66181,plain,
! [X6_7,X1_9,X3_8] :
( ( multiply(X6_7,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_66080]) ).
tff(c_66265,plain,
! [X6_7,X1_9,X3_8] :
( ( multiply(X6_7,sk_c7) != sk_c7 )
| ( inverse(X6_7) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( inverse(X3_8) != sk_c7 )
| ( multiply(sk_c7,multiply(X3_8,sk_c7)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_66205,c_66205,c_66205,c_66205,c_66205,c_66205,c_66205,c_66181]) ).
tff(c_66266,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c7 )
| ( multiply(sk_c7,multiply(X3_8,sk_c7)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_66265]) ).
tff(c_68853,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_66567,c_66305,c_66305,c_2,c_66305,c_66305,c_66266]) ).
tff(c_66215,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_66205,c_65953]) ).
tff(c_66320,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_66305,c_66305,c_66215]) ).
tff(c_68855,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_68853,c_66320]) ).
tff(c_68856,plain,
! [X1_9,X6_7] :
( ( multiply(X1_9,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( multiply(X6_7,sk_c7) != sk_c7 )
| ( inverse(X6_7) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_66265]) ).
tff(c_72902,plain,
! [X1_9,X6_7] :
( ( identity != X1_9 )
| ( inverse(X1_9) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_68895,c_69157,c_68895,c_68895,c_68895,c_69157,c_68895,c_68895,c_68856]) ).
tff(c_72904,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_72902]) ).
tff(c_68910,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_68895,c_68895,c_66215]) ).
tff(c_72906,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72904,c_68910]) ).
tff(c_72908,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_72902]) ).
tff(c_72910,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72908,c_68910]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP212-1 : TPTP v9.0.0. Released v2.5.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:37:28 EDT 2025
% 0.20/0.34 % CPUTime :
% 18.42/7.07 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.83/7.11
% 18.83/7.11 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------