%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP309-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:25:53 PM UTC 2025
% Result : Unsatisfiable 17.57s 6.03s
% Output : CNFRefutation 17.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 21
% Syntax : Number of formulae : 408 ( 356 unt; 0 typ; 0 def)
% Number of atoms : 537 ( 518 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 282 ( 153 ~; 129 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 194 ( 194 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_117,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_105,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c2 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_99,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_87,axiom,
multiply(sk_c5,sk_c6) = sk_c7,
file(unknown,unknown) ).
tff(f_111,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c2 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_153,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c7,sk_c6) != sk_c5 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(sk_c5,sk_c6) != sk_c7 )
| ( multiply(sk_c7,X3) != sk_c6 )
| ( multiply(X4,sk_c7) != X3 )
| ( inverse(X4) != sk_c7 )
| ( multiply(X1,sk_c7) != sk_c6 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X2,sk_c6) != sk_c5 )
| ( inverse(X2) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_108,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c2 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_93,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_90,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_96,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_120,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_123,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_114,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_24591,plain,
! [X_298,Y_299,Z_300] : ( multiply(multiply(X_298,Y_299),Z_300) = multiply(X_298,multiply(Y_299,Z_300)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_24621,plain,
! [X_2,Z_300] : ( multiply(inverse(X_2),multiply(X_2,Z_300)) = multiply(identity,Z_300) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_24591]) ).
tff(c_24635,plain,
! [X_2,Z_300] : ( multiply(inverse(X_2),multiply(X_2,Z_300)) = Z_300 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24621]) ).
tff(c_25553,plain,
! [X_322,Z_323] : ( multiply(inverse(X_322),multiply(X_322,Z_323)) = Z_323 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24621]) ).
tff(c_25799,plain,
! [X_327,Z_328] : ( multiply(inverse(inverse(X_327)),Z_328) = multiply(X_327,Z_328) ),
inference(superposition,[status(thm),theory(equality)],[c_24635,c_25553]) ).
tff(c_25595,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_25553]) ).
tff(c_25810,plain,
! [X_327] : ( multiply(X_327,identity) = X_327 ),
inference(superposition,[status(thm),theory(equality)],[c_25799,c_25595]) ).
tff(c_9027,plain,
! [X_135,Y_136,Z_137] : ( multiply(multiply(X_135,Y_136),Z_137) = multiply(X_135,multiply(Y_136,Z_137)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9060,plain,
! [X_2,Z_137] : ( multiply(inverse(X_2),multiply(X_2,Z_137)) = multiply(identity,Z_137) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9027]) ).
tff(c_9075,plain,
! [X_2,Z_137] : ( multiply(inverse(X_2),multiply(X_2,Z_137)) = Z_137 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9060]) ).
tff(c_10047,plain,
! [X_160,Z_161] : ( multiply(inverse(X_160),multiply(X_160,Z_161)) = Z_161 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9060]) ).
tff(c_10273,plain,
! [X_163,Z_164] : ( multiply(inverse(inverse(X_163)),Z_164) = multiply(X_163,Z_164) ),
inference(superposition,[status(thm),theory(equality)],[c_9075,c_10047]) ).
tff(c_10098,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_10047]) ).
tff(c_10280,plain,
! [X_163] : ( multiply(X_163,identity) = X_163 ),
inference(superposition,[status(thm),theory(equality)],[c_10273,c_10098]) ).
tff(c_44,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_73,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_77,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_73,c_4]) ).
tff(c_18,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_81,plain,
inverse(sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_85,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_81,c_4]) ).
tff(c_9054,plain,
! [Z_137] : ( multiply(sk_c5,multiply(sk_c7,Z_137)) = multiply(identity,Z_137) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_9027]) ).
tff(c_9077,plain,
! [Z_138] : ( multiply(sk_c5,multiply(sk_c7,Z_138)) = Z_138 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9054]) ).
tff(c_9092,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_77,c_9077]) ).
tff(c_8561,plain,
! [X_125,Y_126,Z_127] : ( multiply(multiply(X_125,Y_126),Z_127) = multiply(X_125,multiply(Y_126,Z_127)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_8591,plain,
! [Z_127] : ( multiply(sk_c5,multiply(sk_c7,Z_127)) = multiply(identity,Z_127) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_8561]) ).
tff(c_8614,plain,
! [Z_128] : ( multiply(sk_c5,multiply(sk_c7,Z_128)) = Z_128 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8591]) ).
tff(c_8629,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_77,c_8614]) ).
tff(c_36,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_8117,plain,
multiply(sk_c1,sk_c7) = sk_c2,
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_8597,plain,
! [X_2,Z_127] : ( multiply(inverse(X_2),multiply(X_2,Z_127)) = multiply(identity,Z_127) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_8561]) ).
tff(c_8758,plain,
! [X_131,Z_132] : ( multiply(inverse(X_131),multiply(X_131,Z_132)) = Z_132 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8597]) ).
tff(c_8806,plain,
multiply(inverse(sk_c1),sk_c2) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_8117,c_8758]) ).
tff(c_8831,plain,
multiply(sk_c7,sk_c2) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_73,c_8806]) ).
tff(c_8612,plain,
! [X_2,Z_127] : ( multiply(inverse(X_2),multiply(X_2,Z_127)) = Z_127 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8597]) ).
tff(c_8840,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_8831,c_8612]) ).
tff(c_8849,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_85,c_81,c_8840]) ).
tff(c_127,plain,
! [X_12,Y_13,Z_14] : ( multiply(multiply(X_12,Y_13),Z_14) = multiply(X_12,multiply(Y_13,Z_14)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_157,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_127]) ).
tff(c_417,plain,
! [X_18,Z_19] : ( multiply(inverse(X_18),multiply(X_18,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_157]) ).
tff(c_170,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_157]) ).
tff(c_674,plain,
! [X_23,Z_24] : ( multiply(inverse(inverse(X_23)),Z_24) = multiply(X_23,Z_24) ),
inference(superposition,[status(thm),theory(equality)],[c_417,c_170]) ).
tff(c_447,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_417]) ).
tff(c_685,plain,
! [X_23] : ( multiply(X_23,identity) = X_23 ),
inference(superposition,[status(thm),theory(equality)],[c_674,c_447]) ).
tff(c_32,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_99,plain,
multiply(sk_c7,sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_151,plain,
! [Z_14] : ( multiply(sk_c5,multiply(sk_c7,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_127]) ).
tff(c_172,plain,
! [Z_15] : ( multiply(sk_c5,multiply(sk_c7,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_151]) ).
tff(c_187,plain,
multiply(sk_c5,sk_c6) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_99,c_172]) ).
tff(c_24,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_201,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_187,c_24]) ).
tff(c_213,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_201,c_85]) ).
tff(c_212,plain,
multiply(sk_c2,sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_201,c_99]) ).
tff(c_216,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_201,c_73]) ).
tff(c_40,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_106,plain,
multiply(sk_c1,sk_c7) = sk_c2,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_211,plain,
multiply(sk_c1,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_201,c_106]) ).
tff(c_512,plain,
multiply(inverse(sk_c1),sk_c2) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_211,c_170]) ).
tff(c_518,plain,
sk_c6 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_212,c_216,c_512]) ).
tff(c_522,plain,
multiply(sk_c5,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_518,c_187]) ).
tff(c_524,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_213,c_522]) ).
tff(c_215,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_201,c_81]) ).
tff(c_533,plain,
inverse(identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_215]) ).
tff(c_460,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_216,c_4]) ).
tff(c_576,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_524,c_460]) ).
tff(c_532,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_216]) ).
tff(c_582,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_533,c_576,c_532]) ).
tff(c_529,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_518]) ).
tff(c_583,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_582,c_533]) ).
tff(c_226,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_215,c_4]) ).
tff(c_276,plain,
! [X_16,Z_17] : ( multiply(inverse(X_16),multiply(X_16,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_157]) ).
tff(c_294,plain,
multiply(inverse(sk_c1),sk_c2) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_211,c_276]) ).
tff(c_331,plain,
sk_c6 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_212,c_216,c_294]) ).
tff(c_336,plain,
multiply(sk_c5,sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_331,c_187]) ).
tff(c_338,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_226,c_336]) ).
tff(c_348,plain,
inverse(identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_338,c_215]) ).
tff(c_233,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_216,c_4]) ).
tff(c_358,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_338,c_233]) ).
tff(c_347,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_338,c_216]) ).
tff(c_379,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_348,c_358,c_347]) ).
tff(c_50,plain,
! [X2_9,X1_8,X4_7] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( multiply(sk_c5,sk_c6) != sk_c7 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_52,plain,
! [X2_9,X1_8,X4_7] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_50]) ).
tff(c_221,plain,
! [X2_9,X1_8,X4_7] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c2 )
| ( multiply(X1_8,sk_c2) != sk_c6 )
| ( inverse(X4_7) != sk_c2 )
| ( multiply(sk_c2,multiply(X4_7,sk_c2)) != sk_c6 )
| ( inverse(sk_c2) != sk_c5 )
| ( multiply(sk_c2,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_201,c_201,c_201,c_201,c_201,c_201,c_201,c_52]) ).
tff(c_222,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_221]) ).
tff(c_335,plain,
multiply(sk_c2,sk_c2) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_331,c_222]) ).
tff(c_407,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_379,c_338,c_2,c_338,c_335]) ).
tff(c_408,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(sk_c2) != sk_c5 )
| ( inverse(X4_7) != sk_c2 )
| ( multiply(sk_c2,multiply(X4_7,sk_c2)) != sk_c6 )
| ( inverse(X1_8) != sk_c2 )
| ( multiply(X1_8,sk_c2) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_221]) ).
tff(c_7605,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_685,c_582,c_529,c_529,c_685,c_529,c_524,c_524,c_685,c_529,c_524,c_2,c_524,c_524,c_583,c_582,c_524,c_408]) ).
tff(c_7607,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_7605]) ).
tff(c_7609,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7607,c_583]) ).
tff(c_7610,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 ) ),
inference(splitRight,[status(thm)],[c_7605]) ).
tff(c_7612,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_7610]) ).
tff(c_7614,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7612,c_583]) ).
tff(c_7617,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_7610]) ).
tff(c_7619,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7617,c_583]) ).
tff(c_7620,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_7621,plain,
multiply(sk_c1,sk_c7) != sk_c2,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_38,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_7662,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_7621,c_38]) ).
tff(c_7668,plain,
! [X_106,Y_107,Z_108] : ( multiply(multiply(X_106,Y_107),Z_108) = multiply(X_106,multiply(Y_107,Z_108)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_7707,plain,
! [X_2,Z_108] : ( multiply(inverse(X_2),multiply(X_2,Z_108)) = multiply(identity,Z_108) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_7668]) ).
tff(c_7868,plain,
! [X_112,Z_113] : ( multiply(inverse(X_112),multiply(X_112,Z_113)) = Z_113 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7707]) ).
tff(c_7916,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_7662,c_7868]) ).
tff(c_7934,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_7620,c_7916]) ).
tff(c_7722,plain,
! [X_2,Z_108] : ( multiply(inverse(X_2),multiply(X_2,Z_108)) = Z_108 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7707]) ).
tff(c_7945,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_7934,c_7722]) ).
tff(c_7951,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_7945]) ).
tff(c_7701,plain,
! [Z_108] : ( multiply(sk_c5,multiply(sk_c7,Z_108)) = multiply(identity,Z_108) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_7668]) ).
tff(c_7753,plain,
! [Z_111] : ( multiply(sk_c5,multiply(sk_c7,Z_111)) = Z_111 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7701]) ).
tff(c_7777,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_77,c_7753]) ).
tff(c_7954,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_7951,c_7777]) ).
tff(c_7961,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7954]) ).
tff(c_7774,plain,
multiply(sk_c5,sk_c6) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_99,c_7753]) ).
tff(c_7788,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_7774,c_24]) ).
tff(c_7803,plain,
multiply(sk_c1,sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_7788,c_7621]) ).
tff(c_8098,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7961,c_7803]) ).
tff(c_8100,plain,
multiply(sk_c7,sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_28,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_8122,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_8100,c_28]) ).
tff(c_8126,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8122,c_4]) ).
tff(c_8626,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_8126,c_8614]) ).
tff(c_8658,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8629,c_8626]) ).
tff(c_8154,plain,
! [X_115,Y_116,Z_117] : ( multiply(multiply(X_115,Y_116),Z_117) = multiply(X_115,multiply(Y_116,Z_117)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_8187,plain,
! [Z_117] : ( multiply(sk_c5,multiply(sk_c7,Z_117)) = multiply(identity,Z_117) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_8154]) ).
tff(c_8250,plain,
! [Z_120] : ( multiply(sk_c5,multiply(sk_c7,Z_120)) = Z_120 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8187]) ).
tff(c_8274,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_77,c_8250]) ).
tff(c_8,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_8142,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_8271,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_8126,c_8250]) ).
tff(c_8296,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8274,c_8271]) ).
tff(c_26,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_8148,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_8100,c_26]) ).
tff(c_8297,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8296,c_8148]) ).
tff(c_8190,plain,
! [Z_117] : ( multiply(sk_c7,multiply(sk_c1,Z_117)) = multiply(identity,Z_117) ),
inference(superposition,[status(thm),theory(equality)],[c_77,c_8154]) ).
tff(c_8207,plain,
! [Z_117] : ( multiply(sk_c7,multiply(sk_c1,Z_117)) = Z_117 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8190]) ).
tff(c_8344,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_8297,c_8207]) ).
tff(c_8350,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8142,c_8344]) ).
tff(c_8362,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8350,c_81]) ).
tff(c_8372,plain,
multiply(sk_c5,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8362,c_4]) ).
tff(c_8268,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_8142,c_8250]) ).
tff(c_8413,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8372,c_8268]) ).
tff(c_8364,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8350,c_24]) ).
tff(c_8427,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8413,c_8364]) ).
tff(c_8434,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8274,c_8427]) ).
tff(c_8226,plain,
! [Z_119] : ( multiply(sk_c7,multiply(sk_c1,Z_119)) = Z_119 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8190]) ).
tff(c_8238,plain,
multiply(sk_c7,sk_c2) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_8117,c_8226]) ).
tff(c_8242,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8238,c_8100]) ).
tff(c_8356,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8350,c_8242]) ).
tff(c_8430,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_8413,c_8356]) ).
tff(c_8453,plain,
sk_c1 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_8434,c_8430]) ).
tff(c_8099,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_8433,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8413,c_8099]) ).
tff(c_30,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_8137,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_8100,c_30]) ).
tff(c_8431,plain,
multiply(sk_c4,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8413,c_8137]) ).
tff(c_8537,plain,
multiply(sk_c4,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8434,c_8431]) ).
tff(c_8193,plain,
! [X_2,Z_117] : ( multiply(inverse(X_2),multiply(X_2,Z_117)) = multiply(identity,Z_117) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_8154]) ).
tff(c_8208,plain,
! [X_2,Z_117] : ( multiply(inverse(X_2),multiply(X_2,Z_117)) = Z_117 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8193]) ).
tff(c_8541,plain,
multiply(inverse(sk_c4),sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8537,c_8208]) ).
tff(c_8547,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8433,c_8541]) ).
tff(c_8549,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8453,c_8547]) ).
tff(c_8550,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_8667,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8658,c_8550]) ).
tff(c_8670,plain,
sk_c6 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_8117,c_8667]) ).
tff(c_8683,plain,
multiply(sk_c5,sk_c2) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_8670,c_24]) ).
tff(c_8855,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_8849,c_8683]) ).
tff(c_8860,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8629,c_8855]) ).
tff(c_8707,plain,
! [X2_9,X1_8,X4_7] :
( ( inverse(X2_9) != sk_c2 )
| ( multiply(X2_9,sk_c2) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c2 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c2 )
| ( multiply(sk_c7,sk_c2) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8670,c_81,c_8670,c_8670,c_8670,c_8670,c_52]) ).
tff(c_8708,plain,
multiply(sk_c7,sk_c2) != sk_c5,
inference(splitLeft,[status(thm)],[c_8707]) ).
tff(c_8836,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8831,c_8708]) ).
tff(c_8912,plain,
sk_c5 != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8860,c_8836]) ).
tff(c_8907,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8860,c_73]) ).
tff(c_8906,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8860,c_81]) ).
tff(c_8955,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_8907,c_8906]) ).
tff(c_8956,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8912,c_8955]) ).
tff(c_8958,plain,
multiply(sk_c7,sk_c2) = sk_c5,
inference(splitRight,[status(thm)],[c_8707]) ).
tff(c_8551,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_8678,plain,
multiply(sk_c7,sk_c2) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8670,c_8551]) ).
tff(c_8993,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8958,c_8678]) ).
tff(c_8994,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_8999,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8994,c_4]) ).
tff(c_9089,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_8999,c_9077]) ).
tff(c_9120,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9092,c_9089]) ).
tff(c_9016,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_8100,c_26]) ).
tff(c_9129,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_9120,c_9016]) ).
tff(c_9057,plain,
! [Z_137] : ( multiply(sk_c7,multiply(sk_c1,Z_137)) = multiply(identity,Z_137) ),
inference(superposition,[status(thm),theory(equality)],[c_77,c_9027]) ).
tff(c_9149,plain,
! [Z_140] : ( multiply(sk_c7,multiply(sk_c1,Z_140)) = Z_140 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9057]) ).
tff(c_9164,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_9129,c_9149]) ).
tff(c_9073,plain,
! [Z_137] : ( multiply(sk_c5,multiply(sk_c7,Z_137)) = Z_137 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9054]) ).
tff(c_9172,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9164,c_9073]) ).
tff(c_9178,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_85,c_9172]) ).
tff(c_9205,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_9178,c_24]) ).
tff(c_9208,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9092,c_9205]) ).
tff(c_9147,plain,
! [X2_9,X1_8,X4_7] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_81,c_52]) ).
tff(c_9148,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_9147]) ).
tff(c_9168,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9164,c_9148]) ).
tff(c_9213,plain,
sk_c5 != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9208,c_9168]) ).
tff(c_9219,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9208,c_73]) ).
tff(c_9218,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9208,c_81]) ).
tff(c_9265,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9219,c_9218]) ).
tff(c_9266,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9213,c_9265]) ).
tff(c_9268,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_9147]) ).
tff(c_9306,plain,
! [Z_145] : ( multiply(sk_c7,multiply(sk_c1,Z_145)) = Z_145 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9057]) ).
tff(c_9327,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_9129,c_9306]) ).
tff(c_9331,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9268,c_9327]) ).
tff(c_9339,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9331,c_85]) ).
tff(c_9272,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9268,c_9073]) ).
tff(c_10038,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9339,c_9272]) ).
tff(c_9343,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9331,c_24]) ).
tff(c_10111,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10038,c_9343]) ).
tff(c_10117,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9092,c_10111]) ).
tff(c_9011,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_8100,c_30]) ).
tff(c_10089,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9011,c_10047]) ).
tff(c_10110,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8099,c_10089]) ).
tff(c_10173,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10117,c_10038,c_2,c_10038,c_10110]) ).
tff(c_10177,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10173,c_10117]) ).
tff(c_9427,plain,
! [X_146,Z_147] : ( multiply(inverse(X_146),multiply(X_146,Z_147)) = Z_147 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9060]) ).
tff(c_9628,plain,
! [X_150,Z_151] : ( multiply(inverse(inverse(X_150)),Z_151) = multiply(X_150,Z_151) ),
inference(superposition,[status(thm),theory(equality)],[c_9075,c_9427]) ).
tff(c_9451,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9427]) ).
tff(c_9635,plain,
! [X_150] : ( multiply(X_150,identity) = X_150 ),
inference(superposition,[status(thm),theory(equality)],[c_9628,c_9451]) ).
tff(c_9341,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9331,c_81]) ).
tff(c_9351,plain,
multiply(sk_c5,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9341,c_4]) ).
tff(c_9386,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9351,c_9272]) ).
tff(c_8104,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8099,c_4]) ).
tff(c_9399,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9386,c_8104]) ).
tff(c_9501,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_9399,c_9075]) ).
tff(c_9513,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_9501]) ).
tff(c_9395,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9386,c_9343]) ).
tff(c_9401,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9092,c_9395]) ).
tff(c_9045,plain,
! [Z_137] : ( multiply(sk_c4,multiply(sk_c6,Z_137)) = multiply(sk_c5,Z_137) ),
inference(superposition,[status(thm),theory(equality)],[c_9011,c_9027]) ).
tff(c_9523,plain,
! [Z_137] : ( multiply(sk_c1,Z_137) = Z_137 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9513,c_9401,c_2,c_9386,c_9045]) ).
tff(c_9334,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9331,c_9268]) ).
tff(c_9469,plain,
multiply(sk_c1,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9401,c_9401,c_9386,c_9334]) ).
tff(c_9525,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9523,c_9469]) ).
tff(c_9555,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9525,c_9401]) ).
tff(c_9267,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_9147]) ).
tff(c_9362,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c5 )
| ( multiply(sk_c5,multiply(X4_7,sk_c5)) != sk_c6 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_9331,c_9331,c_9331,c_9331,c_9331,c_9267]) ).
tff(c_9363,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_9362]) ).
tff(c_10012,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_9635,c_9555,c_9386,c_9386,c_9363]) ).
tff(c_9342,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9331,c_73]) ).
tff(c_9408,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_9401,c_9342]) ).
tff(c_9553,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9525,c_9525,c_9408]) ).
tff(c_10014,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10012,c_9553]) ).
tff(c_10015,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(sk_c5,multiply(X4_7,sk_c5)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_9362]) ).
tff(c_24126,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10280,c_10177,c_2,c_10177,c_10038,c_10177,c_10280,c_10177,c_10038,c_10177,c_10015]) ).
tff(c_24128,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_24126]) ).
tff(c_10125,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_10117,c_10117,c_9341]) ).
tff(c_10174,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10173,c_10173,c_10125]) ).
tff(c_24130,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24128,c_10174]) ).
tff(c_24132,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_24126]) ).
tff(c_24134,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24132,c_10174]) ).
tff(c_24136,plain,
inverse(sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_20,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_24168,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_24136,c_20]) ).
tff(c_22,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_24144,plain,
inverse(sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_24145,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24136,c_24144]) ).
tff(c_24146,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_24151,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24146,c_4]) ).
tff(c_24192,plain,
! [X_288,Y_289,Z_290] : ( multiply(multiply(X_288,Y_289),Z_290) = multiply(X_288,multiply(Y_289,Z_290)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_24216,plain,
! [Z_290] : ( multiply(sk_c6,multiply(sk_c4,Z_290)) = multiply(identity,Z_290) ),
inference(superposition,[status(thm),theory(equality)],[c_24151,c_24192]) ).
tff(c_24251,plain,
! [Z_292] : ( multiply(sk_c6,multiply(sk_c4,Z_292)) = Z_292 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24216]) ).
tff(c_24263,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_24168,c_24251]) ).
tff(c_24222,plain,
! [X_2,Z_290] : ( multiply(inverse(X_2),multiply(X_2,Z_290)) = multiply(identity,Z_290) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_24192]) ).
tff(c_24335,plain,
! [X_295,Z_296] : ( multiply(inverse(X_295),multiply(X_295,Z_296)) = Z_296 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24222]) ).
tff(c_24368,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_24263,c_24335]) ).
tff(c_24416,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24368]) ).
tff(c_16,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_24173,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_24136,c_16]) ).
tff(c_24135,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_24140,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24135,c_4]) ).
tff(c_24219,plain,
! [Z_290] : ( multiply(sk_c7,multiply(sk_c3,Z_290)) = multiply(identity,Z_290) ),
inference(superposition,[status(thm),theory(equality)],[c_24140,c_24192]) ).
tff(c_24312,plain,
! [Z_294] : ( multiply(sk_c7,multiply(sk_c3,Z_294)) = Z_294 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24219]) ).
tff(c_24324,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_24173,c_24312]) ).
tff(c_24353,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_24324,c_24335]) ).
tff(c_24414,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24353]) ).
tff(c_24431,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_24414,c_24]) ).
tff(c_24446,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24416,c_24431]) ).
tff(c_24439,plain,
inverse(sk_c7) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_24416,c_24136]) ).
tff(c_24487,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_24446,c_24439]) ).
tff(c_24449,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24446,c_77]) ).
tff(c_24236,plain,
! [X_2,Z_290] : ( multiply(inverse(X_2),multiply(X_2,Z_290)) = Z_290 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24222]) ).
tff(c_24491,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_24449,c_24236]) ).
tff(c_24503,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24491]) ).
tff(c_24452,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24446,c_73]) ).
tff(c_24525,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24503,c_24452]) ).
tff(c_24528,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24487,c_24525]) ).
tff(c_24530,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_24563,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_24530,c_46]) ).
tff(c_48,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_24555,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_24530,c_48]) ).
tff(c_24559,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24555,c_4]) ).
tff(c_24609,plain,
! [Z_300] : ( multiply(sk_c6,multiply(sk_c4,Z_300)) = multiply(identity,Z_300) ),
inference(superposition,[status(thm),theory(equality)],[c_24559,c_24591]) ).
tff(c_24637,plain,
! [Z_301] : ( multiply(sk_c6,multiply(sk_c4,Z_301)) = Z_301 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24609]) ).
tff(c_24649,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_24563,c_24637]) ).
tff(c_25577,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_24649,c_25553]) ).
tff(c_25602,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25577]) ).
tff(c_24687,plain,
! [Z_303] : ( multiply(sk_c4,multiply(sk_c6,Z_303)) = multiply(sk_c5,Z_303) ),
inference(superposition,[status(thm),theory(equality)],[c_24563,c_24591]) ).
tff(c_24702,plain,
multiply(sk_c5,sk_c5) = multiply(sk_c4,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_24649,c_24687]) ).
tff(c_24712,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24563,c_24702]) ).
tff(c_24765,plain,
! [X_305,Z_306] : ( multiply(inverse(X_305),multiply(X_305,Z_306)) = Z_306 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24621]) ).
tff(c_24789,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_24712,c_24765]) ).
tff(c_24817,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24789]) ).
tff(c_42,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_24577,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_24530,c_42]) ).
tff(c_24529,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_24534,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24529,c_4]) ).
tff(c_24618,plain,
! [Z_300] : ( multiply(sk_c7,multiply(sk_c3,Z_300)) = multiply(identity,Z_300) ),
inference(superposition,[status(thm),theory(equality)],[c_24534,c_24591]) ).
tff(c_24663,plain,
! [Z_302] : ( multiply(sk_c7,multiply(sk_c3,Z_302)) = Z_302 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24618]) ).
tff(c_24675,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_24577,c_24663]) ).
tff(c_24543,plain,
inverse(sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_24661,plain,
! [X2_9,X1_8,X4_7] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_24543,c_52]) ).
tff(c_24662,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_24661]) ).
tff(c_24679,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24675,c_24662]) ).
tff(c_24825,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_24817,c_24679]) ).
tff(c_24547,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24543,c_4]) ).
tff(c_24615,plain,
! [Z_300] : ( multiply(sk_c5,multiply(sk_c7,Z_300)) = multiply(identity,Z_300) ),
inference(superposition,[status(thm),theory(equality)],[c_24547,c_24591]) ).
tff(c_24728,plain,
! [Z_304] : ( multiply(sk_c5,multiply(sk_c7,Z_304)) = Z_304 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24615]) ).
tff(c_24740,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_24675,c_24728]) ).
tff(c_24750,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24547,c_24740]) ).
tff(c_24759,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_24750,c_24]) ).
tff(c_24844,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24817,c_24759]) ).
tff(c_24845,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24825,c_24844]) ).
tff(c_24847,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_24661]) ).
tff(c_24855,plain,
! [Z_307] : ( multiply(sk_c7,multiply(sk_c3,Z_307)) = Z_307 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24618]) ).
tff(c_24867,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_24577,c_24855]) ).
tff(c_24871,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24847,c_24867]) ).
tff(c_24880,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24871,c_24]) ).
tff(c_25619,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25602,c_2,c_25602,c_24880]) ).
tff(c_24966,plain,
! [X_309,Z_310] : ( multiply(inverse(X_309),multiply(X_309,Z_310)) = Z_310 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24621]) ).
tff(c_25286,plain,
! [X_315,Z_316] : ( multiply(inverse(inverse(X_315)),Z_316) = multiply(X_315,Z_316) ),
inference(superposition,[status(thm),theory(equality)],[c_24966,c_24635]) ).
tff(c_25023,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_24966]) ).
tff(c_25293,plain,
! [X_315] : ( multiply(X_315,identity) = X_315 ),
inference(superposition,[status(thm),theory(equality)],[c_25286,c_25023]) ).
tff(c_24875,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24871,c_24547]) ).
tff(c_24873,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24871,c_24847]) ).
tff(c_24633,plain,
! [Z_300] : ( multiply(sk_c5,multiply(sk_c7,Z_300)) = Z_300 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_24615]) ).
tff(c_24935,plain,
! [Z_308] : ( multiply(sk_c5,multiply(sk_c5,Z_308)) = Z_308 ),
inference(demodulation,[status(thm),theory(equality)],[c_24871,c_24633]) ).
tff(c_24959,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_24873,c_24935]) ).
tff(c_24965,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24875,c_24959]) ).
tff(c_25005,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_24649,c_24966]) ).
tff(c_25036,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25005]) ).
tff(c_24846,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_7,sk_c7)) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_24661]) ).
tff(c_24899,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c5 )
| ( multiply(sk_c5,multiply(X4_7,sk_c5)) != sk_c6 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_24871,c_24871,c_24871,c_24871,c_24871,c_24846]) ).
tff(c_24900,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_24899]) ).
tff(c_25549,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_25293,c_24965,c_25036,c_24965,c_24900]) ).
tff(c_24876,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_24871,c_24543]) ).
tff(c_25046,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25036,c_25036,c_24876]) ).
tff(c_25551,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25549,c_25046]) ).
tff(c_25552,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(sk_c5,multiply(X4_7,sk_c5)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_24899]) ).
tff(c_33690,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_25810,c_25619,c_25602,c_2,c_25602,c_25602,c_25810,c_25619,c_25602,c_25602,c_25552]) ).
tff(c_33692,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_33690]) ).
tff(c_25606,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25602,c_25602,c_24876]) ).
tff(c_33694,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33692,c_25606]) ).
tff(c_33696,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_33690]) ).
tff(c_33698,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33696,c_25606]) ).
tff(c_33700,plain,
inverse(sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_33722,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_33700,c_20]) ).
tff(c_33699,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_33704,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33699,c_4]) ).
tff(c_33740,plain,
! [X_416,Y_417,Z_418] : ( multiply(multiply(X_416,Y_417),Z_418) = multiply(X_416,multiply(Y_417,Z_418)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33761,plain,
! [Z_418] : ( multiply(sk_c6,multiply(sk_c4,Z_418)) = multiply(identity,Z_418) ),
inference(superposition,[status(thm),theory(equality)],[c_33704,c_33740]) ).
tff(c_33798,plain,
! [Z_420] : ( multiply(sk_c6,multiply(sk_c4,Z_420)) = Z_420 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33761]) ).
tff(c_33816,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_33722,c_33798]) ).
tff(c_33767,plain,
! [X_2,Z_418] : ( multiply(inverse(X_2),multiply(X_2,Z_418)) = multiply(identity,Z_418) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_33740]) ).
tff(c_33869,plain,
! [X_422,Z_423] : ( multiply(inverse(X_422),multiply(X_422,Z_423)) = Z_423 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33767]) ).
tff(c_33899,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_33816,c_33869]) ).
tff(c_33941,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33899]) ).
tff(c_33717,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_33700,c_16]) ).
tff(c_33764,plain,
! [Z_418] : ( multiply(sk_c7,multiply(sk_c3,Z_418)) = multiply(identity,Z_418) ),
inference(superposition,[status(thm),theory(equality)],[c_24534,c_33740]) ).
tff(c_33846,plain,
! [Z_421] : ( multiply(sk_c7,multiply(sk_c3,Z_421)) = Z_421 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33764]) ).
tff(c_33858,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33717,c_33846]) ).
tff(c_33887,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_33858,c_33869]) ).
tff(c_33939,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33887]) ).
tff(c_33955,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33939,c_24]) ).
tff(c_33972,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33941,c_33955]) ).
tff(c_33976,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33972]) ).
tff(c_33975,plain,
inverse(sk_c7) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_33941,c_33700]) ).
tff(c_33992,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_33976,c_33975]) ).
tff(c_33954,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_33939,c_33699]) ).
tff(c_34000,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33954,c_4]) ).
tff(c_33780,plain,
! [X_2,Z_418] : ( multiply(inverse(X_2),multiply(X_2,Z_418)) = Z_418 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33767]) ).
tff(c_34029,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_34000,c_33780]) ).
tff(c_34041,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_34029]) ).
tff(c_34046,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34041,c_33954]) ).
tff(c_34050,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33992,c_34046]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GRP309-1 : TPTP v9.0.0. Released v2.5.0.
% 0.12/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n029.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:41:19 EDT 2025
% 0.13/0.34 % CPUTime :
% 17.57/6.03 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.57/6.07
% 17.57/6.07 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------