%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP113-1 : TPTP v9.0.0. Released v1.1.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 : n023.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:01 PM UTC 2025
% Result : Unsatisfiable 16.91s 7.23s
% Output : CNFRefutation 17.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 16
% Syntax : Number of formulae : 685 ( 540 unt; 0 typ; 0 def)
% Number of atoms : 1007 ( 953 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 407 ( 85 ~; 322 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 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 : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 230 ( 230 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > identity > c > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b,type,
b: $i ).
tff(identity,type,
identity: $i ).
tff(c,type,
c: $i ).
tff(f_91,axiom,
b != c,
file(unknown,unknown) ).
tff(f_95,axiom,
c != identity,
file(unknown,unknown) ).
tff(f_89,axiom,
a != identity,
file(unknown,unknown) ).
tff(f_93,axiom,
b != identity,
file(unknown,unknown) ).
tff(f_75,axiom,
! [X] : ( multiply(X,inverse(X)) = identity ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(b,b) != c )
| ( multiply(b,multiply(b,b)) != a )
| ( multiply(b,multiply(b,multiply(b,b))) != identity ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
! [X] :
( ( X = a )
| ( X = b )
| ( X = c )
| ( X = identity ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_73,axiom,
! [X] : ( multiply(X,identity) = X ),
file(unknown,unknown) ).
tff(f_87,axiom,
a != c,
file(unknown,unknown) ).
tff(f_61,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_85,axiom,
a != b,
file(unknown,unknown) ).
tff(f_68,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_111,axiom,
( ( multiply(a,a) != b )
| ( multiply(a,multiply(a,a)) != c )
| ( multiply(a,multiply(a,multiply(a,a))) != identity ) ),
file(unknown,unknown) ).
tff(f_103,axiom,
( ( multiply(a,a) != identity )
| ( multiply(b,b) != identity )
| ( multiply(c,c) != identity ) ),
file(unknown,unknown) ).
tff(f_127,axiom,
( ( multiply(c,c) != a )
| ( multiply(c,multiply(c,c)) != b )
| ( multiply(c,multiply(c,multiply(c,c))) != identity ) ),
file(unknown,unknown) ).
tff(c_20,plain,
c != b,
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_24,plain,
identity != c,
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_18,plain,
identity != a,
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_22,plain,
identity != b,
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_10,plain,
! [X_7] : ( multiply(X_7,inverse(X_7)) = identity ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_30,plain,
( ( multiply(b,multiply(b,multiply(b,b))) != identity )
| ( multiply(b,multiply(b,b)) != a )
| ( multiply(b,b) != c ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_84085,plain,
multiply(b,b) != c,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_12,plain,
! [X_8] :
( ( identity = X_8 )
| ( c = X_8 )
| ( b = X_8 )
| ( a = X_8 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_8,plain,
! [X_6] : ( multiply(X_6,identity) = X_6 ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_16,plain,
c != a,
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_14,plain,
b != a,
inference(cnfTransformation,[status(thm)],[f_85]) ).
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_68]) ).
tff(c_28,plain,
( ( multiply(a,multiply(a,multiply(a,a))) != identity )
| ( multiply(a,multiply(a,a)) != c )
| ( multiply(a,a) != b ) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_615,plain,
multiply(a,a) != b,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_26,plain,
( ( multiply(c,c) != identity )
| ( multiply(b,b) != identity )
| ( multiply(a,a) != identity ) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_482,plain,
multiply(a,a) != identity,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_486,plain,
( ( multiply(a,a) = c )
| ( multiply(a,a) = b )
| ( multiply(a,a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_482]) ).
tff(c_2030,plain,
( ( multiply(a,a) = c )
| ( multiply(a,a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_615,c_486]) ).
tff(c_2031,plain,
multiply(a,a) = a,
inference(splitLeft,[status(thm)],[c_2030]) ).
tff(c_246,plain,
! [X_65,Y_66,Z_67] : ( multiply(multiply(X_65,Y_66),Z_67) = multiply(X_65,multiply(Y_66,Z_67)) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_490,plain,
! [X_88,Y_89] : ( multiply(X_88,multiply(Y_89,inverse(multiply(X_88,Y_89)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_246,c_10]) ).
tff(c_282,plain,
! [X_2,Z_67] : ( multiply(inverse(X_2),multiply(X_2,Z_67)) = multiply(identity,Z_67) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_246]) ).
tff(c_301,plain,
! [X_2,Z_67] : ( multiply(inverse(X_2),multiply(X_2,Z_67)) = Z_67 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_282]) ).
tff(c_498,plain,
! [Y_89,X_88] : ( multiply(Y_89,inverse(multiply(X_88,Y_89))) = multiply(inverse(X_88),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_490,c_301]) ).
tff(c_589,plain,
! [Y_89,X_88] : ( multiply(Y_89,inverse(multiply(X_88,Y_89))) = inverse(X_88) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_498]) ).
tff(c_2043,plain,
multiply(a,inverse(a)) = inverse(a),
inference(superposition,[status(thm),theory(equality)],[c_2031,c_589]) ).
tff(c_2056,plain,
inverse(a) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_2043]) ).
tff(c_622,plain,
! [Y_96,X_97] : ( multiply(Y_96,inverse(multiply(X_97,Y_96))) = inverse(X_97) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_498]) ).
tff(c_275,plain,
! [X_7,Z_67] : ( multiply(X_7,multiply(inverse(X_7),Z_67)) = multiply(identity,Z_67) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_246]) ).
tff(c_300,plain,
! [X_7,Z_67] : ( multiply(X_7,multiply(inverse(X_7),Z_67)) = Z_67 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_275]) ).
tff(c_1373,plain,
! [X_137,X_138] : ( inverse(multiply(X_137,inverse(X_138))) = multiply(X_138,inverse(X_137)) ),
inference(superposition,[status(thm),theory(equality)],[c_622,c_300]) ).
tff(c_1413,plain,
! [X_138,X_137] : ( multiply(multiply(X_138,inverse(X_137)),multiply(X_137,inverse(X_138))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_1373,c_4]) ).
tff(c_2066,plain,
! [X_137] : ( multiply(multiply(a,inverse(X_137)),multiply(X_137,identity)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_2056,c_1413]) ).
tff(c_2121,plain,
identity = a,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_4,c_6,c_8,c_2066]) ).
tff(c_2123,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_2121]) ).
tff(c_2124,plain,
multiply(a,a) = c,
inference(splitRight,[status(thm)],[c_2030]) ).
tff(c_32,plain,
( ( multiply(c,multiply(c,multiply(c,c))) != identity )
| ( multiply(c,multiply(c,c)) != b )
| ( multiply(c,c) != a ) ),
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_1115,plain,
multiply(c,c) != a,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_124,plain,
! [X_13] :
( ( identity = X_13 )
| ( c = X_13 )
| ( b = X_13 )
| ( a = X_13 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_151,plain,
! [X_7] :
( ( multiply(X_7,identity) = identity )
| ( inverse(X_7) = c )
| ( inverse(X_7) = b )
| ( inverse(X_7) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_10]) ).
tff(c_218,plain,
! [X_7] :
( ( identity = X_7 )
| ( inverse(X_7) = c )
| ( inverse(X_7) = b )
| ( inverse(X_7) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_151]) ).
tff(c_2326,plain,
multiply(inverse(a),c) = a,
inference(superposition,[status(thm),theory(equality)],[c_2124,c_301]) ).
tff(c_2372,plain,
( ( multiply(c,c) = a )
| ( identity = a )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_218,c_2326]) ).
tff(c_2387,plain,
( ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_18,c_1115,c_2372]) ).
tff(c_2719,plain,
inverse(a) = a,
inference(splitLeft,[status(thm)],[c_2387]) ).
tff(c_2771,plain,
multiply(a,a) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2719,c_10]) ).
tff(c_2791,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_2124,c_2771]) ).
tff(c_2793,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_2791]) ).
tff(c_2795,plain,
inverse(a) != a,
inference(splitRight,[status(thm)],[c_2387]) ).
tff(c_305,plain,
! [X_71,Z_72] : ( multiply(X_71,multiply(inverse(X_71),Z_72)) = Z_72 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_275]) ).
tff(c_350,plain,
! [X_71] : ( inverse(inverse(X_71)) = multiply(X_71,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_305]) ).
tff(c_370,plain,
! [X_71] : ( inverse(inverse(X_71)) = X_71 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_350]) ).
tff(c_2356,plain,
multiply(c,inverse(a)) = inverse(inverse(a)),
inference(superposition,[status(thm),theory(equality)],[c_2326,c_589]) ).
tff(c_2380,plain,
multiply(c,inverse(a)) = a,
inference(demodulation,[status(thm),theory(equality)],[c_370,c_2356]) ).
tff(c_2426,plain,
( ( multiply(c,c) = a )
| ( identity = a )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_218,c_2380]) ).
tff(c_2441,plain,
( ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_18,c_1115,c_2426]) ).
tff(c_2808,plain,
inverse(a) = b,
inference(negUnitSimplification,[status(thm)],[c_2795,c_2441]) ).
tff(c_2855,plain,
inverse(b) = a,
inference(superposition,[status(thm),theory(equality)],[c_2808,c_370]) ).
tff(c_2811,plain,
multiply(c,b) = a,
inference(demodulation,[status(thm),theory(equality)],[c_2808,c_2380]) ).
tff(c_2975,plain,
multiply(b,inverse(a)) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_2811,c_589]) ).
tff(c_2989,plain,
multiply(b,b) = inverse(c),
inference(demodulation,[status(thm),theory(equality)],[c_2808,c_2975]) ).
tff(c_789,plain,
multiply(b,b) != c,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_3251,plain,
inverse(c) != c,
inference(demodulation,[status(thm),theory(equality)],[c_2989,c_789]) ).
tff(c_2978,plain,
multiply(inverse(c),a) = b,
inference(superposition,[status(thm),theory(equality)],[c_2811,c_301]) ).
tff(c_3336,plain,
( ( multiply(identity,a) = b )
| ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_2978]) ).
tff(c_3354,plain,
( ( b = a )
| ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3336]) ).
tff(c_3355,plain,
( ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_3251,c_14,c_3354]) ).
tff(c_3640,plain,
inverse(c) = a,
inference(splitLeft,[status(thm)],[c_3355]) ).
tff(c_3687,plain,
inverse(a) = c,
inference(superposition,[status(thm),theory(equality)],[c_3640,c_370]) ).
tff(c_3712,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_2808,c_3687]) ).
tff(c_3714,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_3712]) ).
tff(c_3715,plain,
inverse(c) = b,
inference(splitRight,[status(thm)],[c_3355]) ).
tff(c_3776,plain,
inverse(b) = c,
inference(superposition,[status(thm),theory(equality)],[c_3715,c_370]) ).
tff(c_3801,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_2855,c_3776]) ).
tff(c_3803,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_3801]) ).
tff(c_3805,plain,
multiply(c,c) = a,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_3818,plain,
multiply(inverse(c),a) = c,
inference(superposition,[status(thm),theory(equality)],[c_3805,c_301]) ).
tff(c_3855,plain,
( ( multiply(identity,a) = c )
| ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_3818]) ).
tff(c_3864,plain,
( ( c = a )
| ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3855]) ).
tff(c_3865,plain,
( ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_16,c_3864]) ).
tff(c_4121,plain,
inverse(c) = a,
inference(splitLeft,[status(thm)],[c_3865]) ).
tff(c_160,plain,
! [X_2] :
( ( multiply(identity,X_2) = identity )
| ( inverse(X_2) = c )
| ( inverse(X_2) = b )
| ( inverse(X_2) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_4]) ).
tff(c_4272,plain,
! [X_283] :
( ( identity = X_283 )
| ( inverse(X_283) = c )
| ( inverse(X_283) = b )
| ( inverse(X_283) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_160]) ).
tff(c_506,plain,
! [Y_89,X_7] : ( multiply(Y_89,inverse(multiply(inverse(X_7),Y_89))) = multiply(X_7,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_490,c_300]) ).
tff(c_591,plain,
! [Y_89,X_7] : ( multiply(Y_89,inverse(multiply(inverse(X_7),Y_89))) = X_7 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_506]) ).
tff(c_4287,plain,
! [Y_89,X_283] :
( ( multiply(Y_89,inverse(multiply(c,Y_89))) = X_283 )
| ( identity = X_283 )
| ( inverse(X_283) = b )
| ( inverse(X_283) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_4272,c_591]) ).
tff(c_10327,plain,
! [X_430] :
( ( a = X_430 )
| ( identity = X_430 )
| ( inverse(X_430) = b )
| ( inverse(X_430) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4121,c_589,c_4287]) ).
tff(c_12360,plain,
( ( inverse(b) = b )
| ( b = a )
| ( identity = b )
| ( inverse(b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_10327,c_370]) ).
tff(c_12363,plain,
( ( inverse(b) = b )
| ( b = a )
| ( identity = b )
| ( inverse(b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12360,c_370]) ).
tff(c_12722,plain,
( ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_22,c_14,c_12363]) ).
tff(c_12779,plain,
inverse(b) = a,
inference(splitLeft,[status(thm)],[c_12722]) ).
tff(c_13171,plain,
inverse(a) = b,
inference(superposition,[status(thm),theory(equality)],[c_12779,c_370]) ).
tff(c_4142,plain,
inverse(a) = c,
inference(superposition,[status(thm),theory(equality)],[c_4121,c_370]) ).
tff(c_13214,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_13171,c_4142]) ).
tff(c_13216,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_13214]) ).
tff(c_13217,plain,
inverse(b) = b,
inference(splitRight,[status(thm)],[c_12722]) ).
tff(c_655,plain,
! [X_2,Z_67] : ( multiply(multiply(X_2,Z_67),inverse(Z_67)) = inverse(inverse(X_2)) ),
inference(superposition,[status(thm),theory(equality)],[c_301,c_622]) ).
tff(c_696,plain,
! [X_2,Z_67] : ( multiply(multiply(X_2,Z_67),inverse(Z_67)) = X_2 ),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_655]) ).
tff(c_13271,plain,
! [X_2] : ( multiply(multiply(X_2,b),b) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_13217,c_696]) ).
tff(c_4145,plain,
! [Z_67] : ( multiply(c,multiply(a,Z_67)) = Z_67 ),
inference(superposition,[status(thm),theory(equality)],[c_4121,c_300]) ).
tff(c_269,plain,
! [X_65,Y_66,Z_67] :
( ( multiply(X_65,multiply(Y_66,Z_67)) = multiply(identity,Z_67) )
| ( multiply(X_65,Y_66) = c )
| ( multiply(X_65,Y_66) = b )
| ( multiply(X_65,Y_66) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_246]) ).
tff(c_4962,plain,
! [X_314,Y_315,Z_316] :
( ( multiply(X_314,multiply(Y_315,Z_316)) = Z_316 )
| ( multiply(X_314,Y_315) = c )
| ( multiply(X_314,Y_315) = b )
| ( multiply(X_314,Y_315) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_269]) ).
tff(c_5157,plain,
! [X_314,X_7] :
( ( multiply(X_314,identity) = inverse(X_7) )
| ( multiply(X_314,X_7) = c )
| ( multiply(X_314,X_7) = b )
| ( multiply(X_314,X_7) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_4962]) ).
tff(c_24572,plain,
! [X_804,X_805] :
( ( inverse(X_804) = X_805 )
| ( multiply(X_805,X_804) = c )
| ( multiply(X_805,X_804) = b )
| ( multiply(X_805,X_804) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_5157]) ).
tff(c_4480,plain,
! [Z_294] : ( multiply(a,multiply(c,Z_294)) = Z_294 ),
inference(superposition,[status(thm),theory(equality)],[c_4121,c_301]) ).
tff(c_4518,plain,
! [X_88] : ( multiply(a,inverse(X_88)) = inverse(multiply(X_88,c)) ),
inference(superposition,[status(thm),theory(equality)],[c_589,c_4480]) ).
tff(c_13262,plain,
inverse(multiply(b,c)) = multiply(a,b),
inference(superposition,[status(thm),theory(equality)],[c_13217,c_4518]) ).
tff(c_14836,plain,
multiply(multiply(b,c),multiply(a,b)) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13262,c_10]) ).
tff(c_24710,plain,
( ( multiply(c,multiply(a,b)) = identity )
| ( inverse(c) = b )
| ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_24572,c_14836]) ).
tff(c_25416,plain,
( ( identity = b )
| ( b = a )
| ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4121,c_4145,c_24710]) ).
tff(c_25417,plain,
( ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_14,c_22,c_25416]) ).
tff(c_25679,plain,
multiply(b,c) = a,
inference(splitLeft,[status(thm)],[c_25417]) ).
tff(c_13391,plain,
! [Z_658] : ( multiply(b,multiply(b,Z_658)) = Z_658 ),
inference(superposition,[status(thm),theory(equality)],[c_13217,c_300]) ).
tff(c_13431,plain,
! [Z_658] : ( multiply(Z_658,inverse(multiply(b,Z_658))) = b ),
inference(superposition,[status(thm),theory(equality)],[c_13391,c_696]) ).
tff(c_25714,plain,
multiply(c,inverse(a)) = b,
inference(superposition,[status(thm),theory(equality)],[c_25679,c_13431]) ).
tff(c_25800,plain,
b = a,
inference(demodulation,[status(thm),theory(equality)],[c_3805,c_4142,c_25714]) ).
tff(c_25802,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_25800]) ).
tff(c_25803,plain,
multiply(b,c) = b,
inference(splitRight,[status(thm)],[c_25417]) ).
tff(c_14839,plain,
multiply(multiply(a,b),multiply(b,c)) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13262,c_4]) ).
tff(c_25808,plain,
multiply(multiply(a,b),b) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25803,c_14839]) ).
tff(c_25811,plain,
identity = a,
inference(demodulation,[status(thm),theory(equality)],[c_13271,c_25808]) ).
tff(c_25813,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_25811]) ).
tff(c_25814,plain,
( ( inverse(c) = b )
| ( inverse(c) = c ) ),
inference(splitRight,[status(thm)],[c_3865]) ).
tff(c_25900,plain,
inverse(c) = c,
inference(splitLeft,[status(thm)],[c_25814]) ).
tff(c_25929,plain,
multiply(c,c) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25900,c_10]) ).
tff(c_25939,plain,
identity = a,
inference(demodulation,[status(thm),theory(equality)],[c_3805,c_25929]) ).
tff(c_25941,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_25939]) ).
tff(c_25942,plain,
inverse(c) = b,
inference(splitRight,[status(thm)],[c_25814]) ).
tff(c_3836,plain,
multiply(a,inverse(c)) = c,
inference(superposition,[status(thm),theory(equality)],[c_3818,c_591]) ).
tff(c_25949,plain,
multiply(a,b) = c,
inference(demodulation,[status(thm),theory(equality)],[c_25942,c_3836]) ).
tff(c_222,plain,
! [X_2] :
( ( identity = X_2 )
| ( inverse(X_2) = c )
| ( inverse(X_2) = b )
| ( inverse(X_2) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_160]) ).
tff(c_3815,plain,
multiply(c,inverse(a)) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_3805,c_589]) ).
tff(c_25948,plain,
multiply(c,inverse(a)) = b,
inference(demodulation,[status(thm),theory(equality)],[c_25942,c_3815]) ).
tff(c_26275,plain,
( ( multiply(c,c) = b )
| ( identity = a )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_25948]) ).
tff(c_26290,plain,
( ( b = a )
| ( identity = a )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3805,c_26275]) ).
tff(c_26291,plain,
( ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_18,c_14,c_26290]) ).
tff(c_26380,plain,
inverse(a) = a,
inference(splitLeft,[status(thm)],[c_26291]) ).
tff(c_26409,plain,
multiply(a,a) = identity,
inference(superposition,[status(thm),theory(equality)],[c_26380,c_10]) ).
tff(c_26425,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_482,c_26409]) ).
tff(c_26426,plain,
inverse(a) = b,
inference(splitRight,[status(thm)],[c_26291]) ).
tff(c_26465,plain,
multiply(a,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_26426,c_10]) ).
tff(c_26479,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_25949,c_26465]) ).
tff(c_26481,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_26479]) ).
tff(c_26483,plain,
multiply(b,b) = c,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_27722,plain,
( ( multiply(a,a) = c )
| ( multiply(a,a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_615,c_486]) ).
tff(c_27723,plain,
multiply(a,a) = a,
inference(splitLeft,[status(thm)],[c_27722]) ).
tff(c_27732,plain,
multiply(a,inverse(a)) = inverse(a),
inference(superposition,[status(thm),theory(equality)],[c_27723,c_589]) ).
tff(c_27744,plain,
inverse(a) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_27732]) ).
tff(c_27751,plain,
! [Y_89] : ( multiply(Y_89,inverse(multiply(identity,Y_89))) = a ),
inference(superposition,[status(thm),theory(equality)],[c_27744,c_591]) ).
tff(c_27787,plain,
identity = a,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_2,c_27751]) ).
tff(c_27789,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_27787]) ).
tff(c_27790,plain,
multiply(a,a) = c,
inference(splitRight,[status(thm)],[c_27722]) ).
tff(c_26575,plain,
multiply(c,c) != a,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_26496,plain,
! [Z_5] : ( multiply(b,multiply(b,Z_5)) = multiply(c,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_26483,c_6]) ).
tff(c_26482,plain,
( ( multiply(b,multiply(b,b)) != a )
| ( multiply(b,multiply(b,multiply(b,b))) != identity ) ),
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_26537,plain,
( ( multiply(b,c) != a )
| ( multiply(b,multiply(b,c)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26483,c_26483,c_26482]) ).
tff(c_26538,plain,
multiply(b,multiply(b,c)) != identity,
inference(splitLeft,[status(thm)],[c_26537]) ).
tff(c_26638,plain,
multiply(c,c) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_26496,c_26538]) ).
tff(c_26702,plain,
( ( multiply(c,c) = c )
| ( multiply(c,c) = b )
| ( multiply(c,c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_26638]) ).
tff(c_26705,plain,
( ( multiply(c,c) = c )
| ( multiply(c,c) = b ) ),
inference(negUnitSimplification,[status(thm)],[c_26575,c_26702]) ).
tff(c_27204,plain,
multiply(c,c) = b,
inference(splitLeft,[status(thm)],[c_26705]) ).
tff(c_27877,plain,
multiply(inverse(a),c) = a,
inference(superposition,[status(thm),theory(equality)],[c_27790,c_301]) ).
tff(c_27912,plain,
( ( multiply(c,c) = a )
| ( identity = a )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_27877]) ).
tff(c_27925,plain,
( ( b = a )
| ( identity = a )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_27204,c_27912]) ).
tff(c_27926,plain,
( ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_18,c_14,c_27925]) ).
tff(c_28212,plain,
inverse(a) = a,
inference(splitLeft,[status(thm)],[c_27926]) ).
tff(c_28240,plain,
multiply(a,a) = identity,
inference(superposition,[status(thm),theory(equality)],[c_28212,c_10]) ).
tff(c_28255,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_27790,c_28240]) ).
tff(c_28257,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_28255]) ).
tff(c_28258,plain,
inverse(a) = b,
inference(splitRight,[status(thm)],[c_27926]) ).
tff(c_28290,plain,
inverse(b) = a,
inference(superposition,[status(thm),theory(equality)],[c_28258,c_370]) ).
tff(c_26493,plain,
multiply(inverse(b),c) = b,
inference(superposition,[status(thm),theory(equality)],[c_26483,c_301]) ).
tff(c_26511,plain,
multiply(c,inverse(b)) = inverse(inverse(b)),
inference(superposition,[status(thm),theory(equality)],[c_26493,c_589]) ).
tff(c_26529,plain,
multiply(c,inverse(b)) = b,
inference(demodulation,[status(thm),theory(equality)],[c_370,c_26511]) ).
tff(c_27537,plain,
multiply(c,inverse(b)) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_27204,c_589]) ).
tff(c_27549,plain,
inverse(c) = b,
inference(demodulation,[status(thm),theory(equality)],[c_26529,c_27537]) ).
tff(c_26490,plain,
multiply(b,inverse(c)) = inverse(b),
inference(superposition,[status(thm),theory(equality)],[c_26483,c_589]) ).
tff(c_27556,plain,
multiply(b,b) = inverse(b),
inference(demodulation,[status(thm),theory(equality)],[c_27549,c_26490]) ).
tff(c_27558,plain,
inverse(b) = c,
inference(demodulation,[status(thm),theory(equality)],[c_26483,c_27556]) ).
tff(c_28315,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_28290,c_27558]) ).
tff(c_28317,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_28315]) ).
tff(c_28318,plain,
multiply(c,c) = c,
inference(splitRight,[status(thm)],[c_26705]) ).
tff(c_28333,plain,
multiply(c,inverse(c)) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_28318,c_589]) ).
tff(c_28345,plain,
inverse(c) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_28333]) ).
tff(c_28358,plain,
! [Y_89] : ( multiply(Y_89,inverse(multiply(identity,Y_89))) = c ),
inference(superposition,[status(thm),theory(equality)],[c_28345,c_591]) ).
tff(c_28394,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_2,c_28358]) ).
tff(c_28396,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_28394]) ).
tff(c_28398,plain,
multiply(c,c) = a,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_29139,plain,
! [X_1072] :
( ( identity = X_1072 )
| ( inverse(X_1072) = c )
| ( inverse(X_1072) = b )
| ( inverse(X_1072) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_160]) ).
tff(c_29187,plain,
( ( multiply(c,c) = b )
| ( identity = b )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_29139,c_26493]) ).
tff(c_29254,plain,
( ( b = a )
| ( identity = b )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28398,c_29187]) ).
tff(c_29255,plain,
( ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_22,c_14,c_29254]) ).
tff(c_29267,plain,
inverse(b) = a,
inference(splitLeft,[status(thm)],[c_29255]) ).
tff(c_29274,plain,
multiply(a,c) = b,
inference(demodulation,[status(thm),theory(equality)],[c_29267,c_26493]) ).
tff(c_29290,plain,
inverse(a) = b,
inference(superposition,[status(thm),theory(equality)],[c_29267,c_370]) ).
tff(c_28572,plain,
multiply(inverse(b),inverse(b)) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_26490,c_301]) ).
tff(c_29268,plain,
multiply(a,a) = inverse(c),
inference(demodulation,[status(thm),theory(equality)],[c_29267,c_29267,c_28572]) ).
tff(c_29558,plain,
inverse(c) != b,
inference(demodulation,[status(thm),theory(equality)],[c_29268,c_615]) ).
tff(c_29591,plain,
( ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29268,c_29268,c_29268,c_486]) ).
tff(c_29592,plain,
( ( inverse(c) = c )
| ( inverse(c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_29558,c_29591]) ).
tff(c_29593,plain,
inverse(c) = a,
inference(splitLeft,[status(thm)],[c_29592]) ).
tff(c_29616,plain,
inverse(a) = c,
inference(superposition,[status(thm),theory(equality)],[c_29593,c_370]) ).
tff(c_29636,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_29290,c_29616]) ).
tff(c_29638,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_29636]) ).
tff(c_29639,plain,
inverse(c) = c,
inference(splitRight,[status(thm)],[c_29592]) ).
tff(c_28408,plain,
multiply(inverse(c),a) = c,
inference(superposition,[status(thm),theory(equality)],[c_28398,c_301]) ).
tff(c_28485,plain,
multiply(a,inverse(c)) = inverse(inverse(c)),
inference(superposition,[status(thm),theory(equality)],[c_28408,c_589]) ).
tff(c_28503,plain,
multiply(a,inverse(c)) = c,
inference(demodulation,[status(thm),theory(equality)],[c_370,c_28485]) ).
tff(c_29734,plain,
multiply(a,c) = c,
inference(demodulation,[status(thm),theory(equality)],[c_29639,c_28503]) ).
tff(c_29736,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_29274,c_29734]) ).
tff(c_29738,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_29736]) ).
tff(c_29739,plain,
inverse(b) = b,
inference(splitRight,[status(thm)],[c_29255]) ).
tff(c_29770,plain,
multiply(b,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_29739,c_10]) ).
tff(c_29785,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_26483,c_29770]) ).
tff(c_29787,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_29785]) ).
tff(c_29789,plain,
multiply(b,multiply(b,c)) = identity,
inference(splitRight,[status(thm)],[c_26537]) ).
tff(c_29831,plain,
multiply(inverse(b),identity) = multiply(b,c),
inference(superposition,[status(thm),theory(equality)],[c_29789,c_301]) ).
tff(c_29847,plain,
multiply(b,c) = inverse(b),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_29831]) ).
tff(c_29788,plain,
multiply(b,c) != a,
inference(splitRight,[status(thm)],[c_26537]) ).
tff(c_29838,plain,
( ( multiply(b,identity) = identity )
| ( multiply(b,c) = c )
| ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_29789]) ).
tff(c_29850,plain,
( ( identity = b )
| ( multiply(b,c) = c )
| ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_29838]) ).
tff(c_29851,plain,
( ( multiply(b,c) = c )
| ( multiply(b,c) = b ) ),
inference(negUnitSimplification,[status(thm)],[c_29788,c_22,c_29850]) ).
tff(c_30072,plain,
( ( inverse(b) = c )
| ( inverse(b) = b ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29847,c_29847,c_29851]) ).
tff(c_30073,plain,
inverse(b) = b,
inference(splitLeft,[status(thm)],[c_30072]) ).
tff(c_30096,plain,
multiply(b,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_30073,c_10]) ).
tff(c_30106,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_26483,c_30096]) ).
tff(c_30108,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_30106]) ).
tff(c_30109,plain,
inverse(b) = c,
inference(splitRight,[status(thm)],[c_30072]) ).
tff(c_30126,plain,
inverse(c) = b,
inference(superposition,[status(thm),theory(equality)],[c_30109,c_370]) ).
tff(c_29864,plain,
multiply(c,inverse(inverse(b))) = inverse(b),
inference(superposition,[status(thm),theory(equality)],[c_29847,c_589]) ).
tff(c_29876,plain,
multiply(c,b) = inverse(b),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_29864]) ).
tff(c_29895,plain,
multiply(b,inverse(inverse(b))) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_29876,c_589]) ).
tff(c_29907,plain,
inverse(c) = c,
inference(demodulation,[status(thm),theory(equality)],[c_26483,c_370,c_29895]) ).
tff(c_30145,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_30126,c_29907]) ).
tff(c_30147,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_30145]) ).
tff(c_30149,plain,
multiply(a,a) = b,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_30160,plain,
! [Z_5] : ( multiply(a,multiply(a,Z_5)) = multiply(b,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_30149,c_6]) ).
tff(c_30148,plain,
( ( multiply(a,multiply(a,a)) != c )
| ( multiply(a,multiply(a,multiply(a,a))) != identity ) ),
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_30169,plain,
( ( multiply(a,b) != c )
| ( multiply(a,multiply(a,b)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_30149,c_30148]) ).
tff(c_30170,plain,
multiply(a,multiply(a,b)) != identity,
inference(splitLeft,[status(thm)],[c_30169]) ).
tff(c_56746,plain,
multiply(b,b) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_30160,c_30170]) ).
tff(c_256,plain,
! [X_65,Y_66] : ( multiply(X_65,multiply(Y_66,inverse(multiply(X_65,Y_66)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_246,c_10]) ).
tff(c_30154,plain,
multiply(a,multiply(a,inverse(b))) = identity,
inference(superposition,[status(thm),theory(equality)],[c_30149,c_256]) ).
tff(c_30220,plain,
( ( multiply(a,multiply(a,identity)) = identity )
| ( inverse(b) = c )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_30154]) ).
tff(c_30235,plain,
( ( identity = b )
| ( inverse(b) = c )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_8,c_30220]) ).
tff(c_30236,plain,
( ( inverse(b) = c )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_22,c_30235]) ).
tff(c_57130,plain,
inverse(b) = a,
inference(splitLeft,[status(thm)],[c_30236]) ).
tff(c_56747,plain,
! [Z_2062] : ( multiply(a,multiply(a,Z_2062)) = multiply(b,Z_2062) ),
inference(superposition,[status(thm),theory(equality)],[c_30149,c_6]) ).
tff(c_56803,plain,
multiply(b,inverse(a)) = multiply(a,identity),
inference(superposition,[status(thm),theory(equality)],[c_10,c_56747]) ).
tff(c_56819,plain,
multiply(b,inverse(a)) = a,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_56803]) ).
tff(c_56833,plain,
multiply(inverse(b),a) = inverse(a),
inference(superposition,[status(thm),theory(equality)],[c_56819,c_301]) ).
tff(c_57132,plain,
multiply(a,a) = inverse(a),
inference(demodulation,[status(thm),theory(equality)],[c_57130,c_56833]) ).
tff(c_57135,plain,
inverse(a) = b,
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_57132]) ).
tff(c_57162,plain,
multiply(b,b) = a,
inference(demodulation,[status(thm),theory(equality)],[c_57135,c_56819]) ).
tff(c_30157,plain,
multiply(inverse(a),b) = a,
inference(superposition,[status(thm),theory(equality)],[c_30149,c_301]) ).
tff(c_30187,plain,
( ( multiply(identity,b) = a )
| ( inverse(a) = c )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_30157]) ).
tff(c_30195,plain,
( ( b = a )
| ( inverse(a) = c )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30187]) ).
tff(c_30196,plain,
( ( inverse(a) = c )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_14,c_30195]) ).
tff(c_56050,plain,
inverse(a) = a,
inference(splitLeft,[status(thm)],[c_30196]) ).
tff(c_56082,plain,
multiply(a,a) = identity,
inference(superposition,[status(thm),theory(equality)],[c_56050,c_10]) ).
tff(c_56097,plain,
identity = b,
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_56082]) ).
tff(c_56099,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22,c_56097]) ).
tff(c_56100,plain,
( ( inverse(a) = b )
| ( inverse(a) = c ) ),
inference(splitRight,[status(thm)],[c_30196]) ).
tff(c_56110,plain,
inverse(a) = c,
inference(splitLeft,[status(thm)],[c_56100]) ).
tff(c_56117,plain,
multiply(c,b) = a,
inference(demodulation,[status(thm),theory(equality)],[c_56110,c_30157]) ).
tff(c_30213,plain,
multiply(inverse(a),identity) = multiply(a,inverse(b)),
inference(superposition,[status(thm),theory(equality)],[c_30154,c_301]) ).
tff(c_30232,plain,
multiply(a,inverse(b)) = inverse(a),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_30213]) ).
tff(c_30255,plain,
multiply(inverse(a),inverse(a)) = inverse(b),
inference(superposition,[status(thm),theory(equality)],[c_30232,c_301]) ).
tff(c_56113,plain,
multiply(c,c) = inverse(b),
inference(demodulation,[status(thm),theory(equality)],[c_56110,c_56110,c_30255]) ).
tff(c_30242,plain,
multiply(c,c) != a,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_56373,plain,
inverse(b) != a,
inference(demodulation,[status(thm),theory(equality)],[c_56113,c_30242]) ).
tff(c_56142,plain,
multiply(a,c) = identity,
inference(superposition,[status(thm),theory(equality)],[c_56110,c_10]) ).
tff(c_56116,plain,
multiply(a,inverse(b)) = c,
inference(demodulation,[status(thm),theory(equality)],[c_56110,c_30232]) ).
tff(c_56349,plain,
( ( multiply(a,c) = c )
| ( identity = b )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_56116]) ).
tff(c_56363,plain,
( ( identity = c )
| ( identity = b )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_56142,c_56349]) ).
tff(c_56364,plain,
( ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_22,c_24,c_56363]) ).
tff(c_56415,plain,
inverse(b) = b,
inference(negUnitSimplification,[status(thm)],[c_56373,c_56364]) ).
tff(c_30395,plain,
multiply(b,b) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_30160,c_30170]) ).
tff(c_30916,plain,
inverse(b) = a,
inference(splitLeft,[status(thm)],[c_30236]) ).
tff(c_30920,plain,
multiply(a,a) = inverse(a),
inference(demodulation,[status(thm),theory(equality)],[c_30916,c_30232]) ).
tff(c_30922,plain,
inverse(a) = b,
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_30920]) ).
tff(c_31024,plain,
! [X_1235] :
( ( identity = X_1235 )
| ( inverse(X_1235) = c )
| ( inverse(X_1235) = b )
| ( inverse(X_1235) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_160]) ).
tff(c_40915,plain,
! [X_1452] :
( ( multiply(c,X_1452) = identity )
| ( identity = X_1452 )
| ( inverse(X_1452) = b )
| ( inverse(X_1452) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_31024,c_4]) ).
tff(c_41078,plain,
! [X_1452] :
( ( multiply(inverse(c),identity) = X_1452 )
| ( identity = X_1452 )
| ( inverse(X_1452) = b )
| ( inverse(X_1452) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_40915,c_301]) ).
tff(c_42477,plain,
( ( inverse(c) = c )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_41078]) ).
tff(c_42480,plain,
( ( inverse(c) = c )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_42477,c_370]) ).
tff(c_42881,plain,
( ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_24,c_42480]) ).
tff(c_42947,plain,
inverse(c) = a,
inference(splitLeft,[status(thm)],[c_42881]) ).
tff(c_43838,plain,
inverse(a) = c,
inference(superposition,[status(thm),theory(equality)],[c_42947,c_370]) ).
tff(c_43869,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_30922,c_43838]) ).
tff(c_43871,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_43869]) ).
tff(c_43873,plain,
inverse(c) != a,
inference(splitRight,[status(thm)],[c_42881]) ).
tff(c_42531,plain,
( ( inverse(c) = c )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_41078]) ).
tff(c_42534,plain,
( ( multiply(c,c) = identity )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_42531,c_10]) ).
tff(c_42891,plain,
( ( multiply(c,c) = identity )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_24,c_42534]) ).
tff(c_52896,plain,
( ( multiply(c,c) = identity )
| ( inverse(c) = b ) ),
inference(negUnitSimplification,[status(thm)],[c_43873,c_42891]) ).
tff(c_52897,plain,
inverse(c) = b,
inference(splitLeft,[status(thm)],[c_52896]) ).
tff(c_52960,plain,
inverse(b) = c,
inference(superposition,[status(thm),theory(equality)],[c_52897,c_370]) ).
tff(c_52991,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_30916,c_52960]) ).
tff(c_52993,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_52991]) ).
tff(c_52995,plain,
inverse(c) != b,
inference(splitRight,[status(thm)],[c_52896]) ).
tff(c_30525,plain,
! [Y_1208,X_1209] : ( multiply(Y_1208,inverse(multiply(X_1209,Y_1208))) = inverse(X_1209) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_498]) ).
tff(c_30589,plain,
! [X_2,Z_67] : ( multiply(multiply(X_2,Z_67),inverse(Z_67)) = inverse(inverse(X_2)) ),
inference(superposition,[status(thm),theory(equality)],[c_301,c_30525]) ).
tff(c_30637,plain,
! [X_2,Z_67] : ( multiply(multiply(X_2,Z_67),inverse(Z_67)) = X_2 ),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_30589]) ).
tff(c_30962,plain,
! [X_2] : ( multiply(multiply(X_2,a),b) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_30922,c_30637]) ).
tff(c_30955,plain,
multiply(b,b) = a,
inference(demodulation,[status(thm),theory(equality)],[c_30922,c_30157]) ).
tff(c_43872,plain,
( ( inverse(c) = b )
| ( inverse(c) = c ) ),
inference(splitRight,[status(thm)],[c_42881]) ).
tff(c_43888,plain,
inverse(c) = c,
inference(splitLeft,[status(thm)],[c_43872]) ).
tff(c_44058,plain,
! [Z_67] : ( multiply(c,multiply(c,Z_67)) = Z_67 ),
inference(superposition,[status(thm),theory(equality)],[c_43888,c_300]) ).
tff(c_414,plain,
! [X_80,Z_81] : ( multiply(inverse(X_80),multiply(X_80,Z_81)) = Z_81 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_282]) ).
tff(c_447,plain,
! [X_80,Z_81] :
( ( multiply(inverse(X_80),identity) = Z_81 )
| ( multiply(X_80,Z_81) = c )
| ( multiply(X_80,Z_81) = b )
| ( multiply(X_80,Z_81) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_414]) ).
tff(c_51695,plain,
! [X_1801,Z_1802] :
( ( inverse(X_1801) = Z_1802 )
| ( multiply(X_1801,Z_1802) = c )
| ( multiply(X_1801,Z_1802) = b )
| ( multiply(X_1801,Z_1802) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_447]) ).
tff(c_31174,plain,
! [Z_1245] : ( multiply(a,multiply(b,Z_1245)) = Z_1245 ),
inference(superposition,[status(thm),theory(equality)],[c_30916,c_301]) ).
tff(c_31180,plain,
! [Z_1245] : ( multiply(Z_1245,inverse(multiply(b,Z_1245))) = a ),
inference(superposition,[status(thm),theory(equality)],[c_31174,c_30637]) ).
tff(c_45014,plain,
! [Z_1718] : ( multiply(c,multiply(c,Z_1718)) = Z_1718 ),
inference(superposition,[status(thm),theory(equality)],[c_43888,c_300]) ).
tff(c_45162,plain,
inverse(multiply(b,c)) = multiply(c,a),
inference(superposition,[status(thm),theory(equality)],[c_31180,c_45014]) ).
tff(c_47194,plain,
multiply(multiply(b,c),multiply(c,a)) = identity,
inference(superposition,[status(thm),theory(equality)],[c_45162,c_10]) ).
tff(c_51733,plain,
( ( multiply(c,multiply(c,a)) = identity )
| ( inverse(b) = c )
| ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_51695,c_47194]) ).
tff(c_52493,plain,
( ( identity = a )
| ( c = a )
| ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_30916,c_44058,c_51733]) ).
tff(c_52494,plain,
( ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_16,c_18,c_52493]) ).
tff(c_52761,plain,
multiply(b,c) = a,
inference(splitLeft,[status(thm)],[c_52494]) ).
tff(c_30646,plain,
! [X_1213,Z_1214] : ( multiply(multiply(X_1213,Z_1214),inverse(Z_1214)) = X_1213 ),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_30589]) ).
tff(c_30706,plain,
! [X_1213,X_71] : ( multiply(multiply(X_1213,inverse(X_71)),X_71) = X_1213 ),
inference(superposition,[status(thm),theory(equality)],[c_370,c_30646]) ).
tff(c_45231,plain,
! [X_1722] : ( multiply(multiply(X_1722,c),c) = X_1722 ),
inference(superposition,[status(thm),theory(equality)],[c_43888,c_30706]) ).
tff(c_45279,plain,
! [X_1722] : ( multiply(inverse(multiply(X_1722,c)),X_1722) = c ),
inference(superposition,[status(thm),theory(equality)],[c_45231,c_301]) ).
tff(c_52783,plain,
multiply(inverse(a),b) = c,
inference(superposition,[status(thm),theory(equality)],[c_52761,c_45279]) ).
tff(c_52881,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_30955,c_30922,c_52783]) ).
tff(c_52883,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_52881]) ).
tff(c_52884,plain,
multiply(b,c) = b,
inference(splitRight,[status(thm)],[c_52494]) ).
tff(c_47197,plain,
multiply(multiply(c,a),multiply(b,c)) = identity,
inference(superposition,[status(thm),theory(equality)],[c_45162,c_4]) ).
tff(c_52888,plain,
multiply(multiply(c,a),b) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_52884,c_47197]) ).
tff(c_52891,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_30962,c_52888]) ).
tff(c_52893,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_52891]) ).
tff(c_52894,plain,
inverse(c) = b,
inference(splitRight,[status(thm)],[c_43872]) ).
tff(c_53010,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52995,c_52894]) ).
tff(c_53011,plain,
( ( inverse(b) = b )
| ( inverse(b) = c ) ),
inference(splitRight,[status(thm)],[c_30236]) ).
tff(c_53017,plain,
inverse(b) = c,
inference(splitLeft,[status(thm)],[c_53011]) ).
tff(c_53155,plain,
multiply(c,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_53017,c_4]) ).
tff(c_30358,plain,
multiply(b,b) != c,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_30206,plain,
( ( multiply(a,multiply(a,b)) = c )
| ( multiply(a,multiply(a,b)) = b )
| ( multiply(a,multiply(a,b)) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_30170]) ).
tff(c_54753,plain,
( ( multiply(b,b) = c )
| ( multiply(b,b) = b )
| ( multiply(b,b) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_30160,c_30160,c_30160,c_30206]) ).
tff(c_54754,plain,
( ( multiply(b,b) = b )
| ( multiply(b,b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_30358,c_54753]) ).
tff(c_54755,plain,
multiply(b,b) = a,
inference(splitLeft,[status(thm)],[c_54754]) ).
tff(c_53352,plain,
! [X_1846] : ( multiply(multiply(X_1846,b),c) = X_1846 ),
inference(superposition,[status(thm),theory(equality)],[c_53017,c_30637]) ).
tff(c_53364,plain,
! [X_1846] : ( multiply(inverse(multiply(X_1846,b)),X_1846) = c ),
inference(superposition,[status(thm),theory(equality)],[c_53352,c_301]) ).
tff(c_54766,plain,
multiply(inverse(a),b) = c,
inference(superposition,[status(thm),theory(equality)],[c_54755,c_53364]) ).
tff(c_54797,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_30157,c_54766]) ).
tff(c_54799,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_54797]) ).
tff(c_54800,plain,
multiply(b,b) = b,
inference(splitRight,[status(thm)],[c_54754]) ).
tff(c_54818,plain,
multiply(inverse(b),b) = c,
inference(superposition,[status(thm),theory(equality)],[c_54800,c_53364]) ).
tff(c_54849,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_53155,c_53017,c_54818]) ).
tff(c_54851,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_54849]) ).
tff(c_54852,plain,
inverse(b) = b,
inference(splitRight,[status(thm)],[c_53011]) ).
tff(c_54922,plain,
multiply(b,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_54852,c_10]) ).
tff(c_54933,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_30395,c_54922]) ).
tff(c_54935,plain,
multiply(b,b) = c,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_55242,plain,
! [Z_1949] : ( multiply(b,multiply(b,Z_1949)) = multiply(c,Z_1949) ),
inference(superposition,[status(thm),theory(equality)],[c_54935,c_6]) ).
tff(c_55304,plain,
multiply(c,inverse(b)) = multiply(b,identity),
inference(superposition,[status(thm),theory(equality)],[c_10,c_55242]) ).
tff(c_55321,plain,
multiply(c,inverse(b)) = b,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_55304]) ).
tff(c_56420,plain,
multiply(c,b) = b,
inference(demodulation,[status(thm),theory(equality)],[c_56415,c_55321]) ).
tff(c_56423,plain,
b = a,
inference(demodulation,[status(thm),theory(equality)],[c_56117,c_56420]) ).
tff(c_56425,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_56423]) ).
tff(c_56426,plain,
inverse(a) = b,
inference(splitRight,[status(thm)],[c_56100]) ).
tff(c_56454,plain,
inverse(b) = a,
inference(superposition,[status(thm),theory(equality)],[c_56426,c_370]) ).
tff(c_56430,plain,
multiply(b,b) = inverse(b),
inference(demodulation,[status(thm),theory(equality)],[c_56426,c_56426,c_30255]) ).
tff(c_56435,plain,
inverse(b) = c,
inference(demodulation,[status(thm),theory(equality)],[c_54935,c_56430]) ).
tff(c_56531,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_56454,c_56435]) ).
tff(c_56533,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_56531]) ).
tff(c_56535,plain,
multiply(c,c) = a,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_56539,plain,
multiply(c,multiply(c,inverse(a))) = identity,
inference(superposition,[status(thm),theory(equality)],[c_56535,c_256]) ).
tff(c_56627,plain,
multiply(inverse(c),identity) = multiply(c,inverse(a)),
inference(superposition,[status(thm),theory(equality)],[c_56539,c_301]) ).
tff(c_56646,plain,
multiply(c,inverse(a)) = inverse(c),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_56627]) ).
tff(c_57163,plain,
multiply(c,b) = inverse(c),
inference(demodulation,[status(thm),theory(equality)],[c_57135,c_56646]) ).
tff(c_57395,plain,
multiply(inverse(c),inverse(c)) = b,
inference(superposition,[status(thm),theory(equality)],[c_57163,c_301]) ).
tff(c_57675,plain,
( ( multiply(inverse(c),c) = b )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_57395]) ).
tff(c_57692,plain,
( ( identity = b )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_57675]) ).
tff(c_57693,plain,
( ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_24,c_22,c_57692]) ).
tff(c_57703,plain,
inverse(c) = a,
inference(splitLeft,[status(thm)],[c_57693]) ).
tff(c_56871,plain,
! [Z_2075] : ( multiply(c,multiply(c,Z_2075)) = multiply(a,Z_2075) ),
inference(superposition,[status(thm),theory(equality)],[c_56535,c_6]) ).
tff(c_56924,plain,
multiply(a,inverse(c)) = multiply(c,identity),
inference(superposition,[status(thm),theory(equality)],[c_10,c_56871]) ).
tff(c_56939,plain,
multiply(a,inverse(c)) = c,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_56924]) ).
tff(c_57707,plain,
multiply(a,a) = c,
inference(demodulation,[status(thm),theory(equality)],[c_57703,c_56939]) ).
tff(c_57710,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_57707]) ).
tff(c_57712,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_57710]) ).
tff(c_57713,plain,
inverse(c) = b,
inference(splitRight,[status(thm)],[c_57693]) ).
tff(c_57724,plain,
multiply(b,b) = b,
inference(demodulation,[status(thm),theory(equality)],[c_57713,c_57713,c_57395]) ).
tff(c_57729,plain,
b = a,
inference(demodulation,[status(thm),theory(equality)],[c_57162,c_57724]) ).
tff(c_57731,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_57729]) ).
tff(c_57732,plain,
( ( inverse(b) = b )
| ( inverse(b) = c ) ),
inference(splitRight,[status(thm)],[c_30236]) ).
tff(c_57738,plain,
inverse(b) = c,
inference(splitLeft,[status(thm)],[c_57732]) ).
tff(c_57871,plain,
inverse(c) = b,
inference(superposition,[status(thm),theory(equality)],[c_57738,c_370]) ).
tff(c_57899,plain,
multiply(a,b) = c,
inference(demodulation,[status(thm),theory(equality)],[c_57871,c_56939]) ).
tff(c_57861,plain,
multiply(a,c) = inverse(a),
inference(demodulation,[status(thm),theory(equality)],[c_57738,c_30232]) ).
tff(c_56902,plain,
multiply(c,a) = multiply(a,c),
inference(superposition,[status(thm),theory(equality)],[c_56535,c_56871]) ).
tff(c_56545,plain,
! [Z_5] : ( multiply(c,multiply(c,Z_5)) = multiply(a,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_56535,c_6]) ).
tff(c_56970,plain,
multiply(c,multiply(a,c)) = multiply(a,a),
inference(superposition,[status(thm),theory(equality)],[c_56902,c_56545]) ).
tff(c_56985,plain,
multiply(c,multiply(a,c)) = b,
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_56970]) ).
tff(c_58040,plain,
multiply(c,inverse(a)) = b,
inference(demodulation,[status(thm),theory(equality)],[c_57861,c_56985]) ).
tff(c_58106,plain,
( ( multiply(c,c) = b )
| ( identity = a )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_58040]) ).
tff(c_58118,plain,
( ( b = a )
| ( identity = a )
| ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_56535,c_58106]) ).
tff(c_58119,plain,
( ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_18,c_14,c_58118]) ).
tff(c_58191,plain,
inverse(a) = a,
inference(splitLeft,[status(thm)],[c_58119]) ).
tff(c_58215,plain,
multiply(a,a) = identity,
inference(superposition,[status(thm),theory(equality)],[c_58191,c_10]) ).
tff(c_58230,plain,
identity = b,
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_58215]) ).
tff(c_58232,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22,c_58230]) ).
tff(c_58233,plain,
inverse(a) = b,
inference(splitRight,[status(thm)],[c_58119]) ).
tff(c_58267,plain,
multiply(a,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_58233,c_10]) ).
tff(c_58281,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_57899,c_58267]) ).
tff(c_58283,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_58281]) ).
tff(c_58284,plain,
inverse(b) = b,
inference(splitRight,[status(thm)],[c_57732]) ).
tff(c_58303,plain,
multiply(b,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_58284,c_10]) ).
tff(c_58314,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56746,c_58303]) ).
tff(c_58316,plain,
multiply(a,multiply(a,b)) = identity,
inference(splitRight,[status(thm)],[c_30169]) ).
tff(c_58327,plain,
multiply(inverse(a),identity) = multiply(a,b),
inference(superposition,[status(thm),theory(equality)],[c_58316,c_301]) ).
tff(c_58343,plain,
multiply(a,b) = inverse(a),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_58327]) ).
tff(c_58315,plain,
multiply(a,b) != c,
inference(splitRight,[status(thm)],[c_30169]) ).
tff(c_58334,plain,
( ( multiply(a,identity) = identity )
| ( multiply(a,b) = c )
| ( multiply(a,b) = b )
| ( multiply(a,b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_58316]) ).
tff(c_58346,plain,
( ( identity = a )
| ( multiply(a,b) = c )
| ( multiply(a,b) = b )
| ( multiply(a,b) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_58334]) ).
tff(c_58347,plain,
( ( multiply(a,b) = b )
| ( multiply(a,b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_58315,c_18,c_58346]) ).
tff(c_58572,plain,
( ( inverse(a) = b )
| ( inverse(a) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_58343,c_58343,c_58347]) ).
tff(c_58573,plain,
inverse(a) = a,
inference(splitLeft,[status(thm)],[c_58572]) ).
tff(c_58590,plain,
multiply(a,a) = identity,
inference(superposition,[status(thm),theory(equality)],[c_58573,c_10]) ).
tff(c_58600,plain,
identity = b,
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_58590]) ).
tff(c_58602,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22,c_58600]) ).
tff(c_58603,plain,
inverse(a) = b,
inference(splitRight,[status(thm)],[c_58572]) ).
tff(c_58615,plain,
inverse(b) = a,
inference(superposition,[status(thm),theory(equality)],[c_58603,c_370]) ).
tff(c_58385,plain,
multiply(a,multiply(b,inverse(inverse(a)))) = identity,
inference(superposition,[status(thm),theory(equality)],[c_58343,c_256]) ).
tff(c_58397,plain,
multiply(a,multiply(b,a)) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_370,c_58385]) ).
tff(c_58415,plain,
multiply(inverse(a),identity) = multiply(b,a),
inference(superposition,[status(thm),theory(equality)],[c_58397,c_301]) ).
tff(c_58431,plain,
multiply(b,a) = inverse(a),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_58415]) ).
tff(c_58444,plain,
multiply(b,multiply(a,inverse(inverse(a)))) = identity,
inference(superposition,[status(thm),theory(equality)],[c_58431,c_256]) ).
tff(c_58456,plain,
multiply(b,b) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_30149,c_370,c_58444]) ).
tff(c_58467,plain,
multiply(inverse(b),identity) = b,
inference(superposition,[status(thm),theory(equality)],[c_58456,c_301]) ).
tff(c_58500,plain,
inverse(b) = b,
inference(superposition,[status(thm),theory(equality)],[c_58467,c_8]) ).
tff(c_58634,plain,
b = a,
inference(demodulation,[status(thm),theory(equality)],[c_58615,c_58500]) ).
tff(c_58636,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_58634]) ).
tff(c_58638,plain,
multiply(a,a) = identity,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_58642,plain,
multiply(inverse(a),identity) = a,
inference(superposition,[status(thm),theory(equality)],[c_58638,c_301]) ).
tff(c_58676,plain,
inverse(a) = a,
inference(superposition,[status(thm),theory(equality)],[c_58642,c_8]) ).
tff(c_58812,plain,
! [X_2262,Y_2263] : ( multiply(X_2262,multiply(Y_2263,inverse(multiply(X_2262,Y_2263)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_246,c_10]) ).
tff(c_58836,plain,
! [Y_2263,X_7] : ( multiply(Y_2263,inverse(multiply(inverse(X_7),Y_2263))) = multiply(X_7,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_58812,c_300]) ).
tff(c_59213,plain,
! [Y_2279,X_2280] : ( multiply(Y_2279,inverse(multiply(inverse(X_2280),Y_2279))) = X_2280 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_58836]) ).
tff(c_59343,plain,
! [X_2284,Z_2285] : ( multiply(multiply(X_2284,Z_2285),inverse(Z_2285)) = X_2284 ),
inference(superposition,[status(thm),theory(equality)],[c_301,c_59213]) ).
tff(c_59451,plain,
! [X_2289] : ( multiply(multiply(X_2289,a),a) = X_2289 ),
inference(superposition,[status(thm),theory(equality)],[c_58676,c_59343]) ).
tff(c_59466,plain,
! [X_2289] : ( multiply(inverse(multiply(X_2289,a)),X_2289) = a ),
inference(superposition,[status(thm),theory(equality)],[c_59451,c_301]) ).
tff(c_58741,plain,
multiply(b,b) != c,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_58806,plain,
multiply(c,c) != a,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_58637,plain,
( ( multiply(b,b) != identity )
| ( multiply(c,c) != identity ) ),
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_58659,plain,
multiply(c,c) != identity,
inference(splitLeft,[status(thm)],[c_58637]) ).
tff(c_58663,plain,
( ( multiply(c,c) = c )
| ( multiply(c,c) = b )
| ( multiply(c,c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_58659]) ).
tff(c_60846,plain,
( ( multiply(c,c) = c )
| ( multiply(c,c) = b ) ),
inference(negUnitSimplification,[status(thm)],[c_58806,c_58663]) ).
tff(c_60847,plain,
multiply(c,c) = b,
inference(splitLeft,[status(thm)],[c_60846]) ).
tff(c_60959,plain,
! [Z_2350] : ( multiply(c,multiply(c,Z_2350)) = multiply(b,Z_2350) ),
inference(superposition,[status(thm),theory(equality)],[c_60847,c_6]) ).
tff(c_60989,plain,
multiply(c,b) = multiply(b,c),
inference(superposition,[status(thm),theory(equality)],[c_60847,c_60959]) ).
tff(c_59281,plain,
! [X_2,Z_67] : ( multiply(multiply(X_2,Z_67),inverse(Z_67)) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_301,c_59213]) ).
tff(c_61088,plain,
multiply(multiply(b,c),inverse(b)) = c,
inference(superposition,[status(thm),theory(equality)],[c_60989,c_59281]) ).
tff(c_61685,plain,
( ( multiply(multiply(b,c),c) = c )
| ( identity = b )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_61088]) ).
tff(c_61705,plain,
( ( multiply(b,b) = c )
| ( identity = b )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_60847,c_6,c_61685]) ).
tff(c_61706,plain,
( ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_22,c_58741,c_61705]) ).
tff(c_62064,plain,
inverse(b) = a,
inference(splitLeft,[status(thm)],[c_61706]) ).
tff(c_58828,plain,
! [Y_2263,X_2262] : ( multiply(Y_2263,inverse(multiply(X_2262,Y_2263))) = multiply(inverse(X_2262),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_58812,c_301]) ).
tff(c_59732,plain,
! [Y_2302,X_2303] : ( multiply(Y_2302,inverse(multiply(X_2303,Y_2302))) = inverse(X_2303) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_58828]) ).
tff(c_58933,plain,
! [Y_2263,X_7] : ( multiply(Y_2263,inverse(multiply(inverse(X_7),Y_2263))) = X_7 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_58836]) ).
tff(c_59748,plain,
! [X_2303,X_7] : ( multiply(inverse(multiply(X_2303,inverse(X_7))),inverse(inverse(X_2303))) = X_7 ),
inference(superposition,[status(thm),theory(equality)],[c_59732,c_58933]) ).
tff(c_59861,plain,
! [X_2303,X_7] : ( multiply(inverse(multiply(X_2303,inverse(X_7))),X_2303) = X_7 ),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_59748]) ).
tff(c_62075,plain,
! [X_2303] : ( multiply(inverse(multiply(X_2303,a)),X_2303) = b ),
inference(superposition,[status(thm),theory(equality)],[c_62064,c_59861]) ).
tff(c_62115,plain,
b = a,
inference(demodulation,[status(thm),theory(equality)],[c_59466,c_62075]) ).
tff(c_62117,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_62115]) ).
tff(c_62118,plain,
inverse(b) = b,
inference(splitRight,[status(thm)],[c_61706]) ).
tff(c_58931,plain,
! [Y_2263,X_2262] : ( multiply(Y_2263,inverse(multiply(X_2262,Y_2263))) = inverse(X_2262) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_58828]) ).
tff(c_59735,plain,
! [X_2303,Y_2302] : ( multiply(inverse(multiply(X_2303,Y_2302)),inverse(inverse(X_2303))) = inverse(Y_2302) ),
inference(superposition,[status(thm),theory(equality)],[c_59732,c_58931]) ).
tff(c_59857,plain,
! [X_2303,Y_2302] : ( multiply(inverse(multiply(X_2303,Y_2302)),X_2303) = inverse(Y_2302) ),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_59735]) ).
tff(c_60853,plain,
multiply(inverse(b),c) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_60847,c_59857]) ).
tff(c_62310,plain,
multiply(b,c) = inverse(c),
inference(demodulation,[status(thm),theory(equality)],[c_62118,c_60853]) ).
tff(c_61091,plain,
multiply(inverse(c),multiply(b,c)) = b,
inference(superposition,[status(thm),theory(equality)],[c_60989,c_301]) ).
tff(c_62428,plain,
multiply(inverse(c),inverse(c)) = b,
inference(demodulation,[status(thm),theory(equality)],[c_62310,c_61091]) ).
tff(c_62568,plain,
( ( multiply(inverse(c),c) = b )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_222,c_62428]) ).
tff(c_62596,plain,
( ( identity = b )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_62568]) ).
tff(c_62597,plain,
( ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_24,c_22,c_62596]) ).
tff(c_62834,plain,
inverse(c) = a,
inference(splitLeft,[status(thm)],[c_62597]) ).
tff(c_62850,plain,
! [X_2303] : ( multiply(inverse(multiply(X_2303,a)),X_2303) = c ),
inference(superposition,[status(thm),theory(equality)],[c_62834,c_59861]) ).
tff(c_62895,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_59466,c_62850]) ).
tff(c_62897,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_62895]) ).
tff(c_62898,plain,
inverse(c) = b,
inference(splitRight,[status(thm)],[c_62597]) ).
tff(c_62966,plain,
inverse(b) = c,
inference(superposition,[status(thm),theory(equality)],[c_62898,c_370]) ).
tff(c_62991,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_62118,c_62966]) ).
tff(c_62993,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_62991]) ).
tff(c_62994,plain,
multiply(c,c) = c,
inference(splitRight,[status(thm)],[c_60846]) ).
tff(c_63009,plain,
multiply(c,inverse(c)) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_62994,c_58931]) ).
tff(c_63025,plain,
inverse(c) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_63009]) ).
tff(c_63035,plain,
! [X_2303] : ( multiply(inverse(multiply(X_2303,identity)),X_2303) = c ),
inference(superposition,[status(thm),theory(equality)],[c_63025,c_59861]) ).
tff(c_63078,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_8,c_63035]) ).
tff(c_63080,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_63078]) ).
tff(c_63082,plain,
multiply(c,c) = a,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_63090,plain,
! [Z_5] : ( multiply(c,multiply(c,Z_5)) = multiply(a,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_63082,c_6]) ).
tff(c_63099,plain,
! [Z_2444] : ( multiply(c,multiply(c,Z_2444)) = multiply(a,Z_2444) ),
inference(superposition,[status(thm),theory(equality)],[c_63082,c_6]) ).
tff(c_63134,plain,
multiply(a,inverse(c)) = multiply(c,identity),
inference(superposition,[status(thm),theory(equality)],[c_10,c_63099]) ).
tff(c_63144,plain,
multiply(a,inverse(c)) = c,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_63134]) ).
tff(c_58645,plain,
! [Z_5] : ( multiply(a,multiply(a,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_58638,c_6]) ).
tff(c_58654,plain,
! [Z_5] : ( multiply(a,multiply(a,Z_5)) = Z_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_58645]) ).
tff(c_63174,plain,
multiply(a,c) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_63144,c_58654]) ).
tff(c_63120,plain,
multiply(c,a) = multiply(a,c),
inference(superposition,[status(thm),theory(equality)],[c_63082,c_63099]) ).
tff(c_63215,plain,
multiply(c,a) = inverse(c),
inference(demodulation,[status(thm),theory(equality)],[c_63174,c_63120]) ).
tff(c_63081,plain,
( ( multiply(c,multiply(c,c)) != b )
| ( multiply(c,multiply(c,multiply(c,c))) != identity ) ),
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_63235,plain,
inverse(c) != b,
inference(demodulation,[status(thm),theory(equality)],[c_58638,c_63090,c_63082,c_63215,c_63082,c_63081]) ).
tff(c_63998,plain,
! [X_2492] :
( ( identity = X_2492 )
| ( inverse(X_2492) = c )
| ( inverse(X_2492) = b )
| ( inverse(X_2492) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_160]) ).
tff(c_63222,plain,
multiply(inverse(c),inverse(c)) = a,
inference(superposition,[status(thm),theory(equality)],[c_63215,c_301]) ).
tff(c_64019,plain,
( ( multiply(c,inverse(c)) = a )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_63998,c_63222]) ).
tff(c_64077,plain,
( ( identity = a )
| ( identity = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_64019]) ).
tff(c_64078,plain,
inverse(c) = a,
inference(negUnitSimplification,[status(thm)],[c_63235,c_24,c_18,c_64077]) ).
tff(c_63271,plain,
! [X_2466,Y_2467] : ( multiply(X_2466,multiply(Y_2467,inverse(multiply(X_2466,Y_2467)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_246]) ).
tff(c_63288,plain,
! [Y_2467] : ( multiply(Y_2467,inverse(multiply(a,Y_2467))) = multiply(a,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_63271,c_58654]) ).
tff(c_63463,plain,
! [Y_2471] : ( multiply(Y_2471,inverse(multiply(a,Y_2471))) = a ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_63288]) ).
tff(c_63574,plain,
! [Z_2475] : ( multiply(multiply(a,Z_2475),inverse(Z_2475)) = a ),
inference(superposition,[status(thm),theory(equality)],[c_58654,c_63463]) ).
tff(c_63616,plain,
! [X_71] : ( multiply(multiply(a,inverse(X_71)),X_71) = a ),
inference(superposition,[status(thm),theory(equality)],[c_370,c_63574]) ).
tff(c_64112,plain,
multiply(multiply(a,a),c) = a,
inference(superposition,[status(thm),theory(equality)],[c_64078,c_63616]) ).
tff(c_64141,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_58638,c_64112]) ).
tff(c_64143,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_64141]) ).
tff(c_64145,plain,
multiply(b,b) = c,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_64256,plain,
! [Z_2512] : ( multiply(b,multiply(b,Z_2512)) = multiply(c,Z_2512) ),
inference(superposition,[status(thm),theory(equality)],[c_64145,c_6]) ).
tff(c_64291,plain,
multiply(c,inverse(b)) = multiply(b,identity),
inference(superposition,[status(thm),theory(equality)],[c_10,c_64256]) ).
tff(c_64301,plain,
multiply(c,inverse(b)) = b,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_64291]) ).
tff(c_64303,plain,
multiply(c,c) != a,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_66607,plain,
( ( multiply(c,c) = c )
| ( multiply(c,c) = b ) ),
inference(negUnitSimplification,[status(thm)],[c_64303,c_58663]) ).
tff(c_66608,plain,
multiply(c,c) = b,
inference(splitLeft,[status(thm)],[c_66607]) ).
tff(c_64395,plain,
! [X_2531,Y_2532] : ( multiply(X_2531,multiply(Y_2532,inverse(multiply(X_2531,Y_2532)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_246,c_10]) ).
tff(c_64419,plain,
! [Y_2532,X_2531] : ( multiply(Y_2532,inverse(multiply(X_2531,Y_2532))) = multiply(inverse(X_2531),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_64395,c_301]) ).
tff(c_64549,plain,
! [Y_2532,X_2531] : ( multiply(Y_2532,inverse(multiply(X_2531,Y_2532))) = inverse(X_2531) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_64419]) ).
tff(c_66617,plain,
multiply(c,inverse(b)) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_66608,c_64549]) ).
tff(c_66633,plain,
inverse(c) = b,
inference(demodulation,[status(thm),theory(equality)],[c_64301,c_66617]) ).
tff(c_64427,plain,
! [Y_2532,X_7] : ( multiply(Y_2532,inverse(multiply(inverse(X_7),Y_2532))) = multiply(X_7,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_64395,c_300]) ).
tff(c_64947,plain,
! [Y_2557,X_2558] : ( multiply(Y_2557,inverse(multiply(inverse(X_2558),Y_2557))) = X_2558 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_64427]) ).
tff(c_65031,plain,
! [X_2,Z_67] : ( multiply(multiply(X_2,Z_67),inverse(Z_67)) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_301,c_64947]) ).
tff(c_66658,plain,
! [X_2] : ( multiply(multiply(X_2,c),b) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_66633,c_65031]) ).
tff(c_66836,plain,
! [X_2629,Y_2630,Z_2631] :
( ( multiply(X_2629,multiply(Y_2630,Z_2631)) = Z_2631 )
| ( multiply(X_2629,Y_2630) = c )
| ( multiply(X_2629,Y_2630) = b )
| ( multiply(X_2629,Y_2630) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_269]) ).
tff(c_67003,plain,
! [X_2629] :
( ( multiply(X_2629,identity) = a )
| ( multiply(X_2629,a) = c )
| ( multiply(X_2629,a) = b )
| ( multiply(X_2629,a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_58638,c_66836]) ).
tff(c_82686,plain,
! [X_2881] :
( ( a = X_2881 )
| ( multiply(X_2881,a) = c )
| ( multiply(X_2881,a) = b )
| ( multiply(X_2881,a) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_67003]) ).
tff(c_66673,plain,
! [Z_67] : ( multiply(c,multiply(b,Z_67)) = Z_67 ),
inference(superposition,[status(thm),theory(equality)],[c_66633,c_300]) ).
tff(c_82821,plain,
( ( multiply(c,c) = a )
| ( b = a )
| ( multiply(b,a) = b )
| ( multiply(b,a) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_82686,c_66673]) ).
tff(c_83023,plain,
( ( b = a )
| ( b = a )
| ( multiply(b,a) = b )
| ( multiply(b,a) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_66608,c_82821]) ).
tff(c_83024,plain,
( ( multiply(b,a) = b )
| ( multiply(b,a) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_14,c_14,c_83023]) ).
tff(c_83085,plain,
multiply(b,a) = a,
inference(splitLeft,[status(thm)],[c_83024]) ).
tff(c_64412,plain,
! [Y_2532] : ( multiply(Y_2532,inverse(multiply(a,Y_2532))) = multiply(a,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_64395,c_58654]) ).
tff(c_64583,plain,
! [Y_2536] : ( multiply(Y_2536,inverse(multiply(a,Y_2536))) = a ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_64412]) ).
tff(c_64606,plain,
! [Y_2536] : ( multiply(inverse(Y_2536),a) = inverse(multiply(a,Y_2536)) ),
inference(superposition,[status(thm),theory(equality)],[c_64583,c_301]) ).
tff(c_66649,plain,
inverse(multiply(a,c)) = multiply(b,a),
inference(superposition,[status(thm),theory(equality)],[c_66633,c_64606]) ).
tff(c_71745,plain,
! [X_2744,Y_2745,Z_2746] : ( multiply(inverse(multiply(X_2744,Y_2745)),multiply(X_2744,multiply(Y_2745,Z_2746))) = Z_2746 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_414]) ).
tff(c_73460,plain,
! [X_2775] : ( multiply(inverse(multiply(X_2775,c)),multiply(X_2775,b)) = c ),
inference(superposition,[status(thm),theory(equality)],[c_66608,c_71745]) ).
tff(c_73558,plain,
multiply(multiply(b,a),multiply(a,b)) = c,
inference(superposition,[status(thm),theory(equality)],[c_66649,c_73460]) ).
tff(c_83086,plain,
multiply(a,multiply(a,b)) = c,
inference(demodulation,[status(thm),theory(equality)],[c_83085,c_73558]) ).
tff(c_83091,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_58654,c_83086]) ).
tff(c_83093,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_83091]) ).
tff(c_83094,plain,
multiply(b,a) = b,
inference(splitRight,[status(thm)],[c_83024]) ).
tff(c_64479,plain,
multiply(b,multiply(b,inverse(c))) = identity,
inference(superposition,[status(thm),theory(equality)],[c_64145,c_64395]) ).
tff(c_64697,plain,
multiply(inverse(b),identity) = multiply(b,inverse(c)),
inference(superposition,[status(thm),theory(equality)],[c_64479,c_301]) ).
tff(c_64721,plain,
multiply(b,inverse(c)) = inverse(b),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_64697]) ).
tff(c_66638,plain,
multiply(b,b) = inverse(b),
inference(demodulation,[status(thm),theory(equality)],[c_66633,c_64721]) ).
tff(c_66641,plain,
inverse(b) = c,
inference(demodulation,[status(thm),theory(equality)],[c_64145,c_66638]) ).
tff(c_65710,plain,
! [Y_2587,X_2588] : ( multiply(Y_2587,inverse(multiply(X_2588,Y_2587))) = inverse(X_2588) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_64419]) ).
tff(c_65746,plain,
! [X_2588] : ( multiply(a,inverse(X_2588)) = inverse(multiply(X_2588,a)) ),
inference(superposition,[status(thm),theory(equality)],[c_65710,c_58654]) ).
tff(c_66703,plain,
inverse(multiply(b,a)) = multiply(a,c),
inference(superposition,[status(thm),theory(equality)],[c_66641,c_65746]) ).
tff(c_68102,plain,
multiply(multiply(a,c),multiply(b,a)) = identity,
inference(superposition,[status(thm),theory(equality)],[c_66703,c_4]) ).
tff(c_83098,plain,
multiply(multiply(a,c),b) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_83094,c_68102]) ).
tff(c_83101,plain,
identity = a,
inference(demodulation,[status(thm),theory(equality)],[c_66658,c_83098]) ).
tff(c_83103,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_83101]) ).
tff(c_83104,plain,
multiply(c,c) = c,
inference(splitRight,[status(thm)],[c_66607]) ).
tff(c_83187,plain,
multiply(c,inverse(c)) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_83104,c_64549]) ).
tff(c_83203,plain,
inverse(c) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_83187]) ).
tff(c_64551,plain,
! [Y_2532,X_7] : ( multiply(Y_2532,inverse(multiply(inverse(X_7),Y_2532))) = X_7 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_64427]) ).
tff(c_65726,plain,
! [X_2588,X_7] : ( multiply(inverse(multiply(X_2588,inverse(X_7))),inverse(inverse(X_2588))) = X_7 ),
inference(superposition,[status(thm),theory(equality)],[c_65710,c_64551]) ).
tff(c_65876,plain,
! [X_2588,X_7] : ( multiply(inverse(multiply(X_2588,inverse(X_7))),X_2588) = X_7 ),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_65726]) ).
tff(c_83222,plain,
! [X_2588] : ( multiply(inverse(multiply(X_2588,identity)),X_2588) = c ),
inference(superposition,[status(thm),theory(equality)],[c_83203,c_65876]) ).
tff(c_83263,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_8,c_83222]) ).
tff(c_83265,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_83263]) ).
tff(c_83267,plain,
multiply(c,c) = a,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_83275,plain,
! [Z_5] : ( multiply(c,multiply(c,Z_5)) = multiply(a,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_83267,c_6]) ).
tff(c_83344,plain,
! [Z_2912] : ( multiply(c,multiply(c,Z_2912)) = multiply(a,Z_2912) ),
inference(superposition,[status(thm),theory(equality)],[c_83267,c_6]) ).
tff(c_83385,plain,
multiply(a,inverse(c)) = multiply(c,identity),
inference(superposition,[status(thm),theory(equality)],[c_10,c_83344]) ).
tff(c_83396,plain,
multiply(a,inverse(c)) = c,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_83385]) ).
tff(c_83401,plain,
multiply(a,c) = inverse(c),
inference(superposition,[status(thm),theory(equality)],[c_83396,c_58654]) ).
tff(c_83371,plain,
multiply(c,a) = multiply(a,c),
inference(superposition,[status(thm),theory(equality)],[c_83267,c_83344]) ).
tff(c_83442,plain,
multiply(c,a) = inverse(c),
inference(demodulation,[status(thm),theory(equality)],[c_83401,c_83371]) ).
tff(c_83266,plain,
( ( multiply(c,multiply(c,c)) != b )
| ( multiply(c,multiply(c,multiply(c,c))) != identity ) ),
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_83485,plain,
inverse(c) != b,
inference(demodulation,[status(thm),theory(equality)],[c_58638,c_83275,c_83267,c_83442,c_83267,c_83266]) ).
tff(c_64153,plain,
! [Z_5] : ( multiply(b,multiply(b,Z_5)) = multiply(c,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_64145,c_6]) ).
tff(c_83574,plain,
! [X_2940,Y_2941] : ( multiply(X_2940,multiply(Y_2941,inverse(multiply(X_2940,Y_2941)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_246,c_10]) ).
tff(c_83694,plain,
multiply(b,multiply(b,inverse(c))) = identity,
inference(superposition,[status(thm),theory(equality)],[c_64145,c_83574]) ).
tff(c_83948,plain,
( ( multiply(b,multiply(b,identity)) = identity )
| ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_83694]) ).
tff(c_83966,plain,
( ( identity = c )
| ( inverse(c) = c )
| ( inverse(c) = b )
| ( inverse(c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_64153,c_83948]) ).
tff(c_83967,plain,
( ( inverse(c) = c )
| ( inverse(c) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_83485,c_24,c_83966]) ).
tff(c_84002,plain,
inverse(c) = a,
inference(splitLeft,[status(thm)],[c_83967]) ).
tff(c_84018,plain,
inverse(a) = c,
inference(superposition,[status(thm),theory(equality)],[c_84002,c_370]) ).
tff(c_84033,plain,
c = a,
inference(demodulation,[status(thm),theory(equality)],[c_58676,c_84018]) ).
tff(c_84035,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_84033]) ).
tff(c_84036,plain,
inverse(c) = c,
inference(splitRight,[status(thm)],[c_83967]) ).
tff(c_84066,plain,
multiply(c,c) = identity,
inference(superposition,[status(thm),theory(equality)],[c_84036,c_10]) ).
tff(c_84076,plain,
identity = a,
inference(demodulation,[status(thm),theory(equality)],[c_83267,c_84066]) ).
tff(c_84078,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_84076]) ).
tff(c_84079,plain,
multiply(b,b) != identity,
inference(splitRight,[status(thm)],[c_58637]) ).
tff(c_84084,plain,
( ( multiply(b,b) = c )
| ( multiply(b,b) = b )
| ( multiply(b,b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_84079]) ).
tff(c_86296,plain,
( ( multiply(b,b) = b )
| ( multiply(b,b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_84085,c_84084]) ).
tff(c_86297,plain,
multiply(b,b) = a,
inference(splitLeft,[status(thm)],[c_86296]) ).
tff(c_84377,plain,
! [X_2993,Y_2994] : ( multiply(X_2993,multiply(Y_2994,inverse(multiply(X_2993,Y_2994)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_246]) ).
tff(c_84401,plain,
! [Y_2994,X_2993] : ( multiply(Y_2994,inverse(multiply(X_2993,Y_2994))) = multiply(inverse(X_2993),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_84377,c_301]) ).
tff(c_85527,plain,
! [Y_3047,X_3048] : ( multiply(Y_3047,inverse(multiply(X_3048,Y_3047))) = inverse(X_3048) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_84401]) ).
tff(c_84386,plain,
! [Y_2994] : ( multiply(Y_2994,inverse(multiply(a,Y_2994))) = multiply(a,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_84377,c_58654]) ).
tff(c_84512,plain,
! [Y_2994] : ( multiply(Y_2994,inverse(multiply(a,Y_2994))) = a ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_84386]) ).
tff(c_85561,plain,
! [X_3048] : ( multiply(inverse(multiply(X_3048,a)),inverse(inverse(X_3048))) = a ),
inference(superposition,[status(thm),theory(equality)],[c_85527,c_84512]) ).
tff(c_85698,plain,
! [X_3048] : ( multiply(inverse(multiply(X_3048,a)),X_3048) = a ),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_85561]) ).
tff(c_86548,plain,
! [X_3095,Y_3096,Z_3097] :
( ( multiply(X_3095,multiply(Y_3096,Z_3097)) = Z_3097 )
| ( multiply(X_3095,Y_3096) = c )
| ( multiply(X_3095,Y_3096) = b )
| ( multiply(X_3095,Y_3096) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_269]) ).
tff(c_86789,plain,
! [Y_3096,Z_3097] :
( ( multiply(Y_3096,Z_3097) = Z_3097 )
| ( multiply(identity,Y_3096) = c )
| ( multiply(identity,Y_3096) = b )
| ( multiply(identity,Y_3096) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_86548]) ).
tff(c_87557,plain,
! [Y_3122,Z_3123] :
( ( multiply(Y_3122,Z_3123) = Z_3123 )
| ( c = Y_3122 )
| ( b = Y_3122 )
| ( a = Y_3122 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_2,c_86789]) ).
tff(c_86309,plain,
multiply(inverse(b),a) = b,
inference(superposition,[status(thm),theory(equality)],[c_86297,c_301]) ).
tff(c_87619,plain,
( ( b = a )
| ( inverse(b) = c )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_87557,c_86309]) ).
tff(c_87885,plain,
( ( inverse(b) = c )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(negUnitSimplification,[status(thm)],[c_14,c_87619]) ).
tff(c_90934,plain,
inverse(b) = a,
inference(splitLeft,[status(thm)],[c_87885]) ).
tff(c_84516,plain,
! [Y_2994,X_2993] : ( multiply(Y_2994,inverse(multiply(X_2993,Y_2994))) = inverse(X_2993) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_84401]) ).
tff(c_84409,plain,
! [Y_2994,X_7] : ( multiply(Y_2994,inverse(multiply(inverse(X_7),Y_2994))) = multiply(X_7,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_84377,c_300]) ).
tff(c_87092,plain,
! [Y_3109,X_3110] : ( multiply(Y_3109,inverse(multiply(inverse(X_3110),Y_3109))) = X_3110 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_84409]) ).
tff(c_87179,plain,
! [X_2993,X_3110] : ( multiply(inverse(multiply(X_2993,inverse(X_3110))),inverse(inverse(X_2993))) = X_3110 ),
inference(superposition,[status(thm),theory(equality)],[c_84516,c_87092]) ).
tff(c_87267,plain,
! [X_2993,X_3110] : ( multiply(inverse(multiply(X_2993,inverse(X_3110))),X_2993) = X_3110 ),
inference(demodulation,[status(thm),theory(equality)],[c_370,c_87179]) ).
tff(c_90958,plain,
! [X_2993] : ( multiply(inverse(multiply(X_2993,a)),X_2993) = b ),
inference(superposition,[status(thm),theory(equality)],[c_90934,c_87267]) ).
tff(c_91001,plain,
b = a,
inference(demodulation,[status(thm),theory(equality)],[c_85698,c_90958]) ).
tff(c_91003,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_91001]) ).
tff(c_91004,plain,
( ( inverse(b) = b )
| ( inverse(b) = c ) ),
inference(splitRight,[status(thm)],[c_87885]) ).
tff(c_91018,plain,
inverse(b) = c,
inference(splitLeft,[status(thm)],[c_91004]) ).
tff(c_91061,plain,
inverse(c) = b,
inference(superposition,[status(thm),theory(equality)],[c_91018,c_370]) ).
tff(c_84080,plain,
multiply(c,c) = identity,
inference(splitRight,[status(thm)],[c_58637]) ).
tff(c_84089,plain,
multiply(inverse(c),identity) = c,
inference(superposition,[status(thm),theory(equality)],[c_84080,c_301]) ).
tff(c_84202,plain,
inverse(c) = c,
inference(superposition,[status(thm),theory(equality)],[c_84089,c_8]) ).
tff(c_91097,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_91061,c_84202]) ).
tff(c_91099,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_91097]) ).
tff(c_91100,plain,
inverse(b) = b,
inference(splitRight,[status(thm)],[c_91004]) ).
tff(c_91167,plain,
multiply(b,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_91100,c_10]) ).
tff(c_91187,plain,
identity = a,
inference(demodulation,[status(thm),theory(equality)],[c_86297,c_91167]) ).
tff(c_91189,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_91187]) ).
tff(c_91190,plain,
multiply(b,b) = b,
inference(splitRight,[status(thm)],[c_86296]) ).
tff(c_91206,plain,
multiply(b,inverse(b)) = inverse(b),
inference(superposition,[status(thm),theory(equality)],[c_91190,c_84516]) ).
tff(c_91218,plain,
inverse(b) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_91206]) ).
tff(c_91234,plain,
( ( identity = b )
| ( identity = c )
| ( inverse(b) = b )
| ( inverse(b) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_91218,c_222]) ).
tff(c_91263,plain,
( ( identity = b )
| ( identity = c )
| ( identity = b )
| ( identity = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_91218,c_91218,c_91234]) ).
tff(c_91265,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_22,c_24,c_22,c_91263]) ).
tff(c_91267,plain,
multiply(b,b) = c,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_91295,plain,
! [Z_5] : ( multiply(b,multiply(b,Z_5)) = multiply(c,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_91267,c_6]) ).
tff(c_91266,plain,
( ( multiply(b,multiply(b,b)) != a )
| ( multiply(b,multiply(b,multiply(b,b))) != identity ) ),
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_91352,plain,
( ( multiply(b,c) != a )
| ( multiply(b,multiply(b,c)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_91267,c_91267,c_91266]) ).
tff(c_91353,plain,
multiply(b,multiply(b,c)) != identity,
inference(splitLeft,[status(thm)],[c_91352]) ).
tff(c_91605,plain,
multiply(c,c) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_91295,c_91353]) ).
tff(c_91608,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_84080,c_91605]) ).
tff(c_91610,plain,
multiply(b,multiply(b,c)) = identity,
inference(splitRight,[status(thm)],[c_91352]) ).
tff(c_91721,plain,
multiply(inverse(b),identity) = multiply(b,c),
inference(superposition,[status(thm),theory(equality)],[c_91610,c_301]) ).
tff(c_91736,plain,
multiply(b,c) = inverse(b),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_91721]) ).
tff(c_91609,plain,
multiply(b,c) != a,
inference(splitRight,[status(thm)],[c_91352]) ).
tff(c_91728,plain,
( ( multiply(b,identity) = identity )
| ( multiply(b,c) = c )
| ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_91610]) ).
tff(c_91739,plain,
( ( identity = b )
| ( multiply(b,c) = c )
| ( multiply(b,c) = b )
| ( multiply(b,c) = a ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_91728]) ).
tff(c_91740,plain,
( ( multiply(b,c) = c )
| ( multiply(b,c) = b ) ),
inference(negUnitSimplification,[status(thm)],[c_91609,c_22,c_91739]) ).
tff(c_91937,plain,
( ( inverse(b) = c )
| ( inverse(b) = b ) ),
inference(demodulation,[status(thm),theory(equality)],[c_91736,c_91736,c_91740]) ).
tff(c_91938,plain,
inverse(b) = b,
inference(splitLeft,[status(thm)],[c_91937]) ).
tff(c_91956,plain,
multiply(b,b) = identity,
inference(superposition,[status(thm),theory(equality)],[c_91938,c_10]) ).
tff(c_91966,plain,
identity = c,
inference(demodulation,[status(thm),theory(equality)],[c_91267,c_91956]) ).
tff(c_91968,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_91966]) ).
tff(c_91969,plain,
inverse(b) = c,
inference(splitRight,[status(thm)],[c_91937]) ).
tff(c_91981,plain,
inverse(c) = b,
inference(superposition,[status(thm),theory(equality)],[c_91969,c_370]) ).
tff(c_91271,plain,
multiply(inverse(c),identity) = c,
inference(superposition,[status(thm),theory(equality)],[c_84080,c_301]) ).
tff(c_91682,plain,
inverse(c) = c,
inference(superposition,[status(thm),theory(equality)],[c_91271,c_8]) ).
tff(c_92000,plain,
c = b,
inference(demodulation,[status(thm),theory(equality)],[c_91981,c_91682]) ).
tff(c_92002,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20,c_92000]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP113-1 : TPTP v9.0.0. Released v1.1.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.32 % Computer : n023.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Mon Apr 7 21:17:54 EDT 2025
% 0.12/0.32 % CPUTime :
% 16.91/7.23 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.28/7.32
% 17.28/7.32 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------