%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP264-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 : n027.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:44 PM UTC 2025
% Result : Unsatisfiable 54.18s 41.03s
% Output : CNFRefutation 54.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 29
% Syntax : Number of formulae : 396 ( 305 unt; 0 typ; 0 def)
% Number of atoms : 588 ( 566 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 403 ( 211 ~; 192 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 213 ( 213 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > 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_c9,type,
sk_c9: $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
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_68,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( inverse(sk_c3) = sk_c9 ) ),
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_110,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c7 )
| ( inverse(sk_c3) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_179,axiom,
! [X5,X6,X3,X1,X2,X4] :
( ( multiply(X3,sk_c9) != sk_c8 )
| ( inverse(X3) != sk_c9 )
| ( multiply(X4,sk_c8) != sk_c7 )
| ( inverse(X4) != sk_c8 )
| ( multiply(X1,sk_c9) != sk_c8 )
| ( inverse(X1) != sk_c9 )
| ( multiply(X2,sk_c7) != sk_c8 )
| ( inverse(X2) != sk_c7 )
| ( multiply(sk_c8,X5) != sk_c7 )
| ( multiply(X6,sk_c8) != X5 )
| ( inverse(X6) != sk_c8 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c1,sk_c9) = sk_c8 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c7 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c3) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c3) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(c_34,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_40474,plain,
inverse(sk_c1) = sk_c9,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_40478,plain,
multiply(sk_c9,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40474,c_4]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_95,plain,
inverse(sk_c1) = sk_c9,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_117,plain,
multiply(sk_c1,sk_c9) = sk_c8,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_99,plain,
multiply(sk_c9,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_95,c_4]) ).
tff(c_139,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_160,plain,
! [Z_16] : ( multiply(sk_c9,multiply(sk_c1,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_99,c_139]) ).
tff(c_178,plain,
! [Z_17] : ( multiply(sk_c9,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_160]) ).
tff(c_190,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_117,c_178]) ).
tff(c_166,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_139]) ).
tff(c_465,plain,
! [X_25,Z_26] : ( multiply(inverse(X_25),multiply(X_25,Z_26)) = Z_26 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_166]) ).
tff(c_489,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_190,c_465]) ).
tff(c_524,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_489]) ).
tff(c_537,plain,
multiply(sk_c1,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_117]) ).
tff(c_176,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_166]) ).
tff(c_1480,plain,
! [X_43,Z_44] : ( multiply(inverse(inverse(X_43)),Z_44) = multiply(X_43,Z_44) ),
inference(superposition,[status(thm),theory(equality)],[c_176,c_465]) ).
tff(c_516,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_465]) ).
tff(c_1494,plain,
! [X_43] : ( multiply(X_43,identity) = X_43 ),
inference(superposition,[status(thm),theory(equality)],[c_1480,c_516]) ).
tff(c_906,plain,
! [X_32,Z_33] : ( multiply(inverse(inverse(X_32)),Z_33) = multiply(X_32,Z_33) ),
inference(superposition,[status(thm),theory(equality)],[c_465,c_176]) ).
tff(c_917,plain,
! [X_32] : ( multiply(X_32,identity) = X_32 ),
inference(superposition,[status(thm),theory(equality)],[c_906,c_516]) ).
tff(c_38,plain,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_109,plain,
multiply(sk_c2,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_56,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_81,plain,
inverse(sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_85,plain,
multiply(sk_c8,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_81,c_4]) ).
tff(c_163,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c2,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_139]) ).
tff(c_246,plain,
! [Z_20] : ( multiply(sk_c8,multiply(sk_c2,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_163]) ).
tff(c_258,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_109,c_246]) ).
tff(c_483,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_258,c_465]) ).
tff(c_523,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_483]) ).
tff(c_270,plain,
! [X_21,Z_22] : ( multiply(inverse(X_21),multiply(X_21,Z_22)) = Z_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_166]) ).
tff(c_294,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_190,c_270]) ).
tff(c_329,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_294]) ).
tff(c_344,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_329,c_81]) ).
tff(c_288,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_258,c_270]) ).
tff(c_328,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_288]) ).
tff(c_335,plain,
multiply(sk_c2,sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_328,c_109]) ).
tff(c_395,plain,
multiply(sk_c2,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_329,c_335]) ).
tff(c_64,plain,
! [X2_10,X3_8,X1_9,X4_11,X6_7] :
( ( inverse(X6_7) != sk_c8 )
| ( multiply(sk_c8,multiply(X6_7,sk_c8)) != sk_c7 )
| ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_225,plain,
! [X3_19] :
( ( inverse(X3_19) != sk_c9 )
| ( multiply(X3_19,sk_c9) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_64]) ).
tff(c_232,plain,
inverse(sk_c1) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_117,c_225]) ).
tff(c_244,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_95,c_232]) ).
tff(c_245,plain,
! [X4_11,X1_9,X2_10,X6_7] :
( ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c8 )
| ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(sk_c8,multiply(X6_7,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_269,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c8 )
| ( multiply(sk_c8,multiply(X6_7,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_245]) ).
tff(c_437,plain,
! [X6_24] :
( ( inverse(X6_24) != identity )
| ( multiply(X6_24,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_329,c_2,c_329,c_328,c_329,c_269]) ).
tff(c_443,plain,
inverse(sk_c2) != identity,
inference(superposition,[status(thm),theory(equality)],[c_395,c_437]) ).
tff(c_463,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_344,c_443]) ).
tff(c_464,plain,
! [X2_10,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_245]) ).
tff(c_631,plain,
! [X2_10,X1_9,X4_11] :
( ( inverse(X2_10) != identity )
| ( multiply(X2_10,identity) != identity )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X4_11) != identity )
| ( multiply(X4_11,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_524,c_523,c_524,c_524,c_524,c_523,c_523,c_464]) ).
tff(c_632,plain,
! [X4_11] :
( ( inverse(X4_11) != identity )
| ( multiply(X4_11,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_631]) ).
tff(c_1250,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_917,c_632]) ).
tff(c_538,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_85]) ).
tff(c_636,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_538,c_176]) ).
tff(c_648,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_636]) ).
tff(c_539,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_81]) ).
tff(c_653,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_648,c_539]) ).
tff(c_1252,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1250,c_653]) ).
tff(c_1253,plain,
! [X1_9,X2_10] :
( ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X2_10) != identity )
| ( multiply(X2_10,identity) != identity ) ),
inference(splitRight,[status(thm)],[c_631]) ).
tff(c_32805,plain,
! [X1_9,X2_10] :
( ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1494,c_1253]) ).
tff(c_32807,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_32805]) ).
tff(c_519,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_465]) ).
tff(c_1257,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_538,c_176]) ).
tff(c_1269,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_519,c_1257]) ).
tff(c_1274,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1269,c_539]) ).
tff(c_32809,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32807,c_1274]) ).
tff(c_32811,plain,
! [X1_207] :
( ( inverse(X1_207) != sk_c9 )
| ( multiply(X1_207,sk_c9) != identity ) ),
inference(splitRight,[status(thm)],[c_32805]) ).
tff(c_32875,plain,
inverse(sk_c1) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_537,c_32811]) ).
tff(c_32904,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_95,c_32875]) ).
tff(c_32906,plain,
multiply(sk_c1,sk_c9) != sk_c8,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_16,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_32967,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_32906,c_16]) ).
tff(c_18,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_32956,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_32906,c_18]) ).
tff(c_20,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_32919,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_32906,c_20]) ).
tff(c_32923,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_32919,c_4]) ).
tff(c_32973,plain,
! [X_208,Y_209,Z_210] : ( multiply(multiply(X_208,Y_209),Z_210) = multiply(X_208,multiply(Y_209,Z_210)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33003,plain,
! [Z_210] : ( multiply(sk_c8,multiply(sk_c5,Z_210)) = multiply(identity,Z_210) ),
inference(superposition,[status(thm),theory(equality)],[c_32923,c_32973]) ).
tff(c_33167,plain,
! [Z_217] : ( multiply(sk_c8,multiply(sk_c5,Z_217)) = Z_217 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33003]) ).
tff(c_33179,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_32956,c_33167]) ).
tff(c_33183,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_32967,c_33179]) ).
tff(c_33015,plain,
! [Z_210] : ( multiply(sk_c8,multiply(sk_c2,Z_210)) = multiply(identity,Z_210) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_32973]) ).
tff(c_33046,plain,
! [Z_212] : ( multiply(sk_c8,multiply(sk_c2,Z_212)) = Z_212 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33015]) ).
tff(c_33058,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_109,c_33046]) ).
tff(c_33187,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33183,c_33183,c_33058]) ).
tff(c_33018,plain,
! [X_2,Z_210] : ( multiply(inverse(X_2),multiply(X_2,Z_210)) = multiply(identity,Z_210) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_32973]) ).
tff(c_33267,plain,
! [X_218,Z_219] : ( multiply(inverse(X_218),multiply(X_218,Z_219)) = Z_219 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33018]) ).
tff(c_33294,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33187,c_33267]) ).
tff(c_33349,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33294]) ).
tff(c_33195,plain,
multiply(sk_c1,sk_c9) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33183,c_32906]) ).
tff(c_33359,plain,
multiply(sk_c1,sk_c9) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_33349,c_33195]) ).
tff(c_33333,plain,
multiply(inverse(sk_c9),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_99,c_33267]) ).
tff(c_32905,plain,
inverse(sk_c3) = sk_c9,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_32910,plain,
multiply(sk_c9,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_32905,c_4]) ).
tff(c_33327,plain,
multiply(inverse(sk_c9),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_32910,c_33267]) ).
tff(c_33509,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_33333,c_33327]) ).
tff(c_8,plain,
( ( multiply(sk_c3,sk_c9) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_32950,plain,
multiply(sk_c3,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_32906,c_8]) ).
tff(c_33192,plain,
multiply(sk_c3,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33183,c_32950]) ).
tff(c_33413,plain,
multiply(sk_c3,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33349,c_33192]) ).
tff(c_33510,plain,
multiply(sk_c1,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33509,c_33413]) ).
tff(c_33515,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33359,c_33510]) ).
tff(c_33517,plain,
multiply(sk_c2,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_44,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_33564,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_33517,c_44]) ).
tff(c_46,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_33586,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_33517,c_46]) ).
tff(c_48,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_33544,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_33517,c_48]) ).
tff(c_33548,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33544,c_4]) ).
tff(c_33592,plain,
! [X_220,Y_221,Z_222] : ( multiply(multiply(X_220,Y_221),Z_222) = multiply(X_220,multiply(Y_221,Z_222)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33622,plain,
! [Z_222] : ( multiply(sk_c8,multiply(sk_c5,Z_222)) = multiply(identity,Z_222) ),
inference(superposition,[status(thm),theory(equality)],[c_33548,c_33592]) ).
tff(c_33712,plain,
! [Z_226] : ( multiply(sk_c8,multiply(sk_c5,Z_226)) = Z_226 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33622]) ).
tff(c_33724,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_33586,c_33712]) ).
tff(c_33728,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33564,c_33724]) ).
tff(c_40,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_33570,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_33517,c_40]) ).
tff(c_42,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_33531,plain,
inverse(sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_33517,c_42]) ).
tff(c_33535,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33531,c_4]) ).
tff(c_33625,plain,
! [Z_222] : ( multiply(sk_c7,multiply(sk_c4,Z_222)) = multiply(identity,Z_222) ),
inference(superposition,[status(thm),theory(equality)],[c_33535,c_33592]) ).
tff(c_33689,plain,
! [Z_225] : ( multiply(sk_c7,multiply(sk_c4,Z_225)) = Z_225 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33625]) ).
tff(c_33701,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33570,c_33689]) ).
tff(c_33730,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33728,c_33701]) ).
tff(c_33637,plain,
! [X_2,Z_222] : ( multiply(inverse(X_2),multiply(X_2,Z_222)) = multiply(identity,Z_222) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_33592]) ).
tff(c_33817,plain,
! [X_228,Z_229] : ( multiply(inverse(X_228),multiply(X_228,Z_229)) = Z_229 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33637]) ).
tff(c_33838,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33730,c_33817]) ).
tff(c_33891,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33838]) ).
tff(c_33742,plain,
inverse(sk_c2) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33728,c_81]) ).
tff(c_33764,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33742,c_4]) ).
tff(c_33927,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33891,c_33764]) ).
tff(c_33740,plain,
multiply(sk_c2,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33728,c_33517]) ).
tff(c_33900,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_33891,c_33891,c_33740]) ).
tff(c_34090,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33927,c_33900]) ).
tff(c_34092,plain,
inverse(sk_c1) != sk_c9,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_24,plain,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_34104,plain,
inverse(sk_c3) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_34092,c_24]) ).
tff(c_30,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_34130,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_34092,c_30]) ).
tff(c_32,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_34137,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_34092,c_32]) ).
tff(c_34091,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_34096,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34091,c_4]) ).
tff(c_34166,plain,
! [X_231,Y_232,Z_233] : ( multiply(multiply(X_231,Y_232),Z_233) = multiply(X_231,multiply(Y_232,Z_233)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_34199,plain,
! [Z_233] : ( multiply(sk_c8,multiply(sk_c5,Z_233)) = multiply(identity,Z_233) ),
inference(superposition,[status(thm),theory(equality)],[c_34096,c_34166]) ).
tff(c_34319,plain,
! [Z_238] : ( multiply(sk_c8,multiply(sk_c5,Z_238)) = Z_238 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34199]) ).
tff(c_34331,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_34137,c_34319]) ).
tff(c_34335,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34130,c_34331]) ).
tff(c_26,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_34142,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_34092,c_26]) ).
tff(c_34438,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34335,c_34142]) ).
tff(c_28,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_34112,plain,
inverse(sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_34092,c_28]) ).
tff(c_34116,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34112,c_4]) ).
tff(c_34193,plain,
! [Z_233] : ( multiply(sk_c7,multiply(sk_c4,Z_233)) = multiply(identity,Z_233) ),
inference(superposition,[status(thm),theory(equality)],[c_34116,c_34166]) ).
tff(c_35580,plain,
! [Z_260] : ( multiply(sk_c7,multiply(sk_c4,Z_260)) = Z_260 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34193]) ).
tff(c_35592,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34438,c_35580]) ).
tff(c_34205,plain,
! [X_2,Z_233] : ( multiply(inverse(X_2),multiply(X_2,Z_233)) = multiply(identity,Z_233) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34166]) ).
tff(c_35603,plain,
! [X_261,Z_262] : ( multiply(inverse(X_261),multiply(X_261,Z_262)) = Z_262 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34205]) ).
tff(c_35621,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_35592,c_35603]) ).
tff(c_35679,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_35621]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c9) = sk_c8 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_34153,plain,
multiply(sk_c3,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_34092,c_22]) ).
tff(c_34437,plain,
multiply(sk_c3,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34335,c_34153]) ).
tff(c_35697,plain,
multiply(sk_c3,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35679,c_34437]) ).
tff(c_34217,plain,
! [X_2,Z_233] : ( multiply(inverse(X_2),multiply(X_2,Z_233)) = Z_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34205]) ).
tff(c_36054,plain,
! [X_267,Z_268] : ( multiply(inverse(inverse(X_267)),Z_268) = multiply(X_267,Z_268) ),
inference(superposition,[status(thm),theory(equality)],[c_34217,c_35603]) ).
tff(c_35672,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_35603]) ).
tff(c_36064,plain,
! [X_267] : ( multiply(X_267,identity) = X_267 ),
inference(superposition,[status(thm),theory(equality)],[c_36054,c_35672]) ).
tff(c_34583,plain,
! [X_243,Z_244] : ( multiply(inverse(X_243),multiply(X_243,Z_244)) = Z_244 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34205]) ).
tff(c_35020,plain,
! [X_249,Z_250] : ( multiply(inverse(inverse(X_249)),Z_250) = multiply(X_249,Z_250) ),
inference(superposition,[status(thm),theory(equality)],[c_34583,c_34217]) ).
tff(c_34643,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34583]) ).
tff(c_35030,plain,
! [X_249] : ( multiply(X_249,identity) = X_249 ),
inference(superposition,[status(thm),theory(equality)],[c_35020,c_34643]) ).
tff(c_34108,plain,
multiply(sk_c9,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34104,c_4]) ).
tff(c_34196,plain,
! [Z_233] : ( multiply(sk_c9,multiply(sk_c3,Z_233)) = multiply(identity,Z_233) ),
inference(superposition,[status(thm),theory(equality)],[c_34108,c_34166]) ).
tff(c_34567,plain,
! [Z_242] : ( multiply(sk_c9,multiply(sk_c3,Z_242)) = Z_242 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34196]) ).
tff(c_34579,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_34437,c_34567]) ).
tff(c_34665,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34579,c_34217]) ).
tff(c_34671,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_34665]) ).
tff(c_34342,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34335,c_34130]) ).
tff(c_34344,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34335,c_34091]) ).
tff(c_34341,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34335,c_34137]) ).
tff(c_34233,plain,
! [Z_235] : ( multiply(sk_c8,multiply(sk_c5,Z_235)) = Z_235 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34199]) ).
tff(c_34245,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_34137,c_34233]) ).
tff(c_34249,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34130,c_34245]) ).
tff(c_34252,plain,
multiply(sk_c3,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34249,c_34153]) ).
tff(c_34219,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_64]) ).
tff(c_34264,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34249,c_34219]) ).
tff(c_34295,plain,
inverse(sk_c3) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_34252,c_34264]) ).
tff(c_34304,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34104,c_34295]) ).
tff(c_34305,plain,
! [X4_11,X1_9,X2_10,X6_7] :
( ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c8 )
| ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(sk_c8,multiply(X6_7,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_34336,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c8 )
| ( multiply(sk_c8,multiply(X6_7,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_34305]) ).
tff(c_34403,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X6_7,sk_c7)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34335,c_34335,c_34335,c_34336]) ).
tff(c_34425,plain,
( ( inverse(sk_c5) != sk_c7 )
| ( multiply(sk_c7,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_34341,c_34403]) ).
tff(c_34433,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34342,c_34344,c_34425]) ).
tff(c_34434,plain,
! [X2_10,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_34305]) ).
tff(c_34500,plain,
! [X2_10,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c7 )
| ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34335,c_34335,c_34335,c_34335,c_34434]) ).
tff(c_34501,plain,
! [X4_11] :
( ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_34500]) ).
tff(c_35544,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_35030,c_34671,c_34671,c_34671,c_34501]) ).
tff(c_34442,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34335,c_34091]) ).
tff(c_34452,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34442,c_4]) ).
tff(c_34677,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34671,c_34452]) ).
tff(c_34799,plain,
sk_c5 = identity,
inference(superposition,[status(thm),theory(equality)],[c_34677,c_2]) ).
tff(c_34678,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34671,c_34442]) ).
tff(c_34810,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34799,c_34678]) ).
tff(c_35546,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35544,c_34810]) ).
tff(c_35547,plain,
! [X1_9,X2_10] :
( ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c7 )
| ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_34500]) ).
tff(c_40402,plain,
! [X1_9,X2_10] :
( ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_36064,c_35679,c_35679,c_35679,c_35679,c_35547]) ).
tff(c_40404,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_40402]) ).
tff(c_35703,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35679,c_34116]) ).
tff(c_35834,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_35703,c_2]) ).
tff(c_35704,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35679,c_34112]) ).
tff(c_35845,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35834,c_35704]) ).
tff(c_40406,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_40404,c_35845]) ).
tff(c_40408,plain,
! [X1_314] :
( ( inverse(X1_314) != sk_c9 )
| ( multiply(X1_314,sk_c9) != identity ) ),
inference(splitRight,[status(thm)],[c_40402]) ).
tff(c_40437,plain,
inverse(sk_c3) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_35697,c_40408]) ).
tff(c_40459,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34104,c_40437]) ).
tff(c_40461,plain,
inverse(sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_52,plain,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_40486,plain,
inverse(sk_c3) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_40461,c_52]) ).
tff(c_58,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_40514,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_40461,c_58]) ).
tff(c_60,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_40523,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_40461,c_60]) ).
tff(c_62,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_40499,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_40461,c_62]) ).
tff(c_40503,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40499,c_4]) ).
tff(c_40549,plain,
! [X_315,Y_316,Z_317] : ( multiply(multiply(X_315,Y_316),Z_317) = multiply(X_315,multiply(Y_316,Z_317)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_40576,plain,
! [Z_317] : ( multiply(sk_c8,multiply(sk_c5,Z_317)) = multiply(identity,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_40503,c_40549]) ).
tff(c_40602,plain,
! [Z_318] : ( multiply(sk_c8,multiply(sk_c5,Z_318)) = Z_318 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40576]) ).
tff(c_40614,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_40523,c_40602]) ).
tff(c_40618,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_40514,c_40614]) ).
tff(c_50,plain,
( ( multiply(sk_c3,sk_c9) = sk_c8 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_40528,plain,
multiply(sk_c3,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_40461,c_50]) ).
tff(c_40621,plain,
multiply(sk_c3,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_40618,c_40528]) ).
tff(c_40588,plain,
! [X_2,Z_317] : ( multiply(inverse(X_2),multiply(X_2,Z_317)) = multiply(identity,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_40549]) ).
tff(c_40600,plain,
! [X_2,Z_317] : ( multiply(inverse(X_2),multiply(X_2,Z_317)) = Z_317 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40588]) ).
tff(c_41951,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_40621,c_40600]) ).
tff(c_41957,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_40486,c_41951]) ).
tff(c_41998,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_41957,c_40600]) ).
tff(c_42004,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_41998]) ).
tff(c_42045,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42004,c_40618]) ).
tff(c_40567,plain,
! [Z_317] : ( multiply(sk_c3,multiply(sk_c9,Z_317)) = multiply(sk_c8,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_40528,c_40549]) ).
tff(c_42106,plain,
! [Z_344] : ( multiply(sk_c3,multiply(sk_c9,Z_344)) = Z_344 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42045,c_40567]) ).
tff(c_42124,plain,
multiply(sk_c3,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_40478,c_42106]) ).
tff(c_40490,plain,
multiply(sk_c9,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40486,c_4]) ).
tff(c_42121,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_40490,c_42106]) ).
tff(c_42235,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_42124,c_42121]) ).
tff(c_42041,plain,
multiply(sk_c3,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42004,c_40621]) ).
tff(c_42275,plain,
multiply(sk_c1,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42235,c_42041]) ).
tff(c_41871,plain,
! [X_341,Z_342] : ( multiply(inverse(X_341),multiply(X_341,Z_342)) = Z_342 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40588]) ).
tff(c_42399,plain,
! [X_348,Z_349] : ( multiply(inverse(inverse(X_348)),Z_349) = multiply(X_348,Z_349) ),
inference(superposition,[status(thm),theory(equality)],[c_41871,c_40600]) ).
tff(c_41913,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_41871]) ).
tff(c_42406,plain,
! [X_348] : ( multiply(X_348,identity) = X_348 ),
inference(superposition,[status(thm),theory(equality)],[c_42399,c_41913]) ).
tff(c_54,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_40536,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_40461,c_54]) ).
tff(c_40620,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_40618,c_40536]) ).
tff(c_40460,plain,
inverse(sk_c4) = sk_c7,
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_40465,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_40460,c_4]) ).
tff(c_40585,plain,
! [Z_317] : ( multiply(sk_c7,multiply(sk_c4,Z_317)) = multiply(identity,Z_317) ),
inference(superposition,[status(thm),theory(equality)],[c_40465,c_40549]) ).
tff(c_40677,plain,
! [Z_319] : ( multiply(sk_c7,multiply(sk_c4,Z_319)) = Z_319 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40585]) ).
tff(c_40689,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40620,c_40677]) ).
tff(c_40774,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40689,c_40600]) ).
tff(c_40780,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40774]) ).
tff(c_40789,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40780,c_40618]) ).
tff(c_41005,plain,
! [Z_324] : ( multiply(sk_c3,multiply(sk_c9,Z_324)) = Z_324 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40789,c_40567]) ).
tff(c_41026,plain,
multiply(sk_c3,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_40478,c_41005]) ).
tff(c_41023,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_40490,c_41005]) ).
tff(c_41044,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_41026,c_41023]) ).
tff(c_40784,plain,
multiply(sk_c3,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40780,c_40621]) ).
tff(c_41060,plain,
multiply(sk_c1,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_41044,c_40784]) ).
tff(c_40631,plain,
! [X2_10,X3_8,X1_9,X4_11,X6_7] :
( ( inverse(X6_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X6_7,sk_c7)) != sk_c7 )
| ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c7 )
| ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c7 )
| ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_40618,c_40618,c_40618,c_40618,c_40618,c_40618,c_40618,c_40618,c_64]) ).
tff(c_40632,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_40631]) ).
tff(c_41838,plain,
! [X3_340] :
( ( inverse(X3_340) != sk_c9 )
| ( multiply(X3_340,sk_c9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_40780,c_40632]) ).
tff(c_41845,plain,
inverse(sk_c1) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_41060,c_41838]) ).
tff(c_41862,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40474,c_41845]) ).
tff(c_41863,plain,
! [X4_11,X1_9,X2_10,X6_7] :
( ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c7 )
| ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c7 )
| ( inverse(X6_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X6_7,sk_c7)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_40631]) ).
tff(c_48538,plain,
! [X4_11,X1_9,X2_10,X6_7] :
( ( inverse(X4_11) != identity )
| ( identity != X4_11 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 )
| ( inverse(X6_7) != identity )
| ( identity != X6_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42406,c_42004,c_42004,c_2,c_42004,c_42004,c_42406,c_42004,c_42004,c_42004,c_42004,c_42406,c_42004,c_42004,c_42004,c_41863]) ).
tff(c_48540,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_48538]) ).
tff(c_40625,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_40618,c_40499]) ).
tff(c_42043,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42004,c_40625]) ).
tff(c_42064,plain,
multiply(identity,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42043,c_4]) ).
tff(c_42071,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_42064,c_40600]) ).
tff(c_42083,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42071]) ).
tff(c_42087,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42083,c_42043]) ).
tff(c_48542,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48540,c_42087]) ).
tff(c_48543,plain,
! [X2_10,X1_9,X4_11] :
( ( inverse(X2_10) != identity )
| ( identity != X2_10 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(splitRight,[status(thm)],[c_48538]) ).
tff(c_271019,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_48543]) ).
tff(c_271021,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_271019,c_42087]) ).
tff(c_271022,plain,
! [X1_9,X2_10] :
( ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(splitRight,[status(thm)],[c_48543]) ).
tff(c_271024,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_271022]) ).
tff(c_271026,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_271024,c_42087]) ).
tff(c_271029,plain,
! [X1_888] :
( ( inverse(X1_888) != sk_c9 )
| ( multiply(X1_888,sk_c9) != identity ) ),
inference(splitRight,[status(thm)],[c_271022]) ).
tff(c_271127,plain,
inverse(sk_c1) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_42275,c_271029]) ).
tff(c_271164,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40474,c_271127]) ).
tff(c_271166,plain,
inverse(sk_c1) != sk_c9,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_271180,plain,
inverse(sk_c3) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_271166,c_24]) ).
tff(c_271195,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_271166,c_30]) ).
tff(c_271204,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_40461,c_60]) ).
tff(c_271165,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_271170,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_271165,c_4]) ).
tff(c_271236,plain,
! [X_889,Y_890,Z_891] : ( multiply(multiply(X_889,Y_890),Z_891) = multiply(X_889,multiply(Y_890,Z_891)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_271266,plain,
! [Z_891] : ( multiply(sk_c8,multiply(sk_c5,Z_891)) = multiply(identity,Z_891) ),
inference(superposition,[status(thm),theory(equality)],[c_271170,c_271236]) ).
tff(c_271435,plain,
! [Z_896] : ( multiply(sk_c8,multiply(sk_c5,Z_896)) = Z_896 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_271266]) ).
tff(c_271447,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_271204,c_271435]) ).
tff(c_271451,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_271195,c_271447]) ).
tff(c_271217,plain,
multiply(sk_c3,sk_c9) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_40461,c_50]) ).
tff(c_271184,plain,
multiply(sk_c9,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_271180,c_4]) ).
tff(c_271263,plain,
! [Z_891] : ( multiply(sk_c9,multiply(sk_c3,Z_891)) = multiply(identity,Z_891) ),
inference(superposition,[status(thm),theory(equality)],[c_271184,c_271236]) ).
tff(c_271285,plain,
! [Z_892] : ( multiply(sk_c9,multiply(sk_c3,Z_892)) = Z_892 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_271263]) ).
tff(c_271297,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_271217,c_271285]) ).
tff(c_271454,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(demodulation,[status(thm),theory(equality)],[c_271451,c_271297]) ).
tff(c_271272,plain,
! [X_2,Z_891] : ( multiply(inverse(X_2),multiply(X_2,Z_891)) = multiply(identity,Z_891) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_271236]) ).
tff(c_274223,plain,
! [X_934,Z_935] : ( multiply(inverse(X_934),multiply(X_934,Z_935)) = Z_935 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_271272]) ).
tff(c_274247,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_271454,c_274223]) ).
tff(c_274292,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_274247]) ).
tff(c_271455,plain,
multiply(sk_c3,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_271451,c_271217]) ).
tff(c_274298,plain,
multiply(sk_c3,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_274292,c_271455]) ).
tff(c_271283,plain,
! [X_2,Z_891] : ( multiply(inverse(X_2),multiply(X_2,Z_891)) = Z_891 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_271272]) ).
tff(c_274596,plain,
! [X_940,Z_941] : ( multiply(inverse(inverse(X_940)),Z_941) = multiply(X_940,Z_941) ),
inference(superposition,[status(thm),theory(equality)],[c_274223,c_271283]) ).
tff(c_274283,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_274223]) ).
tff(c_274603,plain,
! [X_940] : ( multiply(X_940,identity) = X_940 ),
inference(superposition,[status(thm),theory(equality)],[c_274596,c_274283]) ).
tff(c_271602,plain,
! [X_899,Z_900] : ( multiply(inverse(X_899),multiply(X_899,Z_900)) = Z_900 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_271272]) ).
tff(c_271975,plain,
! [X_905,Z_906] : ( multiply(inverse(inverse(X_905)),Z_906) = multiply(X_905,Z_906) ),
inference(superposition,[status(thm),theory(equality)],[c_271602,c_271283]) ).
tff(c_271662,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_271602]) ).
tff(c_271982,plain,
! [X_905] : ( multiply(X_905,identity) = X_905 ),
inference(superposition,[status(thm),theory(equality)],[c_271975,c_271662]) ).
tff(c_271626,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_271454,c_271602]) ).
tff(c_271671,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_271626]) ).
tff(c_271332,plain,
! [Z_894] : ( multiply(sk_c8,multiply(sk_c5,Z_894)) = Z_894 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_271266]) ).
tff(c_271344,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_271204,c_271332]) ).
tff(c_271348,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_271195,c_271344]) ).
tff(c_271352,plain,
multiply(sk_c3,sk_c9) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_271348,c_271217]) ).
tff(c_271331,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_64]) ).
tff(c_271404,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c9 )
| ( multiply(X3_8,sk_c9) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_271348,c_271331]) ).
tff(c_271421,plain,
inverse(sk_c3) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_271352,c_271404]) ).
tff(c_271433,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_271180,c_271421]) ).
tff(c_271434,plain,
! [X4_11,X1_9,X2_10,X6_7] :
( ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c8 )
| ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( multiply(sk_c8,multiply(X6_7,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_271528,plain,
! [X4_11,X1_9,X2_10,X6_7] :
( ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c7 )
| ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c7 )
| ( inverse(X6_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X6_7,sk_c7)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_271451,c_271451,c_271451,c_271451,c_271451,c_271451,c_271451,c_271434]) ).
tff(c_271529,plain,
! [X6_7] :
( ( inverse(X6_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X6_7,sk_c7)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_271528]) ).
tff(c_274147,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_271982,c_271671,c_271671,c_2,c_271671,c_271671,c_271529]) ).
tff(c_271459,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_271451,c_271170]) ).
tff(c_271680,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_271671,c_271459]) ).
tff(c_271762,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_271680,c_271283]) ).
tff(c_271774,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_271762]) ).
tff(c_271460,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_271451,c_271165]) ).
tff(c_271683,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_271671,c_271460]) ).
tff(c_271797,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_271774,c_271683]) ).
tff(c_274149,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_274147,c_271797]) ).
tff(c_274150,plain,
! [X2_10,X1_9,X4_11] :
( ( inverse(X2_10) != sk_c7 )
| ( multiply(X2_10,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != sk_c7 )
| ( inverse(X4_11) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_271528]) ).
tff(c_281558,plain,
! [X2_10,X1_9,X4_11] :
( ( inverse(X2_10) != identity )
| ( identity != X2_10 )
| ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X4_11) != identity )
| ( identity != X4_11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_274603,c_274292,c_274292,c_274292,c_274292,c_274603,c_274292,c_274292,c_274292,c_274150]) ).
tff(c_281560,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_281558]) ).
tff(c_274301,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_274292,c_271459]) ).
tff(c_274383,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_274301,c_271283]) ).
tff(c_274395,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_274383]) ).
tff(c_274304,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_274292,c_271460]) ).
tff(c_274418,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_274395,c_274304]) ).
tff(c_281562,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_281560,c_274418]) ).
tff(c_281563,plain,
! [X1_9,X2_10] :
( ( inverse(X1_9) != sk_c9 )
| ( multiply(X1_9,sk_c9) != identity )
| ( inverse(X2_10) != identity )
| ( identity != X2_10 ) ),
inference(splitRight,[status(thm)],[c_281558]) ).
tff(c_285338,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_281563]) ).
tff(c_285340,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_285338,c_274418]) ).
tff(c_285342,plain,
! [X1_1032] :
( ( inverse(X1_1032) != sk_c9 )
| ( multiply(X1_1032,sk_c9) != identity ) ),
inference(splitRight,[status(thm)],[c_281563]) ).
tff(c_285378,plain,
inverse(sk_c3) != sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_274298,c_285342]) ).
tff(c_285401,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_271180,c_285378]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP264-1 : TPTP v9.0.0. Released v2.5.0.
% 0.11/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.33 % Computer : n027.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:39:36 EDT 2025
% 0.13/0.34 % CPUTime :
% 54.18/41.03 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 54.18/41.08
% 54.18/41.08 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------