%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP276-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 : n008.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:46 PM UTC 2025
% Result : Unsatisfiable 21.71s 9.80s
% Output : CNFRefutation 22.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 30
% Syntax : Number of formulae : 440 ( 344 unt; 0 typ; 0 def)
% Number of atoms : 652 ( 629 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 447 ( 235 ~; 212 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 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 : 208 ( 208 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X3,X4,X1,X2] :
( ( multiply(X3,sk_c7) != sk_c6 )
| ( inverse(X3) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X4) != sk_c7 )
| ( multiply(X4,sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(X1,sk_c7) != sk_c6 )
| ( inverse(X1) != sk_c7 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(X2,sk_c5) != sk_c6 )
| ( inverse(X2) != sk_c5 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
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_50234,plain,
! [X_322,Y_323,Z_324] : ( multiply(multiply(X_322,Y_323),Z_324) = multiply(X_322,multiply(Y_323,Z_324)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_50270,plain,
! [X_2,Z_324] : ( multiply(inverse(X_2),multiply(X_2,Z_324)) = multiply(identity,Z_324) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_50234]) ).
tff(c_50282,plain,
! [X_2,Z_324] : ( multiply(inverse(X_2),multiply(X_2,Z_324)) = Z_324 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50270]) ).
tff(c_51520,plain,
! [X_349,Z_350] : ( multiply(inverse(X_349),multiply(X_349,Z_350)) = Z_350 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50270]) ).
tff(c_51780,plain,
! [X_355,Z_356] : ( multiply(inverse(inverse(X_355)),Z_356) = multiply(X_355,Z_356) ),
inference(superposition,[status(thm),theory(equality)],[c_50282,c_51520]) ).
tff(c_51550,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_51520]) ).
tff(c_51787,plain,
! [X_355] : ( multiply(X_355,identity) = X_355 ),
inference(superposition,[status(thm),theory(equality)],[c_51780,c_51550]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_85,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_89,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_14,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_119,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_24,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_98,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_149,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_173,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_149]) ).
tff(c_191,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_173]) ).
tff(c_203,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_119,c_191]) ).
tff(c_179,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_149]) ).
tff(c_237,plain,
! [X_17,Z_18] : ( multiply(inverse(X_17),multiply(X_17,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_261,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_203,c_237]) ).
tff(c_298,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_261]) ).
tff(c_307,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_203]) ).
tff(c_62,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_126,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_164,plain,
! [Z_14] : ( multiply(sk_c2,multiply(sk_c6,Z_14)) = multiply(sk_c7,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_126,c_149]) ).
tff(c_419,plain,
! [Z_20] : ( multiply(sk_c7,Z_20) = multiply(sk_c2,Z_20) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_298,c_164]) ).
tff(c_446,plain,
multiply(sk_c2,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_419,c_102]) ).
tff(c_189,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_179]) ).
tff(c_482,plain,
multiply(inverse(sk_c2),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_446,c_189]) ).
tff(c_491,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_307,c_85,c_482]) ).
tff(c_36,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_113,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_68,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(sk_c7) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_304,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(sk_c7) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_113,c_68]) ).
tff(c_305,plain,
multiply(sk_c6,sk_c5) != sk_c7,
inference(splitLeft,[status(thm)],[c_304]) ).
tff(c_315,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_298,c_305]) ).
tff(c_500,plain,
sk_c5 != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_491,c_315]) ).
tff(c_499,plain,
multiply(sk_c1,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_491,c_491,c_307]) ).
tff(c_506,plain,
inverse(sk_c2) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_491,c_85]) ).
tff(c_449,plain,
multiply(sk_c2,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_419,c_89]) ).
tff(c_589,plain,
multiply(inverse(sk_c2),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_449,c_189]) ).
tff(c_595,plain,
multiply(sk_c1,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_506,c_589]) ).
tff(c_679,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_499,c_595]) ).
tff(c_310,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_113]) ).
tff(c_458,plain,
multiply(sk_c2,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_310,c_419]) ).
tff(c_698,plain,
multiply(sk_c1,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_679,c_458]) ).
tff(c_167,plain,
! [Z_14] : ( multiply(sk_c1,multiply(sk_c7,Z_14)) = multiply(sk_c6,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_119,c_149]) ).
tff(c_639,plain,
! [Z_14] : ( multiply(sk_c1,multiply(sk_c1,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_491,c_2,c_298,c_167]) ).
tff(c_717,plain,
multiply(sk_c1,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_698,c_639]) ).
tff(c_726,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_499,c_717]) ).
tff(c_728,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_500,c_726]) ).
tff(c_730,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_304]) ).
tff(c_740,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_298,c_730]) ).
tff(c_732,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_203]) ).
tff(c_771,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_740,c_740,c_732]) ).
tff(c_279,plain,
multiply(inverse(sk_c7),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_102,c_237]) ).
tff(c_885,plain,
multiply(inverse(sk_c5),identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_740,c_279]) ).
tff(c_276,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_113,c_237]) ).
tff(c_897,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_885,c_740,c_298,c_276]) ).
tff(c_744,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_740,c_98]) ).
tff(c_907,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_897,c_744]) ).
tff(c_729,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_304]) ).
tff(c_845,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != identity )
| ( multiply(X4_7,identity) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != identity )
| ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_298,c_740,c_298,c_740,c_740,c_740,c_298,c_740,c_298,c_740,c_740,c_729]) ).
tff(c_846,plain,
inverse(sk_c5) != sk_c5,
inference(splitLeft,[status(thm)],[c_845]) ).
tff(c_899,plain,
inverse(sk_c1) != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_897,c_897,c_846]) ).
tff(c_964,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_907,c_899]) ).
tff(c_966,plain,
inverse(sk_c5) = sk_c5,
inference(splitRight,[status(thm)],[c_845]) ).
tff(c_1016,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_771,c_966,c_740,c_279]) ).
tff(c_1017,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_1016,c_1016,c_966]) ).
tff(c_735,plain,
multiply(sk_c7,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_298,c_113]) ).
tff(c_808,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_740,c_735]) ).
tff(c_1020,plain,
multiply(sk_c1,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1016,c_1016,c_808]) ).
tff(c_1280,plain,
! [X_31,Z_32] : ( multiply(inverse(inverse(X_31)),Z_32) = multiply(X_31,Z_32) ),
inference(superposition,[status(thm),theory(equality)],[c_189,c_237]) ).
tff(c_291,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_237]) ).
tff(c_1287,plain,
! [X_31] : ( multiply(X_31,identity) = X_31 ),
inference(superposition,[status(thm),theory(equality)],[c_1280,c_291]) ).
tff(c_965,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != identity )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != identity )
| ( multiply(X4_7,identity) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != identity ) ),
inference(splitRight,[status(thm)],[c_845]) ).
tff(c_43515,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c1 )
| ( multiply(X2_9,sk_c1) != identity )
| ( inverse(X1_8) != sk_c1 )
| ( multiply(X1_8,sk_c1) != identity )
| ( sk_c1 != X4_7 )
| ( inverse(X4_7) != sk_c1 )
| ( inverse(X3_6) != sk_c1 )
| ( multiply(X3_6,sk_c1) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1016,c_1016,c_1016,c_1287,c_1016,c_1016,c_1016,c_1016,c_1016,c_965]) ).
tff(c_43517,plain,
! [X3_256] :
( ( inverse(X3_256) != sk_c1 )
| ( multiply(X3_256,sk_c1) != identity ) ),
inference(splitLeft,[status(thm)],[c_43515]) ).
tff(c_43579,plain,
inverse(sk_c1) != sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_1020,c_43517]) ).
tff(c_43607,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1017,c_43579]) ).
tff(c_43608,plain,
! [X4_7,X1_8,X2_9] :
( ( sk_c1 != X4_7 )
| ( inverse(X4_7) != sk_c1 )
| ( inverse(X1_8) != sk_c1 )
| ( multiply(X1_8,sk_c1) != identity )
| ( inverse(X2_9) != sk_c1 )
| ( multiply(X2_9,sk_c1) != identity ) ),
inference(splitRight,[status(thm)],[c_43515]) ).
tff(c_46815,plain,
! [X2_267] :
( ( inverse(X2_267) != sk_c1 )
| ( multiply(X2_267,sk_c1) != identity ) ),
inference(splitLeft,[status(thm)],[c_43608]) ).
tff(c_46877,plain,
inverse(sk_c1) != sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_1020,c_46815]) ).
tff(c_46905,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1017,c_46877]) ).
tff(c_46906,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c1 )
| ( multiply(X1_8,sk_c1) != identity )
| ( sk_c1 != X4_7 )
| ( inverse(X4_7) != sk_c1 ) ),
inference(splitRight,[status(thm)],[c_43608]) ).
tff(c_46908,plain,
inverse(sk_c1) != sk_c1,
inference(splitLeft,[status(thm)],[c_46906]) ).
tff(c_46910,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46908,c_1017]) ).
tff(c_47632,plain,
! [X1_270] :
( ( inverse(X1_270) != sk_c1 )
| ( multiply(X1_270,sk_c1) != identity ) ),
inference(splitRight,[status(thm)],[c_46906]) ).
tff(c_47694,plain,
inverse(sk_c1) != sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_1020,c_47632]) ).
tff(c_47722,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1017,c_47694]) ).
tff(c_47724,plain,
multiply(sk_c2,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_64,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_47767,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_47724,c_64]) ).
tff(c_66,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_47736,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_47724,c_66]) ).
tff(c_47740,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_47736,c_4]) ).
tff(c_47788,plain,
! [X_271,Y_272,Z_273] : ( multiply(multiply(X_271,Y_272),Z_273) = multiply(X_271,multiply(Y_272,Z_273)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_47815,plain,
! [Z_273] : ( multiply(sk_c5,multiply(sk_c4,Z_273)) = multiply(identity,Z_273) ),
inference(superposition,[status(thm),theory(equality)],[c_47740,c_47788]) ).
tff(c_48391,plain,
! [Z_288] : ( multiply(sk_c5,multiply(sk_c4,Z_288)) = Z_288 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47815]) ).
tff(c_48406,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_47767,c_48391]) ).
tff(c_56,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_47772,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_47724,c_56]) ).
tff(c_48040,plain,
! [Z_280] : ( multiply(sk_c1,multiply(sk_c7,Z_280)) = multiply(sk_c6,Z_280) ),
inference(superposition,[status(thm),theory(equality)],[c_119,c_47788]) ).
tff(c_48067,plain,
multiply(sk_c6,sk_c5) = multiply(sk_c1,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_113,c_48040]) ).
tff(c_48078,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_47772,c_48067]) ).
tff(c_47827,plain,
! [Z_273] : ( multiply(sk_c7,multiply(sk_c1,Z_273)) = multiply(identity,Z_273) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_47788]) ).
tff(c_47844,plain,
! [Z_273] : ( multiply(sk_c7,multiply(sk_c1,Z_273)) = Z_273 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47827]) ).
tff(c_48082,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_48078,c_47844]) ).
tff(c_47723,plain,
inverse(sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_47728,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_47723,c_4]) ).
tff(c_47818,plain,
! [Z_273] : ( multiply(sk_c5,multiply(sk_c7,Z_273)) = multiply(identity,Z_273) ),
inference(superposition,[status(thm),theory(equality)],[c_47728,c_47788]) ).
tff(c_48421,plain,
! [Z_289] : ( multiply(sk_c5,multiply(sk_c7,Z_289)) = Z_289 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47818]) ).
tff(c_48445,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_48082,c_48421]) ).
tff(c_48471,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_48406,c_48445]) ).
tff(c_48737,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_48471,c_47723]) ).
tff(c_48017,plain,
! [Z_279] : ( multiply(sk_c7,multiply(sk_c1,Z_279)) = Z_279 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47827]) ).
tff(c_48029,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_119,c_48017]) ).
tff(c_48448,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_48029,c_48421]) ).
tff(c_48472,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47728,c_48448]) ).
tff(c_48492,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_48471,c_47723]) ).
tff(c_48463,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_102,c_48421]) ).
tff(c_60,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_47744,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_47724,c_60]) ).
tff(c_58,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_47779,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_47724,c_58]) ).
tff(c_47849,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_113,c_47772,c_47723,c_68]) ).
tff(c_47969,plain,
! [X3_277] :
( ( inverse(X3_277) != sk_c7 )
| ( multiply(X3_277,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_47849]) ).
tff(c_47982,plain,
inverse(sk_c3) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_47779,c_47969]) ).
tff(c_48002,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_47744,c_47982]) ).
tff(c_48003,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_47849]) ).
tff(c_48285,plain,
! [X2_285] :
( ( inverse(X2_285) != sk_c5 )
| ( multiply(X2_285,sk_c5) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_48003]) ).
tff(c_48295,plain,
inverse(sk_c4) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_47767,c_48285]) ).
tff(c_48310,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_47736,c_48295]) ).
tff(c_48311,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_48003]) ).
tff(c_48474,plain,
! [X4_7] :
( ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_48311]) ).
tff(c_48573,plain,
! [X4_7] :
( ( multiply(X4_7,identity) != sk_c5 )
| ( inverse(X4_7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_48471,c_48472,c_48471,c_48474]) ).
tff(c_48603,plain,
( ( sk_c5 != sk_c1 )
| ( inverse(sk_c5) != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_48463,c_48573]) ).
tff(c_48610,plain,
sk_c5 != sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_48492,c_48603]) ).
tff(c_48496,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_48471,c_98]) ).
tff(c_47833,plain,
! [X_2,Z_273] : ( multiply(inverse(X_2),multiply(X_2,Z_273)) = multiply(identity,Z_273) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_47788]) ).
tff(c_48643,plain,
! [X_291,Z_292] : ( multiply(inverse(X_291),multiply(X_291,Z_292)) = Z_292 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47833]) ).
tff(c_48679,plain,
multiply(inverse(sk_c5),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_47740,c_48643]) ).
tff(c_48695,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_48463,c_48492,c_48679]) ).
tff(c_48510,plain,
multiply(sk_c4,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_48472,c_47767]) ).
tff(c_48706,plain,
multiply(sk_c1,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_48695,c_48510]) ).
tff(c_47846,plain,
! [X_2,Z_273] : ( multiply(inverse(X_2),multiply(X_2,Z_273)) = Z_273 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47833]) ).
tff(c_48710,plain,
multiply(inverse(sk_c1),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_48706,c_47846]) ).
tff(c_48716,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_48463,c_48496,c_48710]) ).
tff(c_48718,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48610,c_48716]) ).
tff(c_48719,plain,
! [X1_8] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_48311]) ).
tff(c_48822,plain,
! [X1_294] :
( ( inverse(X1_294) != sk_c5 )
| ( multiply(X1_294,sk_c5) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_48472,c_48471,c_48471,c_48719]) ).
tff(c_48830,plain,
inverse(inverse(sk_c5)) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_4,c_48822]) ).
tff(c_48838,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_48737,c_48737,c_48830]) ).
tff(c_48840,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_48839,plain,
inverse(sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_48844,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_48839,c_4]) ).
tff(c_48911,plain,
! [X_295,Y_296,Z_297] : ( multiply(multiply(X_295,Y_296),Z_297) = multiply(X_295,multiply(Y_296,Z_297)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_48944,plain,
! [Z_297] : ( multiply(sk_c5,multiply(sk_c7,Z_297)) = multiply(identity,Z_297) ),
inference(superposition,[status(thm),theory(equality)],[c_48844,c_48911]) ).
tff(c_49383,plain,
! [Z_308] : ( multiply(sk_c5,multiply(sk_c7,Z_308)) = Z_308 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48944]) ).
tff(c_49410,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_102,c_49383]) ).
tff(c_49413,plain,
multiply(sk_c5,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_49383]) ).
tff(c_49476,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_49410,c_49413]) ).
tff(c_12,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_48860,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_48840,c_12]) ).
tff(c_48864,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_48860,c_4]) ).
tff(c_49404,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_48864,c_49383]) ).
tff(c_49454,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_49413,c_49404]) ).
tff(c_10,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_48890,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_48840,c_10]) ).
tff(c_49467,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49454,c_48890]) ).
tff(c_49506,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_49476,c_49467]) ).
tff(c_49507,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48840,c_49506]) ).
tff(c_49509,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_38,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_49547,plain,
inverse(sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_49509,c_38]) ).
tff(c_49586,plain,
! [X_310,Y_311,Z_312] : ( multiply(multiply(X_310,Y_311),Z_312) = multiply(X_310,multiply(Y_311,Z_312)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_49631,plain,
! [X_2,Z_312] : ( multiply(inverse(X_2),multiply(X_2,Z_312)) = multiply(identity,Z_312) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_49586]) ).
tff(c_49717,plain,
! [X_316,Z_317] : ( multiply(inverse(X_316),multiply(X_316,Z_317)) = Z_317 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49631]) ).
tff(c_49789,plain,
multiply(inverse(sk_c7),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_102,c_49717]) ).
tff(c_49819,plain,
multiply(sk_c5,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_49547,c_49789]) ).
tff(c_40,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_49572,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_49509,c_40]) ).
tff(c_42,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_49517,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_49509,c_42]) ).
tff(c_49521,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_49517,c_4]) ).
tff(c_49619,plain,
! [Z_312] : ( multiply(sk_c5,multiply(sk_c4,Z_312)) = multiply(identity,Z_312) ),
inference(superposition,[status(thm),theory(equality)],[c_49521,c_49586]) ).
tff(c_49694,plain,
! [Z_315] : ( multiply(sk_c5,multiply(sk_c4,Z_315)) = Z_315 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49619]) ).
tff(c_49706,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_49572,c_49694]) ).
tff(c_49735,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_49706,c_49717]) ).
tff(c_49808,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_49735]) ).
tff(c_32,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_49566,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_49509,c_32]) ).
tff(c_49828,plain,
multiply(identity,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_49808,c_49566]) ).
tff(c_49832,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49828]) ).
tff(c_49845,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_49832,c_98]) ).
tff(c_49795,plain,
multiply(inverse(sk_c7),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_49717]) ).
tff(c_49821,plain,
multiply(sk_c5,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_49547,c_49795]) ).
tff(c_49975,plain,
sk_c2 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_49819,c_49821]) ).
tff(c_49508,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_49513,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_49508,c_4]) ).
tff(c_49780,plain,
multiply(inverse(sk_c7),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_49513,c_49717]) ).
tff(c_49817,plain,
multiply(sk_c5,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_49547,c_49780]) ).
tff(c_49968,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_49821,c_49817]) ).
tff(c_50007,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_49975,c_49968]) ).
tff(c_34,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_49580,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_49509,c_34]) ).
tff(c_49826,plain,
multiply(sk_c3,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49808,c_49580]) ).
tff(c_50019,plain,
multiply(sk_c1,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_50007,c_49832,c_49826]) ).
tff(c_49644,plain,
! [X_2,Z_312] : ( multiply(inverse(X_2),multiply(X_2,Z_312)) = Z_312 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49631]) ).
tff(c_50023,plain,
multiply(inverse(sk_c1),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_50019,c_49644]) ).
tff(c_50029,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_49819,c_49845,c_50023]) ).
tff(c_49843,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_49832,c_49508]) ).
tff(c_49915,plain,
multiply(sk_c5,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_49843,c_4]) ).
tff(c_50087,plain,
multiply(sk_c1,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_50029,c_50007,c_49915]) ).
tff(c_50037,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_50029,c_49832]) ).
tff(c_49831,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_49808,c_49509]) ).
tff(c_50159,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50087,c_50037,c_50029,c_49831]) ).
tff(c_50161,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_26,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_50186,plain,
inverse(sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_50161,c_26]) ).
tff(c_50190,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_50186,c_4]) ).
tff(c_50258,plain,
! [Z_324] : ( multiply(sk_c5,multiply(sk_c7,Z_324)) = multiply(identity,Z_324) ),
inference(superposition,[status(thm),theory(equality)],[c_50190,c_50234]) ).
tff(c_50284,plain,
! [Z_325] : ( multiply(sk_c5,multiply(sk_c7,Z_325)) = Z_325 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50258]) ).
tff(c_50299,plain,
multiply(sk_c5,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_50284]) ).
tff(c_50160,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_50165,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_50160,c_4]) ).
tff(c_50296,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_50165,c_50284]) ).
tff(c_50751,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50299,c_50296]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_50210,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_50161,c_22]) ).
tff(c_50931,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_50751,c_50210]) ).
tff(c_50264,plain,
! [Z_324] : ( multiply(sk_c7,multiply(sk_c3,Z_324)) = multiply(identity,Z_324) ),
inference(superposition,[status(thm),theory(equality)],[c_50165,c_50234]) ).
tff(c_50280,plain,
! [Z_324] : ( multiply(sk_c7,multiply(sk_c3,Z_324)) = Z_324 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50264]) ).
tff(c_50972,plain,
! [Z_337] : ( multiply(sk_c7,multiply(sk_c2,Z_337)) = Z_337 ),
inference(demodulation,[status(thm),theory(equality)],[c_50751,c_50280]) ).
tff(c_50987,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_50931,c_50972]) ).
tff(c_50278,plain,
! [Z_324] : ( multiply(sk_c5,multiply(sk_c7,Z_324)) = Z_324 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50258]) ).
tff(c_51099,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_50987,c_50278]) ).
tff(c_51105,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_50190,c_51099]) ).
tff(c_50314,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50299,c_50296]) ).
tff(c_50348,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_50314,c_50210]) ).
tff(c_50376,plain,
! [Z_327] : ( multiply(sk_c7,multiply(sk_c2,Z_327)) = Z_327 ),
inference(demodulation,[status(thm),theory(equality)],[c_50314,c_50280]) ).
tff(c_50391,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_50348,c_50376]) ).
tff(c_50398,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_50391,c_50278]) ).
tff(c_50404,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_50190,c_50398]) ).
tff(c_30,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_50173,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_50161,c_30]) ).
tff(c_28,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_50203,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_50161,c_28]) ).
tff(c_50406,plain,
! [X_328,Z_329] : ( multiply(inverse(X_328),multiply(X_328,Z_329)) = Z_329 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50270]) ).
tff(c_50451,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_50203,c_50406]) ).
tff(c_50483,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_50173,c_50451]) ).
tff(c_50569,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50299,c_50404,c_50483]) ).
tff(c_20,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_50220,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_50161,c_20]) ).
tff(c_50492,plain,
multiply(identity,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_50404,c_50220]) ).
tff(c_50496,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50492]) ).
tff(c_50505,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_50496,c_50186]) ).
tff(c_50565,plain,
multiply(sk_c5,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_50505,c_4]) ).
tff(c_50632,plain,
multiply(sk_c2,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_50569,c_50569,c_50565]) ).
tff(c_50573,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50569,c_50496]) ).
tff(c_50304,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_50220,c_50186,c_68]) ).
tff(c_50305,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitLeft,[status(thm)],[c_50304]) ).
tff(c_50491,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_50404,c_50305]) ).
tff(c_50730,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50632,c_50573,c_50569,c_50491]) ).
tff(c_50732,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_50304]) ).
tff(c_50736,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_50732,c_50278]) ).
tff(c_51109,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_51105,c_50736]) ).
tff(c_51113,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50299,c_51109]) ).
tff(c_51111,plain,
multiply(identity,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_51105,c_50220]) ).
tff(c_51114,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51111]) ).
tff(c_51155,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_51113,c_51114]) ).
tff(c_51123,plain,
inverse(sk_c7) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_51113,c_50186]) ).
tff(c_51165,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_51155,c_51123]) ).
tff(c_51221,plain,
! [X_341,Z_342] : ( multiply(inverse(X_341),multiply(X_341,Z_342)) = Z_342 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50270]) ).
tff(c_51319,plain,
! [X_344] : ( multiply(inverse(inverse(X_344)),identity) = X_344 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_51221]) ).
tff(c_51325,plain,
! [X_344] : ( multiply(inverse(inverse(inverse(X_344))),X_344) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_51319,c_50282]) ).
tff(c_50995,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_50987,c_50278]) ).
tff(c_51001,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_50190,c_50995]) ).
tff(c_51005,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_51001,c_50736]) ).
tff(c_51009,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50299,c_51005]) ).
tff(c_51007,plain,
multiply(identity,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_51001,c_50220]) ).
tff(c_51010,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51007]) ).
tff(c_51051,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_51009,c_51010]) ).
tff(c_51019,plain,
inverse(sk_c7) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_51009,c_50186]) ).
tff(c_51068,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_51051,c_51019]) ).
tff(c_50761,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_50751,c_50210]) ).
tff(c_50267,plain,
! [Z_324] : ( multiply(sk_c7,multiply(sk_c2,Z_324)) = multiply(identity,Z_324) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_50234]) ).
tff(c_50812,plain,
! [Z_334] : ( multiply(sk_c7,multiply(sk_c2,Z_334)) = Z_334 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50267]) ).
tff(c_50836,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_50761,c_50812]) ).
tff(c_50846,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_50836,c_50278]) ).
tff(c_50853,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_50190,c_50846]) ).
tff(c_50859,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_50853,c_50736]) ).
tff(c_50864,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50299,c_50859]) ).
tff(c_50861,plain,
multiply(identity,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_50853,c_50220]) ).
tff(c_50865,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50861]) ).
tff(c_50900,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50864,c_50865]) ).
tff(c_50873,plain,
inverse(sk_c7) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50864,c_50186]) ).
tff(c_50909,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_50900,c_50873]) ).
tff(c_50913,plain,
multiply(sk_c2,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_50909,c_4]) ).
tff(c_50731,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_50304]) ).
tff(c_50760,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_50731]) ).
tff(c_50880,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c2 )
| ( multiply(X2_9,sk_c2) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_50864,c_50853,c_50864,c_50760]) ).
tff(c_50920,plain,
inverse(sk_c2) != sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_50913,c_50880]) ).
tff(c_50929,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50909,c_50920]) ).
tff(c_50930,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_50731]) ).
tff(c_50991,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_50930]) ).
tff(c_51078,plain,
! [X3_339] :
( ( inverse(X3_339) != sk_c2 )
| ( multiply(X3_339,sk_c2) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_51051,c_51001,c_51051,c_50991]) ).
tff(c_51086,plain,
inverse(inverse(sk_c2)) != sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_4,c_51078]) ).
tff(c_51094,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_51068,c_51068,c_51086]) ).
tff(c_51095,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_50930]) ).
tff(c_51181,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,identity) != sk_c2 )
| ( inverse(X4_7) != sk_c2 )
| ( inverse(X1_8) != sk_c2 )
| ( multiply(X1_8,sk_c2) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_51155,c_51105,c_51155,c_51155,c_51155,c_51105,c_51095]) ).
tff(c_51487,plain,
! [X1_348] :
( ( inverse(X1_348) != sk_c2 )
| ( multiply(X1_348,sk_c2) != identity ) ),
inference(splitLeft,[status(thm)],[c_51181]) ).
tff(c_51491,plain,
inverse(inverse(inverse(inverse(sk_c2)))) != sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_51325,c_51487]) ).
tff(c_51510,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_51165,c_51165,c_51165,c_51165,c_51491]) ).
tff(c_51511,plain,
! [X4_7] :
( ( multiply(X4_7,identity) != sk_c2 )
| ( inverse(X4_7) != sk_c2 ) ),
inference(splitRight,[status(thm)],[c_51181]) ).
tff(c_52213,plain,
inverse(sk_c2) != sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_51787,c_51511]) ).
tff(c_52215,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52213,c_51165]) ).
tff(c_52217,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_48,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_52251,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_52217,c_48]) ).
tff(c_52255,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_52251,c_4]) ).
tff(c_50,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_52218,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_52226,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52217,c_52218]) ).
tff(c_52227,plain,
inverse(sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_52232,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_52227,c_4]) ).
tff(c_52302,plain,
! [X_365,Y_366,Z_367] : ( multiply(multiply(X_365,Y_366),Z_367) = multiply(X_365,multiply(Y_366,Z_367)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_52332,plain,
! [Z_367] : ( multiply(sk_c5,multiply(sk_c7,Z_367)) = multiply(identity,Z_367) ),
inference(superposition,[status(thm),theory(equality)],[c_52232,c_52302]) ).
tff(c_52659,plain,
! [Z_374] : ( multiply(sk_c5,multiply(sk_c7,Z_374)) = Z_374 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52332]) ).
tff(c_52680,plain,
multiply(sk_c5,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_52255,c_52659]) ).
tff(c_52335,plain,
! [X_2,Z_367] : ( multiply(inverse(X_2),multiply(X_2,Z_367)) = multiply(identity,Z_367) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_52302]) ).
tff(c_52407,plain,
! [X_370,Z_371] : ( multiply(inverse(X_370),multiply(X_370,Z_371)) = Z_371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52335]) ).
tff(c_52434,plain,
multiply(inverse(sk_c7),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_52255,c_52407]) ).
tff(c_52460,plain,
multiply(sk_c5,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_52227,c_52434]) ).
tff(c_46,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_52267,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_52217,c_46]) ).
tff(c_52326,plain,
! [Z_367] : ( multiply(sk_c7,multiply(sk_c3,Z_367)) = multiply(identity,Z_367) ),
inference(superposition,[status(thm),theory(equality)],[c_52255,c_52302]) ).
tff(c_52351,plain,
! [Z_368] : ( multiply(sk_c7,multiply(sk_c3,Z_368)) = Z_368 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52326]) ).
tff(c_52363,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_52267,c_52351]) ).
tff(c_52374,plain,
! [Z_369] : ( multiply(sk_c5,multiply(sk_c7,Z_369)) = Z_369 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52332]) ).
tff(c_52386,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_52363,c_52374]) ).
tff(c_52396,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52232,c_52386]) ).
tff(c_44,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_52285,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_52217,c_44]) ).
tff(c_52399,plain,
multiply(identity,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_52396,c_52285]) ).
tff(c_52402,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52399]) ).
tff(c_52468,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_52402,c_52227]) ).
tff(c_52467,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52402,c_52232]) ).
tff(c_52346,plain,
! [X_2,Z_367] : ( multiply(inverse(X_2),multiply(X_2,Z_367)) = Z_367 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52335]) ).
tff(c_52522,plain,
multiply(inverse(sk_c5),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_52467,c_52346]) ).
tff(c_52528,plain,
sk_c5 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_52460,c_52468,c_52522]) ).
tff(c_52490,plain,
multiply(sk_c5,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_52468,c_4]) ).
tff(c_52586,plain,
multiply(sk_c3,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52528,c_52528,c_52490]) ).
tff(c_52537,plain,
sk_c7 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_52528,c_52402]) ).
tff(c_52349,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_52285,c_52227,c_68]) ).
tff(c_52350,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitLeft,[status(thm)],[c_52349]) ).
tff(c_52398,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_52396,c_52350]) ).
tff(c_52630,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52586,c_52537,c_52528,c_52398]) ).
tff(c_52632,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_52349]) ).
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_52636,plain,
! [Z_5] : ( multiply(sk_c7,multiply(sk_c5,Z_5)) = multiply(sk_c6,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_52632,c_6]) ).
tff(c_52698,plain,
multiply(sk_c7,sk_c3) = multiply(sk_c6,identity),
inference(superposition,[status(thm),theory(equality)],[c_52680,c_52636]) ).
tff(c_52704,plain,
multiply(sk_c6,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52255,c_52698]) ).
tff(c_52717,plain,
! [Z_5] : ( multiply(sk_c6,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_52704,c_6]) ).
tff(c_52720,plain,
! [Z_5] : ( multiply(sk_c6,Z_5) = Z_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_52717]) ).
tff(c_52825,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_52720,c_52285]) ).
tff(c_52844,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52825,c_52232]) ).
tff(c_52840,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_52825,c_52632]) ).
tff(c_52881,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52844,c_52840]) ).
tff(c_52677,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_52632,c_52659]) ).
tff(c_52891,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_52881,c_52677]) ).
tff(c_52894,plain,
sk_c5 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_52680,c_52891]) ).
tff(c_52843,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_52825,c_52251]) ).
tff(c_53660,plain,
inverse(sk_c3) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_52894,c_52843]) ).
tff(c_52845,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_52825,c_52227]) ).
tff(c_52869,plain,
multiply(sk_c5,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_52845,c_4]) ).
tff(c_53673,plain,
multiply(sk_c3,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52894,c_52894,c_52869]) ).
tff(c_53706,plain,
! [X_395,Z_396] : ( multiply(inverse(X_395),multiply(X_395,Z_396)) = Z_396 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52335]) ).
tff(c_53944,plain,
! [X_401,Z_402] : ( multiply(inverse(inverse(X_401)),Z_402) = multiply(X_401,Z_402) ),
inference(superposition,[status(thm),theory(equality)],[c_53706,c_52346]) ).
tff(c_53739,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_53706]) ).
tff(c_53951,plain,
! [X_401] : ( multiply(X_401,identity) = X_401 ),
inference(superposition,[status(thm),theory(equality)],[c_53944,c_53739]) ).
tff(c_52905,plain,
inverse(sk_c3) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_52894,c_52843]) ).
tff(c_52925,plain,
multiply(sk_c3,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52894,c_52894,c_52869]) ).
tff(c_52726,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_52720,c_52285]) ).
tff(c_52746,plain,
inverse(sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_52726,c_52227]) ).
tff(c_52745,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52726,c_52232]) ).
tff(c_52741,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_52726,c_52632]) ).
tff(c_52782,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52745,c_52741]) ).
tff(c_52631,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_52349]) ).
tff(c_52722,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_52631]) ).
tff(c_52801,plain,
! [X2_376] :
( ( inverse(X2_376) != sk_c5 )
| ( multiply(X2_376,sk_c5) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_52782,c_52722]) ).
tff(c_52804,plain,
inverse(sk_c5) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_52745,c_52801]) ).
tff(c_52820,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52746,c_52804]) ).
tff(c_52821,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_52631]) ).
tff(c_52899,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != identity )
| ( multiply(X4_7,identity) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_52881,c_52825,c_52825,c_52825,c_52881,c_52825,c_52881,c_52825,c_52825,c_52821]) ).
tff(c_52900,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != identity ) ),
inference(splitLeft,[status(thm)],[c_52899]) ).
tff(c_53635,plain,
! [X3_394] :
( ( inverse(X3_394) != sk_c3 )
| ( multiply(X3_394,sk_c3) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_52894,c_52894,c_52900]) ).
tff(c_53638,plain,
inverse(sk_c3) != sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_52925,c_53635]) ).
tff(c_53654,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52905,c_53638]) ).
tff(c_53655,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,identity) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != identity ) ),
inference(splitRight,[status(thm)],[c_52899]) ).
tff(c_96243,plain,
! [X4_7,X1_8] :
( ( sk_c3 != X4_7 )
| ( inverse(X4_7) != sk_c3 )
| ( inverse(X1_8) != sk_c3 )
| ( multiply(X1_8,sk_c3) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_52894,c_52894,c_52894,c_53951,c_52894,c_53655]) ).
tff(c_96245,plain,
! [X1_627] :
( ( inverse(X1_627) != sk_c3 )
| ( multiply(X1_627,sk_c3) != identity ) ),
inference(splitLeft,[status(thm)],[c_96243]) ).
tff(c_96307,plain,
inverse(sk_c3) != sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_53673,c_96245]) ).
tff(c_96335,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_53660,c_96307]) ).
tff(c_96337,plain,
inverse(sk_c3) != sk_c3,
inference(splitRight,[status(thm)],[c_96243]) ).
tff(c_96339,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_96337,c_53660]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP276-1 : TPTP v9.0.0. Released v2.5.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n008.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:40:17 EDT 2025
% 0.13/0.35 % CPUTime :
% 21.71/9.80 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.95/9.86
% 21.95/9.86 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------