%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP358-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n031.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:26:02 PM UTC 2025
% Result : Unsatisfiable 19.08s 6.79s
% Output : CNFRefutation 19.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 29
% Syntax : Number of formulae : 438 ( 365 unt; 0 typ; 0 def)
% Number of atoms : 602 ( 582 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 339 ( 175 ~; 164 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 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 : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 202 ( 202 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_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_86,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c5) = sk_c6 ) ),
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_113,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(sk_c7,sk_c6) != sk_c8 )
| ( inverse(sk_c8) != sk_c6 )
| ( multiply(sk_c8,X3) != sk_c7 )
| ( multiply(X4,sk_c8) != X3 )
| ( inverse(X4) != sk_c8 )
| ( multiply(X1,sk_c8) != sk_c7 )
| ( inverse(X1) != sk_c8 )
| ( multiply(X2,sk_c7) != sk_c6 )
| ( inverse(X2) != sk_c7 )
| ( inverse(X5) != sk_c6 )
| ( multiply(X5,sk_c8) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c8,sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c8 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c8) = sk_c6 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
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_22,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_98,plain,
inverse(sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_102,plain,
multiply(sk_c6,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_64,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_85,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_64]) ).
tff(c_89,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_38542,plain,
! [X_373,Y_374,Z_375] : ( multiply(multiply(X_373,Y_374),Z_375) = multiply(X_373,multiply(Y_374,Z_375)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_38575,plain,
! [Z_375] : ( multiply(sk_c6,multiply(sk_c8,Z_375)) = multiply(identity,Z_375) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_38542]) ).
tff(c_38596,plain,
! [Z_376] : ( multiply(sk_c6,multiply(sk_c8,Z_376)) = Z_376 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38575]) ).
tff(c_38611,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_89,c_38596]) ).
tff(c_14935,plain,
! [X_170,Y_171,Z_172] : ( multiply(multiply(X_170,Y_171),Z_172) = multiply(X_170,multiply(Y_171,Z_172)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14977,plain,
! [X_2,Z_172] : ( multiply(inverse(X_2),multiply(X_2,Z_172)) = multiply(identity,Z_172) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14935]) ).
tff(c_14990,plain,
! [X_2,Z_172] : ( multiply(inverse(X_2),multiply(X_2,Z_172)) = Z_172 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14977]) ).
tff(c_15908,plain,
! [X_191,Z_192] : ( multiply(inverse(X_191),multiply(X_191,Z_192)) = Z_192 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14977]) ).
tff(c_16149,plain,
! [X_195,Z_196] : ( multiply(inverse(inverse(X_195)),Z_196) = multiply(X_195,Z_196) ),
inference(superposition,[status(thm),theory(equality)],[c_14990,c_15908]) ).
tff(c_15947,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_15908]) ).
tff(c_16156,plain,
! [X_195] : ( multiply(X_195,identity) = X_195 ),
inference(superposition,[status(thm),theory(equality)],[c_16149,c_15947]) ).
tff(c_14971,plain,
! [Z_172] : ( multiply(sk_c6,multiply(sk_c8,Z_172)) = multiply(identity,Z_172) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_14935]) ).
tff(c_14992,plain,
! [Z_173] : ( multiply(sk_c6,multiply(sk_c8,Z_173)) = Z_173 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14971]) ).
tff(c_15007,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_89,c_14992]) ).
tff(c_13440,plain,
! [X_141,Y_142,Z_143] : ( multiply(multiply(X_141,Y_142),Z_143) = multiply(X_141,multiply(Y_142,Z_143)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13479,plain,
! [Z_143] : ( multiply(sk_c6,multiply(sk_c8,Z_143)) = multiply(identity,Z_143) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_13440]) ).
tff(c_13500,plain,
! [Z_144] : ( multiply(sk_c6,multiply(sk_c8,Z_144)) = Z_144 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13479]) ).
tff(c_13518,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_89,c_13500]) ).
tff(c_40,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_120,plain,
multiply(sk_c8,sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_50,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_127,plain,
multiply(sk_c1,sk_c8) = sk_c2,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_149,plain,
! [X_13,Y_14,Z_15] : ( multiply(multiply(X_13,Y_14),Z_15) = multiply(X_13,multiply(Y_14,Z_15)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_176,plain,
! [Z_15] : ( multiply(sk_c8,multiply(sk_c1,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_149]) ).
tff(c_225,plain,
! [Z_17] : ( multiply(sk_c8,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_176]) ).
tff(c_240,plain,
multiply(sk_c8,sk_c2) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_127,c_225]) ).
tff(c_244,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_120,c_240]) ).
tff(c_68,plain,
! [X5_6,X2_9,X1_8,X4_10] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 )
| ( inverse(sk_c8) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_258,plain,
! [X5_6,X2_9,X1_8,X4_10] :
( ( multiply(X5_6,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_10,sk_c7)) != sk_c7 )
| ( inverse(sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_244,c_244,c_244,c_244,c_244,c_244,c_244,c_244,c_68]) ).
tff(c_259,plain,
multiply(sk_c7,sk_c6) != sk_c7,
inference(splitLeft,[status(thm)],[c_258]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_113,plain,
multiply(sk_c7,sk_c6) = sk_c8,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_249,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_244,c_113]) ).
tff(c_297,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_259,c_249]) ).
tff(c_299,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(splitRight,[status(thm)],[c_258]) ).
tff(c_179,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_149]) ).
tff(c_189,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_399,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_299,c_189]) ).
tff(c_405,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_399]) ).
tff(c_307,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_179]) ).
tff(c_510,plain,
! [X_21,Z_22] : ( multiply(inverse(inverse(X_21)),Z_22) = multiply(X_21,Z_22) ),
inference(superposition,[status(thm),theory(equality)],[c_189,c_307]) ).
tff(c_337,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_307]) ).
tff(c_517,plain,
! [X_21] : ( multiply(X_21,identity) = X_21 ),
inference(superposition,[status(thm),theory(equality)],[c_510,c_337]) ).
tff(c_250,plain,
multiply(sk_c6,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_244,c_102]) ).
tff(c_443,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_405,c_250]) ).
tff(c_173,plain,
! [Z_15] : ( multiply(sk_c6,multiply(sk_c8,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_149]) ).
tff(c_191,plain,
! [Z_16] : ( multiply(sk_c6,multiply(sk_c8,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_173]) ).
tff(c_206,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_89,c_191]) ).
tff(c_409,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_405,c_206]) ).
tff(c_410,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_409]) ).
tff(c_253,plain,
inverse(sk_c1) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_244,c_85]) ).
tff(c_416,plain,
inverse(identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_410,c_253]) ).
tff(c_445,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_443,c_416]) ).
tff(c_298,plain,
! [X4_10,X1_8,X2_9,X5_6] :
( ( inverse(sk_c7) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_10,sk_c7)) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_258]) ).
tff(c_8377,plain,
! [X4_10,X1_8,X2_9,X5_6] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( identity != X5_6 )
| ( inverse(X5_6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_405,c_517,c_443,c_405,c_517,c_443,c_405,c_443,c_517,c_443,c_443,c_443,c_517,c_443,c_443,c_2,c_443,c_443,c_445,c_443,c_405,c_298]) ).
tff(c_8379,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8377]) ).
tff(c_8381,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8379,c_445]) ).
tff(c_8382,plain,
! [X2_9,X1_8,X4_10] :
( ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 ) ),
inference(splitRight,[status(thm)],[c_8377]) ).
tff(c_12713,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8382]) ).
tff(c_12715,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12713,c_445]) ).
tff(c_12716,plain,
! [X1_8,X2_9] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(splitRight,[status(thm)],[c_8382]) ).
tff(c_12718,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_12716]) ).
tff(c_12720,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12718,c_445]) ).
tff(c_13373,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_12716]) ).
tff(c_13375,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13373,c_445]) ).
tff(c_13377,plain,
multiply(sk_c1,sk_c8) != sk_c2,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_46,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_13406,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_13377,c_46]) ).
tff(c_13410,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13406,c_4]) ).
tff(c_13512,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_13410,c_13500]) ).
tff(c_13789,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13518,c_13512]) ).
tff(c_44,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_13421,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_13377,c_44]) ).
tff(c_13790,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13789,c_13421]) ).
tff(c_13482,plain,
! [Z_143] : ( multiply(sk_c8,multiply(sk_c1,Z_143)) = multiply(identity,Z_143) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_13440]) ).
tff(c_13807,plain,
! [Z_151] : ( multiply(sk_c8,multiply(sk_c1,Z_151)) = Z_151 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13482]) ).
tff(c_13822,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_13790,c_13807]) ).
tff(c_13496,plain,
! [Z_143] : ( multiply(sk_c6,multiply(sk_c8,Z_143)) = Z_143 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13479]) ).
tff(c_13830,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13822,c_13496]) ).
tff(c_13836,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_13830]) ).
tff(c_13515,plain,
multiply(sk_c6,sk_c7) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_120,c_13500]) ).
tff(c_13842,plain,
multiply(sk_c6,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_13836,c_13515]) ).
tff(c_13849,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13518,c_13842]) ).
tff(c_13799,plain,
sk_c7 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_13790,c_13377]) ).
tff(c_13839,plain,
sk_c2 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_13836,c_13799]) ).
tff(c_13893,plain,
sk_c1 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_13849,c_13839]) ).
tff(c_13847,plain,
multiply(identity,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_13836,c_113]) ).
tff(c_13850,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13847]) ).
tff(c_13886,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13850,c_98]) ).
tff(c_13885,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13850,c_102]) ).
tff(c_13485,plain,
! [X_2,Z_143] : ( multiply(inverse(X_2),multiply(X_2,Z_143)) = multiply(identity,Z_143) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13440]) ).
tff(c_13979,plain,
! [X_154,Z_155] : ( multiply(inverse(X_154),multiply(X_154,Z_155)) = Z_155 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13485]) ).
tff(c_14000,plain,
multiply(inverse(sk_c6),identity) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_13885,c_13979]) ).
tff(c_14029,plain,
sk_c6 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_13518,c_13886,c_14000]) ).
tff(c_13376,plain,
inverse(sk_c4) = sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_13381,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13376,c_4]) ).
tff(c_13844,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13836,c_13381]) ).
tff(c_13954,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_13844,c_2]) ).
tff(c_48,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_13429,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_13377,c_48]) ).
tff(c_13458,plain,
! [Z_143] : ( multiply(sk_c4,multiply(sk_c7,Z_143)) = multiply(sk_c6,Z_143) ),
inference(superposition,[status(thm),theory(equality)],[c_13429,c_13440]) ).
tff(c_14094,plain,
! [Z_143] : ( multiply(sk_c1,Z_143) = Z_143 ),
inference(demodulation,[status(thm),theory(equality)],[c_14029,c_2,c_13954,c_2,c_13836,c_13458]) ).
tff(c_14045,plain,
sk_c8 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_14029,c_13850]) ).
tff(c_13838,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_13836,c_13822]) ).
tff(c_14081,plain,
multiply(sk_c1,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_14045,c_14045,c_13838]) ).
tff(c_14095,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14094,c_14081]) ).
tff(c_14097,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13893,c_14095]) ).
tff(c_14099,plain,
multiply(sk_c8,sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_34,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_14889,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_14099,c_34]) ).
tff(c_14893,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14889,c_4]) ).
tff(c_15004,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_14893,c_14992]) ).
tff(c_15156,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_15007,c_15004]) ).
tff(c_14112,plain,
multiply(sk_c1,sk_c8) = sk_c2,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_14169,plain,
! [X_156,Y_157,Z_158] : ( multiply(multiply(X_156,Y_157),Z_158) = multiply(X_156,multiply(Y_157,Z_158)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14211,plain,
! [Z_158] : ( multiply(sk_c8,multiply(sk_c1,Z_158)) = multiply(identity,Z_158) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_14169]) ).
tff(c_14659,plain,
! [Z_166] : ( multiply(sk_c8,multiply(sk_c1,Z_166)) = Z_166 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14211]) ).
tff(c_14680,plain,
multiply(sk_c8,sk_c2) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_14112,c_14659]) ).
tff(c_14208,plain,
! [Z_158] : ( multiply(sk_c6,multiply(sk_c8,Z_158)) = multiply(identity,Z_158) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_14169]) ).
tff(c_14225,plain,
! [Z_158] : ( multiply(sk_c6,multiply(sk_c8,Z_158)) = Z_158 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14208]) ).
tff(c_14691,plain,
multiply(sk_c6,sk_c8) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_14680,c_14225]) ).
tff(c_14698,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_14691]) ).
tff(c_14229,plain,
! [Z_159] : ( multiply(sk_c6,multiply(sk_c8,Z_159)) = Z_159 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14208]) ).
tff(c_14244,plain,
multiply(sk_c6,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_89,c_14229]) ).
tff(c_14121,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_14099,c_34]) ).
tff(c_14125,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14121,c_4]) ).
tff(c_14241,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_14125,c_14229]) ).
tff(c_14581,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_14244,c_14241]) ).
tff(c_32,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_14161,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14099,c_32]) ).
tff(c_14582,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_14581,c_14161]) ).
tff(c_14585,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14112,c_14582]) ).
tff(c_14596,plain,
multiply(sk_c2,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_14585,c_113]) ).
tff(c_14703,plain,
multiply(identity,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_14698,c_14596]) ).
tff(c_14711,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14703]) ).
tff(c_14595,plain,
multiply(sk_c8,sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14585,c_14099]) ).
tff(c_14684,plain,
sk_c8 != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_14680,c_14595]) ).
tff(c_14700,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_14698,c_14684]) ).
tff(c_14780,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_14711,c_14700]) ).
tff(c_14098,plain,
inverse(sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_42,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_14156,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_14099,c_42]) ).
tff(c_14214,plain,
! [X_2,Z_158] : ( multiply(inverse(X_2),multiply(X_2,Z_158)) = multiply(identity,Z_158) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14169]) ).
tff(c_14717,plain,
! [X_167,Z_168] : ( multiply(inverse(X_167),multiply(X_167,Z_168)) = Z_168 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14214]) ).
tff(c_14747,plain,
multiply(inverse(sk_c5),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_14156,c_14717]) ).
tff(c_14776,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_14098,c_14747]) ).
tff(c_14862,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14711,c_14776]) ).
tff(c_14227,plain,
! [X_2,Z_158] : ( multiply(inverse(X_2),multiply(X_2,Z_158)) = Z_158 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14214]) ).
tff(c_14866,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_14862,c_14227]) ).
tff(c_14872,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_14866]) ).
tff(c_14874,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14780,c_14872]) ).
tff(c_14876,plain,
multiply(sk_c1,sk_c8) != sk_c2,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_14911,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14876,c_44]) ).
tff(c_15157,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_15156,c_14911]) ).
tff(c_14974,plain,
! [Z_172] : ( multiply(sk_c8,multiply(sk_c1,Z_172)) = multiply(identity,Z_172) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_14935]) ).
tff(c_15199,plain,
! [Z_177] : ( multiply(sk_c8,multiply(sk_c1,Z_177)) = Z_177 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14974]) ).
tff(c_15214,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_15157,c_15199]) ).
tff(c_14988,plain,
! [Z_172] : ( multiply(sk_c6,multiply(sk_c8,Z_172)) = Z_172 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14971]) ).
tff(c_15221,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_15214,c_14988]) ).
tff(c_15227,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_15221]) ).
tff(c_15237,plain,
multiply(identity,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_15227,c_113]) ).
tff(c_15239,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15237]) ).
tff(c_15229,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_15227,c_15214]) ).
tff(c_16015,plain,
sk_c6 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_15239,c_15007,c_15239,c_15229]) ).
tff(c_14875,plain,
inverse(sk_c4) = sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_15235,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15227,c_14875]) ).
tff(c_15890,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_15235,c_4]) ).
tff(c_15979,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_15890,c_14990]) ).
tff(c_15991,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15979]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( multiply(sk_c8,sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_14925,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_14099,c_36]) ).
tff(c_15233,plain,
multiply(sk_c4,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15227,c_14925]) ).
tff(c_16072,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16015,c_2,c_15991,c_15233]) ).
tff(c_16020,plain,
sk_c8 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_16015,c_15239]) ).
tff(c_16075,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16072,c_16020]) ).
tff(c_16076,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16072,c_16015]) ).
tff(c_15250,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15239,c_98]) ).
tff(c_15267,plain,
multiply(sk_c6,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_15250,c_4]) ).
tff(c_54,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c1,sk_c8) = sk_c2 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_14918,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_14876,c_54]) ).
tff(c_15248,plain,
multiply(sk_c5,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15239,c_14918]) ).
tff(c_15316,plain,
! [X_178,Z_179] : ( multiply(inverse(X_178),multiply(X_178,Z_179)) = Z_179 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14977]) ).
tff(c_15340,plain,
multiply(inverse(sk_c5),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_15248,c_15316]) ).
tff(c_15376,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15267,c_14098,c_15340]) ).
tff(c_15488,plain,
! [X_181,Z_182] : ( multiply(inverse(inverse(X_181)),Z_182) = multiply(X_181,Z_182) ),
inference(superposition,[status(thm),theory(equality)],[c_15316,c_14990]) ).
tff(c_15367,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_15316]) ).
tff(c_15495,plain,
! [X_181] : ( multiply(X_181,identity) = X_181 ),
inference(superposition,[status(thm),theory(equality)],[c_15488,c_15367]) ).
tff(c_15400,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15376,c_15239]) ).
tff(c_15022,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_15007,c_15004]) ).
tff(c_15023,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_15022,c_14911]) ).
tff(c_15040,plain,
! [Z_174] : ( multiply(sk_c8,multiply(sk_c1,Z_174)) = Z_174 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14974]) ).
tff(c_15055,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_15023,c_15040]) ).
tff(c_15062,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_15055,c_14988]) ).
tff(c_15068,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_15062]) ).
tff(c_15111,plain,
multiply(identity,sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_15068,c_113]) ).
tff(c_15112,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15111]) ).
tff(c_15020,plain,
! [X5_6,X2_9,X1_8,X4_10] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_113,c_98,c_68]) ).
tff(c_15070,plain,
! [X4_175] :
( ( inverse(X4_175) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_175,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_15020]) ).
tff(c_15084,plain,
( ( inverse(sk_c5) != sk_c8 )
| ( multiply(sk_c8,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_14918,c_15070]) ).
tff(c_15100,plain,
( ( sk_c8 != sk_c6 )
| ( multiply(sk_c8,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14098,c_15084]) ).
tff(c_15146,plain,
multiply(sk_c6,sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_15112,c_15068,c_15112,c_15100]) ).
tff(c_15123,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15112,c_98]) ).
tff(c_15150,plain,
multiply(sk_c6,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_15123,c_4]) ).
tff(c_15154,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15146,c_15150]) ).
tff(c_15155,plain,
! [X1_8,X2_9,X5_6] :
( ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_15020]) ).
tff(c_15244,plain,
! [X1_8,X2_9,X5_6] :
( ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != identity )
| ( inverse(X2_9) != identity )
| ( multiply(X2_9,identity) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15227,c_15227,c_15227,c_15155]) ).
tff(c_15245,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_15244]) ).
tff(c_15872,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_15376,c_15495,c_15400,c_15376,c_15245]) ).
tff(c_15399,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15376,c_15376,c_15250]) ).
tff(c_15874,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15872,c_15399]) ).
tff(c_15875,plain,
! [X2_9,X1_8] :
( ( inverse(X2_9) != identity )
| ( multiply(X2_9,identity) != sk_c6 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != identity ) ),
inference(splitRight,[status(thm)],[c_15244]) ).
tff(c_37655,plain,
! [X2_9,X1_8] :
( ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16156,c_16075,c_16075,c_16156,c_16076,c_15875]) ).
tff(c_37657,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_37655]) ).
tff(c_15995,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15991,c_15235]) ).
tff(c_37659,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37657,c_15995]) ).
tff(c_37662,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_37655]) ).
tff(c_37664,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37662,c_15995]) ).
tff(c_37665,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_37670,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37665,c_4]) ).
tff(c_38608,plain,
multiply(sk_c6,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_37670,c_38596]) ).
tff(c_38623,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_38611,c_38608]) ).
tff(c_37666,plain,
multiply(sk_c7,sk_c6) != sk_c8,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_8,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_38525,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_37666,c_8]) ).
tff(c_38632,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_38623,c_38525]) ).
tff(c_38578,plain,
! [Z_375] : ( multiply(sk_c8,multiply(sk_c1,Z_375)) = multiply(identity,Z_375) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_38542]) ).
tff(c_38650,plain,
! [Z_377] : ( multiply(sk_c8,multiply(sk_c1,Z_377)) = Z_377 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38578]) ).
tff(c_38665,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_38632,c_38650]) ).
tff(c_38592,plain,
! [Z_375] : ( multiply(sk_c6,multiply(sk_c8,Z_375)) = Z_375 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38575]) ).
tff(c_38672,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_38665,c_38592]) ).
tff(c_38678,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_38672]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_37679,plain,
inverse(sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_37666,c_14]) ).
tff(c_37683,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37679,c_4]) ).
tff(c_38712,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38678,c_37683]) ).
tff(c_38844,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_38712,c_2]) ).
tff(c_12,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_38518,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_37666,c_12]) ).
tff(c_38710,plain,
multiply(sk_c4,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38678,c_38518]) ).
tff(c_38875,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38844,c_38710]) ).
tff(c_38714,plain,
multiply(identity,sk_c6) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_38678,c_37666]) ).
tff(c_38716,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38714]) ).
tff(c_38877,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_38875,c_38716]) ).
tff(c_38713,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38678,c_37679]) ).
tff(c_38854,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38844,c_38713]) ).
tff(c_38878,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_38875,c_38611]) ).
tff(c_38886,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38878]) ).
tff(c_38896,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_38886,c_85]) ).
tff(c_38898,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38854,c_38896]) ).
tff(c_38908,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38877,c_38898]) ).
tff(c_38910,plain,
inverse(sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_24,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_38952,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_38910,c_24]) ).
tff(c_26,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_38922,plain,
inverse(sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_38910,c_26]) ).
tff(c_38926,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38922,c_4]) ).
tff(c_38983,plain,
! [X_381,Y_382,Z_383] : ( multiply(multiply(X_381,Y_382),Z_383) = multiply(X_381,multiply(Y_382,Z_383)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_39010,plain,
! [Z_383] : ( multiply(sk_c7,multiply(sk_c4,Z_383)) = multiply(identity,Z_383) ),
inference(superposition,[status(thm),theory(equality)],[c_38926,c_38983]) ).
tff(c_39116,plain,
! [Z_388] : ( multiply(sk_c7,multiply(sk_c4,Z_388)) = Z_388 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39010]) ).
tff(c_39134,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_38952,c_39116]) ).
tff(c_39019,plain,
! [X_2,Z_383] : ( multiply(inverse(X_2),multiply(X_2,Z_383)) = multiply(identity,Z_383) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_38983]) ).
tff(c_39164,plain,
! [X_389,Z_390] : ( multiply(inverse(X_389),multiply(X_389,Z_390)) = Z_390 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39019]) ).
tff(c_39182,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_39134,c_39164]) ).
tff(c_39222,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39182]) ).
tff(c_30,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_38961,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_38910,c_30]) ).
tff(c_28,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( inverse(sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_38930,plain,
inverse(sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_38910,c_28]) ).
tff(c_38934,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38930,c_4]) ).
tff(c_39007,plain,
! [Z_383] : ( multiply(sk_c6,multiply(sk_c5,Z_383)) = multiply(identity,Z_383) ),
inference(superposition,[status(thm),theory(equality)],[c_38934,c_38983]) ).
tff(c_39033,plain,
! [Z_384] : ( multiply(sk_c6,multiply(sk_c5,Z_384)) = Z_384 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39007]) ).
tff(c_39045,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_38961,c_39033]) ).
tff(c_39004,plain,
! [Z_383] : ( multiply(sk_c4,multiply(sk_c7,Z_383)) = multiply(sk_c6,Z_383) ),
inference(superposition,[status(thm),theory(equality)],[c_38952,c_38983]) ).
tff(c_39141,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c4,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_39134,c_39004]) ).
tff(c_39147,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39045,c_38952,c_39141]) ).
tff(c_39156,plain,
inverse(sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39147,c_38910]) ).
tff(c_39294,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_39222,c_39222,c_39156]) ).
tff(c_38909,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_39157,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39147,c_38909]) ).
tff(c_39245,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39222,c_39157]) ).
tff(c_39252,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39245,c_4]) ).
tff(c_39031,plain,
! [X_2,Z_383] : ( multiply(inverse(X_2),multiply(X_2,Z_383)) = Z_383 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39019]) ).
tff(c_39259,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_39252,c_39031]) ).
tff(c_39271,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39259]) ).
tff(c_39275,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39271,c_39245]) ).
tff(c_39323,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_39294,c_39275]) ).
tff(c_39325,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_60,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_49385,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_39325,c_60]) ).
tff(c_62,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_39333,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_39334,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_39325,c_39333]) ).
tff(c_39335,plain,
inverse(sk_c4) = sk_c7,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_39340,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39335,c_4]) ).
tff(c_49406,plain,
! [X_513,Y_514,Z_515] : ( multiply(multiply(X_513,Y_514),Z_515) = multiply(X_513,multiply(Y_514,Z_515)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_49430,plain,
! [Z_515] : ( multiply(sk_c7,multiply(sk_c4,Z_515)) = multiply(identity,Z_515) ),
inference(superposition,[status(thm),theory(equality)],[c_39340,c_49406]) ).
tff(c_49452,plain,
! [Z_516] : ( multiply(sk_c7,multiply(sk_c4,Z_516)) = Z_516 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49430]) ).
tff(c_49464,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_49385,c_49452]) ).
tff(c_49439,plain,
! [X_2,Z_515] : ( multiply(inverse(X_2),multiply(X_2,Z_515)) = multiply(identity,Z_515) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_49406]) ).
tff(c_49567,plain,
! [X_520,Z_521] : ( multiply(inverse(X_520),multiply(X_520,Z_521)) = Z_521 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49439]) ).
tff(c_49597,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_49464,c_49567]) ).
tff(c_49630,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_49597]) ).
tff(c_49498,plain,
! [Z_518] : ( multiply(sk_c4,multiply(sk_c7,Z_518)) = multiply(sk_c6,Z_518) ),
inference(superposition,[status(thm),theory(equality)],[c_49385,c_49406]) ).
tff(c_49513,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c4,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_49464,c_49498]) ).
tff(c_49523,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49385,c_49513]) ).
tff(c_66,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_49374,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_39325,c_66]) ).
tff(c_39324,plain,
inverse(sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_39329,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39324,c_4]) ).
tff(c_49436,plain,
! [Z_515] : ( multiply(sk_c6,multiply(sk_c5,Z_515)) = multiply(identity,Z_515) ),
inference(superposition,[status(thm),theory(equality)],[c_39329,c_49406]) ).
tff(c_49531,plain,
! [Z_519] : ( multiply(sk_c6,multiply(sk_c5,Z_519)) = Z_519 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49436]) ).
tff(c_49543,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_49374,c_49531]) ).
tff(c_49547,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49523,c_49543]) ).
tff(c_39414,plain,
! [X_392,Y_393,Z_394] : ( multiply(multiply(X_392,Y_393),Z_394) = multiply(X_392,multiply(Y_393,Z_394)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_39450,plain,
! [X_2,Z_394] : ( multiply(inverse(X_2),multiply(X_2,Z_394)) = multiply(identity,Z_394) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39414]) ).
tff(c_39462,plain,
! [X_2,Z_394] : ( multiply(inverse(X_2),multiply(X_2,Z_394)) = Z_394 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39450]) ).
tff(c_40464,plain,
! [X_415,Z_416] : ( multiply(inverse(X_415),multiply(X_415,Z_416)) = Z_416 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39450]) ).
tff(c_40913,plain,
! [X_423,Z_424] : ( multiply(inverse(inverse(X_423)),Z_424) = multiply(X_423,Z_424) ),
inference(superposition,[status(thm),theory(equality)],[c_39462,c_40464]) ).
tff(c_40512,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_40464]) ).
tff(c_40934,plain,
! [X_423] : ( multiply(X_423,identity) = X_423 ),
inference(superposition,[status(thm),theory(equality)],[c_40913,c_40512]) ).
tff(c_39393,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_39325,c_60]) ).
tff(c_39444,plain,
! [Z_394] : ( multiply(sk_c7,multiply(sk_c4,Z_394)) = multiply(identity,Z_394) ),
inference(superposition,[status(thm),theory(equality)],[c_39340,c_39414]) ).
tff(c_39737,plain,
! [Z_401] : ( multiply(sk_c7,multiply(sk_c4,Z_401)) = Z_401 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39444]) ).
tff(c_39755,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_39393,c_39737]) ).
tff(c_40485,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_39755,c_40464]) ).
tff(c_40519,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_40485]) ).
tff(c_40527,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40519,c_39324]) ).
tff(c_56,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_39378,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_39325,c_56]) ).
tff(c_58,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_39365,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_39325,c_58]) ).
tff(c_39369,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_39365,c_4]) ).
tff(c_39438,plain,
! [Z_394] : ( multiply(sk_c8,multiply(sk_c3,Z_394)) = multiply(identity,Z_394) ),
inference(superposition,[status(thm),theory(equality)],[c_39369,c_39414]) ).
tff(c_39467,plain,
! [Z_395] : ( multiply(sk_c8,multiply(sk_c3,Z_395)) = Z_395 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39438]) ).
tff(c_39479,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_39378,c_39467]) ).
tff(c_39513,plain,
! [X_397,Z_398] : ( multiply(inverse(X_397),multiply(X_397,Z_398)) = Z_398 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39450]) ).
tff(c_39537,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_39479,c_39513]) ).
tff(c_39586,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39537]) ).
tff(c_39546,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_39393,c_39513]) ).
tff(c_39588,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_39335,c_39546]) ).
tff(c_39654,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39586,c_2,c_39586,c_39588]) ).
tff(c_39387,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_39325,c_66]) ).
tff(c_39447,plain,
! [Z_394] : ( multiply(sk_c6,multiply(sk_c5,Z_394)) = multiply(identity,Z_394) ),
inference(superposition,[status(thm),theory(equality)],[c_39329,c_39414]) ).
tff(c_39490,plain,
! [Z_396] : ( multiply(sk_c6,multiply(sk_c5,Z_396)) = Z_396 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39447]) ).
tff(c_39502,plain,
multiply(sk_c6,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_39387,c_39490]) ).
tff(c_39656,plain,
multiply(identity,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_39654,c_39654,c_39502]) ).
tff(c_39663,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39656]) ).
tff(c_39344,plain,
inverse(sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_39465,plain,
! [X5_6,X2_9,X1_8,X4_10] :
( ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 )
| ( multiply(sk_c7,sk_c6) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_39344,c_68]) ).
tff(c_39466,plain,
multiply(sk_c7,sk_c6) != sk_c8,
inference(splitLeft,[status(thm)],[c_39465]) ).
tff(c_39595,plain,
multiply(identity,sk_c6) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_39586,c_39466]) ).
tff(c_39600,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39595]) ).
tff(c_39655,plain,
sk_c8 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_39654,c_39600]) ).
tff(c_39708,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_39663,c_39655]) ).
tff(c_39710,plain,
multiply(sk_c7,sk_c6) = sk_c8,
inference(splitRight,[status(thm)],[c_39465]) ).
tff(c_39759,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_39755,c_39710]) ).
tff(c_39771,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39759,c_39387]) ).
tff(c_40584,plain,
multiply(sk_c5,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40519,c_39771]) ).
tff(c_40588,plain,
multiply(inverse(sk_c5),identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_40584,c_39462]) ).
tff(c_40594,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_40527,c_40588]) ).
tff(c_39860,plain,
! [X_403,Z_404] : ( multiply(inverse(X_403),multiply(X_403,Z_404)) = Z_404 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39450]) ).
tff(c_39902,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_39755,c_39860]) ).
tff(c_39942,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39902]) ).
tff(c_40197,plain,
! [X_408,Z_409] : ( multiply(inverse(inverse(X_408)),Z_409) = multiply(X_408,Z_409) ),
inference(superposition,[status(thm),theory(equality)],[c_39462,c_39860]) ).
tff(c_39929,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39860]) ).
tff(c_40204,plain,
! [X_408] : ( multiply(X_408,identity) = X_408 ),
inference(superposition,[status(thm),theory(equality)],[c_40197,c_39929]) ).
tff(c_39429,plain,
! [Z_394] : ( multiply(sk_c4,multiply(sk_c7,Z_394)) = multiply(sk_c6,Z_394) ),
inference(superposition,[status(thm),theory(equality)],[c_39393,c_39414]) ).
tff(c_39763,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c4,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_39755,c_39429]) ).
tff(c_39769,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39393,c_39763]) ).
tff(c_39893,plain,
multiply(inverse(sk_c5),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_39771,c_39860]) ).
tff(c_39940,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39769,c_39324,c_39893]) ).
tff(c_39968,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39942,c_39940]) ).
tff(c_39709,plain,
! [X4_10,X1_8,X2_9,X5_6] :
( ( inverse(X4_10) != sk_c8 )
| ( multiply(sk_c8,multiply(X4_10,sk_c8)) != sk_c7 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_39465]) ).
tff(c_39789,plain,
! [X4_10,X1_8,X2_9,X5_6] :
( ( inverse(X4_10) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_10,sk_c7)) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( multiply(X5_6,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_39759,c_39759,c_39759,c_39759,c_39759,c_39759,c_39709]) ).
tff(c_39790,plain,
! [X5_6] :
( ( multiply(X5_6,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_39789]) ).
tff(c_40460,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_39942,c_40204,c_39968,c_39942,c_39790]) ).
tff(c_39776,plain,
inverse(sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39759,c_39344]) ).
tff(c_39953,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_39940,c_39776]) ).
tff(c_40074,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39942,c_39942,c_39953]) ).
tff(c_40462,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_40460,c_40074]) ).
tff(c_40463,plain,
! [X2_9,X1_8,X4_10] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(sk_c7,multiply(X4_10,sk_c7)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_39789]) ).
tff(c_48924,plain,
! [X2_9,X1_8,X4_10] :
( ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_40934,c_40594,c_40594,c_2,c_40594,c_40594,c_40934,c_40594,c_40594,c_40594,c_40934,c_40594,c_40519,c_40594,c_40463]) ).
tff(c_48926,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_48924]) ).
tff(c_40533,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40519,c_39776]) ).
tff(c_40599,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_40594,c_40533]) ).
tff(c_48928,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48926,c_40599]) ).
tff(c_48929,plain,
! [X1_8,X2_9] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(splitRight,[status(thm)],[c_48924]) ).
tff(c_48931,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_48929]) ).
tff(c_48933,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48931,c_40599]) ).
tff(c_49337,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_48929]) ).
tff(c_49339,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_49337,c_40599]) ).
tff(c_49340,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_49554,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49547,c_49340]) ).
tff(c_49563,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_49554,c_4]) ).
tff(c_49655,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49630,c_49563]) ).
tff(c_49634,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49630,c_49554]) ).
tff(c_49660,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49655,c_49634]) ).
tff(c_49341,plain,
inverse(sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_49553,plain,
inverse(sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49547,c_49341]) ).
tff(c_49635,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_49630,c_49630,c_49553]) ).
tff(c_49685,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49660,c_49635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GRP358-1 : TPTP v9.0.0. Released v2.5.0.
% 0.04/0.15 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.16/0.37 % Computer : n031.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Mon Apr 7 21:44:07 EDT 2025
% 0.16/0.37 % CPUTime :
% 19.08/6.79 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.08/6.82
% 19.08/6.82 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------