%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP289-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:49 PM UTC 2025
% Result : Unsatisfiable 16.45s 5.42s
% Output : CNFRefutation 17.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 27
% Syntax : Number of formulae : 649 ( 547 unt; 0 typ; 0 def)
% Number of atoms : 867 ( 831 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 508 ( 290 ~; 218 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 297 ( 297 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
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_128,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c7,sk_c6) != sk_c5 )
| ( multiply(X3,sk_c7) != sk_c6 )
| ( inverse(X3) != sk_c7 )
| ( multiply(X4,sk_c6) != sk_c5 )
| ( inverse(X4) != sk_c6 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( inverse(X2) != sk_c6 )
| ( multiply(X2,sk_c5) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_20,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_6259,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_30,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_87,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_91,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_87,c_4]) ).
tff(c_6301,plain,
! [X_121,Y_122,Z_123] : ( multiply(multiply(X_121,Y_122),Z_123) = multiply(X_121,multiply(Y_122,Z_123)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_6337,plain,
! [Z_123] : ( multiply(sk_c7,multiply(sk_c1,Z_123)) = multiply(identity,Z_123) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_6301]) ).
tff(c_6357,plain,
! [Z_124] : ( multiply(sk_c7,multiply(sk_c1,Z_124)) = Z_124 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6337]) ).
tff(c_6369,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_6259,c_6357]) ).
tff(c_6373,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_6369]) ).
tff(c_6380,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6373,c_102]) ).
tff(c_6343,plain,
! [X_2,Z_123] : ( multiply(inverse(X_2),multiply(X_2,Z_123)) = multiply(identity,Z_123) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_6301]) ).
tff(c_6443,plain,
! [X_125,Z_126] : ( multiply(inverse(X_125),multiply(X_125,Z_126)) = Z_126 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6343]) ).
tff(c_6464,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_6380,c_6443]) ).
tff(c_6499,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_6464]) ).
tff(c_50,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_75,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_79,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_75,c_4]) ).
tff(c_6507,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6499,c_79]) ).
tff(c_6355,plain,
! [X_2,Z_123] : ( multiply(inverse(X_2),multiply(X_2,Z_123)) = Z_123 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6343]) ).
tff(c_6658,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_6507,c_6355]) ).
tff(c_6670,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_6658]) ).
tff(c_44,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_107,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_4444,plain,
! [X_87,Y_88,Z_89] : ( multiply(multiply(X_87,Y_88),Z_89) = multiply(X_87,multiply(Y_88,Z_89)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_4483,plain,
! [Z_89] : ( multiply(sk_c6,multiply(sk_c2,Z_89)) = multiply(identity,Z_89) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_4444]) ).
tff(c_4513,plain,
! [Z_91] : ( multiply(sk_c6,multiply(sk_c2,Z_91)) = Z_91 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4483]) ).
tff(c_4525,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_107,c_4513]) ).
tff(c_4474,plain,
! [Z_89] : ( multiply(sk_c2,multiply(sk_c6,Z_89)) = multiply(sk_c5,Z_89) ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_4444]) ).
tff(c_5603,plain,
multiply(sk_c5,sk_c5) = multiply(sk_c2,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_4525,c_4474]) ).
tff(c_5609,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_107,c_5603]) ).
tff(c_113,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_134,plain,
! [X_12,Y_13,Z_14] : ( multiply(multiply(X_12,Y_13),Z_14) = multiply(X_12,multiply(Y_13,Z_14)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_158,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_134]) ).
tff(c_374,plain,
! [Z_20] : ( multiply(sk_c7,multiply(sk_c1,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_386,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_113,c_374]) ).
tff(c_390,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_386]) ).
tff(c_161,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_134]) ).
tff(c_179,plain,
! [Z_15] : ( multiply(sk_c6,multiply(sk_c2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_191,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_107,c_179]) ).
tff(c_164,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_134]) ).
tff(c_270,plain,
! [X_18,Z_19] : ( multiply(inverse(X_18),multiply(X_18,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_297,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_191,c_270]) ).
tff(c_324,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_297]) ).
tff(c_235,plain,
! [Z_17] : ( multiply(sk_c7,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_247,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_113,c_235]) ).
tff(c_251,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_247]) ).
tff(c_58,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_177,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_58]) ).
tff(c_178,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_177]) ).
tff(c_253,plain,
multiply(sk_c6,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_251,c_178]) ).
tff(c_258,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_191,c_253]) ).
tff(c_328,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_324,c_258]) ).
tff(c_255,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_251,c_102]) ).
tff(c_363,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_324,c_2,c_324,c_255]) ).
tff(c_364,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_328,c_363]) ).
tff(c_366,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_524,plain,
multiply(sk_c6,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_366]) ).
tff(c_867,plain,
! [Z_29] : ( multiply(sk_c6,multiply(sk_c2,Z_29)) = Z_29 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_879,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_107,c_867]) ).
tff(c_883,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_879]) ).
tff(c_885,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_883,c_524]) ).
tff(c_174,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_953,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_885,c_174]) ).
tff(c_959,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_953]) ).
tff(c_895,plain,
! [X_30,Z_31] : ( multiply(inverse(X_30),multiply(X_30,Z_31)) = Z_31 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_1148,plain,
! [X_35,Z_36] : ( multiply(inverse(inverse(X_35)),Z_36) = multiply(X_35,Z_36) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_895]) ).
tff(c_922,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_895]) ).
tff(c_1159,plain,
! [X_35] : ( multiply(X_35,identity) = X_35 ),
inference(superposition,[status(thm),theory(equality)],[c_1148,c_922]) ).
tff(c_976,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_959,c_883]) ).
tff(c_572,plain,
! [Z_23] : ( multiply(sk_c6,multiply(sk_c2,Z_23)) = Z_23 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_584,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_107,c_572]) ).
tff(c_588,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_524,c_584]) ).
tff(c_590,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_588,c_524]) ).
tff(c_614,plain,
! [X_24,Z_25] : ( multiply(inverse(X_24),multiply(X_24,Z_25)) = Z_25 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_632,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_590,c_614]) ).
tff(c_654,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_632]) ).
tff(c_595,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_588,c_75]) ).
tff(c_603,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_595,c_4]) ).
tff(c_674,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_654,c_603]) ).
tff(c_656,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_654,c_595]) ).
tff(c_679,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_674,c_656]) ).
tff(c_754,plain,
! [X_26] : ( multiply(inverse(inverse(X_26)),identity) = X_26 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_614]) ).
tff(c_760,plain,
! [X_26] : ( multiply(inverse(inverse(inverse(X_26))),X_26) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_754,c_174]) ).
tff(c_657,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_654,c_588]) ).
tff(c_397,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_87]) ).
tff(c_393,plain,
multiply(sk_c6,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_366]) ).
tff(c_439,plain,
! [Z_21] : ( multiply(sk_c6,multiply(sk_c2,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_451,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_107,c_439]) ).
tff(c_455,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_393,c_451]) ).
tff(c_394,plain,
multiply(sk_c1,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_113]) ).
tff(c_458,plain,
multiply(sk_c1,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_455,c_394]) ).
tff(c_365,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_391,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_365]) ).
tff(c_467,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_455,c_455,c_391]) ).
tff(c_512,plain,
inverse(sk_c1) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_458,c_467]) ).
tff(c_521,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_397,c_512]) ).
tff(c_522,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_365]) ).
tff(c_540,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_390,c_390,c_390,c_522]) ).
tff(c_541,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_540]) ).
tff(c_812,plain,
! [X3_28] :
( ( inverse(X3_28) != identity )
| ( multiply(X3_28,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_657,c_654,c_654,c_541]) ).
tff(c_816,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_760,c_812]) ).
tff(c_835,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_679,c_679,c_679,c_679,c_816]) ).
tff(c_836,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_540]) ).
tff(c_4375,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_959,c_1159,c_976,c_959,c_1159,c_976,c_959,c_976,c_836]) ).
tff(c_4377,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_4375]) ).
tff(c_889,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_883,c_79]) ).
tff(c_1032,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_959,c_889]) ).
tff(c_890,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_883,c_75]) ).
tff(c_975,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_959,c_890]) ).
tff(c_1033,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1032,c_975]) ).
tff(c_4379,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4377,c_1033]) ).
tff(c_4381,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_4375]) ).
tff(c_4383,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4381,c_1033]) ).
tff(c_4385,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_26,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_4433,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_4385,c_26]) ).
tff(c_24,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_4393,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_4399,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4393,c_4385]) ).
tff(c_4400,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_4405,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4400,c_4]) ).
tff(c_4468,plain,
! [Z_89] : ( multiply(sk_c6,multiply(sk_c4,Z_89)) = multiply(identity,Z_89) ),
inference(superposition,[status(thm),theory(equality)],[c_4405,c_4444]) ).
tff(c_5626,plain,
! [Z_110] : ( multiply(sk_c6,multiply(sk_c4,Z_110)) = Z_110 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4468]) ).
tff(c_5641,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_4433,c_5626]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_5572,plain,
! [Z_109] : ( multiply(sk_c2,multiply(sk_c6,Z_109)) = multiply(sk_c5,Z_109) ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_4444]) ).
tff(c_5596,plain,
multiply(sk_c5,sk_c2) = multiply(sk_c2,identity),
inference(superposition,[status(thm),theory(equality)],[c_79,c_5572]) ).
tff(c_5874,plain,
! [Z_116] : ( multiply(sk_c7,multiply(sk_c6,Z_116)) = multiply(sk_c5,Z_116) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_4444]) ).
tff(c_5904,plain,
multiply(sk_c7,identity) = multiply(sk_c5,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_79,c_5874]) ).
tff(c_5910,plain,
multiply(sk_c7,identity) = multiply(sk_c2,identity),
inference(demodulation,[status(thm),theory(equality)],[c_5596,c_5904]) ).
tff(c_5914,plain,
! [Z_5] : ( multiply(multiply(sk_c2,identity),Z_5) = multiply(sk_c7,multiply(identity,Z_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_5910,c_6]) ).
tff(c_5939,plain,
! [Z_117] : ( multiply(sk_c7,Z_117) = multiply(sk_c2,Z_117) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_6,c_5914]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_4423,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_4385,c_22]) ).
tff(c_4384,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_4389,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4384,c_4]) ).
tff(c_4471,plain,
! [Z_89] : ( multiply(sk_c7,multiply(sk_c3,Z_89)) = multiply(identity,Z_89) ),
inference(superposition,[status(thm),theory(equality)],[c_4389,c_4444]) ).
tff(c_5851,plain,
! [Z_115] : ( multiply(sk_c7,multiply(sk_c3,Z_115)) = Z_115 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4471]) ).
tff(c_5863,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4423,c_5851]) ).
tff(c_5948,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5939,c_5863]) ).
tff(c_4497,plain,
! [Z_89] : ( multiply(sk_c6,multiply(sk_c2,Z_89)) = Z_89 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4483]) ).
tff(c_6170,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_5948,c_4497]) ).
tff(c_6176,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5641,c_6170]) ).
tff(c_6183,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6176,c_6176,c_5863]) ).
tff(c_6195,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5609,c_6183]) ).
tff(c_6002,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_5948,c_4497]) ).
tff(c_6008,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5641,c_6002]) ).
tff(c_6015,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6008,c_6008,c_5863]) ).
tff(c_6027,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5609,c_6015]) ).
tff(c_6042,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6027,c_75]) ).
tff(c_5975,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5863,c_5939]) ).
tff(c_6152,plain,
multiply(sk_c2,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6027,c_6008,c_5975]) ).
tff(c_4609,plain,
! [Z_94] : ( multiply(sk_c6,multiply(sk_c4,Z_94)) = Z_94 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4468]) ).
tff(c_4624,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_4433,c_4609]) ).
tff(c_4486,plain,
! [X_2,Z_89] : ( multiply(inverse(X_2),multiply(X_2,Z_89)) = multiply(identity,Z_89) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4444]) ).
tff(c_4688,plain,
! [X_96,Z_97] : ( multiply(inverse(X_96),multiply(X_96,Z_97)) = Z_97 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4486]) ).
tff(c_4736,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_4525,c_4688]) ).
tff(c_4796,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4736]) ).
tff(c_4812,plain,
multiply(sk_c6,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4796,c_4525]) ).
tff(c_4562,plain,
! [Z_93] : ( multiply(sk_c2,multiply(sk_c6,Z_93)) = multiply(sk_c5,Z_93) ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_4444]) ).
tff(c_4589,plain,
multiply(sk_c5,sk_c2) = multiply(sk_c2,identity),
inference(superposition,[status(thm),theory(equality)],[c_79,c_4562]) ).
tff(c_4809,plain,
multiply(sk_c2,identity) = multiply(identity,sk_c2),
inference(demodulation,[status(thm),theory(equality)],[c_4796,c_4589]) ).
tff(c_4820,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4809]) ).
tff(c_18,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_4428,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_4385,c_18]) ).
tff(c_4583,plain,
multiply(sk_c5,sk_c7) = multiply(sk_c2,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_4428,c_4562]) ).
tff(c_4805,plain,
multiply(sk_c2,identity) = multiply(identity,sk_c7),
inference(demodulation,[status(thm),theory(equality)],[c_4796,c_4796,c_4583]) ).
tff(c_4818,plain,
multiply(sk_c2,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4805]) ).
tff(c_4987,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_4820,c_4818]) ).
tff(c_5002,plain,
inverse(sk_c1) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_4987,c_87]) ).
tff(c_4787,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4688]) ).
tff(c_5035,plain,
multiply(inverse(sk_c2),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_5002,c_4787]) ).
tff(c_5044,plain,
sk_c6 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_4812,c_75,c_5035]) ).
tff(c_4530,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_4428,c_58]) ).
tff(c_4646,plain,
! [X3_95] :
( ( inverse(X3_95) != sk_c7 )
| ( multiply(X3_95,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_4530]) ).
tff(c_4664,plain,
( ( inverse(identity) != sk_c7 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_4646]) ).
tff(c_4666,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_4664]) ).
tff(c_4991,plain,
sk_c6 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_4987,c_4666]) ).
tff(c_5046,plain,
sk_c2 != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_5044,c_4991]) ).
tff(c_4631,plain,
multiply(sk_c5,sk_c6) = multiply(sk_c2,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_4624,c_4474]) ).
tff(c_4804,plain,
multiply(sk_c2,identity) = multiply(identity,sk_c6),
inference(demodulation,[status(thm),theory(equality)],[c_4796,c_4796,c_4631]) ).
tff(c_4817,plain,
multiply(sk_c2,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4804]) ).
tff(c_5152,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_5044,c_4820,c_4817]) ).
tff(c_5153,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5046,c_5152]) ).
tff(c_5155,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_4664]) ).
tff(c_4539,plain,
! [Z_92] : ( multiply(sk_c7,multiply(sk_c3,Z_92)) = Z_92 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4471]) ).
tff(c_4551,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4423,c_4539]) ).
tff(c_5158,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5155,c_5155,c_4551]) ).
tff(c_5169,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4624,c_5158]) ).
tff(c_5184,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5169,c_5155]) ).
tff(c_4660,plain,
( ( inverse(inverse(sk_c7)) != sk_c7 )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4646]) ).
tff(c_5312,plain,
( ( inverse(inverse(sk_c5)) != sk_c5 )
| ( sk_c5 != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5169,c_5184,c_5184,c_4660]) ).
tff(c_5313,plain,
sk_c5 != identity,
inference(splitLeft,[status(thm)],[c_5312]) ).
tff(c_4577,plain,
multiply(sk_c5,sk_c5) = multiply(sk_c2,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_4525,c_4562]) ).
tff(c_4593,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_107,c_4577]) ).
tff(c_5362,plain,
! [X_105,Z_106] : ( multiply(inverse(X_105),multiply(X_105,Z_106)) = Z_106 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4486]) ).
tff(c_5419,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_4593,c_5362]) ).
tff(c_5438,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5419]) ).
tff(c_5440,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5313,c_5438]) ).
tff(c_5442,plain,
sk_c5 = identity,
inference(splitRight,[status(thm)],[c_5312]) ).
tff(c_5154,plain,
inverse(identity) != sk_c7,
inference(splitRight,[status(thm)],[c_4664]) ).
tff(c_5223,plain,
inverse(identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5184,c_5154]) ).
tff(c_5454,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_5442,c_5223]) ).
tff(c_5194,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5169,c_79]) ).
tff(c_5444,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5442,c_5194]) ).
tff(c_4498,plain,
! [X_2,Z_89] : ( multiply(inverse(X_2),multiply(X_2,Z_89)) = Z_89 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4486]) ).
tff(c_5550,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_5444,c_4498]) ).
tff(c_5562,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5550]) ).
tff(c_5195,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5169,c_75]) ).
tff(c_5452,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5442,c_5195]) ).
tff(c_5566,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5562,c_5452]) ).
tff(c_5570,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5454,c_5566]) ).
tff(c_5571,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_4530]) ).
tff(c_5811,plain,
! [X2_114] :
( ( multiply(X2_114,sk_c5) != sk_c6 )
| ( inverse(X2_114) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_5571]) ).
tff(c_5828,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4433,c_5811]) ).
tff(c_5841,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4400,c_5828]) ).
tff(c_5842,plain,
! [X1_8,X4_7] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_5571]) ).
tff(c_5998,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_5842]) ).
tff(c_6111,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6027,c_6027,c_5998]) ).
tff(c_6156,plain,
inverse(sk_c2) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_6152,c_6111]) ).
tff(c_6165,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6042,c_6156]) ).
tff(c_6166,plain,
! [X1_8] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_5842]) ).
tff(c_6201,plain,
! [X1_120] :
( ( multiply(X1_120,sk_c6) != sk_c5 )
| ( inverse(X1_120) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6176,c_6176,c_6166]) ).
tff(c_6211,plain,
inverse(sk_c2) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_107,c_6201]) ).
tff(c_6222,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_6211]) ).
tff(c_6242,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6195,c_6222]) ).
tff(c_6243,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_6244,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_6296,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_6244,c_46]) ).
tff(c_6476,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_6296,c_6443]) ).
tff(c_6500,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6243,c_6476]) ).
tff(c_6544,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6499,c_2,c_6499,c_6500]) ).
tff(c_6505,plain,
multiply(sk_c2,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6499,c_6244]) ).
tff(c_6654,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_6544,c_6505]) ).
tff(c_6674,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_6670,c_6654]) ).
tff(c_6679,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6674]) ).
tff(c_6680,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_42,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_6699,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_6244,c_42]) ).
tff(c_6681,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_6716,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_6681,c_26]) ).
tff(c_6248,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6243,c_4]) ).
tff(c_6723,plain,
! [X_127,Y_128,Z_129] : ( multiply(multiply(X_127,Y_128),Z_129) = multiply(X_127,multiply(Y_128,Z_129)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_6750,plain,
! [Z_129] : ( multiply(sk_c6,multiply(sk_c4,Z_129)) = multiply(identity,Z_129) ),
inference(superposition,[status(thm),theory(equality)],[c_6248,c_6723]) ).
tff(c_6828,plain,
! [Z_133] : ( multiply(sk_c6,multiply(sk_c4,Z_133)) = Z_133 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6750]) ).
tff(c_6840,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_6716,c_6828]) ).
tff(c_6709,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_6681,c_18]) ).
tff(c_6819,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_6709,c_58]) ).
tff(c_6924,plain,
! [X3_135] :
( ( inverse(X3_135) != sk_c7 )
| ( multiply(X3_135,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_6819]) ).
tff(c_6945,plain,
( ( inverse(identity) != sk_c7 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_6924]) ).
tff(c_6947,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_6945]) ).
tff(c_6762,plain,
! [X_2,Z_129] : ( multiply(inverse(X_2),multiply(X_2,Z_129)) = multiply(identity,Z_129) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_6723]) ).
tff(c_6774,plain,
! [X_2,Z_129] : ( multiply(inverse(X_2),multiply(X_2,Z_129)) = Z_129 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6762]) ).
tff(c_6851,plain,
! [Z_134] : ( multiply(sk_c7,multiply(sk_c6,Z_134)) = multiply(sk_c5,Z_134) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_6723]) ).
tff(c_6863,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_6840,c_6851]) ).
tff(c_6872,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_6709,c_6851]) ).
tff(c_6907,plain,
multiply(sk_c5,sk_c7) = multiply(sk_c5,sk_c6),
inference(demodulation,[status(thm),theory(equality)],[c_6863,c_6872]) ).
tff(c_6950,plain,
! [X_136,Z_137] : ( multiply(inverse(X_136),multiply(X_136,Z_137)) = Z_137 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6762]) ).
tff(c_6968,plain,
multiply(inverse(sk_c5),multiply(sk_c5,sk_c6)) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_6907,c_6950]) ).
tff(c_7047,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6774,c_6968]) ).
tff(c_7049,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6947,c_7047]) ).
tff(c_7051,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_6945]) ).
tff(c_6685,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6680,c_4]) ).
tff(c_6747,plain,
! [Z_129] : ( multiply(sk_c7,multiply(sk_c3,Z_129)) = multiply(identity,Z_129) ),
inference(superposition,[status(thm),theory(equality)],[c_6685,c_6723]) ).
tff(c_6802,plain,
! [Z_132] : ( multiply(sk_c7,multiply(sk_c3,Z_132)) = Z_132 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6747]) ).
tff(c_6814,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_6699,c_6802]) ).
tff(c_7058,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_7051,c_7051,c_6814]) ).
tff(c_7069,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6840,c_7058]) ).
tff(c_7084,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_7069,c_7051]) ).
tff(c_7050,plain,
inverse(identity) != sk_c7,
inference(splitRight,[status(thm)],[c_6945]) ).
tff(c_7119,plain,
inverse(identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_7084,c_7050]) ).
tff(c_7092,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7069,c_79]) ).
tff(c_6878,plain,
multiply(sk_c7,identity) = multiply(sk_c5,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_79,c_6851]) ).
tff(c_7056,plain,
multiply(sk_c6,identity) = multiply(sk_c5,sk_c2),
inference(demodulation,[status(thm),theory(equality)],[c_7051,c_6878]) ).
tff(c_7219,plain,
multiply(sk_c5,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7092,c_7069,c_7056]) ).
tff(c_7223,plain,
! [Z_5] : ( multiply(sk_c5,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_7219,c_6]) ).
tff(c_7230,plain,
! [Z_139] : ( multiply(sk_c5,Z_139) = Z_139 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_7223]) ).
tff(c_7089,plain,
multiply(sk_c5,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7069,c_6248]) ).
tff(c_7239,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_7230,c_7089]) ).
tff(c_7091,plain,
inverse(sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_7069,c_6243]) ).
tff(c_7275,plain,
inverse(identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_7239,c_7091]) ).
tff(c_7279,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7119,c_7275]) ).
tff(c_7280,plain,
! [X4_7,X1_8,X2_9] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_6819]) ).
tff(c_7385,plain,
! [X2_142] :
( ( multiply(X2_142,sk_c5) != sk_c6 )
| ( inverse(X2_142) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_7280]) ).
tff(c_7395,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_6716,c_7385]) ).
tff(c_7407,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6243,c_7395]) ).
tff(c_7408,plain,
! [X1_8,X4_7] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_7280]) ).
tff(c_7513,plain,
! [X4_145] :
( ( inverse(X4_145) != sk_c6 )
| ( multiply(X4_145,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_7408]) ).
tff(c_7534,plain,
( ( inverse(identity) != sk_c6 )
| ( sk_c6 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_7513]) ).
tff(c_7538,plain,
sk_c6 != sk_c5,
inference(splitLeft,[status(thm)],[c_7534]) ).
tff(c_7416,plain,
! [Z_143] : ( multiply(sk_c6,multiply(sk_c4,Z_143)) = Z_143 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6750]) ).
tff(c_7428,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_6716,c_7416]) ).
tff(c_7439,plain,
! [Z_144] : ( multiply(sk_c7,multiply(sk_c6,Z_144)) = multiply(sk_c5,Z_144) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_6723]) ).
tff(c_7451,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_7428,c_7439]) ).
tff(c_7460,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_6709,c_7439]) ).
tff(c_7495,plain,
multiply(sk_c5,sk_c7) = multiply(sk_c5,sk_c6),
inference(demodulation,[status(thm),theory(equality)],[c_7451,c_7460]) ).
tff(c_7541,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_6762]) ).
tff(c_7559,plain,
multiply(inverse(sk_c5),multiply(sk_c5,sk_c6)) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_7495,c_7541]) ).
tff(c_7638,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6774,c_7559]) ).
tff(c_7664,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_7638,c_7638,c_6814]) ).
tff(c_7675,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_7428,c_7664]) ).
tff(c_7677,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7538,c_7675]) ).
tff(c_7679,plain,
sk_c6 = sk_c5,
inference(splitRight,[status(thm)],[c_7534]) ).
tff(c_7523,plain,
( ( inverse(sk_c3) != sk_c6 )
| ( sk_c7 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_6699,c_7513]) ).
tff(c_7536,plain,
( ( sk_c7 != sk_c6 )
| ( sk_c7 != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6680,c_7523]) ).
tff(c_7771,plain,
( ( sk_c7 != sk_c5 )
| ( sk_c7 != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7679,c_7536]) ).
tff(c_7772,plain,
sk_c7 != sk_c5,
inference(splitLeft,[status(thm)],[c_7771]) ).
tff(c_7698,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7679,c_79]) ).
tff(c_7466,plain,
multiply(sk_c7,identity) = multiply(sk_c5,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_79,c_7439]) ).
tff(c_7747,plain,
multiply(sk_c7,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7698,c_7466]) ).
tff(c_7811,plain,
! [Z_5] : ( multiply(sk_c7,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_7747,c_6]) ).
tff(c_7827,plain,
! [Z_149] : ( multiply(sk_c7,Z_149) = Z_149 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_7811]) ).
tff(c_7842,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_7827,c_6685]) ).
tff(c_7692,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_7679,c_6699]) ).
tff(c_7864,plain,
multiply(identity,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_7842,c_7692]) ).
tff(c_7868,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7864]) ).
tff(c_7870,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7772,c_7868]) ).
tff(c_7872,plain,
sk_c7 = sk_c5,
inference(splitRight,[status(thm)],[c_7771]) ).
tff(c_7871,plain,
sk_c7 != sk_c5,
inference(splitRight,[status(thm)],[c_7771]) ).
tff(c_7889,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7872,c_7871]) ).
tff(c_7891,plain,
! [X1_150] :
( ( multiply(X1_150,sk_c6) != sk_c7 )
| ( inverse(X1_150) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_7408]) ).
tff(c_7901,plain,
inverse(sk_c3) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_6699,c_7891]) ).
tff(c_7916,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6680,c_7901]) ).
tff(c_7918,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_9309,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_7918,c_16]) ).
tff(c_7926,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_8515,plain,
! [X_164,Y_165,Z_166] : ( multiply(multiply(X_164,Y_165),Z_166) = multiply(X_164,multiply(Y_165,Z_166)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_8551,plain,
! [Z_166] : ( multiply(sk_c6,multiply(sk_c2,Z_166)) = multiply(identity,Z_166) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_8515]) ).
tff(c_8570,plain,
! [Z_167] : ( multiply(sk_c6,multiply(sk_c2,Z_167)) = Z_167 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8551]) ).
tff(c_8582,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_7926,c_8570]) ).
tff(c_8554,plain,
! [X_2,Z_166] : ( multiply(inverse(X_2),multiply(X_2,Z_166)) = multiply(identity,Z_166) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_8515]) ).
tff(c_8697,plain,
! [X_172,Z_173] : ( multiply(inverse(X_172),multiply(X_172,Z_173)) = Z_173 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8554]) ).
tff(c_8736,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_8582,c_8697]) ).
tff(c_8790,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_8736]) ).
tff(c_7956,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_7918,c_16]) ).
tff(c_8536,plain,
! [Z_166] : ( multiply(sk_c4,multiply(sk_c5,Z_166)) = multiply(sk_c6,Z_166) ),
inference(superposition,[status(thm),theory(equality)],[c_7956,c_8515]) ).
tff(c_8915,plain,
! [Z_175] : ( multiply(sk_c6,Z_175) = multiply(sk_c4,Z_175) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8790,c_8536]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_7935,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_7918,c_14]) ).
tff(c_7939,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_7935,c_4]) ).
tff(c_8942,plain,
multiply(sk_c4,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8915,c_7939]) ).
tff(c_8801,plain,
multiply(sk_c6,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8790,c_8582]) ).
tff(c_8566,plain,
! [X_2,Z_166] : ( multiply(inverse(X_2),multiply(X_2,Z_166)) = Z_166 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8554]) ).
tff(c_9024,plain,
multiply(inverse(sk_c4),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_8942,c_8566]) ).
tff(c_9033,plain,
sk_c6 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_8801,c_7935,c_9024]) ).
tff(c_8803,plain,
multiply(sk_c4,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8790,c_7956]) ).
tff(c_9040,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_9033,c_8803]) ).
tff(c_7968,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_7980,plain,
! [X_151,Y_152,Z_153] : ( multiply(multiply(X_151,Y_152),Z_153) = multiply(X_151,multiply(Y_152,Z_153)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_8016,plain,
! [Z_153] : ( multiply(sk_c7,multiply(sk_c1,Z_153)) = multiply(identity,Z_153) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_7980]) ).
tff(c_8036,plain,
! [Z_154] : ( multiply(sk_c7,multiply(sk_c1,Z_154)) = Z_154 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8016]) ).
tff(c_8048,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_7968,c_8036]) ).
tff(c_8052,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_8048,c_7918]) ).
tff(c_8019,plain,
! [Z_153] : ( multiply(sk_c6,multiply(sk_c2,Z_153)) = multiply(identity,Z_153) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_7980]) ).
tff(c_8063,plain,
! [Z_155] : ( multiply(sk_c6,multiply(sk_c2,Z_155)) = Z_155 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8019]) ).
tff(c_8075,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_7926,c_8063]) ).
tff(c_8022,plain,
! [X_2,Z_153] : ( multiply(inverse(X_2),multiply(X_2,Z_153)) = multiply(identity,Z_153) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_7980]) ).
tff(c_8167,plain,
! [X_159,Z_160] : ( multiply(inverse(X_159),multiply(X_159,Z_160)) = Z_160 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8022]) ).
tff(c_8197,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_8075,c_8167]) ).
tff(c_8262,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_8197]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_7974,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_7918,c_8]) ).
tff(c_8061,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( sk_c7 != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8048,c_7974,c_58]) ).
tff(c_8062,plain,
sk_c7 != sk_c5,
inference(splitLeft,[status(thm)],[c_8061]) ).
tff(c_8276,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_8262,c_8062]) ).
tff(c_8206,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_8048,c_8167]) ).
tff(c_8264,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_8206]) ).
tff(c_8277,plain,
multiply(sk_c6,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8262,c_7974]) ).
tff(c_8500,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8264,c_8277]) ).
tff(c_8501,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8276,c_8500]) ).
tff(c_8503,plain,
sk_c7 = sk_c5,
inference(splitRight,[status(thm)],[c_8061]) ).
tff(c_8504,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8052,c_8503]) ).
tff(c_8505,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_8802,plain,
multiply(sk_c6,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8790,c_8505]) ).
tff(c_8924,plain,
multiply(sk_c4,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8915,c_8802]) ).
tff(c_8539,plain,
! [Z_166] : ( multiply(sk_c6,multiply(sk_c4,Z_166)) = multiply(identity,Z_166) ),
inference(superposition,[status(thm),theory(equality)],[c_7939,c_8515]) ).
tff(c_8645,plain,
! [Z_170] : ( multiply(sk_c6,multiply(sk_c4,Z_170)) = Z_170 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8539]) ).
tff(c_8660,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_7956,c_8645]) ).
tff(c_8670,plain,
! [Z_5] : ( multiply(sk_c6,multiply(sk_c6,Z_5)) = multiply(sk_c5,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_8660,c_6]) ).
tff(c_9214,plain,
! [Z_179] : ( multiply(sk_c4,multiply(sk_c4,Z_179)) = Z_179 ),
inference(demodulation,[status(thm),theory(equality)],[c_9033,c_9033,c_2,c_8790,c_8670]) ).
tff(c_9247,plain,
multiply(sk_c4,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_8924,c_9214]) ).
tff(c_9258,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_9040,c_9247]) ).
tff(c_8805,plain,
multiply(sk_c7,sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_8790,c_7918]) ).
tff(c_9038,plain,
multiply(sk_c7,sk_c4) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_9033,c_8805]) ).
tff(c_9263,plain,
multiply(sk_c4,sk_c4) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_9258,c_9038]) ).
tff(c_9275,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8942,c_9263]) ).
tff(c_9276,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_9281,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9276,c_4]) ).
tff(c_9714,plain,
! [X_190,Y_191,Z_192] : ( multiply(multiply(X_190,Y_191),Z_192) = multiply(X_190,multiply(Y_191,Z_192)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9738,plain,
! [Z_192] : ( multiply(sk_c6,multiply(sk_c4,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_9281,c_9714]) ).
tff(c_9790,plain,
! [Z_195] : ( multiply(sk_c6,multiply(sk_c4,Z_195)) = Z_195 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9738]) ).
tff(c_9802,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9309,c_9790]) ).
tff(c_9277,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_9304,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9277,c_42]) ).
tff(c_7917,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_7922,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_7917,c_4]) ).
tff(c_9741,plain,
! [Z_192] : ( multiply(sk_c7,multiply(sk_c3,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_7922,c_9714]) ).
tff(c_9813,plain,
! [Z_196] : ( multiply(sk_c7,multiply(sk_c3,Z_196)) = Z_196 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9741]) ).
tff(c_9825,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9304,c_9813]) ).
tff(c_9332,plain,
! [X_180,Y_181,Z_182] : ( multiply(multiply(X_180,Y_181),Z_182) = multiply(X_180,multiply(Y_181,Z_182)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9359,plain,
! [Z_182] : ( multiply(sk_c6,multiply(sk_c4,Z_182)) = multiply(identity,Z_182) ),
inference(superposition,[status(thm),theory(equality)],[c_9281,c_9332]) ).
tff(c_9460,plain,
! [Z_186] : ( multiply(sk_c6,multiply(sk_c4,Z_186)) = Z_186 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9359]) ).
tff(c_9472,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9309,c_9460]) ).
tff(c_9318,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_9365,plain,
! [Z_182] : ( multiply(sk_c7,multiply(sk_c1,Z_182)) = multiply(identity,Z_182) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_9332]) ).
tff(c_9400,plain,
! [Z_184] : ( multiply(sk_c7,multiply(sk_c1,Z_184)) = Z_184 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9365]) ).
tff(c_9412,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_9318,c_9400]) ).
tff(c_9424,plain,
! [Z_185] : ( multiply(sk_c1,multiply(sk_c7,Z_185)) = multiply(sk_c6,Z_185) ),
inference(superposition,[status(thm),theory(equality)],[c_9318,c_9332]) ).
tff(c_9439,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c1,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_9412,c_9424]) ).
tff(c_9452,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_9318,c_9439]) ).
tff(c_9476,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9472,c_9452]) ).
tff(c_9484,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9476,c_9476,c_9472]) ).
tff(c_9371,plain,
! [X_2,Z_182] : ( multiply(inverse(X_2),multiply(X_2,Z_182)) = multiply(identity,Z_182) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9332]) ).
tff(c_9383,plain,
! [X_2,Z_182] : ( multiply(inverse(X_2),multiply(X_2,Z_182)) = Z_182 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9371]) ).
tff(c_9617,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_9484,c_9383]) ).
tff(c_9623,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_9617]) ).
tff(c_9416,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9412,c_7918]) ).
tff(c_9660,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_9623,c_9416]) ).
tff(c_38,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_9325,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_9277,c_38]) ).
tff(c_9489,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9476,c_9325]) ).
tff(c_9700,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9623,c_2,c_9623,c_9489]) ).
tff(c_9701,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9660,c_9700]) ).
tff(c_9702,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_10046,plain,
! [Z_201] : ( multiply(sk_c6,multiply(sk_c7,Z_201)) = multiply(sk_c5,Z_201) ),
inference(superposition,[status(thm),theory(equality)],[c_9702,c_9714]) ).
tff(c_10061,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_9825,c_10046]) ).
tff(c_10071,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9802,c_10061]) ).
tff(c_9750,plain,
! [X_2,Z_192] : ( multiply(inverse(X_2),multiply(X_2,Z_192)) = multiply(identity,Z_192) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9714]) ).
tff(c_9762,plain,
! [X_2,Z_192] : ( multiply(inverse(X_2),multiply(X_2,Z_192)) = Z_192 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9750]) ).
tff(c_10075,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10071,c_9762]) ).
tff(c_10081,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10075]) ).
tff(c_10088,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10081,c_10081,c_9825]) ).
tff(c_10097,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10088]) ).
tff(c_10092,plain,
multiply(identity,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10081,c_7918]) ).
tff(c_10098,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10092]) ).
tff(c_10132,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_10097,c_10098]) ).
tff(c_10135,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10097,c_10097,c_9802]) ).
tff(c_10146,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10135]) ).
tff(c_10156,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10132,c_10146]) ).
tff(c_10158,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_28,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_10183,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_10158,c_28]) ).
tff(c_10263,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10183,c_58]) ).
tff(c_10264,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_10263]) ).
tff(c_10157,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_32,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_10202,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_10158,c_32]) ).
tff(c_10162,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10157,c_4]) ).
tff(c_10216,plain,
! [X_203,Y_204,Z_205] : ( multiply(multiply(X_203,Y_204),Z_205) = multiply(X_203,multiply(Y_204,Z_205)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_10243,plain,
! [Z_205] : ( multiply(sk_c7,multiply(sk_c3,Z_205)) = multiply(identity,Z_205) ),
inference(superposition,[status(thm),theory(equality)],[c_10162,c_10216]) ).
tff(c_10317,plain,
! [Z_209] : ( multiply(sk_c7,multiply(sk_c3,Z_209)) = Z_209 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10243]) ).
tff(c_10329,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_10202,c_10317]) ).
tff(c_10455,plain,
! [Z_213] : ( multiply(sk_c3,multiply(sk_c6,Z_213)) = multiply(sk_c7,Z_213) ),
inference(superposition,[status(thm),theory(equality)],[c_10202,c_10216]) ).
tff(c_10482,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_10183,c_10455]) ).
tff(c_10493,plain,
multiply(sk_c3,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10329,c_10482]) ).
tff(c_10249,plain,
! [X_2,Z_205] : ( multiply(inverse(X_2),multiply(X_2,Z_205)) = multiply(identity,Z_205) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_10216]) ).
tff(c_10260,plain,
! [X_2,Z_205] : ( multiply(inverse(X_2),multiply(X_2,Z_205)) = Z_205 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10249]) ).
tff(c_10497,plain,
multiply(inverse(sk_c3),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10493,c_10260]) ).
tff(c_10506,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10157,c_10497]) ).
tff(c_10508,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10264,c_10506]) ).
tff(c_10510,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_10263]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_10197,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10158,c_36]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_10166,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10158,c_34]) ).
tff(c_10170,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10166,c_4]) ).
tff(c_10240,plain,
! [Z_205] : ( multiply(sk_c6,multiply(sk_c4,Z_205)) = multiply(identity,Z_205) ),
inference(superposition,[status(thm),theory(equality)],[c_10170,c_10216]) ).
tff(c_10518,plain,
! [Z_214] : ( multiply(sk_c6,multiply(sk_c4,Z_214)) = Z_214 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10240]) ).
tff(c_10530,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10197,c_10518]) ).
tff(c_11205,plain,
! [Z_227] : ( multiply(sk_c3,multiply(sk_c6,Z_227)) = multiply(sk_c7,Z_227) ),
inference(superposition,[status(thm),theory(equality)],[c_10202,c_10216]) ).
tff(c_11223,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_10530,c_11205]) ).
tff(c_11239,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10510,c_11223]) ).
tff(c_10601,plain,
! [Z_217] : ( multiply(sk_c7,multiply(sk_c3,Z_217)) = Z_217 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10243]) ).
tff(c_10613,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_10202,c_10601]) ).
tff(c_11229,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_10183,c_11205]) ).
tff(c_11240,plain,
multiply(sk_c3,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10613,c_11229]) ).
tff(c_11252,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11239,c_11240]) ).
tff(c_11272,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11252,c_10202]) ).
tff(c_11279,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11239,c_11272]) ).
tff(c_11288,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11279,c_10157]) ).
tff(c_10642,plain,
! [Z_218] : ( multiply(sk_c3,multiply(sk_c6,Z_218)) = multiply(sk_c7,Z_218) ),
inference(superposition,[status(thm),theory(equality)],[c_10202,c_10216]) ).
tff(c_10660,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_10530,c_10642]) ).
tff(c_10676,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10510,c_10660]) ).
tff(c_10666,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_10183,c_10642]) ).
tff(c_10677,plain,
multiply(sk_c3,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10613,c_10666]) ).
tff(c_10689,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10676,c_10677]) ).
tff(c_10707,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_10689,c_10202]) ).
tff(c_10714,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10676,c_10707]) ).
tff(c_10724,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10714,c_10157]) ).
tff(c_10509,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_10263]) ).
tff(c_10617,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_10509]) ).
tff(c_10737,plain,
! [X2_219] :
( ( multiply(X2_219,sk_c5) != sk_c5 )
| ( inverse(X2_219) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10689,c_10689,c_10617]) ).
tff(c_10753,plain,
inverse(sk_c3) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_10676,c_10737]) ).
tff(c_10770,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10724,c_10753]) ).
tff(c_10771,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_10509]) ).
tff(c_10814,plain,
! [X3_220] :
( ( inverse(X3_220) != sk_c7 )
| ( multiply(X3_220,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_10771]) ).
tff(c_10835,plain,
( ( inverse(identity) != sk_c7 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_10814]) ).
tff(c_10837,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_10835]) ).
tff(c_10514,plain,
! [Z_5] : ( multiply(sk_c7,multiply(sk_c6,Z_5)) = multiply(sk_c5,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_10510,c_6]) ).
tff(c_10562,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_10530,c_10514]) ).
tff(c_10534,plain,
! [Z_215] : ( multiply(sk_c7,multiply(sk_c6,Z_215)) = multiply(sk_c5,Z_215) ),
inference(superposition,[status(thm),theory(equality)],[c_10510,c_6]) ).
tff(c_10549,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_10183,c_10534]) ).
tff(c_10796,plain,
multiply(sk_c5,sk_c7) = multiply(sk_c5,sk_c6),
inference(demodulation,[status(thm),theory(equality)],[c_10562,c_10549]) ).
tff(c_10840,plain,
! [X_221,Z_222] : ( multiply(inverse(X_221),multiply(X_221,Z_222)) = Z_222 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10249]) ).
tff(c_10858,plain,
multiply(inverse(sk_c5),multiply(sk_c5,sk_c6)) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10796,c_10840]) ).
tff(c_10928,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10260,c_10858]) ).
tff(c_10930,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10837,c_10928]) ).
tff(c_10932,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_10835]) ).
tff(c_10938,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_10932,c_10932,c_10613]) ).
tff(c_10947,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10530,c_10938]) ).
tff(c_10954,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10947,c_10932]) ).
tff(c_10931,plain,
inverse(identity) != sk_c7,
inference(splitRight,[status(thm)],[c_10835]) ).
tff(c_10982,plain,
inverse(identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10954,c_10931]) ).
tff(c_10962,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10947,c_75]) ).
tff(c_11002,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10962,c_4]) ).
tff(c_10555,plain,
multiply(sk_c7,identity) = multiply(sk_c5,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_79,c_10534]) ).
tff(c_10937,plain,
multiply(sk_c6,identity) = multiply(sk_c5,sk_c2),
inference(demodulation,[status(thm),theory(equality)],[c_10932,c_10555]) ).
tff(c_11052,plain,
multiply(sk_c5,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11002,c_10947,c_10937]) ).
tff(c_11056,plain,
! [Z_5] : ( multiply(sk_c5,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_11052,c_6]) ).
tff(c_11122,plain,
! [Z_225] : ( multiply(sk_c5,Z_225) = Z_225 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_11056]) ).
tff(c_10959,plain,
multiply(sk_c5,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10947,c_10170]) ).
tff(c_11128,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_11122,c_10959]) ).
tff(c_10960,plain,
inverse(sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10947,c_10166]) ).
tff(c_11155,plain,
inverse(identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11128,c_10960]) ).
tff(c_11159,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10982,c_11155]) ).
tff(c_11160,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_10771]) ).
tff(c_11170,plain,
! [X1_226] :
( ( multiply(X1_226,sk_c6) != sk_c7 )
| ( inverse(X1_226) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_11160]) ).
tff(c_11183,plain,
inverse(sk_c3) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10202,c_11170]) ).
tff(c_11195,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10157,c_11183]) ).
tff(c_11196,plain,
! [X4_7] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_11160]) ).
tff(c_11301,plain,
! [X4_228] :
( ( inverse(X4_228) != sk_c5 )
| ( multiply(X4_228,sk_c5) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11252,c_11252,c_11196]) ).
tff(c_11317,plain,
inverse(sk_c3) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11239,c_11301]) ).
tff(c_11334,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_11288,c_11317]) ).
tff(c_11336,plain,
inverse(sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_56,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_11374,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_11336,c_56]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_11361,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_11336,c_54]) ).
tff(c_11365,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11361,c_4]) ).
tff(c_11406,plain,
! [X_229,Y_230,Z_231] : ( multiply(multiply(X_229,Y_230),Z_231) = multiply(X_229,multiply(Y_230,Z_231)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11430,plain,
! [Z_231] : ( multiply(sk_c6,multiply(sk_c4,Z_231)) = multiply(identity,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_11365,c_11406]) ).
tff(c_11452,plain,
! [Z_232] : ( multiply(sk_c6,multiply(sk_c4,Z_232)) = Z_232 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11430]) ).
tff(c_11464,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11374,c_11452]) ).
tff(c_52,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_11381,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11336,c_52]) ).
tff(c_11335,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_11340,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11335,c_4]) ).
tff(c_11436,plain,
! [Z_231] : ( multiply(sk_c7,multiply(sk_c3,Z_231)) = multiply(identity,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_11340,c_11406]) ).
tff(c_11475,plain,
! [Z_233] : ( multiply(sk_c7,multiply(sk_c3,Z_233)) = Z_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11436]) ).
tff(c_11487,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11381,c_11475]) ).
tff(c_48,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_11392,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_11336,c_48]) ).
tff(c_11677,plain,
! [Z_239] : ( multiply(sk_c6,multiply(sk_c7,Z_239)) = multiply(sk_c5,Z_239) ),
inference(superposition,[status(thm),theory(equality)],[c_11392,c_11406]) ).
tff(c_11695,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_11487,c_11677]) ).
tff(c_11708,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11464,c_11695]) ).
tff(c_11439,plain,
! [X_2,Z_231] : ( multiply(inverse(X_2),multiply(X_2,Z_231)) = multiply(identity,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11406]) ).
tff(c_11450,plain,
! [X_2,Z_231] : ( multiply(inverse(X_2),multiply(X_2,Z_231)) = Z_231 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11439]) ).
tff(c_11712,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11708,c_11450]) ).
tff(c_11721,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11712]) ).
tff(c_11729,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_11721,c_11721,c_11487]) ).
tff(c_11740,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11729]) ).
tff(c_11427,plain,
! [Z_231] : ( multiply(sk_c4,multiply(sk_c5,Z_231)) = multiply(sk_c6,Z_231) ),
inference(superposition,[status(thm),theory(equality)],[c_11374,c_11406]) ).
tff(c_11715,plain,
multiply(sk_c6,sk_c7) = multiply(sk_c4,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_11708,c_11427]) ).
tff(c_11722,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11392,c_11374,c_11715]) ).
tff(c_11778,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11740,c_11722]) ).
tff(c_11492,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11392,c_58]) ).
tff(c_11493,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_11492]) ).
tff(c_11730,plain,
multiply(identity,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11721,c_11493]) ).
tff(c_11741,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11730]) ).
tff(c_11788,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_11778,c_11740,c_11741]) ).
tff(c_11790,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_11492]) ).
tff(c_11840,plain,
! [Z_243] : ( multiply(sk_c3,multiply(sk_c6,Z_243)) = multiply(sk_c7,Z_243) ),
inference(superposition,[status(thm),theory(equality)],[c_11381,c_11406]) ).
tff(c_11855,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_11464,c_11840]) ).
tff(c_11868,plain,
multiply(sk_c3,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11790,c_11855]) ).
tff(c_11861,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c3,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_11392,c_11840]) ).
tff(c_11893,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11868,c_11487,c_11861]) ).
tff(c_11897,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11893,c_11893,c_11464]) ).
tff(c_12504,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11897,c_11450]) ).
tff(c_12510,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12504]) ).
tff(c_12453,plain,
! [X_254,Z_255] : ( multiply(inverse(X_254),multiply(X_254,Z_255)) = Z_255 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11439]) ).
tff(c_12668,plain,
! [X_258,Z_259] : ( multiply(inverse(inverse(X_258)),Z_259) = multiply(X_258,Z_259) ),
inference(superposition,[status(thm),theory(equality)],[c_11450,c_12453]) ).
tff(c_12483,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12453]) ).
tff(c_12675,plain,
! [X_258] : ( multiply(X_258,identity) = X_258 ),
inference(superposition,[status(thm),theory(equality)],[c_12668,c_12483]) ).
tff(c_11968,plain,
! [X_244,Z_245] : ( multiply(inverse(X_244),multiply(X_244,Z_245)) = Z_245 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11439]) ).
tff(c_12174,plain,
! [X_247,Z_248] : ( multiply(inverse(inverse(X_247)),Z_248) = multiply(X_247,Z_248) ),
inference(superposition,[status(thm),theory(equality)],[c_11968,c_11450]) ).
tff(c_12010,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11968]) ).
tff(c_12181,plain,
! [X_247] : ( multiply(X_247,identity) = X_247 ),
inference(superposition,[status(thm),theory(equality)],[c_12174,c_12010]) ).
tff(c_11989,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_11897,c_11968]) ).
tff(c_12018,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11989]) ).
tff(c_11900,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_11893,c_11381]) ).
tff(c_11906,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11868,c_11900]) ).
tff(c_11789,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_11492]) ).
tff(c_11819,plain,
! [X2_242] :
( ( multiply(X2_242,sk_c5) != sk_c6 )
| ( inverse(X2_242) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_11789]) ).
tff(c_11826,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11374,c_11819]) ).
tff(c_11838,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_11361,c_11826]) ).
tff(c_11839,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_11789]) ).
tff(c_11921,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c5) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11906,c_11893,c_11906,c_11893,c_11893,c_11906,c_11906,c_11893,c_11839]) ).
tff(c_11922,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_11921]) ).
tff(c_12435,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_12181,c_12018,c_12018,c_12018,c_11922]) ).
tff(c_11916,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11906,c_11335]) ).
tff(c_11933,plain,
multiply(sk_c5,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11916,c_4]) ).
tff(c_12043,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12018,c_11933]) ).
tff(c_12025,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12018,c_11916]) ).
tff(c_12058,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12043,c_12025]) ).
tff(c_12437,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12435,c_12058]) ).
tff(c_12438,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c5 )
| ( inverse(X1_8) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_11921]) ).
tff(c_23701,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_12510,c_12675,c_12510,c_12510,c_12675,c_12510,c_12510,c_12510,c_12438]) ).
tff(c_23703,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_23701]) ).
tff(c_11915,plain,
multiply(sk_c5,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11906,c_11340]) ).
tff(c_12593,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12510,c_11915]) ).
tff(c_12527,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12510,c_11916]) ).
tff(c_12594,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12593,c_12527]) ).
tff(c_23705,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23703,c_12594]) ).
tff(c_23707,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_23701]) ).
tff(c_23709,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23707,c_12594]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : GRP289-1 : TPTP v9.0.0. Released v2.5.0.
% 0.08/0.10 % 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.10/0.29 % Computer : n029.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Mon Apr 7 21:40:49 EDT 2025
% 0.10/0.29 % CPUTime :
% 16.45/5.42 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.74/5.55
% 16.74/5.55 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------