%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP251-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n010.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:42 PM UTC 2025
% Result : Unsatisfiable 116.62s 99.31s
% Output : CNFRefutation 117.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 39
% Syntax : Number of formulae : 712 ( 568 unt; 0 typ; 0 def)
% Number of atoms : 1111 (1065 equ)
% Maximal formula atoms : 13 ( 1 avg)
% Number of connectives : 862 ( 463 ~; 399 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 446 ( 446 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c9 > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c10 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c10,type,
sk_c10: $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c9,type,
sk_c9: $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_227,axiom,
! [X5,X6,X3,X7,X1,X2,X4] :
( ( multiply(X4,sk_c10) != sk_c9 )
| ( inverse(X4) != sk_c10 )
| ( multiply(X5,sk_c9) != sk_c8 )
| ( inverse(X5) != sk_c9 )
| ( inverse(X6) != sk_c9 )
| ( multiply(X6,sk_c8) != sk_c9 )
| ( multiply(X1,sk_c10) != sk_c9 )
| ( inverse(X1) != sk_c10 )
| ( multiply(X2,sk_c8) != sk_c9 )
| ( inverse(X2) != sk_c8 )
| ( multiply(sk_c9,X3) != sk_c8 )
| ( multiply(X7,sk_c9) != X3 )
| ( inverse(X7) != sk_c9 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_179,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_182,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c9) = sk_c8 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c9,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( inverse(sk_c6) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
file(unknown,unknown) ).
tff(c_28,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_121,plain,
inverse(sk_c1) = sk_c10,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_125,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_121,c_4]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_20,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_167,plain,
multiply(sk_c1,sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_196,plain,
! [X_15,Y_16,Z_17] : ( multiply(multiply(X_15,Y_16),Z_17) = multiply(X_15,multiply(Y_16,Z_17)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_223,plain,
! [Z_17] : ( multiply(sk_c10,multiply(sk_c1,Z_17)) = multiply(identity,Z_17) ),
inference(superposition,[status(thm),theory(equality)],[c_125,c_196]) ).
tff(c_317,plain,
! [Z_21] : ( multiply(sk_c10,multiply(sk_c1,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_223]) ).
tff(c_329,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_167,c_317]) ).
tff(c_229,plain,
! [X_2,Z_17] : ( multiply(inverse(X_2),multiply(X_2,Z_17)) = multiply(identity,Z_17) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_196]) ).
tff(c_576,plain,
! [X_27,Z_28] : ( multiply(inverse(X_27),multiply(X_27,Z_28)) = Z_28 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_229]) ).
tff(c_600,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_329,c_576]) ).
tff(c_650,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_600]) ).
tff(c_668,plain,
multiply(sk_c1,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_650,c_167]) ).
tff(c_240,plain,
! [X_2,Z_17] : ( multiply(inverse(X_2),multiply(X_2,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_229]) ).
tff(c_1937,plain,
! [X_48,Z_49] : ( multiply(inverse(inverse(X_48)),Z_49) = multiply(X_48,Z_49) ),
inference(superposition,[status(thm),theory(equality)],[c_240,c_576]) ).
tff(c_642,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_576]) ).
tff(c_1947,plain,
! [X_48] : ( multiply(X_48,identity) = X_48 ),
inference(superposition,[status(thm),theory(equality)],[c_1937,c_642]) ).
tff(c_1054,plain,
! [X_34,Z_35] : ( multiply(inverse(inverse(X_34)),Z_35) = multiply(X_34,Z_35) ),
inference(superposition,[status(thm),theory(equality)],[c_576,c_240]) ).
tff(c_1068,plain,
! [X_34] : ( multiply(X_34,identity) = X_34 ),
inference(superposition,[status(thm),theory(equality)],[c_1054,c_642]) ).
tff(c_48,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_154,plain,
multiply(sk_c2,sk_c9) = sk_c8,
inference(splitLeft,[status(thm)],[c_48]) ).
tff(c_56,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_109,plain,
inverse(sk_c2) = sk_c9,
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_113,plain,
multiply(sk_c9,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_109,c_4]) ).
tff(c_226,plain,
! [Z_17] : ( multiply(sk_c9,multiply(sk_c2,Z_17)) = multiply(identity,Z_17) ),
inference(superposition,[status(thm),theory(equality)],[c_113,c_196]) ).
tff(c_340,plain,
! [Z_22] : ( multiply(sk_c9,multiply(sk_c2,Z_22)) = Z_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_226]) ).
tff(c_352,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_154,c_340]) ).
tff(c_594,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_352,c_576]) ).
tff(c_649,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_594]) ).
tff(c_364,plain,
! [X_23,Z_24] : ( multiply(inverse(X_23),multiply(X_23,Z_24)) = Z_24 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_229]) ).
tff(c_388,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_329,c_364]) ).
tff(c_438,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_388]) ).
tff(c_460,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_438,c_109]) ).
tff(c_382,plain,
multiply(inverse(sk_c9),sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_352,c_364]) ).
tff(c_437,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_382]) ).
tff(c_448,plain,
multiply(sk_c2,sk_c9) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_437,c_154]) ).
tff(c_521,plain,
multiply(sk_c2,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_438,c_448]) ).
tff(c_92,plain,
! [X5_6,X4_12,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 )
| ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_289,plain,
! [X4_20] :
( ( inverse(X4_20) != sk_c10 )
| ( multiply(X4_20,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_92]) ).
tff(c_296,plain,
inverse(sk_c1) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_167,c_289]) ).
tff(c_308,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_121,c_296]) ).
tff(c_309,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_92]) ).
tff(c_363,plain,
! [X7_9] :
( ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_309]) ).
tff(c_551,plain,
! [X7_26] :
( ( inverse(X7_26) != identity )
| ( multiply(X7_26,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_438,c_2,c_438,c_437,c_438,c_363]) ).
tff(c_554,plain,
inverse(sk_c2) != identity,
inference(superposition,[status(thm),theory(equality)],[c_521,c_551]) ).
tff(c_574,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_460,c_554]) ).
tff(c_575,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_309]) ).
tff(c_762,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != identity )
| ( multiply(X2_11,identity) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( multiply(X6_7,identity) != identity )
| ( inverse(X6_7) != identity )
| ( inverse(X5_6) != identity )
| ( multiply(X5_6,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_650,c_649,c_650,c_650,c_650,c_649,c_650,c_650,c_649,c_649,c_575]) ).
tff(c_763,plain,
! [X5_6] :
( ( inverse(X5_6) != identity )
| ( multiply(X5_6,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_762]) ).
tff(c_1739,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_1068,c_763]) ).
tff(c_671,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_650,c_113]) ).
tff(c_779,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_671,c_240]) ).
tff(c_791,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_779]) ).
tff(c_672,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_650,c_109]) ).
tff(c_796,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_791,c_672]) ).
tff(c_1741,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1739,c_796]) ).
tff(c_1742,plain,
! [X6_7,X1_10,X2_11] :
( ( multiply(X6_7,identity) != identity )
| ( inverse(X6_7) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( inverse(X2_11) != identity )
| ( multiply(X2_11,identity) != identity ) ),
inference(splitRight,[status(thm)],[c_762]) ).
tff(c_122640,plain,
! [X6_7,X1_10,X2_11] :
( ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1947,c_1947,c_1742]) ).
tff(c_122642,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_122640]) ).
tff(c_645,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_576]) ).
tff(c_1758,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_671,c_240]) ).
tff(c_1770,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_645,c_1758]) ).
tff(c_1808,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1770,c_672]) ).
tff(c_122644,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_122642,c_1808]) ).
tff(c_122645,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(splitRight,[status(thm)],[c_122640]) ).
tff(c_122647,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_122645]) ).
tff(c_122649,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_122647,c_1808]) ).
tff(c_124841,plain,
! [X1_425] :
( ( inverse(X1_425) != sk_c10 )
| ( multiply(X1_425,sk_c10) != identity ) ),
inference(splitRight,[status(thm)],[c_122645]) ).
tff(c_124927,plain,
inverse(sk_c1) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_668,c_124841]) ).
tff(c_124961,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_121,c_124927]) ).
tff(c_124963,plain,
multiply(sk_c1,sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_16,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_125010,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_124963,c_16]) ).
tff(c_18,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_125027,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_124963,c_18]) ).
tff(c_124962,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_124967,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_124962,c_4]) ).
tff(c_125037,plain,
! [X_426,Y_427,Z_428] : ( multiply(multiply(X_426,Y_427),Z_428) = multiply(X_426,multiply(Y_427,Z_428)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_125070,plain,
! [Z_428] : ( multiply(sk_c9,multiply(sk_c6,Z_428)) = multiply(identity,Z_428) ),
inference(superposition,[status(thm),theory(equality)],[c_124967,c_125037]) ).
tff(c_125164,plain,
! [Z_432] : ( multiply(sk_c9,multiply(sk_c6,Z_432)) = Z_432 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_125070]) ).
tff(c_125176,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_125027,c_125164]) ).
tff(c_125180,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_125010,c_125176]) ).
tff(c_125085,plain,
! [Z_428] : ( multiply(sk_c9,multiply(sk_c2,Z_428)) = multiply(identity,Z_428) ),
inference(superposition,[status(thm),theory(equality)],[c_113,c_125037]) ).
tff(c_125140,plain,
! [Z_431] : ( multiply(sk_c9,multiply(sk_c2,Z_431)) = Z_431 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_125085]) ).
tff(c_125152,plain,
multiply(sk_c9,sk_c8) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_154,c_125140]) ).
tff(c_125182,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_125180,c_125180,c_125152]) ).
tff(c_125088,plain,
! [X_2,Z_428] : ( multiply(inverse(X_2),multiply(X_2,Z_428)) = multiply(identity,Z_428) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_125037]) ).
tff(c_125253,plain,
! [X_434,Z_435] : ( multiply(inverse(X_434),multiply(X_434,Z_435)) = Z_435 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_125088]) ).
tff(c_125274,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_125182,c_125253]) ).
tff(c_125317,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_125274]) ).
tff(c_125191,plain,
multiply(sk_c1,sk_c10) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_125180,c_124963]) ).
tff(c_125395,plain,
multiply(sk_c1,sk_c10) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_125317,c_125191]) ).
tff(c_125304,plain,
multiply(inverse(sk_c10),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_125,c_125253]) ).
tff(c_10,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_124977,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_124963,c_10]) ).
tff(c_124981,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_124977,c_4]) ).
tff(c_125298,plain,
multiply(inverse(sk_c10),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_124981,c_125253]) ).
tff(c_125510,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_125304,c_125298]) ).
tff(c_8,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_125022,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_124963,c_8]) ).
tff(c_125187,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_125180,c_125022]) ).
tff(c_125405,plain,
multiply(sk_c4,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_125317,c_125187]) ).
tff(c_125511,plain,
multiply(sk_c1,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_125510,c_125405]) ).
tff(c_125515,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_125395,c_125511]) ).
tff(c_125517,plain,
multiply(sk_c2,sk_c9) != sk_c8,
inference(splitRight,[status(thm)],[c_48]) ).
tff(c_44,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_127300,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_125517,c_44]) ).
tff(c_46,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_127288,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_125517,c_46]) ).
tff(c_125516,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_48]) ).
tff(c_125521,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_125516,c_4]) ).
tff(c_127319,plain,
! [X_470,Y_471,Z_472] : ( multiply(multiply(X_470,Y_471),Z_472) = multiply(X_470,multiply(Y_471,Z_472)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_127352,plain,
! [Z_472] : ( multiply(sk_c9,multiply(sk_c6,Z_472)) = multiply(identity,Z_472) ),
inference(superposition,[status(thm),theory(equality)],[c_125521,c_127319]) ).
tff(c_127504,plain,
! [Z_480] : ( multiply(sk_c9,multiply(sk_c6,Z_480)) = Z_480 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127352]) ).
tff(c_127516,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_127288,c_127504]) ).
tff(c_127520,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_127300,c_127516]) ).
tff(c_84,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_125525,plain,
multiply(sk_c3,sk_c8) = sk_c9,
inference(splitLeft,[status(thm)],[c_84]) ).
tff(c_76,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_133,plain,
inverse(sk_c3) = sk_c9,
inference(splitLeft,[status(thm)],[c_76]) ).
tff(c_138,plain,
multiply(sk_c9,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_133,c_4]) ).
tff(c_125600,plain,
! [X_436,Y_437,Z_438] : ( multiply(multiply(X_436,Y_437),Z_438) = multiply(X_436,multiply(Y_437,Z_438)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_125639,plain,
! [Z_438] : ( multiply(sk_c9,multiply(sk_c3,Z_438)) = multiply(identity,Z_438) ),
inference(superposition,[status(thm),theory(equality)],[c_138,c_125600]) ).
tff(c_125764,plain,
! [Z_445] : ( multiply(sk_c9,multiply(sk_c3,Z_445)) = Z_445 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_125639]) ).
tff(c_125776,plain,
multiply(sk_c9,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_125525,c_125764]) ).
tff(c_40,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_125586,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_125517,c_40]) ).
tff(c_42,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_125540,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_125517,c_42]) ).
tff(c_125544,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_125540,c_4]) ).
tff(c_125630,plain,
! [Z_438] : ( multiply(sk_c8,multiply(sk_c5,Z_438)) = multiply(identity,Z_438) ),
inference(superposition,[status(thm),theory(equality)],[c_125544,c_125600]) ).
tff(c_125842,plain,
! [Z_449] : ( multiply(sk_c8,multiply(sk_c5,Z_449)) = Z_449 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_125630]) ).
tff(c_125857,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_125586,c_125842]) ).
tff(c_125636,plain,
! [Z_438] : ( multiply(sk_c3,multiply(sk_c8,Z_438)) = multiply(sk_c9,Z_438) ),
inference(superposition,[status(thm),theory(equality)],[c_125525,c_125600]) ).
tff(c_125864,plain,
multiply(sk_c9,sk_c9) = multiply(sk_c3,sk_c8),
inference(superposition,[status(thm),theory(equality)],[c_125857,c_125636]) ).
tff(c_125870,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_125776,c_125525,c_125864]) ).
tff(c_125976,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_125870,c_125857]) ).
tff(c_125648,plain,
! [X_2,Z_438] : ( multiply(inverse(X_2),multiply(X_2,Z_438)) = multiply(identity,Z_438) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_125600]) ).
tff(c_126104,plain,
! [X_451,Z_452] : ( multiply(inverse(X_451),multiply(X_451,Z_452)) = Z_452 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_125648]) ).
tff(c_126146,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_125976,c_126104]) ).
tff(c_126204,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_126146]) ).
tff(c_125992,plain,
multiply(sk_c8,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_125870,c_113]) ).
tff(c_126220,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_126204,c_125992]) ).
tff(c_126406,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_126220,c_2]) ).
tff(c_125988,plain,
multiply(sk_c2,sk_c8) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_125870,c_125517]) ).
tff(c_126214,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_126204,c_126204,c_125988]) ).
tff(c_126416,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_126406,c_126214]) ).
tff(c_126421,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_126416]) ).
tff(c_126423,plain,
multiply(sk_c3,sk_c8) != sk_c9,
inference(splitRight,[status(thm)],[c_84]) ).
tff(c_86,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_126479,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_126423,c_86]) ).
tff(c_126474,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_125517,c_46]) ).
tff(c_126505,plain,
! [X_454,Y_455,Z_456] : ( multiply(multiply(X_454,Y_455),Z_456) = multiply(X_454,multiply(Y_455,Z_456)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_126541,plain,
! [Z_456] : ( multiply(sk_c9,multiply(sk_c6,Z_456)) = multiply(identity,Z_456) ),
inference(superposition,[status(thm),theory(equality)],[c_125521,c_126505]) ).
tff(c_126679,plain,
! [Z_463] : ( multiply(sk_c9,multiply(sk_c6,Z_463)) = Z_463 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_126541]) ).
tff(c_126691,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_126474,c_126679]) ).
tff(c_126695,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_126479,c_126691]) ).
tff(c_12,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_126469,plain,
multiply(sk_c1,sk_c10) = sk_c9,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_126547,plain,
! [Z_456] : ( multiply(sk_c10,multiply(sk_c1,Z_456)) = multiply(identity,Z_456) ),
inference(superposition,[status(thm),theory(equality)],[c_125,c_126505]) ).
tff(c_126643,plain,
! [Z_461] : ( multiply(sk_c10,multiply(sk_c1,Z_461)) = Z_461 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_126547]) ).
tff(c_126655,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_126469,c_126643]) ).
tff(c_126813,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_126695,c_126655]) ).
tff(c_126553,plain,
! [X_2,Z_456] : ( multiply(inverse(X_2),multiply(X_2,Z_456)) = multiply(identity,Z_456) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_126505]) ).
tff(c_126567,plain,
! [X_2,Z_456] : ( multiply(inverse(X_2),multiply(X_2,Z_456)) = Z_456 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_126553]) ).
tff(c_127001,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_126813,c_126567]) ).
tff(c_127007,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_127001]) ).
tff(c_126825,plain,
inverse(sk_c3) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_126695,c_133]) ).
tff(c_126842,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_126825,c_4]) ).
tff(c_127120,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127007,c_126842]) ).
tff(c_126821,plain,
multiply(sk_c3,sk_c8) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_126695,c_126423]) ).
tff(c_127011,plain,
multiply(sk_c3,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_127007,c_127007,c_126821]) ).
tff(c_127281,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127120,c_127011]) ).
tff(c_127283,plain,
multiply(sk_c1,sk_c10) != sk_c9,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_127293,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_127283,c_8]) ).
tff(c_38,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_126446,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_125517,c_38]) ).
tff(c_126450,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_126446,c_4]) ).
tff(c_127346,plain,
! [Z_472] : ( multiply(sk_c10,multiply(sk_c4,Z_472)) = multiply(identity,Z_472) ),
inference(superposition,[status(thm),theory(equality)],[c_126450,c_127319]) ).
tff(c_127481,plain,
! [Z_479] : ( multiply(sk_c10,multiply(sk_c4,Z_479)) = Z_479 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127346]) ).
tff(c_127493,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_127293,c_127481]) ).
tff(c_127522,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_127520,c_127493]) ).
tff(c_127364,plain,
! [X_2,Z_472] : ( multiply(inverse(X_2),multiply(X_2,Z_472)) = multiply(identity,Z_472) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_127319]) ).
tff(c_127603,plain,
! [X_481,Z_482] : ( multiply(inverse(X_481),multiply(X_481,Z_482)) = Z_482 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127364]) ).
tff(c_127621,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_127522,c_127603]) ).
tff(c_127679,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_127621]) ).
tff(c_127534,plain,
multiply(sk_c8,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_127520,c_138]) ).
tff(c_127803,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127679,c_127534]) ).
tff(c_127531,plain,
multiply(sk_c3,sk_c8) != sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_127520,c_126423]) ).
tff(c_127813,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127803,c_127679,c_127679,c_127531]) ).
tff(c_127815,plain,
inverse(sk_c3) != sk_c9,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_72,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_127882,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_127815,c_72]) ).
tff(c_74,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_127875,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_127815,c_74]) ).
tff(c_127814,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_127819,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_127814,c_4]) ).
tff(c_127904,plain,
! [X_484,Y_485,Z_486] : ( multiply(multiply(X_484,Y_485),Z_486) = multiply(X_484,multiply(Y_485,Z_486)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_127937,plain,
! [Z_486] : ( multiply(sk_c9,multiply(sk_c6,Z_486)) = multiply(identity,Z_486) ),
inference(superposition,[status(thm),theory(equality)],[c_127819,c_127904]) ).
tff(c_127987,plain,
! [Z_489] : ( multiply(sk_c9,multiply(sk_c6,Z_489)) = Z_489 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127937]) ).
tff(c_127999,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_127875,c_127987]) ).
tff(c_128003,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_127882,c_127999]) ).
tff(c_64,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_127887,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_127815,c_64]) ).
tff(c_128100,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_128003,c_127887]) ).
tff(c_66,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_127842,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_127815,c_66]) ).
tff(c_127846,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_127842,c_4]) ).
tff(c_127931,plain,
! [Z_486] : ( multiply(sk_c10,multiply(sk_c4,Z_486)) = multiply(identity,Z_486) ),
inference(superposition,[status(thm),theory(equality)],[c_127846,c_127904]) ).
tff(c_131550,plain,
! [Z_533] : ( multiply(sk_c10,multiply(sk_c4,Z_533)) = Z_533 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127931]) ).
tff(c_131562,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_128100,c_131550]) ).
tff(c_127946,plain,
! [X_2,Z_486] : ( multiply(inverse(X_2),multiply(X_2,Z_486)) = multiply(identity,Z_486) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_127904]) ).
tff(c_131573,plain,
! [X_534,Z_535] : ( multiply(inverse(X_534),multiply(X_534,Z_535)) = Z_535 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127946]) ).
tff(c_131591,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_131562,c_131573]) ).
tff(c_131652,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_131591]) ).
tff(c_131673,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_131652,c_128003]) ).
tff(c_127919,plain,
! [Z_486] : ( multiply(sk_c4,multiply(sk_c10,Z_486)) = multiply(sk_c9,Z_486) ),
inference(superposition,[status(thm),theory(equality)],[c_127887,c_127904]) ).
tff(c_131857,plain,
! [Z_538] : ( multiply(sk_c4,multiply(sk_c10,Z_538)) = Z_538 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_131673,c_127919]) ).
tff(c_131887,plain,
multiply(sk_c4,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_125,c_131857]) ).
tff(c_131884,plain,
multiply(sk_c4,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_127846,c_131857]) ).
tff(c_131969,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_131887,c_131884]) ).
tff(c_131665,plain,
multiply(sk_c10,identity) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_131652,c_131562]) ).
tff(c_131875,plain,
multiply(sk_c4,sk_c10) = identity,
inference(superposition,[status(thm),theory(equality)],[c_131665,c_131857]) ).
tff(c_132000,plain,
multiply(sk_c1,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_131969,c_131875]) ).
tff(c_127959,plain,
! [X_2,Z_486] : ( multiply(inverse(X_2),multiply(X_2,Z_486)) = Z_486 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127946]) ).
tff(c_132078,plain,
! [X_540,Z_541] : ( multiply(inverse(inverse(X_540)),Z_541) = multiply(X_540,Z_541) ),
inference(superposition,[status(thm),theory(equality)],[c_131573,c_127959]) ).
tff(c_131645,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_131573]) ).
tff(c_132085,plain,
! [X_540] : ( multiply(X_540,identity) = X_540 ),
inference(superposition,[status(thm),theory(equality)],[c_132078,c_131645]) ).
tff(c_128198,plain,
! [X_493,Z_494] : ( multiply(inverse(X_493),multiply(X_493,Z_494)) = Z_494 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127946]) ).
tff(c_128703,plain,
! [X_499,Z_500] : ( multiply(inverse(inverse(X_499)),Z_500) = multiply(X_499,Z_500) ),
inference(superposition,[status(thm),theory(equality)],[c_128198,c_127959]) ).
tff(c_128270,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_128198]) ).
tff(c_128710,plain,
! [X_499] : ( multiply(X_499,identity) = X_499 ),
inference(superposition,[status(thm),theory(equality)],[c_128703,c_128270]) ).
tff(c_128175,plain,
! [Z_492] : ( multiply(sk_c10,multiply(sk_c4,Z_492)) = Z_492 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_127931]) ).
tff(c_128187,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_128100,c_128175]) ).
tff(c_128216,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_128187,c_128198]) ).
tff(c_128277,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_128216]) ).
tff(c_128007,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_128003,c_127887]) ).
tff(c_128004,plain,
! [X4_12] :
( ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_92]) ).
tff(c_128042,plain,
! [X4_12] :
( ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_128003,c_128004]) ).
tff(c_128073,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_128007,c_128042]) ).
tff(c_128082,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_127842,c_128073]) ).
tff(c_128083,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_92]) ).
tff(c_128135,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_128003,c_128003,c_128003,c_128003,c_128003,c_128003,c_128003,c_128003,c_128003,c_128083]) ).
tff(c_128136,plain,
! [X7_9] :
( ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_128135]) ).
tff(c_131508,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_128710,c_128277,c_128277,c_2,c_128277,c_128277,c_128136]) ).
tff(c_70,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_127829,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_127815,c_70]) ).
tff(c_127833,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_127829,c_4]) ).
tff(c_128299,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_128277,c_127833]) ).
tff(c_128417,plain,
sk_c5 = identity,
inference(superposition,[status(thm),theory(equality)],[c_128299,c_2]) ).
tff(c_128300,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_128277,c_127829]) ).
tff(c_128428,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_128417,c_128300]) ).
tff(c_131510,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_131508,c_128428]) ).
tff(c_131511,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_128135]) ).
tff(c_140440,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_132085,c_131652,c_131652,c_131652,c_131652,c_132085,c_131652,c_131652,c_131652,c_132085,c_131652,c_131652,c_131652,c_131511]) ).
tff(c_140442,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_140440]) ).
tff(c_131674,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_131652,c_127833]) ).
tff(c_131792,plain,
sk_c5 = identity,
inference(superposition,[status(thm),theory(equality)],[c_131674,c_2]) ).
tff(c_131675,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_131652,c_127829]) ).
tff(c_131803,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_131792,c_131675]) ).
tff(c_140444,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_140442,c_131803]) ).
tff(c_140445,plain,
! [X6_7,X1_10,X2_11] :
( ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_140440]) ).
tff(c_398947,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_140445]) ).
tff(c_398949,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_398947,c_131803]) ).
tff(c_398950,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(splitRight,[status(thm)],[c_140445]) ).
tff(c_398952,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_398950]) ).
tff(c_398954,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_398952,c_131803]) ).
tff(c_400974,plain,
! [X1_1136] :
( ( inverse(X1_1136) != sk_c10 )
| ( multiply(X1_1136,sk_c10) != identity ) ),
inference(splitRight,[status(thm)],[c_398950]) ).
tff(c_401072,plain,
inverse(sk_c1) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_132000,c_400974]) ).
tff(c_401109,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_121,c_401072]) ).
tff(c_401111,plain,
inverse(sk_c1) != sk_c10,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_24,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_401123,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_401111,c_24]) ).
tff(c_30,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_401163,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_401111,c_30]) ).
tff(c_32,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_401152,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_401111,c_32]) ).
tff(c_34,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_401137,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_401111,c_34]) ).
tff(c_401141,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_401137,c_4]) ).
tff(c_401212,plain,
! [X_1137,Y_1138,Z_1139] : ( multiply(multiply(X_1137,Y_1138),Z_1139) = multiply(X_1137,multiply(Y_1138,Z_1139)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_401242,plain,
! [Z_1139] : ( multiply(sk_c9,multiply(sk_c6,Z_1139)) = multiply(identity,Z_1139) ),
inference(superposition,[status(thm),theory(equality)],[c_401141,c_401212]) ).
tff(c_401408,plain,
! [Z_1148] : ( multiply(sk_c9,multiply(sk_c6,Z_1148)) = Z_1148 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_401242]) ).
tff(c_401420,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_401152,c_401408]) ).
tff(c_401424,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_401163,c_401420]) ).
tff(c_26,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_401185,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_401111,c_26]) ).
tff(c_401110,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_401115,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_401110,c_4]) ).
tff(c_401248,plain,
! [Z_1139] : ( multiply(sk_c8,multiply(sk_c5,Z_1139)) = multiply(identity,Z_1139) ),
inference(superposition,[status(thm),theory(equality)],[c_401115,c_401212]) ).
tff(c_401369,plain,
! [Z_1146] : ( multiply(sk_c8,multiply(sk_c5,Z_1146)) = Z_1146 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_401248]) ).
tff(c_401381,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_401185,c_401369]) ).
tff(c_401427,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_401424,c_401381]) ).
tff(c_401254,plain,
! [X_2,Z_1139] : ( multiply(inverse(X_2),multiply(X_2,Z_1139)) = multiply(identity,Z_1139) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_401212]) ).
tff(c_404806,plain,
! [X_1189,Z_1190] : ( multiply(inverse(X_1189),multiply(X_1189,Z_1190)) = Z_1190 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_401254]) ).
tff(c_404839,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_401427,c_404806]) ).
tff(c_404884,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_404839]) ).
tff(c_22,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_401194,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_401111,c_22]) ).
tff(c_401429,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_401424,c_401194]) ).
tff(c_404898,plain,
multiply(sk_c4,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_404884,c_401429]) ).
tff(c_401267,plain,
! [X_2,Z_1139] : ( multiply(inverse(X_2),multiply(X_2,Z_1139)) = Z_1139 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_401254]) ).
tff(c_405210,plain,
! [X_1195,Z_1196] : ( multiply(inverse(inverse(X_1195)),Z_1196) = multiply(X_1195,Z_1196) ),
inference(superposition,[status(thm),theory(equality)],[c_404806,c_401267]) ).
tff(c_404875,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_404806]) ).
tff(c_405220,plain,
! [X_1195] : ( multiply(X_1195,identity) = X_1195 ),
inference(superposition,[status(thm),theory(equality)],[c_405210,c_404875]) ).
tff(c_401529,plain,
! [X_1149,Z_1150] : ( multiply(inverse(X_1149),multiply(X_1149,Z_1150)) = Z_1150 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_401254]) ).
tff(c_401933,plain,
! [X_1155,Z_1156] : ( multiply(inverse(inverse(X_1155)),Z_1156) = multiply(X_1155,Z_1156) ),
inference(superposition,[status(thm),theory(equality)],[c_401529,c_401267]) ).
tff(c_401598,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_401529]) ).
tff(c_401943,plain,
! [X_1155] : ( multiply(X_1155,identity) = X_1155 ),
inference(superposition,[status(thm),theory(equality)],[c_401933,c_401598]) ).
tff(c_401562,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_401427,c_401529]) ).
tff(c_401607,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_401562]) ).
tff(c_401335,plain,
! [X4_1144] :
( ( inverse(X4_1144) != sk_c10 )
| ( multiply(X4_1144,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_92]) ).
tff(c_401342,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_401194,c_401335]) ).
tff(c_401354,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_401123,c_401342]) ).
tff(c_401355,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_92]) ).
tff(c_401464,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_401424,c_401424,c_401424,c_401424,c_401424,c_401424,c_401424,c_401424,c_401424,c_401355]) ).
tff(c_401465,plain,
! [X7_9] :
( ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_401464]) ).
tff(c_404739,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_401943,c_401607,c_401607,c_2,c_401607,c_401607,c_401465]) ).
tff(c_401438,plain,
inverse(sk_c2) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_401424,c_109]) ).
tff(c_401453,plain,
multiply(sk_c8,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_401438,c_4]) ).
tff(c_401639,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_401607,c_401453]) ).
tff(c_401624,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_401607,c_401438]) ).
tff(c_401654,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_401639,c_401624]) ).
tff(c_404741,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_404739,c_401654]) ).
tff(c_404742,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_401464]) ).
tff(c_412485,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_405220,c_404884,c_404884,c_404884,c_404884,c_405220,c_404884,c_404884,c_404884,c_405220,c_404884,c_404884,c_404884,c_404742]) ).
tff(c_412487,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_412485]) ).
tff(c_404916,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_404884,c_401453]) ).
tff(c_404901,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_404884,c_401438]) ).
tff(c_404931,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_404916,c_404901]) ).
tff(c_412489,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_412487,c_404931]) ).
tff(c_412490,plain,
! [X6_7,X1_10,X2_11] :
( ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_412485]) ).
tff(c_457731,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_412490]) ).
tff(c_457733,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_457731,c_404931]) ).
tff(c_457734,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(splitRight,[status(thm)],[c_412490]) ).
tff(c_457736,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_457734]) ).
tff(c_457738,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_457736,c_404931]) ).
tff(c_459032,plain,
! [X1_1427] :
( ( inverse(X1_1427) != sk_c10 )
| ( multiply(X1_1427,sk_c10) != identity ) ),
inference(splitRight,[status(thm)],[c_457734]) ).
tff(c_459107,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_404898,c_459032]) ).
tff(c_459138,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_401123,c_459107]) ).
tff(c_459140,plain,
inverse(sk_c2) != sk_c9,
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_52,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_579767,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_459140,c_52]) ).
tff(c_579788,plain,
inverse(sk_c1) = sk_c10,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_579792,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_579788,c_4]) ).
tff(c_58,plain,
( ( multiply(sk_c9,sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_579827,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_459140,c_58]) ).
tff(c_459177,plain,
inverse(sk_c1) = sk_c10,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_459181,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_459177,c_4]) ).
tff(c_459226,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_459140,c_58]) ).
tff(c_60,plain,
( ( multiply(sk_c6,sk_c9) = sk_c7 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_459209,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_459140,c_60]) ).
tff(c_62,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_459164,plain,
inverse(sk_c6) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_459140,c_62]) ).
tff(c_459168,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_459164,c_4]) ).
tff(c_459253,plain,
! [X_1428,Y_1429,Z_1430] : ( multiply(multiply(X_1428,Y_1429),Z_1430) = multiply(X_1428,multiply(Y_1429,Z_1430)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_459286,plain,
! [Z_1430] : ( multiply(sk_c9,multiply(sk_c6,Z_1430)) = multiply(identity,Z_1430) ),
inference(superposition,[status(thm),theory(equality)],[c_459168,c_459253]) ).
tff(c_459333,plain,
! [Z_1432] : ( multiply(sk_c9,multiply(sk_c6,Z_1432)) = Z_1432 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_459286]) ).
tff(c_459345,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_459209,c_459333]) ).
tff(c_459349,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_459226,c_459345]) ).
tff(c_50,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_459215,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_459140,c_50]) ).
tff(c_459190,plain,
inverse(sk_c4) = sk_c10,
inference(negUnitSimplification,[status(thm)],[c_459140,c_52]) ).
tff(c_459194,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_459190,c_4]) ).
tff(c_459280,plain,
! [Z_1430] : ( multiply(sk_c10,multiply(sk_c4,Z_1430)) = multiply(identity,Z_1430) ),
inference(superposition,[status(thm),theory(equality)],[c_459194,c_459253]) ).
tff(c_459310,plain,
! [Z_1431] : ( multiply(sk_c10,multiply(sk_c4,Z_1431)) = Z_1431 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_459280]) ).
tff(c_459322,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_459215,c_459310]) ).
tff(c_459449,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_459349,c_459322]) ).
tff(c_459295,plain,
! [X_2,Z_1430] : ( multiply(inverse(X_2),multiply(X_2,Z_1430)) = multiply(identity,Z_1430) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_459253]) ).
tff(c_462521,plain,
! [X_1473,Z_1474] : ( multiply(inverse(X_1473),multiply(X_1473,Z_1474)) = Z_1474 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_459295]) ).
tff(c_462563,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_459449,c_462521]) ).
tff(c_462611,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_462563]) ).
tff(c_462633,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_462611,c_459349]) ).
tff(c_459274,plain,
! [Z_1430] : ( multiply(sk_c4,multiply(sk_c10,Z_1430)) = multiply(sk_c9,Z_1430) ),
inference(superposition,[status(thm),theory(equality)],[c_459215,c_459253]) ).
tff(c_462856,plain,
! [Z_1476] : ( multiply(sk_c4,multiply(sk_c10,Z_1476)) = Z_1476 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_462633,c_459274]) ).
tff(c_462883,plain,
multiply(sk_c4,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_459181,c_462856]) ).
tff(c_462880,plain,
multiply(sk_c4,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_459194,c_462856]) ).
tff(c_462913,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_462883,c_462880]) ).
tff(c_459452,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_459349,c_459215]) ).
tff(c_462626,plain,
multiply(sk_c4,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_462611,c_459452]) ).
tff(c_462932,plain,
multiply(sk_c1,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_462913,c_462626]) ).
tff(c_459308,plain,
! [X_2,Z_1430] : ( multiply(inverse(X_2),multiply(X_2,Z_1430)) = Z_1430 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_459295]) ).
tff(c_463041,plain,
! [X_1479,Z_1480] : ( multiply(inverse(inverse(X_1479)),Z_1480) = multiply(X_1479,Z_1480) ),
inference(superposition,[status(thm),theory(equality)],[c_462521,c_459308]) ).
tff(c_462599,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_462521]) ).
tff(c_463048,plain,
! [X_1479] : ( multiply(X_1479,identity) = X_1479 ),
inference(superposition,[status(thm),theory(equality)],[c_463041,c_462599]) ).
tff(c_459593,plain,
! [X_1436,Z_1437] : ( multiply(inverse(X_1436),multiply(X_1436,Z_1437)) = Z_1437 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_459295]) ).
tff(c_460113,plain,
! [X_1442,Z_1443] : ( multiply(inverse(inverse(X_1442)),Z_1443) = multiply(X_1442,Z_1443) ),
inference(superposition,[status(thm),theory(equality)],[c_459593,c_459308]) ).
tff(c_459671,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_459593]) ).
tff(c_460120,plain,
! [X_1442] : ( multiply(X_1442,identity) = X_1442 ),
inference(superposition,[status(thm),theory(equality)],[c_460113,c_459671]) ).
tff(c_459635,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_459449,c_459593]) ).
tff(c_459683,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_459635]) ).
tff(c_459355,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_459349,c_459215]) ).
tff(c_459350,plain,
! [X4_12] :
( ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_92]) ).
tff(c_459410,plain,
! [X4_12] :
( ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_459349,c_459350]) ).
tff(c_459434,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_459355,c_459410]) ).
tff(c_459446,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_459190,c_459434]) ).
tff(c_459447,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_92]) ).
tff(c_459512,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_459349,c_459349,c_459349,c_459349,c_459349,c_459349,c_459349,c_459349,c_459349,c_459447]) ).
tff(c_459513,plain,
! [X7_9] :
( ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_459512]) ).
tff(c_462438,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_460120,c_459683,c_459683,c_2,c_459683,c_459683,c_459513]) ).
tff(c_459139,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_459144,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_459139,c_4]) ).
tff(c_459706,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_459683,c_459144]) ).
tff(c_459788,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_459706,c_459308]) ).
tff(c_459800,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_459788]) ).
tff(c_459707,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_459683,c_459139]) ).
tff(c_459804,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_459800,c_459707]) ).
tff(c_462440,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_462438,c_459804]) ).
tff(c_462441,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_459512]) ).
tff(c_469879,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_463048,c_462611,c_462611,c_462611,c_462611,c_463048,c_462611,c_462611,c_462611,c_463048,c_462611,c_462611,c_462611,c_462441]) ).
tff(c_469881,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_469879]) ).
tff(c_462634,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_462611,c_459144]) ).
tff(c_462716,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_462634,c_459308]) ).
tff(c_462728,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_462716]) ).
tff(c_462635,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_462611,c_459139]) ).
tff(c_462732,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_462728,c_462635]) ).
tff(c_469883,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_469881,c_462732]) ).
tff(c_469884,plain,
! [X6_7,X1_10,X2_11] :
( ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_469879]) ).
tff(c_517700,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_469884]) ).
tff(c_517702,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_517700,c_462732]) ).
tff(c_517703,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(splitRight,[status(thm)],[c_469884]) ).
tff(c_517705,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_517703]) ).
tff(c_517707,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_517705,c_462732]) ).
tff(c_519375,plain,
! [X1_1719] :
( ( inverse(X1_1719) != sk_c10 )
| ( multiply(X1_1719,sk_c10) != identity ) ),
inference(splitRight,[status(thm)],[c_517703]) ).
tff(c_519450,plain,
inverse(sk_c1) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_462932,c_519375]) ).
tff(c_519481,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_459177,c_519450]) ).
tff(c_519482,plain,
inverse(sk_c4) = sk_c10,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_519483,plain,
inverse(sk_c1) != sk_c10,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_519522,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_519483,c_30]) ).
tff(c_519501,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_519483,c_32]) ).
tff(c_519554,plain,
! [X_1720,Y_1721,Z_1722] : ( multiply(multiply(X_1720,Y_1721),Z_1722) = multiply(X_1720,multiply(Y_1721,Z_1722)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_519584,plain,
! [Z_1722] : ( multiply(sk_c9,multiply(sk_c6,Z_1722)) = multiply(identity,Z_1722) ),
inference(superposition,[status(thm),theory(equality)],[c_459168,c_519554]) ).
tff(c_520350,plain,
! [Z_1738] : ( multiply(sk_c9,multiply(sk_c6,Z_1738)) = Z_1738 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_519584]) ).
tff(c_520362,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_519501,c_520350]) ).
tff(c_520366,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_519522,c_520362]) ).
tff(c_519512,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_459140,c_50]) ).
tff(c_519487,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_519482,c_4]) ).
tff(c_519581,plain,
! [Z_1722] : ( multiply(sk_c10,multiply(sk_c4,Z_1722)) = multiply(identity,Z_1722) ),
inference(superposition,[status(thm),theory(equality)],[c_519487,c_519554]) ).
tff(c_519607,plain,
! [Z_1723] : ( multiply(sk_c10,multiply(sk_c4,Z_1723)) = Z_1723 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_519581]) ).
tff(c_519619,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_519512,c_519607]) ).
tff(c_520371,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_520366,c_519619]) ).
tff(c_519593,plain,
! [X_2,Z_1722] : ( multiply(inverse(X_2),multiply(X_2,Z_1722)) = multiply(identity,Z_1722) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_519554]) ).
tff(c_523254,plain,
! [X_1773,Z_1774] : ( multiply(inverse(X_1773),multiply(X_1773,Z_1774)) = Z_1774 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_519593]) ).
tff(c_523272,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_520371,c_523254]) ).
tff(c_523327,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_523272]) ).
tff(c_520373,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_520366,c_519512]) ).
tff(c_523338,plain,
multiply(sk_c4,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_523327,c_520373]) ).
tff(c_519605,plain,
! [X_2,Z_1722] : ( multiply(inverse(X_2),multiply(X_2,Z_1722)) = Z_1722 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_519593]) ).
tff(c_523631,plain,
! [X_1777,Z_1778] : ( multiply(inverse(inverse(X_1777)),Z_1778) = multiply(X_1777,Z_1778) ),
inference(superposition,[status(thm),theory(equality)],[c_519605,c_523254]) ).
tff(c_523320,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_523254]) ).
tff(c_523641,plain,
! [X_1777] : ( multiply(X_1777,identity) = X_1777 ),
inference(superposition,[status(thm),theory(equality)],[c_523631,c_523320]) ).
tff(c_520458,plain,
! [X_1739,Z_1740] : ( multiply(inverse(X_1739),multiply(X_1739,Z_1740)) = Z_1740 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_519593]) ).
tff(c_520835,plain,
! [X_1743,Z_1744] : ( multiply(inverse(inverse(X_1743)),Z_1744) = multiply(X_1743,Z_1744) ),
inference(superposition,[status(thm),theory(equality)],[c_519605,c_520458]) ).
tff(c_520524,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_520458]) ).
tff(c_520845,plain,
! [X_1743] : ( multiply(X_1743,identity) = X_1743 ),
inference(superposition,[status(thm),theory(equality)],[c_520835,c_520524]) ).
tff(c_520476,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_520371,c_520458]) ).
tff(c_520531,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_520476]) ).
tff(c_519730,plain,
! [X_1727,Z_1728] : ( multiply(inverse(X_1727),multiply(X_1727,Z_1728)) = Z_1728 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_519593]) ).
tff(c_520136,plain,
! [X_1734,Z_1735] : ( multiply(inverse(inverse(X_1734)),Z_1735) = multiply(X_1734,Z_1735) ),
inference(superposition,[status(thm),theory(equality)],[c_519605,c_519730]) ).
tff(c_519781,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_519730]) ).
tff(c_520150,plain,
! [X_1734] : ( multiply(X_1734,identity) = X_1734 ),
inference(superposition,[status(thm),theory(equality)],[c_520136,c_519781]) ).
tff(c_520202,plain,
! [X_1736] : ( multiply(X_1736,identity) = X_1736 ),
inference(superposition,[status(thm),theory(equality)],[c_520136,c_519781]) ).
tff(c_519769,plain,
multiply(inverse(sk_c10),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_519487,c_519730]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_520000,plain,
! [Z_5] : ( multiply(inverse(sk_c10),multiply(identity,Z_5)) = multiply(sk_c4,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_519769,c_6]) ).
tff(c_520003,plain,
! [Z_5] : ( multiply(inverse(sk_c10),Z_5) = multiply(sk_c4,Z_5) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_520000]) ).
tff(c_520213,plain,
multiply(sk_c4,identity) = inverse(sk_c10),
inference(superposition,[status(thm),theory(equality)],[c_520202,c_520003]) ).
tff(c_520285,plain,
inverse(sk_c10) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_520150,c_520213]) ).
tff(c_519654,plain,
! [Z_1725] : ( multiply(sk_c9,multiply(sk_c6,Z_1725)) = Z_1725 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_519584]) ).
tff(c_519666,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_519501,c_519654]) ).
tff(c_519670,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_519522,c_519666]) ).
tff(c_54,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( inverse(sk_c2) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_519506,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_459140,c_54]) ).
tff(c_519590,plain,
! [Z_1722] : ( multiply(sk_c8,multiply(sk_c5,Z_1722)) = multiply(identity,Z_1722) ),
inference(superposition,[status(thm),theory(equality)],[c_459144,c_519554]) ).
tff(c_519630,plain,
! [Z_1724] : ( multiply(sk_c8,multiply(sk_c5,Z_1724)) = Z_1724 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_519590]) ).
tff(c_519642,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_519506,c_519630]) ).
tff(c_519672,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_519670,c_519642]) ).
tff(c_519751,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_519672,c_519730]) ).
tff(c_519788,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_519751]) ).
tff(c_519646,plain,
! [X4_12] :
( ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_92]) ).
tff(c_519688,plain,
! [X4_1726] :
( ( inverse(X4_1726) != sk_c10 )
| ( multiply(X4_1726,sk_c10) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_519670,c_519646]) ).
tff(c_519696,plain,
( ( inverse(inverse(sk_c10)) != sk_c10 )
| ( sk_c8 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_519688]) ).
tff(c_520036,plain,
inverse(inverse(sk_c10)) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_519788,c_519696]) ).
tff(c_520303,plain,
inverse(sk_c4) != sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_520285,c_520036]) ).
tff(c_520308,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_519482,c_520303]) ).
tff(c_520309,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_92]) ).
tff(c_520392,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_520366,c_520366,c_520366,c_520366,c_520366,c_520366,c_520366,c_520366,c_520366,c_520309]) ).
tff(c_520393,plain,
! [X7_9] :
( ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_520392]) ).
tff(c_523186,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_520845,c_520531,c_520531,c_2,c_520531,c_520531,c_520393]) ).
tff(c_459152,plain,
inverse(sk_c3) = sk_c9,
inference(splitLeft,[status(thm)],[c_76]) ).
tff(c_520379,plain,
inverse(sk_c3) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_520366,c_459152]) ).
tff(c_520397,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_520379,c_4]) ).
tff(c_520563,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_520531,c_520397]) ).
tff(c_520546,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_520531,c_520379]) ).
tff(c_520592,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_520563,c_520546]) ).
tff(c_523188,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_523186,c_520592]) ).
tff(c_523189,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_520392]) ).
tff(c_530351,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_523641,c_523327,c_523327,c_523327,c_523327,c_523641,c_523327,c_523327,c_523327,c_523641,c_523327,c_523327,c_523327,c_523189]) ).
tff(c_530353,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_530351]) ).
tff(c_523193,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_520379,c_4]) ).
tff(c_523359,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_523327,c_523193]) ).
tff(c_523342,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_523327,c_520379]) ).
tff(c_523388,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_523359,c_523342]) ).
tff(c_530355,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_530353,c_523388]) ).
tff(c_530356,plain,
! [X6_7,X1_10,X2_11] :
( ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_530351]) ).
tff(c_578021,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_530356]) ).
tff(c_578023,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_578021,c_523388]) ).
tff(c_578024,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(splitRight,[status(thm)],[c_530356]) ).
tff(c_578026,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_578024]) ).
tff(c_578028,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_578026,c_523388]) ).
tff(c_579647,plain,
! [X1_2012] :
( ( inverse(X1_2012) != sk_c10 )
| ( multiply(X1_2012,sk_c10) != identity ) ),
inference(splitRight,[status(thm)],[c_578024]) ).
tff(c_579722,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_523338,c_579647]) ).
tff(c_579753,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_519482,c_579722]) ).
tff(c_579755,plain,
inverse(sk_c3) != sk_c9,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_579814,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_579755,c_74]) ).
tff(c_579754,plain,
inverse(sk_c6) = sk_c9,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_579759,plain,
multiply(sk_c9,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_579754,c_4]) ).
tff(c_579852,plain,
! [X_2013,Y_2014,Z_2015] : ( multiply(multiply(X_2013,Y_2014),Z_2015) = multiply(X_2013,multiply(Y_2014,Z_2015)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_579885,plain,
! [Z_2015] : ( multiply(sk_c9,multiply(sk_c6,Z_2015)) = multiply(identity,Z_2015) ),
inference(superposition,[status(thm),theory(equality)],[c_579759,c_579852]) ).
tff(c_580804,plain,
! [Z_2033] : ( multiply(sk_c9,multiply(sk_c6,Z_2033)) = Z_2033 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_579885]) ).
tff(c_580816,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_579814,c_580804]) ).
tff(c_580820,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_579827,c_580816]) ).
tff(c_579803,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_459140,c_50]) ).
tff(c_579771,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_579767,c_4]) ).
tff(c_579882,plain,
! [Z_2015] : ( multiply(sk_c10,multiply(sk_c4,Z_2015)) = multiply(identity,Z_2015) ),
inference(superposition,[status(thm),theory(equality)],[c_579771,c_579852]) ).
tff(c_579905,plain,
! [Z_2016] : ( multiply(sk_c10,multiply(sk_c4,Z_2016)) = Z_2016 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_579882]) ).
tff(c_579917,plain,
multiply(sk_c10,sk_c9) = sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_579803,c_579905]) ).
tff(c_580823,plain,
multiply(sk_c10,sk_c8) = sk_c10,
inference(demodulation,[status(thm),theory(equality)],[c_580820,c_579917]) ).
tff(c_579891,plain,
! [X_2,Z_2015] : ( multiply(inverse(X_2),multiply(X_2,Z_2015)) = multiply(identity,Z_2015) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_579852]) ).
tff(c_583463,plain,
! [X_2068,Z_2069] : ( multiply(inverse(X_2068),multiply(X_2068,Z_2069)) = Z_2069 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_579891]) ).
tff(c_583481,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_580823,c_583463]) ).
tff(c_583533,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_583481]) ).
tff(c_583547,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_583533,c_580820]) ).
tff(c_579876,plain,
! [Z_2015] : ( multiply(sk_c4,multiply(sk_c10,Z_2015)) = multiply(sk_c9,Z_2015) ),
inference(superposition,[status(thm),theory(equality)],[c_579803,c_579852]) ).
tff(c_583634,plain,
! [Z_2071] : ( multiply(sk_c4,multiply(sk_c10,Z_2071)) = Z_2071 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_583547,c_579876]) ).
tff(c_583655,plain,
multiply(sk_c4,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_579792,c_583634]) ).
tff(c_583658,plain,
multiply(sk_c4,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_579771,c_583634]) ).
tff(c_583822,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_583655,c_583658]) ).
tff(c_580827,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_580820,c_579803]) ).
tff(c_583617,plain,
multiply(sk_c4,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_583533,c_580827]) ).
tff(c_583841,plain,
multiply(sk_c1,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_583822,c_583617]) ).
tff(c_579903,plain,
! [X_2,Z_2015] : ( multiply(inverse(X_2),multiply(X_2,Z_2015)) = Z_2015 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_579891]) ).
tff(c_583920,plain,
! [X_2074,Z_2075] : ( multiply(inverse(inverse(X_2074)),Z_2075) = multiply(X_2074,Z_2075) ),
inference(superposition,[status(thm),theory(equality)],[c_583463,c_579903]) ).
tff(c_583526,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_583463]) ).
tff(c_583927,plain,
! [X_2074] : ( multiply(X_2074,identity) = X_2074 ),
inference(superposition,[status(thm),theory(equality)],[c_583920,c_583526]) ).
tff(c_580885,plain,
! [X_2034,Z_2035] : ( multiply(inverse(X_2034),multiply(X_2034,Z_2035)) = Z_2035 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_579891]) ).
tff(c_581342,plain,
! [X_2040,Z_2041] : ( multiply(inverse(inverse(X_2040)),Z_2041) = multiply(X_2040,Z_2041) ),
inference(superposition,[status(thm),theory(equality)],[c_580885,c_579903]) ).
tff(c_580948,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_580885]) ).
tff(c_581349,plain,
! [X_2040] : ( multiply(X_2040,identity) = X_2040 ),
inference(superposition,[status(thm),theory(equality)],[c_581342,c_580948]) ).
tff(c_580903,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_580823,c_580885]) ).
tff(c_580955,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_580903]) ).
tff(c_579952,plain,
! [Z_2018] : ( multiply(sk_c9,multiply(sk_c6,Z_2018)) = Z_2018 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_579885]) ).
tff(c_579964,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_579814,c_579952]) ).
tff(c_579968,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_579827,c_579964]) ).
tff(c_68,plain,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_579819,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_579755,c_68]) ).
tff(c_579888,plain,
! [Z_2015] : ( multiply(sk_c8,multiply(sk_c5,Z_2015)) = multiply(identity,Z_2015) ),
inference(superposition,[status(thm),theory(equality)],[c_459144,c_579852]) ).
tff(c_579929,plain,
! [Z_2017] : ( multiply(sk_c8,multiply(sk_c5,Z_2017)) = Z_2017 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_579888]) ).
tff(c_579941,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_579819,c_579929]) ).
tff(c_579970,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_579968,c_579941]) ).
tff(c_580045,plain,
! [X_2020,Z_2021] : ( multiply(inverse(X_2020),multiply(X_2020,Z_2021)) = Z_2021 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_579891]) ).
tff(c_580063,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_579970,c_580045]) ).
tff(c_580115,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_580063]) ).
tff(c_580518,plain,
! [X_2027,Z_2028] : ( multiply(inverse(inverse(X_2027)),Z_2028) = multiply(X_2027,Z_2028) ),
inference(superposition,[status(thm),theory(equality)],[c_580045,c_579903]) ).
tff(c_580108,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_580045]) ).
tff(c_580566,plain,
! [X_2029] : ( multiply(X_2029,identity) = X_2029 ),
inference(superposition,[status(thm),theory(equality)],[c_580518,c_580108]) ).
tff(c_580130,plain,
sk_c9 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_580115,c_579968]) ).
tff(c_580296,plain,
! [Z_2024] : ( multiply(sk_c4,multiply(sk_c10,Z_2024)) = Z_2024 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_580130,c_579876]) ).
tff(c_580317,plain,
multiply(sk_c4,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_579792,c_580296]) ).
tff(c_580320,plain,
multiply(sk_c4,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_579771,c_580296]) ).
tff(c_580398,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_580317,c_580320]) ).
tff(c_580096,plain,
multiply(inverse(sk_c10),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_579771,c_580045]) ).
tff(c_580452,plain,
multiply(inverse(sk_c10),identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_580398,c_580096]) ).
tff(c_580583,plain,
inverse(sk_c10) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_580566,c_580452]) ).
tff(c_579921,plain,
! [X4_12] :
( ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_92]) ).
tff(c_579985,plain,
! [X4_2019] :
( ( inverse(X4_2019) != sk_c10 )
| ( multiply(X4_2019,sk_c10) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_579968,c_579921]) ).
tff(c_579993,plain,
( ( inverse(inverse(sk_c10)) != sk_c10 )
| ( sk_c8 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_579985]) ).
tff(c_580772,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_580115,c_579788,c_580583,c_579993]) ).
tff(c_580773,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_92]) ).
tff(c_580836,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_580820,c_580820,c_580820,c_580820,c_580820,c_580820,c_580820,c_580820,c_580820,c_580773]) ).
tff(c_580837,plain,
! [X7_9] :
( ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_580836]) ).
tff(c_583412,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_581349,c_580955,c_580955,c_2,c_580955,c_580955,c_580837]) ).
tff(c_580971,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_580955,c_459144]) ).
tff(c_581095,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_580971,c_579903]) ).
tff(c_581107,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_581095]) ).
tff(c_580972,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_580955,c_459139]) ).
tff(c_581111,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_581107,c_580972]) ).
tff(c_583414,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_583412,c_581111]) ).
tff(c_583415,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_580836]) ).
tff(c_590445,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_583927,c_583533,c_583533,c_583533,c_583533,c_583927,c_583533,c_583533,c_583533,c_583927,c_583533,c_583533,c_583533,c_583415]) ).
tff(c_590447,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_590445]) ).
tff(c_583549,plain,
multiply(identity,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_583533,c_459144]) ).
tff(c_583673,plain,
multiply(inverse(identity),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_583549,c_579903]) ).
tff(c_583685,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_583673]) ).
tff(c_583550,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_583533,c_459139]) ).
tff(c_583689,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_583685,c_583550]) ).
tff(c_590449,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_590447,c_583689]) ).
tff(c_590450,plain,
! [X6_7,X1_10,X2_11] :
( ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_590445]) ).
tff(c_643288,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_590450]) ).
tff(c_643290,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_643288,c_583689]) ).
tff(c_643291,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(splitRight,[status(thm)],[c_590450]) ).
tff(c_643293,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_643291]) ).
tff(c_643295,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_643293,c_583689]) ).
tff(c_645014,plain,
! [X1_2326] :
( ( inverse(X1_2326) != sk_c10 )
| ( multiply(X1_2326,sk_c10) != identity ) ),
inference(splitRight,[status(thm)],[c_643291]) ).
tff(c_645092,plain,
inverse(sk_c1) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_583841,c_645014]) ).
tff(c_645124,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_579788,c_645092]) ).
tff(c_645126,plain,
inverse(sk_c1) != sk_c10,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_645132,plain,
multiply(sk_c9,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_645126,c_30]) ).
tff(c_645138,plain,
multiply(sk_c6,sk_c9) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_645126,c_32]) ).
tff(c_645183,plain,
! [X_2327,Y_2328,Z_2329] : ( multiply(multiply(X_2327,Y_2328),Z_2329) = multiply(X_2327,multiply(Y_2328,Z_2329)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_645213,plain,
! [Z_2329] : ( multiply(sk_c9,multiply(sk_c6,Z_2329)) = multiply(identity,Z_2329) ),
inference(superposition,[status(thm),theory(equality)],[c_579759,c_645183]) ).
tff(c_645382,plain,
! [Z_2334] : ( multiply(sk_c9,multiply(sk_c6,Z_2334)) = Z_2334 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_645213]) ).
tff(c_645394,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_645138,c_645382]) ).
tff(c_645398,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_645132,c_645394]) ).
tff(c_645125,plain,
multiply(sk_c5,sk_c8) = sk_c9,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_645216,plain,
! [Z_2329] : ( multiply(sk_c8,multiply(sk_c5,Z_2329)) = multiply(identity,Z_2329) ),
inference(superposition,[status(thm),theory(equality)],[c_459144,c_645183]) ).
tff(c_645255,plain,
! [Z_2331] : ( multiply(sk_c8,multiply(sk_c5,Z_2331)) = Z_2331 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_645216]) ).
tff(c_645267,plain,
multiply(sk_c8,sk_c9) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_645125,c_645255]) ).
tff(c_645400,plain,
multiply(sk_c8,sk_c8) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_645398,c_645267]) ).
tff(c_645219,plain,
! [X_2,Z_2329] : ( multiply(inverse(X_2),multiply(X_2,Z_2329)) = multiply(identity,Z_2329) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_645183]) ).
tff(c_647533,plain,
! [X_2363,Z_2364] : ( multiply(inverse(X_2363),multiply(X_2363,Z_2364)) = Z_2364 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_645219]) ).
tff(c_647554,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_645400,c_647533]) ).
tff(c_647601,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_647554]) ).
tff(c_645143,plain,
multiply(sk_c4,sk_c10) = sk_c9,
inference(negUnitSimplification,[status(thm)],[c_459140,c_50]) ).
tff(c_645402,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_645398,c_645143]) ).
tff(c_647607,plain,
multiply(sk_c4,sk_c10) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_647601,c_645402]) ).
tff(c_645230,plain,
! [X_2,Z_2329] : ( multiply(inverse(X_2),multiply(X_2,Z_2329)) = Z_2329 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_645219]) ).
tff(c_647905,plain,
! [X_2368,Z_2369] : ( multiply(inverse(inverse(X_2368)),Z_2369) = multiply(X_2368,Z_2369) ),
inference(superposition,[status(thm),theory(equality)],[c_645230,c_647533]) ).
tff(c_647593,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_647533]) ).
tff(c_647915,plain,
! [X_2368] : ( multiply(X_2368,identity) = X_2368 ),
inference(superposition,[status(thm),theory(equality)],[c_647905,c_647593]) ).
tff(c_645473,plain,
! [X_2335,Z_2336] : ( multiply(inverse(X_2335),multiply(X_2335,Z_2336)) = Z_2336 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_645219]) ).
tff(c_645845,plain,
! [X_2340,Z_2341] : ( multiply(inverse(inverse(X_2340)),Z_2341) = multiply(X_2340,Z_2341) ),
inference(superposition,[status(thm),theory(equality)],[c_645230,c_645473]) ).
tff(c_645533,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_645473]) ).
tff(c_645855,plain,
! [X_2340] : ( multiply(X_2340,identity) = X_2340 ),
inference(superposition,[status(thm),theory(equality)],[c_645845,c_645533]) ).
tff(c_645494,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_645400,c_645473]) ).
tff(c_645541,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_645494]) ).
tff(c_645279,plain,
! [Z_2332] : ( multiply(sk_c9,multiply(sk_c6,Z_2332)) = Z_2332 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_645213]) ).
tff(c_645291,plain,
multiply(sk_c9,sk_c7) = sk_c9,
inference(superposition,[status(thm),theory(equality)],[c_645138,c_645279]) ).
tff(c_645295,plain,
sk_c9 = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_645132,c_645291]) ).
tff(c_645299,plain,
multiply(sk_c4,sk_c10) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_645295,c_645143]) ).
tff(c_645271,plain,
! [X4_12] :
( ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c9 ) ),
inference(splitLeft,[status(thm)],[c_92]) ).
tff(c_645318,plain,
! [X4_12] :
( ( inverse(X4_12) != sk_c10 )
| ( multiply(X4_12,sk_c10) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_645295,c_645271]) ).
tff(c_645361,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_645299,c_645318]) ).
tff(c_645373,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_579767,c_645361]) ).
tff(c_645374,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c9 )
| ( multiply(X5_6,sk_c9) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c9 )
| ( inverse(X6_7) != sk_c9 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c9 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c9 )
| ( inverse(X7_9) != sk_c9 )
| ( multiply(sk_c9,multiply(X7_9,sk_c9)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_92]) ).
tff(c_645414,plain,
! [X5_6,X1_10,X7_9,X6_7,X2_11] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_645398,c_645398,c_645398,c_645398,c_645398,c_645398,c_645398,c_645398,c_645398,c_645374]) ).
tff(c_645415,plain,
! [X7_9] :
( ( inverse(X7_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X7_9,sk_c8)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_645414]) ).
tff(c_647472,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_645855,c_645541,c_645541,c_2,c_645541,c_645541,c_645415]) ).
tff(c_645406,plain,
multiply(sk_c8,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_645398,c_579759]) ).
tff(c_645644,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_645541,c_645406]) ).
tff(c_645408,plain,
inverse(sk_c6) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_645398,c_579754]) ).
tff(c_645553,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_645541,c_645408]) ).
tff(c_645646,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_645644,c_645553]) ).
tff(c_647474,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_647472,c_645646]) ).
tff(c_647475,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != sk_c8 )
| ( multiply(X2_11,sk_c8) != sk_c8 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != sk_c8 )
| ( multiply(X6_7,sk_c8) != sk_c8 )
| ( inverse(X6_7) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_645414]) ).
tff(c_653921,plain,
! [X2_11,X1_10,X6_7,X5_6] :
( ( inverse(X2_11) != identity )
| ( identity != X2_11 )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_647915,c_647601,c_647601,c_647601,c_647601,c_647915,c_647601,c_647601,c_647601,c_647915,c_647601,c_647601,c_647601,c_647475]) ).
tff(c_653923,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_653921]) ).
tff(c_647704,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_647601,c_645406]) ).
tff(c_647613,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_647601,c_645408]) ).
tff(c_647706,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_647704,c_647613]) ).
tff(c_653925,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_653923,c_647706]) ).
tff(c_653926,plain,
! [X6_7,X1_10,X2_11] :
( ( identity != X6_7 )
| ( inverse(X6_7) != identity )
| ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( inverse(X2_11) != identity )
| ( identity != X2_11 ) ),
inference(splitRight,[status(thm)],[c_653921]) ).
tff(c_708923,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_653926]) ).
tff(c_708925,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_708923,c_647706]) ).
tff(c_708926,plain,
! [X1_10,X6_7] :
( ( inverse(X1_10) != sk_c10 )
| ( multiply(X1_10,sk_c10) != identity )
| ( identity != X6_7 )
| ( inverse(X6_7) != identity ) ),
inference(splitRight,[status(thm)],[c_653926]) ).
tff(c_708928,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_708926]) ).
tff(c_708930,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_708928,c_647706]) ).
tff(c_708933,plain,
! [X1_2619] :
( ( inverse(X1_2619) != sk_c10 )
| ( multiply(X1_2619,sk_c10) != identity ) ),
inference(splitRight,[status(thm)],[c_708926]) ).
tff(c_709011,plain,
inverse(sk_c4) != sk_c10,
inference(superposition,[status(thm),theory(equality)],[c_647607,c_708933]) ).
tff(c_709043,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_579767,c_709011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GRP251-1 : TPTP v9.0.0. Released v2.5.0.
% 0.03/0.12 % 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.33 % Computer : n010.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 21:39:17 EDT 2025
% 0.12/0.33 % CPUTime :
% 116.62/99.31 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 116.74/99.39
% 116.74/99.39 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------