%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP082-1 : TPTP v9.0.0. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n007.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:24:57 PM UTC 2025
% Result : Unsatisfiable 204.19s 156.71s
% Output : CNFRefutation 204.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 3
% Syntax : Number of formulae : 271 ( 268 unt; 0 typ; 0 def)
% Number of atoms : 276 ( 273 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 18 ( 13 ~; 5 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 991 ( 991 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > double_divide > #nlpp > inverse > c3 > b3 > b2 > b1 > a3 > a2 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a1,type,
a1: $i ).
tff(a3,type,
a3: $i ).
tff(c3,type,
c3: $i ).
tff(b2,type,
b2: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(double_divide,type,
double_divide: ( $i * $i ) > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b1,type,
b1: $i ).
tff(b3,type,
b3: $i ).
tff(a2,type,
a2: $i ).
tff(f_28,axiom,
! [X,Y] : ( multiply(X,Y) = inverse(double_divide(Y,X)) ),
file(unknown,unknown) ).
tff(f_25,axiom,
! [X,Y,Z,U] : ( double_divide(inverse(X),inverse(double_divide(inverse(double_divide(X,double_divide(Y,Z))),double_divide(U,double_divide(Y,U))))) = Z ),
file(unknown,unknown) ).
tff(f_36,axiom,
( ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [Y_6,X_5] : ( inverse(double_divide(Y_6,X_5)) = multiply(X_5,Y_6) ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3,U_4] : ( double_divide(inverse(X_1),inverse(double_divide(inverse(double_divide(X_1,double_divide(Y_2,Z_3))),double_divide(U_4,double_divide(Y_2,U_4))))) = Z_3 ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_7,plain,
! [X_1,U_4,Y_2,Z_3] : ( double_divide(inverse(X_1),multiply(double_divide(U_4,double_divide(Y_2,U_4)),multiply(double_divide(Y_2,Z_3),X_1))) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4,c_2]) ).
tff(c_17,plain,
! [X_9,U_10,Y_11,Z_12] : ( double_divide(inverse(X_9),multiply(double_divide(U_10,double_divide(Y_11,U_10)),multiply(double_divide(Y_11,Z_12),X_9))) = Z_12 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4,c_2]) ).
tff(c_471263,plain,
! [U_2155,X_2156,Z_2154,U_2157,Y_2158,X_2153] : ( multiply(double_divide(U_2155,double_divide(Y_2158,U_2155)),multiply(double_divide(Y_2158,Z_2154),X_2156)) = double_divide(inverse(X_2153),multiply(double_divide(U_2157,double_divide(inverse(X_2156),U_2157)),multiply(Z_2154,X_2153))) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_17]) ).
tff(c_471530,plain,
! [U_2159,Y_2160,X_2161,Z_2162] : ( multiply(double_divide(U_2159,double_divide(Y_2160,U_2159)),multiply(double_divide(Y_2160,double_divide(inverse(X_2161),Z_2162)),X_2161)) = Z_2162 ),
inference(superposition,[status(thm),theory(equality)],[c_471263,c_7]) ).
tff(c_471645,plain,
! [U_2159,Y_6,Y_2160,X_5,Z_2162] : ( multiply(double_divide(U_2159,double_divide(Y_2160,U_2159)),multiply(double_divide(Y_2160,double_divide(multiply(X_5,Y_6),Z_2162)),double_divide(Y_6,X_5))) = Z_2162 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_471530]) ).
tff(c_471420,plain,
! [U_2155,Y_2158,X_2156,Z_3] : ( multiply(double_divide(U_2155,double_divide(Y_2158,U_2155)),multiply(double_divide(Y_2158,double_divide(inverse(X_2156),Z_3)),X_2156)) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_471263,c_7]) ).
tff(c_41,plain,
! [Y_6,Y_11,U_10,X_5,Z_12] : ( double_divide(multiply(X_5,Y_6),multiply(double_divide(U_10,double_divide(Y_11,U_10)),multiply(double_divide(Y_11,Z_12),double_divide(Y_6,X_5)))) = Z_12 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17]) ).
tff(c_471398,plain,
! [Z_2154,Y_6,U_2157,X_2153,X_5] : ( double_divide(multiply(X_5,Y_6),double_divide(inverse(X_2153),multiply(double_divide(U_2157,double_divide(inverse(double_divide(Y_6,X_5)),U_2157)),multiply(Z_2154,X_2153)))) = Z_2154 ),
inference(superposition,[status(thm),theory(equality)],[c_471263,c_41]) ).
tff(c_472175,plain,
! [Y_2177,X_2176,U_2179,Z_2178,X_2180] : ( double_divide(multiply(X_2180,Y_2177),double_divide(inverse(X_2176),multiply(double_divide(U_2179,double_divide(multiply(X_2180,Y_2177),U_2179)),multiply(Z_2178,X_2176)))) = Z_2178 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_471398]) ).
tff(c_472302,plain,
! [U_2155,X_2156,Z_3,X_2176,Y_2158,U_2179,Z_2178] : ( double_divide(Z_3,double_divide(inverse(X_2176),multiply(double_divide(U_2179,double_divide(multiply(double_divide(U_2155,double_divide(Y_2158,U_2155)),multiply(double_divide(Y_2158,double_divide(inverse(X_2156),Z_3)),X_2156)),U_2179)),multiply(Z_2178,X_2176)))) = Z_2178 ),
inference(superposition,[status(thm),theory(equality)],[c_471420,c_472175]) ).
tff(c_472433,plain,
! [Z_2181,X_2182,U_2183,Z_2184] : ( double_divide(Z_2181,double_divide(inverse(X_2182),multiply(double_divide(U_2183,double_divide(Z_2181,U_2183)),multiply(Z_2184,X_2182)))) = Z_2184 ),
inference(demodulation,[status(thm),theory(equality)],[c_471420,c_472302]) ).
tff(c_473189,plain,
! [X_2197,Z_2198,Z_2196,U_2199,U_2200] : ( multiply(double_divide(U_2200,double_divide(Z_2196,U_2200)),multiply(Z_2198,X_2197)) = multiply(double_divide(U_2199,double_divide(Z_2196,U_2199)),multiply(Z_2198,X_2197)) ),
inference(superposition,[status(thm),theory(equality)],[c_472433,c_471420]) ).
tff(c_473500,plain,
! [U_2159,Y_6,Y_2160,Z_2196,X_5,U_2199,Z_2162,U_2200] : ( multiply(double_divide(U_2200,double_divide(Z_2196,U_2200)),Z_2162) = multiply(double_divide(U_2199,double_divide(Z_2196,U_2199)),multiply(double_divide(U_2159,double_divide(Y_2160,U_2159)),multiply(double_divide(Y_2160,double_divide(multiply(X_5,Y_6),Z_2162)),double_divide(Y_6,X_5)))) ),
inference(superposition,[status(thm),theory(equality)],[c_471645,c_473189]) ).
tff(c_473672,plain,
! [U_2204,Z_2202,Z_2203,U_2201] : ( multiply(double_divide(U_2204,double_divide(Z_2202,U_2204)),Z_2203) = multiply(double_divide(U_2201,double_divide(Z_2202,U_2201)),Z_2203) ),
inference(demodulation,[status(thm),theory(equality)],[c_471645,c_473500]) ).
tff(c_473768,plain,
! [U_2155,U_2201,U_2204,Z_2203] : ( multiply(double_divide(U_2155,double_divide(U_2201,U_2155)),multiply(double_divide(U_2204,double_divide(inverse(Z_2203),U_2204)),Z_2203)) = U_2201 ),
inference(superposition,[status(thm),theory(equality)],[c_473672,c_471420]) ).
tff(c_474608,plain,
! [U_2211,U_2212,U_2213,Z_2214] : ( multiply(double_divide(U_2211,double_divide(U_2212,U_2211)),multiply(double_divide(U_2213,double_divide(inverse(Z_2214),U_2213)),Z_2214)) = U_2212 ),
inference(superposition,[status(thm),theory(equality)],[c_473672,c_471420]) ).
tff(c_472625,plain,
! [Z_2181,Z_2184,Y_6,U_2183,X_5] : ( double_divide(Z_2181,double_divide(multiply(X_5,Y_6),multiply(double_divide(U_2183,double_divide(Z_2181,U_2183)),multiply(Z_2184,double_divide(Y_6,X_5))))) = Z_2184 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_472433]) ).
tff(c_474642,plain,
! [U_2213,Y_6,X_5,U_2212] : ( double_divide(U_2213,double_divide(inverse(double_divide(Y_6,X_5)),U_2213)) = double_divide(U_2212,double_divide(multiply(X_5,Y_6),U_2212)) ),
inference(superposition,[status(thm),theory(equality)],[c_474608,c_472625]) ).
tff(c_476028,plain,
! [U_2227,X_2225,Y_2226,U_2224] : ( double_divide(U_2227,double_divide(multiply(X_2225,Y_2226),U_2227)) = double_divide(U_2224,double_divide(multiply(X_2225,Y_2226),U_2224)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_474642]) ).
tff(c_476595,plain,
! [U_2155,U_2201,U_2227,U_2204,Z_2203,U_2224] : ( double_divide(U_2227,double_divide(U_2201,U_2227)) = double_divide(U_2224,double_divide(multiply(double_divide(U_2155,double_divide(U_2201,U_2155)),multiply(double_divide(U_2204,double_divide(inverse(Z_2203),U_2204)),Z_2203)),U_2224)) ),
inference(superposition,[status(thm),theory(equality)],[c_473768,c_476028]) ).
tff(c_476799,plain,
! [U_2230,U_2229,U_2228] : ( double_divide(U_2230,double_divide(U_2229,U_2230)) = double_divide(U_2228,double_divide(U_2229,U_2228)) ),
inference(demodulation,[status(thm),theory(equality)],[c_473768,c_476595]) ).
tff(c_477442,plain,
! [U_2231,U_2232,U_2233] : ( multiply(double_divide(U_2231,U_2232),U_2232) = inverse(double_divide(U_2233,double_divide(U_2231,U_2233))) ),
inference(superposition,[status(thm),theory(equality)],[c_476799,c_4]) ).
tff(c_473650,plain,
! [U_2200,Z_2196,Z_2162,U_2199] : ( multiply(double_divide(U_2200,double_divide(Z_2196,U_2200)),Z_2162) = multiply(double_divide(U_2199,double_divide(Z_2196,U_2199)),Z_2162) ),
inference(demodulation,[status(thm),theory(equality)],[c_471645,c_473500]) ).
tff(c_477475,plain,
! [U_2199,Z_2196,U_2231,U_2233] : ( multiply(double_divide(U_2199,double_divide(Z_2196,U_2199)),double_divide(Z_2196,U_2231)) = inverse(double_divide(U_2233,double_divide(U_2231,U_2233))) ),
inference(superposition,[status(thm),theory(equality)],[c_477442,c_473650]) ).
tff(c_485456,plain,
! [U_2300,U_2301,U_2302,Z_2303] : ( multiply(double_divide(U_2300,double_divide(U_2301,U_2300)),inverse(multiply(double_divide(U_2302,double_divide(inverse(Z_2303),U_2302)),Z_2303))) = U_2301 ),
inference(superposition,[status(thm),theory(equality)],[c_473768,c_474608]) ).
tff(c_485495,plain,
! [U_2155,U_2201,U_2302,Z_2303] : ( multiply(double_divide(U_2155,double_divide(U_2201,U_2155)),inverse(inverse(multiply(double_divide(U_2302,double_divide(inverse(Z_2303),U_2302)),Z_2303)))) = U_2201 ),
inference(superposition,[status(thm),theory(equality)],[c_485456,c_473768]) ).
tff(c_471423,plain,
! [U_2155,X_2156,U_4,Z_2154,U_2157,Y_2158,X_2153] : ( double_divide(inverse(multiply(double_divide(Y_2158,Z_2154),X_2156)),multiply(double_divide(U_4,double_divide(U_2155,U_4)),double_divide(inverse(X_2153),multiply(double_divide(U_2157,double_divide(inverse(X_2156),U_2157)),multiply(Z_2154,X_2153))))) = double_divide(Y_2158,U_2155) ),
inference(superposition,[status(thm),theory(equality)],[c_471263,c_7]) ).
tff(c_35,plain,
! [U_4,Z_3,U_10,X_1,X_9,Y_2] : ( multiply(double_divide(U_4,double_divide(Y_2,U_4)),multiply(double_divide(Y_2,Z_3),X_1)) = double_divide(inverse(X_9),multiply(double_divide(U_10,double_divide(inverse(X_1),U_10)),multiply(Z_3,X_9))) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_17]) ).
tff(c_477592,plain,
! [U_2232,U_4,U_2231,U_2233] : ( double_divide(inverse(U_2232),multiply(double_divide(U_4,double_divide(U_2231,U_4)),inverse(double_divide(U_2233,double_divide(U_2231,U_2233))))) = U_2232 ),
inference(superposition,[status(thm),theory(equality)],[c_477442,c_7]) ).
tff(c_482244,plain,
! [U_2274,U_2275,U_2276,U_2277] : ( double_divide(inverse(U_2274),multiply(double_divide(U_2275,double_divide(U_2276,U_2275)),multiply(double_divide(U_2276,U_2277),U_2277))) = U_2274 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_477592]) ).
tff(c_512780,plain,
! [U_2428,X_2429,U_2430,X_2431] : ( double_divide(inverse(U_2428),double_divide(inverse(X_2429),multiply(double_divide(U_2430,double_divide(inverse(X_2431),U_2430)),multiply(X_2431,X_2429)))) = U_2428 ),
inference(superposition,[status(thm),theory(equality)],[c_35,c_482244]) ).
tff(c_513672,plain,
! [U_4,Z_3,U_10,X_1,U_2428,X_9,U_2430,Y_2] : ( double_divide(inverse(U_2428),double_divide(inverse(multiply(double_divide(Y_2,Z_3),X_1)),multiply(double_divide(U_2430,double_divide(inverse(double_divide(U_4,double_divide(Y_2,U_4))),U_2430)),double_divide(inverse(X_9),multiply(double_divide(U_10,double_divide(inverse(X_1),U_10)),multiply(Z_3,X_9)))))) = U_2428 ),
inference(superposition,[status(thm),theory(equality)],[c_35,c_512780]) ).
tff(c_513785,plain,
! [U_2432,Y_2433,U_2434] : ( double_divide(inverse(U_2432),double_divide(Y_2433,multiply(double_divide(Y_2433,U_2434),U_2434))) = U_2432 ),
inference(demodulation,[status(thm),theory(equality)],[c_471423,c_4,c_513672]) ).
tff(c_515448,plain,
! [X_2439,Y_2440,Y_2441,U_2442] : ( double_divide(multiply(X_2439,Y_2440),double_divide(Y_2441,multiply(double_divide(Y_2441,U_2442),U_2442))) = double_divide(Y_2440,X_2439) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_513785]) ).
tff(c_516240,plain,
! [Y_2441,U_2442,X_2439,Y_2440] : ( multiply(double_divide(Y_2441,multiply(double_divide(Y_2441,U_2442),U_2442)),multiply(X_2439,Y_2440)) = inverse(double_divide(Y_2440,X_2439)) ),
inference(superposition,[status(thm),theory(equality)],[c_515448,c_4]) ).
tff(c_516963,plain,
! [Y_2444,U_2445,X_2446,Y_2447] : ( multiply(double_divide(Y_2444,multiply(double_divide(Y_2444,U_2445),U_2445)),multiply(X_2446,Y_2447)) = multiply(X_2446,Y_2447) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_516240]) ).
tff(c_517235,plain,
! [U_2155,U_2201,U_2302,Y_2444,Z_2303,U_2445] : ( multiply(double_divide(Y_2444,multiply(double_divide(Y_2444,U_2445),U_2445)),U_2201) = multiply(double_divide(U_2155,double_divide(U_2201,U_2155)),inverse(inverse(multiply(double_divide(U_2302,double_divide(inverse(Z_2303),U_2302)),Z_2303)))) ),
inference(superposition,[status(thm),theory(equality)],[c_485495,c_516963]) ).
tff(c_517696,plain,
! [Y_2448,U_2449,U_2450] : ( multiply(double_divide(Y_2448,multiply(double_divide(Y_2448,U_2449),U_2449)),U_2450) = U_2450 ),
inference(demodulation,[status(thm),theory(equality)],[c_485495,c_517235]) ).
tff(c_533362,plain,
! [Y_2501,U_2502,U_2503,U_2504] : ( multiply(double_divide(Y_2501,U_2502),U_2502) = double_divide(inverse(U_2503),multiply(double_divide(U_2504,double_divide(Y_2501,U_2504)),U_2503)) ),
inference(superposition,[status(thm),theory(equality)],[c_517696,c_7]) ).
tff(c_534752,plain,
! [Z_2196,U_2502,U_2231,U_2233] : ( multiply(double_divide(Z_2196,U_2502),U_2502) = double_divide(inverse(double_divide(Z_2196,U_2231)),inverse(double_divide(U_2233,double_divide(U_2231,U_2233)))) ),
inference(superposition,[status(thm),theory(equality)],[c_477475,c_533362]) ).
tff(c_534999,plain,
! [Z_2505,U_2506,U_2507,U_2508] : ( multiply(double_divide(Z_2505,U_2506),U_2506) = double_divide(multiply(U_2507,Z_2505),multiply(double_divide(U_2507,U_2508),U_2508)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4,c_534752]) ).
tff(c_517655,plain,
! [Y_2444,U_2445,U_2201] : ( multiply(double_divide(Y_2444,multiply(double_divide(Y_2444,U_2445),U_2445)),U_2201) = U_2201 ),
inference(demodulation,[status(thm),theory(equality)],[c_485495,c_517235]) ).
tff(c_539173,plain,
! [Z_2517,U_2518,U_2519,U_2520] : ( multiply(double_divide(Z_2517,double_divide(multiply(U_2518,Z_2517),multiply(double_divide(U_2518,U_2519),U_2519))),U_2520) = U_2520 ),
inference(superposition,[status(thm),theory(equality)],[c_534999,c_517655]) ).
tff(c_474835,plain,
! [U_2211,U_2212,Y_6,U_2213,X_5] : ( multiply(double_divide(U_2211,double_divide(U_2212,U_2211)),multiply(double_divide(U_2213,double_divide(multiply(X_5,Y_6),U_2213)),double_divide(Y_6,X_5))) = U_2212 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_474608]) ).
tff(c_539536,plain,
! [U_2211,U_2212,U_2518,U_2519] : ( multiply(double_divide(U_2211,double_divide(U_2212,U_2211)),double_divide(multiply(double_divide(U_2518,U_2519),U_2519),U_2518)) = U_2212 ),
inference(superposition,[status(thm),theory(equality)],[c_539173,c_474835]) ).
tff(c_476777,plain,
! [U_2227,U_2201,U_2224] : ( double_divide(U_2227,double_divide(U_2201,U_2227)) = double_divide(U_2224,double_divide(U_2201,U_2224)) ),
inference(demodulation,[status(thm),theory(equality)],[c_473768,c_476595]) ).
tff(c_514086,plain,
! [Y_2433,U_2434,U_2432,U_2227] : ( double_divide(double_divide(Y_2433,multiply(double_divide(Y_2433,U_2434),U_2434)),U_2432) = double_divide(U_2227,double_divide(inverse(U_2432),U_2227)) ),
inference(superposition,[status(thm),theory(equality)],[c_513785,c_476777]) ).
tff(c_518206,plain,
! [U_2200,U_2199,Z_2196,U_2450] : ( multiply(double_divide(U_2200,multiply(double_divide(U_2199,double_divide(Z_2196,U_2199)),double_divide(Z_2196,U_2200))),U_2450) = U_2450 ),
inference(superposition,[status(thm),theory(equality)],[c_473650,c_517696]) ).
tff(c_539288,plain,
! [U_2200,U_2518,U_2519,U_2450] : ( multiply(double_divide(U_2200,double_divide(multiply(U_2518,multiply(double_divide(U_2518,U_2519),U_2519)),U_2200)),U_2450) = U_2450 ),
inference(superposition,[status(thm),theory(equality)],[c_539173,c_518206]) ).
tff(c_472412,plain,
! [Z_3,X_2176,U_2179,Z_2178] : ( double_divide(Z_3,double_divide(inverse(X_2176),multiply(double_divide(U_2179,double_divide(Z_3,U_2179)),multiply(Z_2178,X_2176)))) = Z_2178 ),
inference(demodulation,[status(thm),theory(equality)],[c_471420,c_472302]) ).
tff(c_543618,plain,
! [U_2532,U_2533,U_2534,U_2535] : ( multiply(double_divide(U_2532,double_divide(multiply(U_2533,multiply(double_divide(U_2533,U_2534),U_2534)),U_2532)),U_2535) = U_2535 ),
inference(superposition,[status(thm),theory(equality)],[c_539173,c_518206]) ).
tff(c_544838,plain,
! [U_2533,X_2176,U_2179,Z_2178,U_2535,U_2534] : ( multiply(double_divide(double_divide(inverse(X_2176),multiply(double_divide(U_2179,double_divide(multiply(U_2533,multiply(double_divide(U_2533,U_2534),U_2534)),U_2179)),multiply(Z_2178,X_2176))),Z_2178),U_2535) = U_2535 ),
inference(superposition,[status(thm),theory(equality)],[c_472412,c_543618]) ).
tff(c_547219,plain,
! [X_2544,Z_2545,U_2546] : ( multiply(double_divide(double_divide(inverse(X_2544),multiply(Z_2545,X_2544)),Z_2545),U_2546) = U_2546 ),
inference(demodulation,[status(thm),theory(equality)],[c_539288,c_544838]) ).
tff(c_547676,plain,
! [U_2227,U_2434,U_2546] : ( multiply(double_divide(U_2227,double_divide(inverse(double_divide(inverse(U_2434),U_2434)),U_2227)),U_2546) = U_2546 ),
inference(superposition,[status(thm),theory(equality)],[c_514086,c_547219]) ).
tff(c_549971,plain,
! [U_2554,U_2555,U_2556] : ( multiply(double_divide(U_2554,double_divide(multiply(U_2555,inverse(U_2555)),U_2554)),U_2556) = U_2556 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_547676]) ).
tff(c_551127,plain,
! [U_2557,U_2558,U_2559] : ( multiply(U_2557,inverse(U_2557)) = double_divide(multiply(double_divide(U_2558,U_2559),U_2559),U_2558) ),
inference(superposition,[status(thm),theory(equality)],[c_549971,c_539536]) ).
tff(c_551952,plain,
! [U_2558,U_4,Z_3,U_2559,Y_2] : ( double_divide(inverse(inverse(double_divide(Y_2,Z_3))),multiply(double_divide(U_4,double_divide(Y_2,U_4)),double_divide(multiply(double_divide(U_2558,U_2559),U_2559),U_2558))) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_551127,c_7]) ).
tff(c_552457,plain,
! [Z_3,Y_2] : ( double_divide(inverse(multiply(Z_3,Y_2)),Y_2) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_539536,c_4,c_551952]) ).
tff(c_513784,plain,
! [U_2428,Y_2,U_4] : ( double_divide(inverse(U_2428),double_divide(Y_2,multiply(double_divide(Y_2,U_4),U_4))) = U_2428 ),
inference(demodulation,[status(thm),theory(equality)],[c_471423,c_4,c_513672]) ).
tff(c_523175,plain,
! [Y_2472,U_2473,U_2474,U_2475] : ( double_divide(double_divide(Y_2472,multiply(double_divide(Y_2472,U_2473),U_2473)),U_2474) = double_divide(U_2475,double_divide(inverse(U_2474),U_2475)) ),
inference(superposition,[status(thm),theory(equality)],[c_513785,c_476777]) ).
tff(c_524820,plain,
! [U_2474,Y_2472,U_2473,U_2475] : ( multiply(U_2474,double_divide(Y_2472,multiply(double_divide(Y_2472,U_2473),U_2473))) = inverse(double_divide(U_2475,double_divide(inverse(U_2474),U_2475))) ),
inference(superposition,[status(thm),theory(equality)],[c_523175,c_4]) ).
tff(c_552478,plain,
! [Z_2560,Y_2561] : ( double_divide(inverse(multiply(Z_2560,Y_2561)),Y_2561) = Z_2560 ),
inference(demodulation,[status(thm),theory(equality)],[c_539536,c_4,c_551952]) ).
tff(c_553131,plain,
! [U_2475,U_2474,Y_2472,U_2473] : ( double_divide(inverse(inverse(double_divide(U_2475,double_divide(inverse(U_2474),U_2475)))),double_divide(Y_2472,multiply(double_divide(Y_2472,U_2473),U_2473))) = U_2474 ),
inference(superposition,[status(thm),theory(equality)],[c_524820,c_552478]) ).
tff(c_553369,plain,
! [U_2474,U_2475] : ( multiply(double_divide(inverse(U_2474),U_2475),U_2475) = U_2474 ),
inference(demodulation,[status(thm),theory(equality)],[c_513784,c_4,c_553131]) ).
tff(c_551832,plain,
! [U_2558,Z_3,U_2559,U_2179,U_2557] : ( double_divide(Z_3,double_divide(inverse(inverse(U_2557)),multiply(double_divide(U_2179,double_divide(Z_3,U_2179)),double_divide(multiply(double_divide(U_2558,U_2559),U_2559),U_2558)))) = U_2557 ),
inference(superposition,[status(thm),theory(equality)],[c_551127,c_472412]) ).
tff(c_559326,plain,
! [Z_2578,U_2579] : ( double_divide(Z_2578,double_divide(inverse(inverse(U_2579)),Z_2578)) = U_2579 ),
inference(demodulation,[status(thm),theory(equality)],[c_539536,c_551832]) ).
tff(c_517984,plain,
! [Y_2448,U_2449,U_2450,U_4] : ( multiply(double_divide(Y_2448,U_2449),U_2449) = double_divide(inverse(U_2450),multiply(double_divide(U_4,double_divide(Y_2448,U_4)),U_2450)) ),
inference(superposition,[status(thm),theory(equality)],[c_517696,c_7]) ).
tff(c_559460,plain,
! [U_2579,U_2449,U_2450] : ( multiply(double_divide(inverse(inverse(U_2579)),U_2449),U_2449) = double_divide(inverse(U_2450),multiply(U_2579,U_2450)) ),
inference(superposition,[status(thm),theory(equality)],[c_559326,c_517984]) ).
tff(c_560616,plain,
! [U_2580,U_2581] : ( double_divide(inverse(U_2580),multiply(U_2581,U_2580)) = inverse(U_2581) ),
inference(demodulation,[status(thm),theory(equality)],[c_553369,c_559460]) ).
tff(c_561578,plain,
! [U_2582,U_2583] : ( multiply(inverse(U_2582),multiply(U_2582,U_2583)) = U_2583 ),
inference(superposition,[status(thm),theory(equality)],[c_560616,c_553369]) ).
tff(c_560552,plain,
! [U_2450,U_2579] : ( double_divide(inverse(U_2450),multiply(U_2579,U_2450)) = inverse(U_2579) ),
inference(demodulation,[status(thm),theory(equality)],[c_553369,c_559460]) ).
tff(c_561587,plain,
! [U_2582,U_2583] : ( double_divide(inverse(multiply(U_2582,U_2583)),U_2583) = inverse(inverse(U_2582)) ),
inference(superposition,[status(thm),theory(equality)],[c_561578,c_560552]) ).
tff(c_562033,plain,
! [U_2582] : ( inverse(inverse(U_2582)) = U_2582 ),
inference(demodulation,[status(thm),theory(equality)],[c_552457,c_561587]) ).
tff(c_552449,plain,
! [Z_3,U_2557] : ( double_divide(Z_3,double_divide(inverse(inverse(U_2557)),Z_3)) = U_2557 ),
inference(demodulation,[status(thm),theory(equality)],[c_539536,c_551832]) ).
tff(c_562109,plain,
! [Z_3,U_2557] : ( double_divide(Z_3,double_divide(U_2557,Z_3)) = U_2557 ),
inference(demodulation,[status(thm),theory(equality)],[c_562033,c_552449]) ).
tff(c_477312,plain,
! [U_2229,U_2228,U_2230] : ( multiply(double_divide(U_2229,U_2228),U_2228) = inverse(double_divide(U_2230,double_divide(U_2229,U_2230))) ),
inference(superposition,[status(thm),theory(equality)],[c_476799,c_4]) ).
tff(c_562965,plain,
! [U_2229,U_2228] : ( multiply(double_divide(U_2229,U_2228),U_2228) = inverse(U_2229) ),
inference(demodulation,[status(thm),theory(equality)],[c_562109,c_477312]) ).
tff(c_564556,plain,
! [Y_2610,U_2611] : ( multiply(double_divide(Y_2610,inverse(Y_2610)),U_2611) = U_2611 ),
inference(demodulation,[status(thm),theory(equality)],[c_562965,c_517655]) ).
tff(c_560626,plain,
! [U_2581,U_2580] : ( multiply(inverse(U_2581),multiply(U_2581,U_2580)) = U_2580 ),
inference(superposition,[status(thm),theory(equality)],[c_560616,c_553369]) ).
tff(c_564602,plain,
! [Y_2610,U_2611] : ( multiply(inverse(double_divide(Y_2610,inverse(Y_2610))),U_2611) = U_2611 ),
inference(superposition,[status(thm),theory(equality)],[c_564556,c_560626]) ).
tff(c_564666,plain,
! [Y_2610,U_2611] : ( multiply(multiply(inverse(Y_2610),Y_2610),U_2611) = U_2611 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_564602]) ).
tff(c_136220,plain,
! [U_854,Z_853,X_855,Y_857,U_856,X_852] : ( multiply(double_divide(U_854,double_divide(Y_857,U_854)),multiply(double_divide(Y_857,Z_853),X_855)) = double_divide(inverse(X_852),multiply(double_divide(U_856,double_divide(inverse(X_855),U_856)),multiply(Z_853,X_852))) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_17]) ).
tff(c_136430,plain,
! [U_858,Y_859,X_860,Z_861] : ( multiply(double_divide(U_858,double_divide(Y_859,U_858)),multiply(double_divide(Y_859,double_divide(inverse(X_860),Z_861)),X_860)) = Z_861 ),
inference(superposition,[status(thm),theory(equality)],[c_136220,c_7]) ).
tff(c_136524,plain,
! [Y_6,X_5,Y_859,U_858,Z_861] : ( multiply(double_divide(U_858,double_divide(Y_859,U_858)),multiply(double_divide(Y_859,double_divide(multiply(X_5,Y_6),Z_861)),double_divide(Y_6,X_5))) = Z_861 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_136430]) ).
tff(c_136338,plain,
! [U_854,Y_857,X_855,Z_3] : ( multiply(double_divide(U_854,double_divide(Y_857,U_854)),multiply(double_divide(Y_857,double_divide(inverse(X_855),Z_3)),X_855)) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_136220,c_7]) ).
tff(c_136316,plain,
! [Z_853,Y_6,U_856,X_5,X_852] : ( double_divide(multiply(X_5,Y_6),double_divide(inverse(X_852),multiply(double_divide(U_856,double_divide(inverse(double_divide(Y_6,X_5)),U_856)),multiply(Z_853,X_852)))) = Z_853 ),
inference(superposition,[status(thm),theory(equality)],[c_136220,c_41]) ).
tff(c_137156,plain,
! [X_884,X_880,Z_881,U_883,Y_882] : ( double_divide(multiply(X_884,Y_882),double_divide(inverse(X_880),multiply(double_divide(U_883,double_divide(multiply(X_884,Y_882),U_883)),multiply(Z_881,X_880)))) = Z_881 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_136316]) ).
tff(c_137268,plain,
! [X_880,U_854,Z_881,U_883,Z_3,X_855,Y_857] : ( double_divide(Z_3,double_divide(inverse(X_880),multiply(double_divide(U_883,double_divide(multiply(double_divide(U_854,double_divide(Y_857,U_854)),multiply(double_divide(Y_857,double_divide(inverse(X_855),Z_3)),X_855)),U_883)),multiply(Z_881,X_880)))) = Z_881 ),
inference(superposition,[status(thm),theory(equality)],[c_136338,c_137156]) ).
tff(c_137363,plain,
! [Z_885,X_886,U_887,Z_888] : ( double_divide(Z_885,double_divide(inverse(X_886),multiply(double_divide(U_887,double_divide(Z_885,U_887)),multiply(Z_888,X_886)))) = Z_888 ),
inference(demodulation,[status(thm),theory(equality)],[c_136338,c_137268]) ).
tff(c_138116,plain,
! [Z_906,U_902,Z_905,X_903,U_904] : ( multiply(double_divide(U_904,double_divide(Z_905,U_904)),multiply(Z_906,X_903)) = multiply(double_divide(U_902,double_divide(Z_905,U_902)),multiply(Z_906,X_903)) ),
inference(superposition,[status(thm),theory(equality)],[c_137363,c_136338]) ).
tff(c_138403,plain,
! [U_902,Z_905,Y_6,U_904,X_5,Y_859,U_858,Z_861] : ( multiply(double_divide(U_904,double_divide(Z_905,U_904)),Z_861) = multiply(double_divide(U_902,double_divide(Z_905,U_902)),multiply(double_divide(U_858,double_divide(Y_859,U_858)),multiply(double_divide(Y_859,double_divide(multiply(X_5,Y_6),Z_861)),double_divide(Y_6,X_5)))) ),
inference(superposition,[status(thm),theory(equality)],[c_136524,c_138116]) ).
tff(c_138541,plain,
! [U_910,Z_908,Z_909,U_907] : ( multiply(double_divide(U_910,double_divide(Z_908,U_910)),Z_909) = multiply(double_divide(U_907,double_divide(Z_908,U_907)),Z_909) ),
inference(demodulation,[status(thm),theory(equality)],[c_136524,c_138403]) ).
tff(c_138645,plain,
! [U_854,U_907,U_910,Z_909] : ( multiply(double_divide(U_854,double_divide(U_907,U_854)),multiply(double_divide(U_910,double_divide(inverse(Z_909),U_910)),Z_909)) = U_907 ),
inference(superposition,[status(thm),theory(equality)],[c_138541,c_136338]) ).
tff(c_139367,plain,
! [U_917,U_918,U_919,Z_920] : ( multiply(double_divide(U_917,double_divide(U_918,U_917)),multiply(double_divide(U_919,double_divide(inverse(Z_920),U_919)),Z_920)) = U_918 ),
inference(superposition,[status(thm),theory(equality)],[c_138541,c_136338]) ).
tff(c_137531,plain,
! [Z_885,Y_6,X_5,U_887,Z_888] : ( double_divide(Z_885,double_divide(multiply(X_5,Y_6),multiply(double_divide(U_887,double_divide(Z_885,U_887)),multiply(Z_888,double_divide(Y_6,X_5))))) = Z_888 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_137363]) ).
tff(c_139401,plain,
! [U_919,Y_6,X_5,U_918] : ( double_divide(U_919,double_divide(inverse(double_divide(Y_6,X_5)),U_919)) = double_divide(U_918,double_divide(multiply(X_5,Y_6),U_918)) ),
inference(superposition,[status(thm),theory(equality)],[c_139367,c_137531]) ).
tff(c_140649,plain,
! [U_933,X_931,Y_932,U_930] : ( double_divide(U_933,double_divide(multiply(X_931,Y_932),U_933)) = double_divide(U_930,double_divide(multiply(X_931,Y_932),U_930)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_139401]) ).
tff(c_141166,plain,
! [U_910,U_854,U_933,Z_909,U_930,U_907] : ( double_divide(U_933,double_divide(U_907,U_933)) = double_divide(U_930,double_divide(multiply(double_divide(U_854,double_divide(U_907,U_854)),multiply(double_divide(U_910,double_divide(inverse(Z_909),U_910)),Z_909)),U_930)) ),
inference(superposition,[status(thm),theory(equality)],[c_138645,c_140649]) ).
tff(c_141340,plain,
! [U_936,U_935,U_934] : ( double_divide(U_936,double_divide(U_935,U_936)) = double_divide(U_934,double_divide(U_935,U_934)) ),
inference(demodulation,[status(thm),theory(equality)],[c_138645,c_141166]) ).
tff(c_141919,plain,
! [U_937,U_938,U_939] : ( multiply(double_divide(U_937,U_938),U_938) = inverse(double_divide(U_939,double_divide(U_937,U_939))) ),
inference(superposition,[status(thm),theory(equality)],[c_141340,c_4]) ).
tff(c_141803,plain,
! [U_935,U_934,U_936] : ( multiply(double_divide(U_935,U_934),U_934) = inverse(double_divide(U_936,double_divide(U_935,U_936))) ),
inference(superposition,[status(thm),theory(equality)],[c_141340,c_4]) ).
tff(c_142160,plain,
! [U_940,U_942,U_941] : ( multiply(double_divide(U_940,U_942),U_942) = multiply(double_divide(U_940,U_941),U_941) ),
inference(superposition,[status(thm),theory(equality)],[c_141919,c_141803]) ).
tff(c_138525,plain,
! [U_904,Z_905,Z_861,U_902] : ( multiply(double_divide(U_904,double_divide(Z_905,U_904)),Z_861) = multiply(double_divide(U_902,double_divide(Z_905,U_902)),Z_861) ),
inference(demodulation,[status(thm),theory(equality)],[c_136524,c_138403]) ).
tff(c_142194,plain,
! [U_940,U_942,U_902,Z_905] : ( multiply(double_divide(U_940,U_942),U_942) = multiply(double_divide(U_902,double_divide(Z_905,U_902)),double_divide(Z_905,U_940)) ),
inference(superposition,[status(thm),theory(equality)],[c_142160,c_138525]) ).
tff(c_136341,plain,
! [U_854,Z_853,U_4,X_855,Y_857,U_856,X_852] : ( double_divide(inverse(multiply(double_divide(Y_857,Z_853),X_855)),multiply(double_divide(U_4,double_divide(U_854,U_4)),double_divide(inverse(X_852),multiply(double_divide(U_856,double_divide(inverse(X_855),U_856)),multiply(Z_853,X_852))))) = double_divide(Y_857,U_854) ),
inference(superposition,[status(thm),theory(equality)],[c_136220,c_7]) ).
tff(c_142044,plain,
! [U_938,U_4,U_937,U_939] : ( double_divide(inverse(U_938),multiply(double_divide(U_4,double_divide(U_937,U_4)),inverse(double_divide(U_939,double_divide(U_937,U_939))))) = U_938 ),
inference(superposition,[status(thm),theory(equality)],[c_141919,c_7]) ).
tff(c_145769,plain,
! [U_978,U_979,U_980,U_981] : ( double_divide(inverse(U_978),multiply(double_divide(U_979,double_divide(U_980,U_979)),multiply(double_divide(U_980,U_981),U_981))) = U_978 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_142044]) ).
tff(c_170280,plain,
! [U_1120,X_1121,U_1122,X_1123] : ( double_divide(inverse(U_1120),double_divide(inverse(X_1121),multiply(double_divide(U_1122,double_divide(inverse(X_1123),U_1122)),multiply(X_1123,X_1121)))) = U_1120 ),
inference(superposition,[status(thm),theory(equality)],[c_35,c_145769]) ).
tff(c_171108,plain,
! [U_1120,U_4,Z_3,U_10,X_1,U_1122,X_9,Y_2] : ( double_divide(inverse(U_1120),double_divide(inverse(multiply(double_divide(Y_2,Z_3),X_1)),multiply(double_divide(U_1122,double_divide(inverse(double_divide(U_4,double_divide(Y_2,U_4))),U_1122)),double_divide(inverse(X_9),multiply(double_divide(U_10,double_divide(inverse(X_1),U_10)),multiply(Z_3,X_9)))))) = U_1120 ),
inference(superposition,[status(thm),theory(equality)],[c_35,c_170280]) ).
tff(c_171212,plain,
! [U_1124,Y_1125,U_1126] : ( double_divide(inverse(U_1124),double_divide(Y_1125,multiply(double_divide(Y_1125,U_1126),U_1126))) = U_1124 ),
inference(demodulation,[status(thm),theory(equality)],[c_136341,c_4,c_171108]) ).
tff(c_171764,plain,
! [U_1124,U_940,U_902,Z_905] : ( double_divide(inverse(U_1124),double_divide(U_940,multiply(double_divide(U_902,double_divide(Z_905,U_902)),double_divide(Z_905,U_940)))) = U_1124 ),
inference(superposition,[status(thm),theory(equality)],[c_142194,c_171212]) ).
tff(c_141322,plain,
! [U_933,U_907,U_930] : ( double_divide(U_933,double_divide(U_907,U_933)) = double_divide(U_930,double_divide(U_907,U_930)) ),
inference(demodulation,[status(thm),theory(equality)],[c_138645,c_141166]) ).
tff(c_171495,plain,
! [Y_1125,U_1126,U_1124,U_933] : ( double_divide(double_divide(Y_1125,multiply(double_divide(Y_1125,U_1126),U_1126)),U_1124) = double_divide(U_933,double_divide(inverse(U_1124),U_933)) ),
inference(superposition,[status(thm),theory(equality)],[c_171212,c_141322]) ).
tff(c_143330,plain,
! [U_958,U_959,U_960,U_961] : ( double_divide(double_divide(U_958,U_959),double_divide(U_960,double_divide(U_958,U_960))) = double_divide(U_961,double_divide(U_959,U_961)) ),
inference(superposition,[status(thm),theory(equality)],[c_141340,c_141322]) ).
tff(c_143908,plain,
! [U_960,U_958,U_959,U_961] : ( multiply(double_divide(U_960,double_divide(U_958,U_960)),double_divide(U_958,U_959)) = inverse(double_divide(U_961,double_divide(U_959,U_961))) ),
inference(superposition,[status(thm),theory(equality)],[c_143330,c_4]) ).
tff(c_148651,plain,
! [U_1003,U_1004,U_1005,Z_1006] : ( multiply(double_divide(U_1003,double_divide(U_1004,U_1003)),inverse(multiply(double_divide(U_1005,double_divide(inverse(Z_1006),U_1005)),Z_1006))) = U_1004 ),
inference(superposition,[status(thm),theory(equality)],[c_138645,c_139367]) ).
tff(c_166296,plain,
! [U_1095,U_1096,U_1097,Z_1098] : ( multiply(double_divide(U_1095,double_divide(U_1096,U_1095)),inverse(inverse(multiply(double_divide(U_1097,double_divide(inverse(Z_1098),U_1097)),Z_1098)))) = U_1096 ),
inference(superposition,[status(thm),theory(equality)],[c_148651,c_136338]) ).
tff(c_166746,plain,
! [U_1097,Y_6,U_1096,X_5,U_1095] : ( multiply(double_divide(U_1095,double_divide(U_1096,U_1095)),inverse(inverse(multiply(double_divide(U_1097,double_divide(multiply(X_5,Y_6),U_1097)),double_divide(Y_6,X_5))))) = U_1096 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_166296]) ).
tff(c_174673,plain,
! [X_1139,Y_1140,Y_1141,U_1142] : ( double_divide(multiply(X_1139,Y_1140),double_divide(Y_1141,multiply(double_divide(Y_1141,U_1142),U_1142))) = double_divide(Y_1140,X_1139) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_171212]) ).
tff(c_175408,plain,
! [Y_1141,U_1142,X_1139,Y_1140] : ( multiply(double_divide(Y_1141,multiply(double_divide(Y_1141,U_1142),U_1142)),multiply(X_1139,Y_1140)) = inverse(double_divide(Y_1140,X_1139)) ),
inference(superposition,[status(thm),theory(equality)],[c_174673,c_4]) ).
tff(c_176081,plain,
! [Y_1144,U_1145,X_1146,Y_1147] : ( multiply(double_divide(Y_1144,multiply(double_divide(Y_1144,U_1145),U_1145)),multiply(X_1146,Y_1147)) = multiply(X_1146,Y_1147) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_175408]) ).
tff(c_176342,plain,
! [Y_1144,U_1097,Y_6,U_1145,U_1096,X_5,U_1095] : ( multiply(double_divide(Y_1144,multiply(double_divide(Y_1144,U_1145),U_1145)),U_1096) = multiply(double_divide(U_1095,double_divide(U_1096,U_1095)),inverse(inverse(multiply(double_divide(U_1097,double_divide(multiply(X_5,Y_6),U_1097)),double_divide(Y_6,X_5))))) ),
inference(superposition,[status(thm),theory(equality)],[c_166746,c_176081]) ).
tff(c_176768,plain,
! [Y_1148,U_1149,U_1150] : ( multiply(double_divide(Y_1148,multiply(double_divide(Y_1148,U_1149),U_1149)),U_1150) = U_1150 ),
inference(demodulation,[status(thm),theory(equality)],[c_166746,c_176342]) ).
tff(c_188389,plain,
! [Y_1191,U_1192,U_1193,U_1194] : ( multiply(double_divide(Y_1191,U_1192),U_1192) = double_divide(inverse(U_1193),multiply(double_divide(U_1194,double_divide(Y_1191,U_1194)),U_1193)) ),
inference(superposition,[status(thm),theory(equality)],[c_176768,c_7]) ).
tff(c_189662,plain,
! [U_958,U_1192,U_959,U_961] : ( multiply(double_divide(U_958,U_1192),U_1192) = double_divide(inverse(double_divide(U_958,U_959)),inverse(double_divide(U_961,double_divide(U_959,U_961)))) ),
inference(superposition,[status(thm),theory(equality)],[c_143908,c_188389]) ).
tff(c_189869,plain,
! [U_1195,U_1196,U_1197,U_1198] : ( multiply(double_divide(U_1195,U_1196),U_1196) = double_divide(multiply(U_1197,U_1195),multiply(double_divide(U_1197,U_1198),U_1198)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4,c_189662]) ).
tff(c_176728,plain,
! [Y_1144,U_1145,U_1096] : ( multiply(double_divide(Y_1144,multiply(double_divide(Y_1144,U_1145),U_1145)),U_1096) = U_1096 ),
inference(demodulation,[status(thm),theory(equality)],[c_166746,c_176342]) ).
tff(c_193153,plain,
! [U_1206,U_1207,U_1208,U_1209] : ( multiply(double_divide(U_1206,double_divide(multiply(U_1207,U_1206),multiply(double_divide(U_1207,U_1208),U_1208))),U_1209) = U_1209 ),
inference(superposition,[status(thm),theory(equality)],[c_189869,c_176728]) ).
tff(c_143905,plain,
! [U_959,U_961,U_958,U_960] : ( multiply(double_divide(U_959,U_961),U_961) = inverse(double_divide(double_divide(U_958,U_959),double_divide(U_960,double_divide(U_958,U_960)))) ),
inference(superposition,[status(thm),theory(equality)],[c_143330,c_4]) ).
tff(c_177170,plain,
! [U_959,U_958,U_960,U_1150] : ( multiply(double_divide(U_959,inverse(double_divide(double_divide(U_958,U_959),double_divide(U_960,double_divide(U_958,U_960))))),U_1150) = U_1150 ),
inference(superposition,[status(thm),theory(equality)],[c_143905,c_176768]) ).
tff(c_177271,plain,
! [U_959,U_960,U_958,U_1150] : ( multiply(double_divide(U_959,multiply(double_divide(U_960,double_divide(U_958,U_960)),double_divide(U_958,U_959))),U_1150) = U_1150 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_177170]) ).
tff(c_193243,plain,
! [U_959,U_1207,U_1208,U_1150] : ( multiply(double_divide(U_959,double_divide(multiply(U_1207,multiply(double_divide(U_1207,U_1208),U_1208)),U_959)),U_1150) = U_1150 ),
inference(superposition,[status(thm),theory(equality)],[c_193153,c_177271]) ).
tff(c_137348,plain,
! [Z_3,X_880,U_883,Z_881] : ( double_divide(Z_3,double_divide(inverse(X_880),multiply(double_divide(U_883,double_divide(Z_3,U_883)),multiply(Z_881,X_880)))) = Z_881 ),
inference(demodulation,[status(thm),theory(equality)],[c_136338,c_137268]) ).
tff(c_194362,plain,
! [U_1210,U_1211,U_1212,U_1213] : ( multiply(double_divide(U_1210,double_divide(multiply(U_1211,multiply(double_divide(U_1211,U_1212),U_1212)),U_1210)),U_1213) = U_1213 ),
inference(superposition,[status(thm),theory(equality)],[c_193153,c_177271]) ).
tff(c_195444,plain,
! [X_880,Z_881,U_883,U_1211,U_1212,U_1213] : ( multiply(double_divide(double_divide(inverse(X_880),multiply(double_divide(U_883,double_divide(multiply(U_1211,multiply(double_divide(U_1211,U_1212),U_1212)),U_883)),multiply(Z_881,X_880))),Z_881),U_1213) = U_1213 ),
inference(superposition,[status(thm),theory(equality)],[c_137348,c_194362]) ).
tff(c_196999,plain,
! [X_1218,Z_1219,U_1220] : ( multiply(double_divide(double_divide(inverse(X_1218),multiply(Z_1219,X_1218)),Z_1219),U_1220) = U_1220 ),
inference(demodulation,[status(thm),theory(equality)],[c_193243,c_195444]) ).
tff(c_197405,plain,
! [U_933,U_1126,U_1220] : ( multiply(double_divide(U_933,double_divide(inverse(double_divide(inverse(U_1126),U_1126)),U_933)),U_1220) = U_1220 ),
inference(superposition,[status(thm),theory(equality)],[c_171495,c_196999]) ).
tff(c_198525,plain,
! [U_1224,U_1225,U_1226] : ( multiply(double_divide(U_1224,double_divide(multiply(U_1225,inverse(U_1225)),U_1224)),U_1226) = U_1226 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_197405]) ).
tff(c_205369,plain,
! [U_1241,U_1242,U_1243] : ( multiply(double_divide(U_1241,double_divide(U_1242,U_1241)),double_divide(inverse(U_1243),U_1243)) = U_1242 ),
inference(superposition,[status(thm),theory(equality)],[c_198525,c_136524]) ).
tff(c_205730,plain,
! [U_1243,U_942] : ( multiply(double_divide(U_1243,U_942),U_942) = inverse(U_1243) ),
inference(superposition,[status(thm),theory(equality)],[c_205369,c_142194]) ).
tff(c_210095,plain,
! [U_1264,U_1265] : ( inverse(double_divide(U_1264,double_divide(U_1265,U_1264))) = inverse(U_1265) ),
inference(demodulation,[status(thm),theory(equality)],[c_205730,c_141803]) ).
tff(c_210131,plain,
! [U_902,Z_905,U_1265,U_1264,U_940] : ( double_divide(inverse(U_1265),double_divide(U_940,multiply(double_divide(U_902,double_divide(Z_905,U_902)),double_divide(Z_905,U_940)))) = double_divide(U_1264,double_divide(U_1265,U_1264)) ),
inference(superposition,[status(thm),theory(equality)],[c_210095,c_171764]) ).
tff(c_210403,plain,
! [U_1264,U_1265] : ( double_divide(U_1264,double_divide(U_1265,U_1264)) = U_1265 ),
inference(demodulation,[status(thm),theory(equality)],[c_171764,c_210131]) ).
tff(c_141343,plain,
! [U_935,U_934,U_936,U_930] : ( double_divide(double_divide(U_935,U_934),double_divide(U_936,double_divide(U_935,U_936))) = double_divide(U_930,double_divide(U_934,U_930)) ),
inference(superposition,[status(thm),theory(equality)],[c_141340,c_141322]) ).
tff(c_210458,plain,
! [U_935,U_934] : ( double_divide(double_divide(U_935,U_934),U_935) = U_934 ),
inference(demodulation,[status(thm),theory(equality)],[c_210403,c_210403,c_141343]) ).
tff(c_199063,plain,
! [U_858,U_1224,U_1225] : ( multiply(double_divide(U_858,double_divide(U_1224,U_858)),double_divide(inverse(U_1225),U_1225)) = U_1224 ),
inference(superposition,[status(thm),theory(equality)],[c_198525,c_136524]) ).
tff(c_210650,plain,
! [U_1275,U_1276] : ( multiply(U_1275,double_divide(inverse(U_1276),U_1276)) = U_1275 ),
inference(demodulation,[status(thm),theory(equality)],[c_210403,c_199063]) ).
tff(c_210725,plain,
! [U_1275,X_5,Y_6] : ( multiply(U_1275,double_divide(multiply(X_5,Y_6),double_divide(Y_6,X_5))) = U_1275 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_210650]) ).
tff(c_197685,plain,
! [U_933,U_1126,U_1220] : ( multiply(double_divide(U_933,double_divide(multiply(U_1126,inverse(U_1126)),U_933)),U_1220) = U_1220 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_197405]) ).
tff(c_213748,plain,
! [U_1324,U_1325] : ( multiply(U_1324,inverse(U_1324)) = double_divide(inverse(U_1325),U_1325) ),
inference(superposition,[status(thm),theory(equality)],[c_197685,c_205369]) ).
tff(c_287625,plain,
! [U_1673,X_1674,Y_1675] : ( multiply(U_1673,inverse(U_1673)) = double_divide(multiply(X_1674,Y_1675),double_divide(Y_1675,X_1674)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_213748]) ).
tff(c_136229,plain,
! [U_854,Z_853,U_4,Z_3,X_855,Y_857,U_856,X_852,X_9,Y_2] : ( multiply(double_divide(U_4,double_divide(Y_2,U_4)),multiply(double_divide(Y_2,Z_3),X_852)) = double_divide(inverse(X_9),multiply(double_divide(multiply(double_divide(U_856,double_divide(inverse(X_855),U_856)),multiply(Z_853,X_852)),multiply(double_divide(U_854,double_divide(Y_857,U_854)),multiply(double_divide(Y_857,Z_853),X_855))),multiply(Z_3,X_9))) ),
inference(superposition,[status(thm),theory(equality)],[c_136220,c_35]) ).
tff(c_259992,plain,
! [Z_853,Z_3,X_855,Y_857,X_852,X_9,Y_2] : ( multiply(Y_2,multiply(double_divide(Y_2,Z_3),X_852)) = double_divide(inverse(X_9),multiply(double_divide(multiply(inverse(X_855),multiply(Z_853,X_852)),multiply(Y_857,multiply(double_divide(Y_857,Z_853),X_855))),multiply(Z_3,X_9))) ),
inference(demodulation,[status(thm),theory(equality)],[c_210403,c_210403,c_210403,c_136229]) ).
tff(c_136356,plain,
! [U_854,Z_853,U_4,Z_3,Y_857,U_10,X_1,X_852,X_9,Y_2] : ( multiply(double_divide(U_854,double_divide(Y_857,U_854)),multiply(double_divide(Y_857,Z_853),X_9)) = double_divide(inverse(X_852),multiply(double_divide(multiply(double_divide(U_10,double_divide(inverse(X_1),U_10)),multiply(Z_3,X_9)),multiply(double_divide(U_4,double_divide(Y_2,U_4)),multiply(double_divide(Y_2,Z_3),X_1))),multiply(Z_853,X_852))) ),
inference(superposition,[status(thm),theory(equality)],[c_35,c_136220]) ).
tff(c_270642,plain,
! [Y_857,Z_853,X_9,Y_2] : ( multiply(Y_857,multiply(double_divide(Y_857,Z_853),X_9)) = multiply(Y_2,multiply(double_divide(Y_2,Z_853),X_9)) ),
inference(demodulation,[status(thm),theory(equality)],[c_259992,c_210403,c_210403,c_210403,c_136356]) ).
tff(c_287765,plain,
! [Z_853,Y_857,X_1674,Y_2,Y_1675] : ( multiply(Y_857,multiply(double_divide(Y_857,Z_853),inverse(double_divide(Y_2,Z_853)))) = multiply(Y_2,double_divide(multiply(X_1674,Y_1675),double_divide(Y_1675,X_1674))) ),
inference(superposition,[status(thm),theory(equality)],[c_287625,c_270642]) ).
tff(c_419352,plain,
! [Y_2029,Z_2030,Y_2031] : ( multiply(Y_2029,multiply(double_divide(Y_2029,Z_2030),multiply(Z_2030,Y_2031))) = Y_2031 ),
inference(demodulation,[status(thm),theory(equality)],[c_210725,c_4,c_287765]) ).
tff(c_441616,plain,
! [U_2070,U_2071,Y_2072] : ( multiply(double_divide(U_2070,U_2071),multiply(U_2071,multiply(U_2070,Y_2072))) = Y_2072 ),
inference(superposition,[status(thm),theory(equality)],[c_210458,c_419352]) ).
tff(c_210517,plain,
! [U_1268,U_1269] : ( double_divide(double_divide(U_1268,U_1269),U_1268) = U_1269 ),
inference(demodulation,[status(thm),theory(equality)],[c_210403,c_210403,c_141343]) ).
tff(c_210733,plain,
! [U_1277,U_1278] : ( multiply(U_1277,double_divide(U_1277,U_1278)) = inverse(U_1278) ),
inference(superposition,[status(thm),theory(equality)],[c_210517,c_4]) ).
tff(c_141922,plain,
! [U_937,U_938,U_934] : ( multiply(double_divide(U_937,U_938),U_938) = multiply(double_divide(U_937,U_934),U_934) ),
inference(superposition,[status(thm),theory(equality)],[c_141919,c_141803]) ).
tff(c_197267,plain,
! [X_1218,U_1220,U_934] : ( multiply(double_divide(double_divide(inverse(X_1218),multiply(U_1220,X_1218)),U_934),U_934) = U_1220 ),
inference(superposition,[status(thm),theory(equality)],[c_196999,c_141922]) ).
tff(c_210771,plain,
! [U_1277,U_1278,U_934] : ( multiply(double_divide(double_divide(inverse(double_divide(U_1277,U_1278)),inverse(U_1278)),U_934),U_934) = U_1277 ),
inference(superposition,[status(thm),theory(equality)],[c_210733,c_197267]) ).
tff(c_210817,plain,
! [U_1278,U_1277] : ( multiply(inverse(U_1278),multiply(U_1278,U_1277)) = U_1277 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_205730,c_4,c_210771]) ).
tff(c_442176,plain,
! [U_2070,U_2071,Y_2072] : ( multiply(inverse(double_divide(U_2070,U_2071)),Y_2072) = multiply(U_2071,multiply(U_2070,Y_2072)) ),
inference(superposition,[status(thm),theory(equality)],[c_441616,c_210817]) ).
tff(c_443041,plain,
! [U_2071,U_2070,Y_2072] : ( multiply(multiply(U_2071,U_2070),Y_2072) = multiply(U_2071,multiply(U_2070,Y_2072)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_442176]) ).
tff(c_293,plain,
! [Z_40,Y_44,U_43,X_42,X_39,U_41] : ( multiply(double_divide(U_41,double_divide(Y_44,U_41)),multiply(double_divide(Y_44,Z_40),X_42)) = double_divide(inverse(X_39),multiply(double_divide(U_43,double_divide(inverse(X_42),U_43)),multiply(Z_40,X_39))) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_17]) ).
tff(c_492,plain,
! [U_45,Y_46,X_47,Z_48] : ( multiply(double_divide(U_45,double_divide(Y_46,U_45)),multiply(double_divide(Y_46,double_divide(inverse(X_47),Z_48)),X_47)) = Z_48 ),
inference(superposition,[status(thm),theory(equality)],[c_293,c_7]) ).
tff(c_585,plain,
! [U_45,Y_6,Z_48,X_5,Y_46] : ( multiply(double_divide(U_45,double_divide(Y_46,U_45)),multiply(double_divide(Y_46,double_divide(multiply(X_5,Y_6),Z_48)),double_divide(Y_6,X_5))) = Z_48 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_492]) ).
tff(c_410,plain,
! [U_41,Y_44,X_42,Z_3] : ( multiply(double_divide(U_41,double_divide(Y_44,U_41)),multiply(double_divide(Y_44,double_divide(inverse(X_42),Z_3)),X_42)) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_293,c_7]) ).
tff(c_388,plain,
! [Z_40,Y_6,U_43,X_5,X_39] : ( double_divide(multiply(X_5,Y_6),double_divide(inverse(X_39),multiply(double_divide(U_43,double_divide(inverse(double_divide(Y_6,X_5)),U_43)),multiply(Z_40,X_39)))) = Z_40 ),
inference(superposition,[status(thm),theory(equality)],[c_293,c_41]) ).
tff(c_1008,plain,
! [Y_64,U_62,X_65,X_66,Z_63] : ( double_divide(multiply(X_66,Y_64),double_divide(inverse(X_65),multiply(double_divide(U_62,double_divide(multiply(X_66,Y_64),U_62)),multiply(Z_63,X_65)))) = Z_63 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_388]) ).
tff(c_1111,plain,
! [U_62,X_65,Z_3,Y_44,X_42,Z_63,U_41] : ( double_divide(Z_3,double_divide(inverse(X_65),multiply(double_divide(U_62,double_divide(multiply(double_divide(U_41,double_divide(Y_44,U_41)),multiply(double_divide(Y_44,double_divide(inverse(X_42),Z_3)),X_42)),U_62)),multiply(Z_63,X_65)))) = Z_63 ),
inference(superposition,[status(thm),theory(equality)],[c_410,c_1008]) ).
tff(c_1381,plain,
! [Z_72,X_73,U_74,Z_75] : ( double_divide(Z_72,double_divide(inverse(X_73),multiply(double_divide(U_74,double_divide(Z_72,U_74)),multiply(Z_75,X_73)))) = Z_75 ),
inference(demodulation,[status(thm),theory(equality)],[c_410,c_1111]) ).
tff(c_1683,plain,
! [Z_81,U_80,X_83,Z_82,U_84] : ( multiply(double_divide(U_84,double_divide(Z_81,U_84)),multiply(Z_82,X_83)) = multiply(double_divide(U_80,double_divide(Z_81,U_80)),multiply(Z_82,X_83)) ),
inference(superposition,[status(thm),theory(equality)],[c_1381,c_410]) ).
tff(c_1948,plain,
! [U_45,Z_81,U_80,Y_6,U_84,Z_48,X_5,Y_46] : ( multiply(double_divide(U_84,double_divide(Z_81,U_84)),Z_48) = multiply(double_divide(U_80,double_divide(Z_81,U_80)),multiply(double_divide(U_45,double_divide(Y_46,U_45)),multiply(double_divide(Y_46,double_divide(multiply(X_5,Y_6),Z_48)),double_divide(Y_6,X_5)))) ),
inference(superposition,[status(thm),theory(equality)],[c_585,c_1683]) ).
tff(c_2066,plain,
! [U_88,Z_86,Z_87,U_85] : ( multiply(double_divide(U_88,double_divide(Z_86,U_88)),Z_87) = multiply(double_divide(U_85,double_divide(Z_86,U_85)),Z_87) ),
inference(demodulation,[status(thm),theory(equality)],[c_585,c_1948]) ).
tff(c_2154,plain,
! [U_41,U_85,U_88,Z_87] : ( multiply(double_divide(U_41,double_divide(U_85,U_41)),multiply(double_divide(U_88,double_divide(inverse(Z_87),U_88)),Z_87)) = U_85 ),
inference(superposition,[status(thm),theory(equality)],[c_2066,c_410]) ).
tff(c_2631,plain,
! [U_94,U_95,U_96,Z_97] : ( multiply(double_divide(U_94,double_divide(U_95,U_94)),multiply(double_divide(U_96,double_divide(inverse(Z_97),U_96)),Z_97)) = U_95 ),
inference(superposition,[status(thm),theory(equality)],[c_2066,c_410]) ).
tff(c_1541,plain,
! [Z_75,Y_6,Z_72,X_5,U_74] : ( double_divide(Z_72,double_divide(multiply(X_5,Y_6),multiply(double_divide(U_74,double_divide(Z_72,U_74)),multiply(Z_75,double_divide(Y_6,X_5))))) = Z_75 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1381]) ).
tff(c_2645,plain,
! [U_96,Y_6,X_5,U_95] : ( double_divide(U_96,double_divide(inverse(double_divide(Y_6,X_5)),U_96)) = double_divide(U_95,double_divide(multiply(X_5,Y_6),U_95)) ),
inference(superposition,[status(thm),theory(equality)],[c_2631,c_1541]) ).
tff(c_4253,plain,
! [U_116,X_114,Y_115,U_113] : ( double_divide(U_116,double_divide(multiply(X_114,Y_115),U_116)) = double_divide(U_113,double_divide(multiply(X_114,Y_115),U_113)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2645]) ).
tff(c_4748,plain,
! [U_116,Z_87,U_113,U_88,U_85,U_41] : ( double_divide(U_116,double_divide(U_85,U_116)) = double_divide(U_113,double_divide(multiply(double_divide(U_41,double_divide(U_85,U_41)),multiply(double_divide(U_88,double_divide(inverse(Z_87),U_88)),Z_87)),U_113)) ),
inference(superposition,[status(thm),theory(equality)],[c_2154,c_4253]) ).
tff(c_4860,plain,
! [U_116,U_85,U_113] : ( double_divide(U_116,double_divide(U_85,U_116)) = double_divide(U_113,double_divide(U_85,U_113)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2154,c_4748]) ).
tff(c_11956,plain,
! [U_188,U_189,U_190,Z_191] : ( multiply(double_divide(U_188,double_divide(U_189,U_188)),inverse(multiply(double_divide(U_190,double_divide(inverse(Z_191),U_190)),Z_191))) = U_189 ),
inference(superposition,[status(thm),theory(equality)],[c_2154,c_2631]) ).
tff(c_16538,plain,
! [U_227,U_228,U_229,Z_230] : ( multiply(double_divide(U_227,double_divide(U_228,U_227)),inverse(inverse(multiply(double_divide(U_229,double_divide(inverse(Z_230),U_229)),Z_230)))) = U_228 ),
inference(superposition,[status(thm),theory(equality)],[c_11956,c_2154]) ).
tff(c_16868,plain,
! [U_228,U_229,Y_6,X_5,U_227] : ( multiply(double_divide(U_227,double_divide(U_228,U_227)),inverse(inverse(multiply(double_divide(U_229,double_divide(multiply(X_5,Y_6),U_229)),double_divide(Y_6,X_5))))) = U_228 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16538]) ).
tff(c_2807,plain,
! [U_94,U_95,Y_6,U_96,X_5] : ( multiply(double_divide(U_94,double_divide(U_95,U_94)),multiply(double_divide(U_96,double_divide(multiply(X_5,Y_6),U_96)),double_divide(Y_6,X_5))) = U_95 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2631]) ).
tff(c_4874,plain,
! [U_119,U_118,U_117] : ( double_divide(U_119,double_divide(U_118,U_119)) = double_divide(U_117,double_divide(U_118,U_117)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2154,c_4748]) ).
tff(c_5401,plain,
! [U_120,U_121,U_122] : ( multiply(double_divide(U_120,U_121),U_121) = inverse(double_divide(U_122,double_divide(U_120,U_122))) ),
inference(superposition,[status(thm),theory(equality)],[c_4874,c_4]) ).
tff(c_5535,plain,
! [U_121,U_4,U_120,U_122] : ( double_divide(inverse(U_121),multiply(double_divide(U_4,double_divide(U_120,U_4)),inverse(double_divide(U_122,double_divide(U_120,U_122))))) = U_121 ),
inference(superposition,[status(thm),theory(equality)],[c_5401,c_7]) ).
tff(c_10086,plain,
! [U_168,U_169,U_170,U_171] : ( double_divide(inverse(U_168),multiply(double_divide(U_169,double_divide(U_170,U_169)),multiply(double_divide(U_170,U_171),U_171))) = U_168 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5535]) ).
tff(c_17343,plain,
! [U_236,X_237,U_238,X_239] : ( double_divide(inverse(U_236),double_divide(inverse(X_237),multiply(double_divide(U_238,double_divide(inverse(X_239),U_238)),multiply(X_239,X_237)))) = U_236 ),
inference(superposition,[status(thm),theory(equality)],[c_35,c_10086]) ).
tff(c_17714,plain,
! [U_236,Y_6,X_5,U_96] : ( double_divide(inverse(U_236),double_divide(inverse(double_divide(Y_6,X_5)),inverse(double_divide(U_96,double_divide(multiply(X_5,Y_6),U_96))))) = U_236 ),
inference(superposition,[status(thm),theory(equality)],[c_2807,c_17343]) ).
tff(c_19627,plain,
! [U_250,X_251,Y_252,U_253] : ( double_divide(inverse(U_250),double_divide(multiply(X_251,Y_252),multiply(double_divide(multiply(X_251,Y_252),U_253),U_253))) = U_250 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4,c_17714]) ).
tff(c_19954,plain,
! [U_228,U_250,U_229,U_253,Y_6,X_5,U_227] : ( double_divide(inverse(U_250),double_divide(U_228,multiply(double_divide(multiply(double_divide(U_227,double_divide(U_228,U_227)),inverse(inverse(multiply(double_divide(U_229,double_divide(multiply(X_5,Y_6),U_229)),double_divide(Y_6,X_5))))),U_253),U_253))) = U_250 ),
inference(superposition,[status(thm),theory(equality)],[c_16868,c_19627]) ).
tff(c_20271,plain,
! [U_254,U_255,U_256] : ( double_divide(inverse(U_254),double_divide(U_255,multiply(double_divide(U_255,U_256),U_256))) = U_254 ),
inference(demodulation,[status(thm),theory(equality)],[c_16868,c_19954]) ).
tff(c_20683,plain,
! [U_254,U_113,U_116,U_85] : ( double_divide(inverse(U_254),double_divide(U_113,multiply(double_divide(U_116,double_divide(U_85,U_116)),double_divide(U_85,U_113)))) = U_254 ),
inference(superposition,[status(thm),theory(equality)],[c_4860,c_20271]) ).
tff(c_20469,plain,
! [U_255,U_256,U_254,U_113] : ( double_divide(double_divide(U_255,multiply(double_divide(U_255,U_256),U_256)),U_254) = double_divide(U_113,double_divide(inverse(U_254),U_113)) ),
inference(superposition,[status(thm),theory(equality)],[c_20271,c_4860]) ).
tff(c_6472,plain,
! [U_135,U_136,U_137,U_138] : ( double_divide(double_divide(U_135,U_136),double_divide(U_137,double_divide(U_135,U_137))) = double_divide(U_138,double_divide(U_136,U_138)) ),
inference(superposition,[status(thm),theory(equality)],[c_4860,c_4874]) ).
tff(c_6986,plain,
! [U_137,U_135,U_136,U_138] : ( multiply(double_divide(U_137,double_divide(U_135,U_137)),double_divide(U_135,U_136)) = inverse(double_divide(U_138,double_divide(U_136,U_138))) ),
inference(superposition,[status(thm),theory(equality)],[c_6472,c_4]) ).
tff(c_20735,plain,
! [U_257,U_258,U_259] : ( multiply(double_divide(U_257,multiply(double_divide(U_257,U_258),U_258)),inverse(U_259)) = inverse(U_259) ),
inference(superposition,[status(thm),theory(equality)],[c_20271,c_4]) ).
tff(c_20980,plain,
! [U_257,U_258,X_5,Y_6] : ( multiply(double_divide(U_257,multiply(double_divide(U_257,U_258),U_258)),multiply(X_5,Y_6)) = inverse(double_divide(Y_6,X_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20735]) ).
tff(c_22720,plain,
! [U_271,U_272,X_273,Y_274] : ( multiply(double_divide(U_271,multiply(double_divide(U_271,U_272),U_272)),multiply(X_273,Y_274)) = multiply(X_273,Y_274) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20980]) ).
tff(c_22923,plain,
! [U_228,U_271,U_229,Y_6,X_5,U_272,U_227] : ( multiply(double_divide(U_271,multiply(double_divide(U_271,U_272),U_272)),U_228) = multiply(double_divide(U_227,double_divide(U_228,U_227)),inverse(inverse(multiply(double_divide(U_229,double_divide(multiply(X_5,Y_6),U_229)),double_divide(Y_6,X_5))))) ),
inference(superposition,[status(thm),theory(equality)],[c_16868,c_22720]) ).
tff(c_23170,plain,
! [U_275,U_276,U_277] : ( multiply(double_divide(U_275,multiply(double_divide(U_275,U_276),U_276)),U_277) = U_277 ),
inference(demodulation,[status(thm),theory(equality)],[c_16868,c_22923]) ).
tff(c_31221,plain,
! [U_323,U_324,U_325,U_326] : ( multiply(double_divide(U_323,U_324),U_324) = double_divide(inverse(U_325),multiply(double_divide(U_326,double_divide(U_323,U_326)),U_325)) ),
inference(superposition,[status(thm),theory(equality)],[c_23170,c_7]) ).
tff(c_32112,plain,
! [U_135,U_324,U_136,U_138] : ( multiply(double_divide(U_135,U_324),U_324) = double_divide(inverse(double_divide(U_135,U_136)),inverse(double_divide(U_138,double_divide(U_136,U_138)))) ),
inference(superposition,[status(thm),theory(equality)],[c_6986,c_31221]) ).
tff(c_32312,plain,
! [U_327,U_328,U_329,U_330] : ( multiply(double_divide(U_327,U_328),U_328) = double_divide(multiply(U_329,U_327),multiply(double_divide(U_329,U_330),U_330)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4,c_32112]) ).
tff(c_6983,plain,
! [U_136,U_138,U_135,U_137] : ( multiply(double_divide(U_136,U_138),U_138) = inverse(double_divide(double_divide(U_135,U_136),double_divide(U_137,double_divide(U_135,U_137)))) ),
inference(superposition,[status(thm),theory(equality)],[c_6472,c_4]) ).
tff(c_23424,plain,
! [U_136,U_135,U_137,U_277] : ( multiply(double_divide(U_136,inverse(double_divide(double_divide(U_135,U_136),double_divide(U_137,double_divide(U_135,U_137))))),U_277) = U_277 ),
inference(superposition,[status(thm),theory(equality)],[c_6983,c_23170]) ).
tff(c_23512,plain,
! [U_136,U_137,U_135,U_277] : ( multiply(double_divide(U_136,multiply(double_divide(U_137,double_divide(U_135,U_137)),double_divide(U_135,U_136))),U_277) = U_277 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_23424]) ).
tff(c_36475,plain,
! [U_346,U_347,U_348,U_349] : ( multiply(double_divide(U_346,double_divide(multiply(U_347,U_346),multiply(double_divide(U_347,U_348),U_348))),U_349) = U_349 ),
inference(superposition,[status(thm),theory(equality)],[c_32312,c_23512]) ).
tff(c_36600,plain,
! [U_136,U_347,U_348,U_277] : ( multiply(double_divide(U_136,double_divide(multiply(U_347,multiply(double_divide(U_347,U_348),U_348)),U_136)),U_277) = U_277 ),
inference(superposition,[status(thm),theory(equality)],[c_36475,c_23512]) ).
tff(c_1179,plain,
! [Z_3,X_65,U_62,Z_63] : ( double_divide(Z_3,double_divide(inverse(X_65),multiply(double_divide(U_62,double_divide(Z_3,U_62)),multiply(Z_63,X_65)))) = Z_63 ),
inference(demodulation,[status(thm),theory(equality)],[c_410,c_1111]) ).
tff(c_37417,plain,
! [U_350,U_351,U_352,U_353] : ( multiply(double_divide(U_350,double_divide(multiply(U_351,multiply(double_divide(U_351,U_352),U_352)),U_350)),U_353) = U_353 ),
inference(superposition,[status(thm),theory(equality)],[c_36475,c_23512]) ).
tff(c_38269,plain,
! [U_62,X_65,U_353,Z_63,U_351,U_352] : ( multiply(double_divide(double_divide(inverse(X_65),multiply(double_divide(U_62,double_divide(multiply(U_351,multiply(double_divide(U_351,U_352),U_352)),U_62)),multiply(Z_63,X_65))),Z_63),U_353) = U_353 ),
inference(superposition,[status(thm),theory(equality)],[c_1179,c_37417]) ).
tff(c_39381,plain,
! [X_358,Z_359,U_360] : ( multiply(double_divide(double_divide(inverse(X_358),multiply(Z_359,X_358)),Z_359),U_360) = U_360 ),
inference(demodulation,[status(thm),theory(equality)],[c_36600,c_38269]) ).
tff(c_39759,plain,
! [U_113,U_256,U_360] : ( multiply(double_divide(U_113,double_divide(inverse(double_divide(inverse(U_256),U_256)),U_113)),U_360) = U_360 ),
inference(superposition,[status(thm),theory(equality)],[c_20469,c_39381]) ).
tff(c_40602,plain,
! [U_364,U_365,U_366] : ( multiply(double_divide(U_364,double_divide(multiply(U_365,inverse(U_365)),U_364)),U_366) = U_366 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39759]) ).
tff(c_44113,plain,
! [U_373,U_374,U_375] : ( multiply(double_divide(U_373,double_divide(U_374,U_373)),double_divide(inverse(U_375),U_375)) = U_374 ),
inference(superposition,[status(thm),theory(equality)],[c_40602,c_585]) ).
tff(c_2052,plain,
! [U_84,Z_81,Z_48,U_80] : ( multiply(double_divide(U_84,double_divide(Z_81,U_84)),Z_48) = multiply(double_divide(U_80,double_divide(Z_81,U_80)),Z_48) ),
inference(demodulation,[status(thm),theory(equality)],[c_585,c_1948]) ).
tff(c_5306,plain,
! [U_118,U_119,U_117] : ( multiply(double_divide(U_118,U_119),U_119) = inverse(double_divide(U_117,double_divide(U_118,U_117))) ),
inference(superposition,[status(thm),theory(equality)],[c_4874,c_4]) ).
tff(c_5640,plain,
! [U_123,U_125,U_124] : ( multiply(double_divide(U_123,U_125),U_125) = multiply(double_divide(U_123,U_124),U_124) ),
inference(superposition,[status(thm),theory(equality)],[c_5401,c_5306]) ).
tff(c_5866,plain,
! [U_84,U_125,U_80,Z_81] : ( multiply(double_divide(U_84,U_125),U_125) = multiply(double_divide(U_80,double_divide(Z_81,U_80)),double_divide(Z_81,U_84)) ),
inference(superposition,[status(thm),theory(equality)],[c_2052,c_5640]) ).
tff(c_44407,plain,
! [U_375,U_125] : ( multiply(double_divide(U_375,U_125),U_125) = inverse(U_375) ),
inference(superposition,[status(thm),theory(equality)],[c_44113,c_5866]) ).
tff(c_41054,plain,
! [U_45,U_364,U_365] : ( multiply(double_divide(U_45,double_divide(U_364,U_45)),double_divide(inverse(U_365),U_365)) = U_364 ),
inference(superposition,[status(thm),theory(equality)],[c_40602,c_585]) ).
tff(c_39937,plain,
! [U_113,U_256,U_360] : ( multiply(double_divide(U_113,double_divide(multiply(U_256,inverse(U_256)),U_113)),U_360) = U_360 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39759]) ).
tff(c_47434,plain,
! [U_393,U_394] : ( multiply(U_393,inverse(U_393)) = double_divide(inverse(U_394),U_394) ),
inference(superposition,[status(thm),theory(equality)],[c_44113,c_39937]) ).
tff(c_1481,plain,
! [X_73,U_74,Z_72,Z_75] : ( multiply(double_divide(inverse(X_73),multiply(double_divide(U_74,double_divide(Z_72,U_74)),multiply(Z_75,X_73))),Z_72) = inverse(Z_75) ),
inference(superposition,[status(thm),theory(equality)],[c_1381,c_4]) ).
tff(c_47870,plain,
! [U_393,U_74,Z_72,U_394] : ( multiply(double_divide(inverse(inverse(U_393)),multiply(double_divide(U_74,double_divide(Z_72,U_74)),double_divide(inverse(U_394),U_394))),Z_72) = inverse(U_393) ),
inference(superposition,[status(thm),theory(equality)],[c_47434,c_1481]) ).
tff(c_48702,plain,
! [U_397] : ( inverse(inverse(inverse(U_397))) = inverse(U_397) ),
inference(demodulation,[status(thm),theory(equality)],[c_44407,c_41054,c_47870]) ).
tff(c_48744,plain,
! [U_397,U_113,U_116,U_85] : ( double_divide(inverse(U_397),double_divide(U_113,multiply(double_divide(U_116,double_divide(U_85,U_116)),double_divide(U_85,U_113)))) = inverse(inverse(U_397)) ),
inference(superposition,[status(thm),theory(equality)],[c_48702,c_20683]) ).
tff(c_48904,plain,
! [U_397] : ( inverse(inverse(U_397)) = U_397 ),
inference(demodulation,[status(thm),theory(equality)],[c_20683,c_48744]) ).
tff(c_32303,plain,
! [U_135,U_324,U_136,U_138] : ( multiply(double_divide(U_135,U_324),U_324) = double_divide(multiply(U_136,U_135),multiply(double_divide(U_136,U_138),U_138)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4,c_32112]) ).
tff(c_56312,plain,
! [U_490,U_491] : ( double_divide(multiply(U_490,U_491),inverse(U_490)) = inverse(U_491) ),
inference(demodulation,[status(thm),theory(equality)],[c_44407,c_44407,c_32303]) ).
tff(c_56512,plain,
! [U_375,U_125] : ( double_divide(inverse(U_375),inverse(double_divide(U_375,U_125))) = inverse(U_125) ),
inference(superposition,[status(thm),theory(equality)],[c_44407,c_56312]) ).
tff(c_57297,plain,
! [U_497,U_498] : ( double_divide(inverse(U_497),multiply(U_498,U_497)) = inverse(U_498) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_56512]) ).
tff(c_57491,plain,
! [U_125,U_375] : ( double_divide(inverse(U_125),inverse(U_375)) = inverse(double_divide(U_375,U_125)) ),
inference(superposition,[status(thm),theory(equality)],[c_44407,c_57297]) ).
tff(c_65366,plain,
! [U_548,U_549] : ( double_divide(inverse(U_548),inverse(U_549)) = multiply(U_548,U_549) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_57491]) ).
tff(c_65588,plain,
! [U_397,U_549] : ( multiply(inverse(U_397),U_549) = double_divide(U_397,inverse(U_549)) ),
inference(superposition,[status(thm),theory(equality)],[c_48904,c_65366]) ).
tff(c_48925,plain,
! [U_398] : ( inverse(inverse(U_398)) = U_398 ),
inference(demodulation,[status(thm),theory(equality)],[c_20683,c_48744]) ).
tff(c_49114,plain,
! [X_5,Y_6] : ( inverse(multiply(X_5,Y_6)) = double_divide(Y_6,X_5) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_48925]) ).
tff(c_44253,plain,
! [U_375,U_277] : ( multiply(double_divide(U_375,inverse(U_375)),U_277) = U_277 ),
inference(superposition,[status(thm),theory(equality)],[c_44113,c_23512]) ).
tff(c_5404,plain,
! [U_120,U_121,U_119] : ( multiply(double_divide(U_120,U_121),U_121) = multiply(double_divide(U_120,U_119),U_119) ),
inference(superposition,[status(thm),theory(equality)],[c_5401,c_5306]) ).
tff(c_41336,plain,
! [U_120,U_119,U_365] : ( multiply(double_divide(U_120,U_119),U_119) = double_divide(multiply(U_365,inverse(U_365)),U_120) ),
inference(superposition,[status(thm),theory(equality)],[c_5404,c_40602]) ).
tff(c_54444,plain,
! [U_473,U_474] : ( double_divide(multiply(U_473,inverse(U_473)),U_474) = inverse(U_474) ),
inference(superposition,[status(thm),theory(equality)],[c_44113,c_41336]) ).
tff(c_54602,plain,
! [U_375,U_474] : ( double_divide(inverse(double_divide(U_375,inverse(U_375))),U_474) = inverse(U_474) ),
inference(superposition,[status(thm),theory(equality)],[c_44253,c_54444]) ).
tff(c_54648,plain,
! [U_375,U_474] : ( double_divide(multiply(inverse(U_375),U_375),U_474) = inverse(U_474) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_54602]) ).
tff(c_44128,plain,
! [U_256,U_375] : ( multiply(U_256,inverse(U_256)) = double_divide(inverse(U_375),U_375) ),
inference(superposition,[status(thm),theory(equality)],[c_44113,c_39937]) ).
tff(c_54650,plain,
! [U_475,U_476] : ( double_divide(inverse(U_475),double_divide(U_476,inverse(U_476))) = U_475 ),
inference(superposition,[status(thm),theory(equality)],[c_44113,c_20683]) ).
tff(c_57541,plain,
! [U_499,U_500] : ( multiply(U_499,inverse(U_499)) = double_divide(U_500,inverse(U_500)) ),
inference(superposition,[status(thm),theory(equality)],[c_44128,c_54650]) ).
tff(c_54780,plain,
! [U_256,U_476] : ( multiply(U_256,inverse(U_256)) = double_divide(U_476,inverse(U_476)) ),
inference(superposition,[status(thm),theory(equality)],[c_44128,c_54650]) ).
tff(c_65633,plain,
! [U_551,U_550] : ( double_divide(U_551,inverse(U_551)) = double_divide(U_550,inverse(U_550)) ),
inference(superposition,[status(thm),theory(equality)],[c_57541,c_54780]) ).
tff(c_66017,plain,
! [U_375,U_551] : ( inverse(inverse(multiply(inverse(U_375),U_375))) = double_divide(U_551,inverse(U_551)) ),
inference(superposition,[status(thm),theory(equality)],[c_54648,c_65633]) ).
tff(c_68096,plain,
! [U_565,U_566] : ( multiply(inverse(U_565),U_565) = double_divide(U_566,inverse(U_566)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_49114,c_66017]) ).
tff(c_6,plain,
( ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_163,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(splitLeft,[status(thm)],[c_6]) ).
tff(c_68411,plain,
! [U_566] : ( multiply(inverse(a1),a1) != double_divide(U_566,inverse(U_566)) ),
inference(superposition,[status(thm),theory(equality)],[c_68096,c_163]) ).
tff(c_136000,plain,
! [U_566] : ( double_divide(a1,inverse(a1)) != double_divide(U_566,inverse(U_566)) ),
inference(demodulation,[status(thm),theory(equality)],[c_65588,c_68411]) ).
tff(c_136004,plain,
$false,
inference(reflexivity,[status(thm),theory(equality)],[c_136000]) ).
tff(c_136005,plain,
( ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
inference(splitRight,[status(thm)],[c_6]) ).
tff(c_136017,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(splitLeft,[status(thm)],[c_136005]) ).
tff(c_470845,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_443041,c_136017]) ).
tff(c_470846,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(splitRight,[status(thm)],[c_136005]) ).
tff(c_565642,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_564666,c_470846]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.09 % Problem : GRP082-1 : TPTP v9.0.0. Bugfixed v2.3.0.
% 0.07/0.10 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.10/0.29 % Computer : n007.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Mon Apr 7 21:16:23 EDT 2025
% 0.10/0.29 % CPUTime :
% 204.19/156.71 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 204.38/156.75
% 204.38/156.75 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------