MetiTarski 2.5 (built 11 Oct 2016) run on host voron (Tue Oct 11 15:07:02 2016) with --verbose 0 --time 60; 3 threads Session test3-polyml Original command: runmetit.pl --time 60 --thre 3 --suff test3-polyml abs-problem-10; proved; 0.1 seconds abs-problem-11; proved; 0.1 seconds abs-problem-12; proved; 0.2 seconds abs-problem-13; proved; 0.1 seconds abs-problem-14; proved; 1.0 seconds abs-problem-15; proved; 0.4 seconds abs-problem-16; proved; 7.4 seconds abs-problem-17-weak; proved; 0.3 seconds abs-problem-17; proved; 0.6 seconds abs-problem-1; proved; 0.0 seconds abs-problem-2; proved; 0.1 seconds abs-problem-3; proved; 0.4 seconds abs-problem-4; proved; 0.1 seconds abs-problem-5-sqrt-weak2; proved; 1.6 seconds abs-problem-5-sqrt-weak; proved; 2.5 seconds abs-problem-5-sqrt; gave up; 37.5 seconds, max weight = 1999 abs-problem-5-weak; proved; 0.3 seconds abs-problem-5; gave up; 6.0 seconds, max weight = 1914 abs-problem-6; proved; 0.0 seconds abs-problem-7; proved; 0.1 seconds abs-problem-8; proved; 0.3 seconds abs-problem-9; proved; 0.1 seconds Arthan1; proved; 2.3 seconds Arthan1A; proved; 0.3 seconds, max weight = 1867 Arthan1B; proved; 1.9 seconds Arthan1C; proved; 0.1 seconds, max weight = 1867 ArthanKM2-sincos; proved; 0.4 seconds ArthanKM2; proved; 0.2 seconds, max weight = 1867 ArthanM2-sincos; proved; 1.5 seconds ArthanM2; proved; 0.9 seconds asin-1-1var; proved; 0.2 seconds asin-1; proved; 2.4 seconds asin-2; proved; 0.4 seconds asin-3; proved; 0.2 seconds asin-3abs; proved; 0.2 seconds asin-4; proved; 0.4 seconds asin-5-weak; proved; 1.1 seconds asin-5; proved; 1.7 seconds asin-6-weak; proved; 0.5 seconds asin-6; proved; 0.4 seconds asin-7; proved; 1.2 seconds asin-8-sqrt1; proved; 1.9 seconds asin-8-sqrt2; proved; 5.0 seconds; 3.2 seconds (RCF) asin-8-sqrt3; proved; 8.0 seconds; 3.9 seconds (RCF) asin-8-sqrt4; timed out asin-8-vars4; timed out asin-8; timed out atan-error-analysis-1-weak; proved; 0.1 seconds atan-error-analysis-1; proved; 0.3 seconds atan-error-analysis-2-weak; proved; 0.5 seconds atan-error-analysis-2; proved; 0.1 seconds atan-error-analysis-3-weak; proved; 0.2 seconds atan-error-analysis-3; proved; 0.2 seconds atan-error-analysis-4-weak; proved; 0.1 seconds atan-error-analysis-4; proved; 0.2 seconds atan-error-analysis-5; proved; 0.0 seconds atan-problem-1-sqrt-max; proved; 0.3 seconds atan-problem-1-sqrt-weak; proved; 3.6 seconds atan-problem-1-sqrt; timed out atan-problem-1-weak; proved; 0.3 seconds atan-problem-10; proved; 0.3 seconds atan-problem-11; proved; 0.1 seconds atan-problem-12; proved; 0.1 seconds atan-problem-13; proved; 0.4 seconds atan-problem-1; timed out atan-problem-2-sqrt-weak; timed out atan-problem-2-sqrt-weakest21; proved; 38.3 seconds atan-problem-2-sqrt-weakT1; proved; 4.4 seconds; 3.7 seconds (RCF) atan-problem-2-sqrt-weakT2; proved; 3.3 seconds, max weight = 771 atan-problem-2-sqrt; timed out atan-problem-2-weak2; timed out atan-problem-2-weak; timed out atan-problem-2-weakest21; proved; 15.2 seconds; 14.7 seconds (RCF) atan-problem-2-weakest31; proved; 3.0 seconds; 2.4 seconds (RCF) atan-problem-2-weakestT; timed out atan-problem-2-weakT; timed out atan-problem-2; timed out atan-problem-7; proved; 0.1 seconds atan-problem-8; proved; 0.0 seconds atan-problem-9; proved; 0.0 seconds atan-vega-1-weak; proved; 5.8 seconds, max weight = 1177 atan-vega-1; timed out atan-vega-2-weak; proved; 9.8 seconds; 8.8 seconds (RCF) atan-vega-2; timed out atan-vega-3-weak; timed out atan-vega-3; timed out Bessel_Krasikov_Thm2; gave up; 6.0 seconds, max weight = 728 Bessel_Landau; proved; 1.6 seconds bottom-plate-mixer; proved; 0.2 seconds cbrt-problem-1; proved; 0.1 seconds cbrt-problem-2-weak; timed out cbrt-problem-2; timed out cbrt-problem-3-weak; timed out cbrt-problem-3; timed out cbrt-problem-4-weak-2var; proved; 0.1 seconds cbrt-problem-4-weak; proved; 0.2 seconds cbrt-problem-4; gave up; 4.9 seconds, max weight = 1644 cbrt-problem-5a; timed out cbrt-problem-5b-weak; proved; 41.5 seconds cbrt-problem-5b; timed out cbrt-problem-6a; proved; 0.2 seconds cbrt-problem-6b; proved; 0.5 seconds Chua-1-IL-L-sincos; proved; 1.3 seconds Chua-1-IL-L; proved; 1.3 seconds Chua-1-IL-U-sincos; proved; 1.0 seconds Chua-1-IL-U; proved; 1.1 seconds Chua-1-VC1-L-sincos; proved; 1.5 seconds Chua-1-VC1-L; proved; 1.8 seconds; 1.6 seconds (RCF) Chua-1-VC1-U-sincos; proved; 4.3 seconds; 2.7 seconds (RCF) Chua-1-VC1-U; proved; 0.8 seconds Chua-1-VC2-L-sincos; proved; 1.9 seconds Chua-1-VC2-L; proved; 0.9 seconds Chua-1-VC2-U-sincos; proved; 1.3 seconds Chua-1-VC2-U; proved; 1.9 seconds; 1.8 seconds (RCF) Chua-2-IL-L-sincos; proved; 0.2 seconds Chua-2-IL-L; proved; 0.2 seconds Chua-2-IL-U-sincos; proved; 0.6 seconds Chua-2-IL-U; proved; 5.5 seconds; 5.3 seconds (RCF) Chua-2-VC1-L-sincos; proved; 0.2 seconds Chua-2-VC1-L; timed out Chua-2-VC1-U-sincos; proved; 0.4 seconds Chua-2-VC1-U; proved; 4.0 seconds; 3.7 seconds (RCF) Chua-2-VC2-L-sincos; proved; 0.3 seconds Chua-2-VC2-L; proved; 0.3 seconds Chua-2-VC2-U-sincos; proved; 0.6 seconds Chua-2-VC2-U; proved; 2.8 seconds; 2.4 seconds (RCF) Chua; proved; 0.2 seconds CMOS-opamp; proved; 10.7 seconds; 10.1 seconds (RCF) Colpitts-BJT-1-VC2+VC1; proved; 0.3 seconds Colpitts-BJT-2-VC2+VC1; proved; 0.9 seconds CONVOI-weak2; proved; 0.3 seconds CONVOI-weak; proved; 0.3 seconds CONVOI2-sincos-weak; proved; 0.3 seconds CONVOI2-sincos; timed out CONVOI2; timed out CONVOI; proved; 0.2 seconds cos-3410-a; proved; 0.1 seconds cos-3410-b; proved; 0.4 seconds cos-3411-a-weak2; timed out cos-3411-a-weak; timed out cos-3411-a; timed out cos-3411-b-weak; timed out cos-3411-b; timed out cos-3411-c; proved; 0.3 seconds cos-error-analysis-1; proved; 0.0 seconds cos-error-analysis-2; proved; 0.1 seconds cos-error-analysis-3; proved; 0.1 seconds cos-error-analysis-4; proved; 0.1 seconds cos-error-analysis-5; proved; 0.1 seconds cos-error-analysis-6; proved; 0.1 seconds cos-error-analysis-7; proved; 0.7 seconds cos-power-1-weak; timed out cos-power-1; timed out cos-power-2; proved; 2.9 seconds cos-problem-1-weak; proved; 0.1 seconds cos-problem-10-weak; proved; 41.9 seconds; 29.7 seconds (RCF), max weight = 736 cos-problem-10; timed out cos-problem-11; proved; 0.0 seconds cos-problem-12; proved; 0.0 seconds cos-problem-1; gave up; 0.6 seconds, max weight = 1088 cos-problem-2-weak; proved; 0.9 seconds cos-problem-2; gave up; 4.5 seconds; 3.1 seconds (RCF), max weight = 882 cos-problem-3; proved; 0.0 seconds cos-problem-4; proved; 0.0 seconds cos-problem-5-sqrt; proved; 1.4 seconds cos-problem-5; proved; 0.9 seconds cos-problem-9-weak; timed out cos-problem-9; timed out cosec-problem-1a; proved; 0.2 seconds cosec-problem-1b; proved; 0.6 seconds cosec-problem-2a; proved; 2.4 seconds; 2.1 seconds (RCF) cosec-problem-2b; proved; 2.2 seconds; 2.0 seconds (RCF) cosec-problem-3a-weak; proved; 3.7 seconds; 3.4 seconds (RCF) cosec-problem-3a; proved; 6.0 seconds; 5.7 seconds (RCF) cosec-problem-3b; proved; 11.0 seconds; 10.4 seconds (RCF) cosh-3612a-weak; proved; 0.2 seconds cosh-3612a; gave up; 10.7 seconds, max weight = 1997 cosh-3612b-weak; proved; 0.7 seconds cosh-3612b; gave up; 10.9 seconds, max weight = 1767 cosh-369; proved; 7.5 seconds cot-error-analysis-Intel-1; proved; 1.1 seconds doa-chesi-1; gave up; 0.0 seconds doa-chesi-2; gave up; 0.0 seconds drill-stick-stability; proved; 6.8 seconds, max weight = 788 ellipse-check-1-fun; proved; 19.7 seconds, max weight = 1136 ellipse-check-1; proved; 15.5 seconds; 6.2 seconds (RCF), max weight = 1136 ellipse-check-2-fun; proved; 71.9 seconds; 36.4 seconds (RCF), max weight = 1296 ellipse-check-2-nested-fun; timed out ellipse-check-2-two-fun; proved; 66.7 seconds; 35.2 seconds (RCF), max weight = 1296 ellipse-check-2-weak2; proved; 22.1 seconds; 9.7 seconds (RCF), max weight = 994 ellipse-check-2-weak; proved; 81.0 seconds; 35.7 seconds (RCF), max weight = 1296 ellipse-check-2; proved; 64.3 seconds; 39.2 seconds (RCF), max weight = 1296 ellipse-check-3-fun; timed out ellipse-check-3-ln-fun; proved; 16.5 seconds; 7.0 seconds (RCF), max weight = 839 ellipse-check-3-ln; proved; 13.1 seconds; 6.6 seconds (RCF), max weight = 839 ellipse-check-3-weak; proved; 60.3 seconds, max weight = 795 ellipse-check-3; timed out ellipse-check-4-atan-fun; proved; 3.2 seconds ellipse-check-4-atan; proved; 4.1 seconds; 2.7 seconds (RCF) ellipse-check-4-fun; timed out ellipse-check-4; timed out exp-361-2; proved; 0.3 seconds exp-361-4; proved; 0.9 seconds exp-361-6-e; proved; 2.4 seconds, max weight = 1304 exp-361-6-scaled; proved; 4.2 seconds, max weight = 1598 exp-361-6-weak; proved; 50.0 seconds, max weight = 1997 exp-361-6; timed out exp-361-neg-2; proved; 2.6 seconds exp-361-neg-4-e; proved; 9.7 seconds, max weight = 1777 exp-361-neg-4; proved; 0.2 seconds exp-361-neg-6-e; proved; 12.6 seconds, max weight = 1777 exp-361-neg-6-weak; proved; 3.1 seconds, max weight = 832 exp-361-neg-6; proved; 8.1 seconds, max weight = 967 exp-362-100c; proved; 1.9 seconds exp-362-2a; proved; 0.0 seconds exp-362-2b; proved; 0.2 seconds exp-362-2c; proved; 0.1 seconds exp-362-60a-weak; proved; 5.8 seconds; 3.9 seconds (RCF), max weight = 1065 exp-362-60a; gave up; 6.0 seconds, max weight = 1065 exp-362-60b; proved; 4.8 seconds; 3.6 seconds (RCF) exp-362-6a; proved; 0.0 seconds exp-362-6b; proved; 0.2 seconds exp-error-analysis-1; proved; 0.1 seconds exp-error-analysis-2; proved; 0.1 seconds exp-error-analysis-3; proved; 0.1 seconds exp-error-analysis-4; proved; 0.1 seconds exp-error-analysis-5; proved; 0.1 seconds exp-error-analysis-6; proved; 0.2 seconds exp-error-analysis-7; proved; 0.5 seconds exp-fun-ineq-b-cbrt; proved; 4.6 seconds exp-fun-ineq-b-corrected; proved; 27.1 seconds exp-fun-ineq-b-weak; timed out exp-fun-ineq-b; proved; 24.9 seconds exp-fun-ineq-c-I-15; proved; 12.7 seconds; 5.6 seconds (RCF), max weight = 1793 exp-fun-ineq-c-I-6; proved; 4.6 seconds, max weight = 1813 exp-fun-ineq-c-II-15; proved; 0.1 seconds exp-fun-ineq-c-II-6; proved; 0.1 seconds exp-fun-ineq-c-III-15; proved; 0.0 seconds exp-fun-ineq-c-III-6; proved; 0.0 seconds exp-hyperbolic-1; proved; 1.8 seconds exp-hyperbolic-2; proved; 0.5 seconds exp-ln-2-sqrt-weak2; proved; 0.2 seconds exp-ln-2-sqrt-weak; proved; 0.2 seconds exp-ln-2-sqrt; gave up; 3.8 seconds, max weight = 1267 exp-ln-2-weak; proved; 25.8 seconds, max weight = 646 exp-ln-2; proved; 20.7 seconds exp-log-nest-weak; timed out exp-log-nest; timed out exp-log-problem-1; proved; 0.1 seconds exp-lower-13-sqrt-weak2; proved; 0.6 seconds exp-lower-13-sqrt-weak; proved; 2.3 seconds exp-lower-13-sqrt; proved; 0.1 seconds exp-lower-13; proved; 0.0 seconds exp-lower-14-sqrt-weak; proved; 0.9 seconds exp-lower-14-sqrt; proved; 0.1 seconds exp-lower-14; proved; 0.0 seconds exp-lower-15; proved; 0.0 seconds exp-lower-16; proved; 0.0 seconds exp-lower-17; proved; 0.0 seconds exp-lower-18; proved; 0.0 seconds exp-lower-1; proved; 0.0 seconds exp-lower-2; proved; 0.0 seconds exp-lower-3; proved; 0.0 seconds exp-lower-4; proved; 0.0 seconds exp-lower-5; proved; 0.0 seconds exp-lower-6; proved; 0.0 seconds exp-lower-7; proved; 0.0 seconds exp-lower-8; proved; 0.0 seconds exp-lower-9; proved; 0.0 seconds exp-over-squared; proved; 1.3 seconds, max weight = 1209 exp-pi-weak1; timed out exp-pi-weak2; timed out exp-pi; gave up; 6.4 seconds, max weight = 1182 exp-problem-10-2-sqrt-weak; proved; 1.9 seconds exp-problem-10-2-sqrt; timed out exp-problem-10-2; timed out exp-problem-10-3-cbrt-weak; proved; 15.9 seconds exp-problem-10-3-cbrt; timed out exp-problem-10-3-weak; proved; 11.2 seconds; 10.7 seconds (RCF) exp-problem-10-3; timed out exp-problem-10; proved; 1.1 seconds exp-problem-1; proved; 0.1 seconds exp-problem-2; proved; 0.1 seconds exp-problem-3; proved; 0.1 seconds exp-problem-4; proved; 0.1 seconds exp-problem-5; proved; 0.1 seconds exp-problem-6; proved; 0.1 seconds exp-problem-7; proved; 0.0 seconds exp-problem-8-weak2; proved; 0.3 seconds exp-problem-8-weak; proved; 0.1 seconds exp-problem-8; gave up; 10.2 seconds, max weight = 1878 exp-problem-9-weak2; proved; 0.6 seconds exp-problem-9; proved; 13.8 seconds, max weight = 1999 exp-upper-10-div; proved; 0.1 seconds exp-upper-10; proved; 0.0 seconds exp-upper-11; proved; 0.0 seconds exp-upper-12; proved; 0.0 seconds exp-upper-13; proved; 0.1 seconds exp-upper-14; proved; 0.1 seconds exp-upper-15; proved; 0.1 seconds exp-upper-16; proved; 0.1 seconds exp-upper-17; proved; 0.2 seconds exp-upper-18; proved; 0.1 seconds exp-upper-19; proved; 0.1 seconds exp-upper-1; proved; 0.1 seconds exp-upper-20; proved; 0.1 seconds exp-upper-2; proved; 0.0 seconds exp-upper-3; proved; 0.1 seconds exp-upper-4; proved; 0.1 seconds exp-upper-5; proved; 0.1 seconds exp-upper-6; proved; 0.1 seconds exp-upper-7; proved; 0.1 seconds exp-upper-8; proved; 0.1 seconds exp-upper-9-div; proved; 0.1 seconds exp-upper-9; proved; 0.1 seconds FlightAvoidance9VARS-1; timed out FlightAvoidance9VARS-2; timed out FOCUS; proved; 0.0 seconds ground-problem-10; proved; 0.0 seconds ground-problem-11; proved; 0.0 seconds ground-problem-12; proved; 0.0 seconds ground-problem-13; proved; 0.0 seconds ground-problem-14; proved; 0.0 seconds ground-problem-15; proved; 0.0 seconds ground-problem-16; proved; 0.0 seconds ground-problem-17; proved; 0.0 seconds ground-problem-18; proved; 0.1 seconds ground-problem-19; proved; 0.2 seconds ground-problem-1; proved; 0.0 seconds ground-problem-20; proved; 0.1 seconds ground-problem-21; proved; 0.0 seconds ground-problem-22; proved; 0.0 seconds ground-problem-2; proved; 0.0 seconds ground-problem-3; proved; 0.0 seconds ground-problem-4; proved; 0.0 seconds ground-problem-5; proved; 0.0 seconds ground-problem-6; proved; 0.0 seconds ground-problem-7; proved; 0.0 seconds ground-problem-8; proved; 0.0 seconds ground-problem-9; proved; 0.0 seconds heartdipole; timed out HEATING; proved; 0.2 seconds Integrator; proved; 0.0 seconds keymaera-frocos-damped-pendulum; proved; 0.1 seconds keymaera-frocos-whirling-pendulum; timed out KeYmaera_damped_pendulum; proved; 0.2 seconds KeYmaera_damped_pendulum_general; proved; 0.2 seconds log-3615-sqrt; proved; 1.4 seconds log-3615; proved; 0.8 seconds log-error-analysis-1; proved; 0.2 seconds log-error-analysis-2-weak; proved; 0.1 seconds log-error-analysis-2; proved; 0.1 seconds log-error-analysis-3-weak; proved; 0.1 seconds log-error-analysis-3; proved; 0.1 seconds log-error-analysis-4-weak; proved; 0.1 seconds log-error-analysis-4; proved; 0.1 seconds log-fun-ineq-a1; proved; 0.0 seconds log-fun-ineq-a2; proved; 0.0 seconds log-fun-ineq-b1; proved; 0.1 seconds log-fun-ineq-b2; proved; 0.1 seconds log-fun-ineq-e-weak; timed out log-fun-ineq-e; timed out log-fun-ineq-f10-weak; proved; 1.4 seconds log-fun-ineq-f10; gave up; 22.5 seconds; 18.4 seconds (RCF), max weight = 1311 log-fun-ineq-f1; proved; 0.4 seconds log-fun-ineq-f2-sqrt; proved; 6.1 seconds log-fun-ineq-f2; proved; 3.7 seconds; 3.5 seconds (RCF) log-fun-ineq-f3; timed out log-fun-ineq-f; proved; 0.7 seconds log-fun-ineq-fneg10; proved; 2.0 seconds log-fun-ineq-fneg1; proved; 0.7 seconds log-fun-ineq-fneg2; proved; 1.3 seconds log-fun-ineq-fneg3; proved; 1.3 seconds log-fun-ineq-g; proved; 0.1 seconds log-lower-10; proved; 0.0 seconds log-lower-11; proved; 0.0 seconds log-lower-12; proved; 0.2 seconds log-lower-13; proved; 0.0 seconds log-lower-14; proved; 0.0 seconds log-lower-16; proved; 0.0 seconds log-lower-17-sqrt-weak; proved; 0.6 seconds log-lower-17-sqrt; gave up; 4.3 seconds, max weight = 1842 log-lower-17-weak; proved; 0.2 seconds log-lower-17; gave up; 4.6 seconds, max weight = 1736 log-lower-1; proved; 0.0 seconds log-lower-20-cbrt; proved; 1.1 seconds log-lower-20-weak2; proved; 0.6 seconds log-lower-20; gave up; 3.1 seconds, max weight = 1204 log-lower-21; proved; 0.1 seconds log-lower-22; proved; 0.1 seconds log-lower-23; proved; 0.1 seconds log-lower-24; proved; 0.1 seconds log-lower-2; proved; 0.0 seconds log-lower-3; proved; 0.0 seconds log-lower-4; proved; 0.3 seconds log-lower-5; proved; 0.0 seconds log-lower-6; proved; 0.0 seconds log-lower-7; proved; 0.0 seconds log-lower-8; proved; 0.0 seconds log-lower-9; proved; 0.0 seconds log-lower-zero; proved; 0.0 seconds log-nest-exp-twovars-weak1; timed out log-nest-exp-twovars-weak2; timed out log-nest-exp-twovars; timed out log-nest-exp-upper1; proved; 0.1 seconds log-nest-exp-upper2; proved; 0.7 seconds log-nest-exp-weak; proved; 27.5 seconds; 12.5 seconds (RCF), max weight = 600 log-nest-exp; timed out log-problem-1; proved; 0.0 seconds log-problem-2-weak; proved; 7.1 seconds log-problem-2; timed out log-problem-3-weak; proved; 0.0 seconds log-problem-3; gave up; 3.8 seconds, max weight = 1994 log-upper-10; proved; 0.0 seconds log-upper-11; proved; 0.0 seconds log-upper-12; proved; 0.0 seconds log-upper-13; proved; 0.0 seconds log-upper-14; proved; 0.0 seconds log-upper-16; proved; 0.0 seconds log-upper-18-sqrt-weak2; proved; 0.2 seconds log-upper-18-sqrt-weak; proved; 0.4 seconds log-upper-18-sqrt; gave up; 4.4 seconds, max weight = 1541 log-upper-18-weak; proved; 0.2 seconds log-upper-18; gave up; 4.4 seconds, max weight = 1851 log-upper-1; proved; 0.0 seconds log-upper-20-cbrt; proved; 3.9 seconds log-upper-20-weak; proved; 0.7 seconds log-upper-20; proved; 0.8 seconds log-upper-21-sqrt-weak2; proved; 1.1 seconds log-upper-21-sqrt-weak; proved; 1.0 seconds log-upper-21-sqrt; gave up; 9.9 seconds, max weight = 1494 log-upper-21-weak; proved; 0.6 seconds log-upper-21; gave up; 7.3 seconds, max weight = 1753 log-upper-22-sqrt; proved; 0.4 seconds log-upper-22; proved; 0.1 seconds log-upper-23-cbrt; proved; 1.1 seconds log-upper-23; proved; 0.4 seconds log-upper-24; proved; 0.0 seconds log-upper-25-weak; proved; 1.1 seconds log-upper-25; gave up; 3.3 seconds, max weight = 1384 log-upper-26; proved; 0.1 seconds log-upper-27-sqrt-weak; proved; 1.9 seconds log-upper-27-sqrt; timed out log-upper-27-weak; timed out log-upper-27; timed out log-upper-28-weak; proved; 2.9 seconds log-upper-28; gave up; 3.1 seconds, max weight = 1510 log-upper-29; proved; 0.0 seconds log-upper-2; proved; 0.0 seconds log-upper-30-weak; proved; 40.2 seconds; 20.1 seconds (RCF) log-upper-30; gave up; 2.0 seconds, max weight = 763 log-upper-3; proved; 0.0 seconds log-upper-4; proved; 0.0 seconds log-upper-5; proved; 0.0 seconds log-upper-6; proved; 0.0 seconds log-upper-7; proved; 0.0 seconds log-upper-8; proved; 0.0 seconds log-upper-9; proved; 0.0 seconds lotka-volterra-upper-Yrange; timed out Mastellone2c; proved; 1.1 seconds math-overflow-problem-1-weak; timed out math-overflow-problem-1; timed out max-1; proved; 0.0 seconds max-2; proved; 0.0 seconds max-min-1; proved; 0.0 seconds max-min-2; proved; 0.0 seconds max-sin-1; proved; 0.1 seconds max-sin-2; proved; 6.7 seconds; 3.8 seconds (RCF), max weight = 858 Melquiond1; proved; 0.1 seconds MUTANT-1; proved; 0.0 seconds MUTANT-2-h; proved; 0.8 seconds MUTANT-2; proved; 0.0 seconds MUTANT-3-h; proved; 0.8 seconds MUTANT-3; proved; 0.0 seconds NAVIGATION-1; proved; 0.0 seconds NAVIGATION-2; proved; 0.0 seconds nfm-check-gain-1; proved; 6.9 seconds; 5.7 seconds (RCF) nfm-check-gain-2; proved; 5.8 seconds; 4.2 seconds (RCF) nfm-check-gain-3; proved; 33.2 seconds; 29.7 seconds (RCF), max weight = 822 nfm-lower-right-verify; proved; 12.4 seconds; 10.2 seconds (RCF) nfm-middle-right-verify-1; proved; 0.2 seconds nfm-middle-right-verify-2; proved; 0.9 seconds nfm-middle-right-verify-3; proved; 0.1 seconds nfm-upper-right-verify; proved; 0.5 seconds Nichols-Plot-Disk-Drive-Meets-1-1; proved; 0.2 seconds Nichols-Plot-Disk-Drive-Meets-1-2; proved; 0.3 seconds Nichols-Plot-Disk-Drive-Meets-1-3; proved; 0.0 seconds Nichols-Plot-Disk-Drive-Meets-1-4; proved; 3.7 seconds; 3.0 seconds (RCF) Nichols-Plot-Disk-Drive-Meets-1-5; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-1-6-scaled; proved; 0.3 seconds Nichols-Plot-Disk-Drive-Meets-1-6-weak; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-1-6; proved; 1.2 seconds Nichols-Plot-Disk-Drive-Meets-1-7-weak; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-1-7; proved; 0.3 seconds Nichols-Plot-Disk-Drive-Meets-1-8-weak; proved; 0.0 seconds Nichols-Plot-Disk-Drive-Meets-1-8; proved; 0.2 seconds Nichols-Plot-Disk-Drive-Meets-2-1; proved; 0.2 seconds Nichols-Plot-Disk-Drive-Meets-2-2; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-2-3; proved; 3.0 seconds; 2.9 seconds (RCF) Nichols-Plot-Disk-Drive-Meets-2-4; proved; 3.9 seconds; 3.3 seconds (RCF) Nichols-Plot-Disk-Drive-Meets-2-5-weak; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-2-5; proved; 1.7 seconds Nichols-Plot-Disk-Drive-Meets-2-6-weak; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-2-6; proved; 0.4 seconds Nichols-Plot-Disk-Drive-Meets-2-7-weak; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-2-7; proved; 5.4 seconds, max weight = 831 Nichols-Plot-Disk-Drive-Meets-2-8-weak; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-2-8; proved; 0.4 seconds Nichols-Plot-Disk-Drive-Meets-3-1; proved; 0.1 seconds Nichols-Plot-Disk-Drive-Meets-3-2; proved; 0.1 seconds Nichols-Plot-Inverted-Pendulum-Fails-1-1; proved; 0.2 seconds Nichols-Plot-Inverted-Pendulum-Fails-1-2; proved; 0.0 seconds Nichols-Plot-Inverted-Pendulum-Fails-1-3; proved; 0.2 seconds Nichols-Plot-Inverted-Pendulum-Fails-1-4; proved; 4.1 seconds; 3.5 seconds (RCF) Nichols-Plot-Inverted-Pendulum-Fails-1-5-weak; proved; 0.1 seconds Nichols-Plot-Inverted-Pendulum-Fails-1-5; proved; 3.2 seconds Nichols-Plot-Inverted-Pendulum-Fails-1-6-sqrt; proved; 1.2 seconds Nichols-Plot-Inverted-Pendulum-Fails-1-6; proved; 1.4 seconds Nichols-Plot-Inverted-Pendulum-Fails-2-1; proved; 0.0 seconds Nichols-Plot-Inverted-Pendulum-Fails-2-2; proved; 0.7 seconds Nichols-Plot-Inverted-Pendulum-Fails-2-3; proved; 0.2 seconds Nichols-Plot-Inverted-Pendulum-Fails-2-4; proved; 1.5 seconds Nichols-Plot-Inverted-Pendulum-Fails-2-5-weak; proved; 0.2 seconds Nichols-Plot-Inverted-Pendulum-Fails-2-5; proved; 0.8 seconds Nichols-Plot-Inverted-Pendulum-Fails-3-1-sqrt; proved; 0.0 seconds Nichols-Plot-Inverted-Pendulum-Fails-3-1; proved; 0.0 seconds Nichols-Plot-Inverted-Pendulum-Fails-3-2; proved; 0.1 seconds Nichols-Plot-Inverted-Pendulum-Meets-1-1; proved; 0.2 seconds Nichols-Plot-Inverted-Pendulum-Meets-1-2; proved; 0.0 seconds Nichols-Plot-Inverted-Pendulum-Meets-1-3; proved; 0.3 seconds Nichols-Plot-Inverted-Pendulum-Meets-1-4; proved; 3.0 seconds; 2.3 seconds (RCF) Nichols-Plot-Inverted-Pendulum-Meets-1-5-weak; proved; 0.1 seconds Nichols-Plot-Inverted-Pendulum-Meets-1-5; proved; 0.3 seconds Nichols-Plot-Inverted-Pendulum-Meets-2-1; proved; 0.0 seconds Nichols-Plot-Inverted-Pendulum-Meets-2-2; proved; 0.6 seconds Nichols-Plot-Inverted-Pendulum-Meets-2-3; proved; 0.3 seconds Nichols-Plot-Inverted-Pendulum-Meets-2-4; proved; 0.9 seconds Nichols-Plot-Inverted-Pendulum-Meets-2-5-weak; proved; 0.2 seconds Nichols-Plot-Inverted-Pendulum-Meets-2-5; proved; 1.2 seconds Nichols-Plot-Inverted-Pendulum-Meets-3-1; proved; 0.0 seconds Nichols-Plot-Inverted-Pendulum-Meets-3-2; proved; 0.1 seconds Nichols-Plot-Simple-Example-1; proved; 0.5 seconds Nichols-Plot-Simple-Example-2; proved; 0.0 seconds Nichols-Plot-Simple-Example-3-weak; proved; 0.1 seconds Nichols-Plot-Simple-Example-3; proved; 0.1 seconds Nichols-Plot-Simple-Example-4; proved; 0.1 seconds nthrt_cbrt-problem-1; proved; 0.2 seconds nthrt_cbrt-problem-4-weak-2var; proved; 0.2 seconds, max weight = 675 nthrt_cbrt-problem-4-weak; proved; 0.4 seconds, max weight = 675 nthrt_cbrt-problem-5a; timed out nthrt_cbrt-problem-5b-weak; proved; 73.3 seconds, max weight = 622 polypaver-bench-exp-3d; timed out polypaver-bench-exp; timed out polypaver-bench-sqrt-3d; timed out polypaver-bench-sqrt; timed out polypaver-proval-cosine-abs; proved; 0.1 seconds polypaver-proval-cosine; proved; 0.1 seconds polypaver-sqrt-circles-1a; proved; 0.0 seconds polypaver-sqrt-circles-2a; proved; 0.0 seconds polypaver-sqrt43-int-3vars_A; proved; 0.1 seconds polypaver-sqrt43-int-3vars_B; proved; 0.1 seconds polypaver-sqrt43-int-4vars_A; proved; 19.3 seconds; 19.1 seconds (RCF) polypaver-sqrt43-int-4vars_B; proved; 10.2 seconds; 9.9 seconds (RCF) polypaver-sqrt43-int_A; timed out polypaver-sqrt43-int_B; proved; 0.2 seconds polypaver-sqrt43_A; proved; 0.1 seconds polypaver-sqrt43_B; proved; 0.1 seconds RL-high-pass-circuit-gain; proved; 0.1 seconds RL-high-pass-circuit; proved; 0.0 seconds sin-3425a-1var; proved; 0.1 seconds sin-3425a-weak; proved; 7.1 seconds; 7.0 seconds (RCF) sin-3425a; proved; 9.7 seconds; 9.5 seconds (RCF) sin-3425b-1var; proved; 0.2 seconds sin-3425b-weak; proved; 55.1 seconds; 54.9 seconds (RCF) sin-3425b; timed out sin-3426-1a; proved; 0.2 seconds sin-3426-1b; proved; 0.4 seconds sin-3426-2a; proved; 1.6 seconds sin-3426-2b; proved; 1.4 seconds sin-3426-3a-weak; proved; 2.4 seconds; 2.2 seconds (RCF) sin-3426-3a; proved; 4.3 seconds; 3.9 seconds (RCF) sin-3426-3b-weak; proved; 0.9 seconds sin-3426-3b; proved; 1.8 seconds sin-3426-4a-weak; proved; 8.3 seconds; 7.7 seconds (RCF), max weight = 783 sin-3426-4a; proved; 17.4 seconds; 16.6 seconds (RCF), max weight = 783 sin-3426-4b-weak; proved; 2.5 seconds; 2.1 seconds (RCF), max weight = 768 sin-3426-4b; proved; 5.5 seconds; 4.7 seconds (RCF), max weight = 768 sin-344-2-weak; timed out sin-344-2; timed out sin-344-3-weak; proved; 0.8 seconds sin-344-3; timed out sin-344-4; timed out sin-cos-2var1; proved; 0.9 seconds sin-cos-2var2; timed out sin-cos-2var3; proved; 28.6 seconds; 28.3 seconds (RCF) sin-cos-2var4; timed out sin-cos-2var5; timed out sin-cos-2var6; timed out sin-cos-2var7; timed out sin-cos-2var8; timed out sin-cos-2var9; timed out sin-cos-346-a-sqrt; proved; 2.7 seconds, max weight = 1012 sin-cos-346-a; proved; 0.3 seconds sin-cos-346-b-sqrt; proved; 2.4 seconds sin-cos-346-b-weak; proved; 16.9 seconds; 16.4 seconds (RCF) sin-cos-346-b; proved; 7.4 seconds; 5.2 seconds (RCF) sin-cos-346-c; proved; 5.3 seconds; 4.8 seconds (RCF) sin-cos-problem-1; proved; 0.1 seconds sin-cos-problem-2; proved; 0.1 seconds sin-cos-problem-3-weak; proved; 0.3 seconds sin-cos-problem-3; gave up; 13.4 seconds, max weight = 1234 sin-cos-problem-4; proved; 0.1 seconds sin-cos-problem-5-weak; proved; 0.3 seconds sin-cos-problem-5; gave up; 3.0 seconds, max weight = 723 sin-cos-problem-6; proved; 0.1 seconds sin-cos-problem-7-weak; proved; 66.0 seconds, max weight = 1226 sin-cos-problem-7-weakest; proved; 5.8 seconds; 3.4 seconds (RCF), max weight = 735 sin-cos-problem-7; proved; 12.6 seconds, max weight = 1094 sin-cos-problem-diff1a; proved; 0.5 seconds sin-cos-problem-diff1b; proved; 0.6 seconds sin-cos-problem-diff2a; proved; 1.3 seconds sin-cos-problem-diff2b; proved; 3.2 seconds sin-cos-problem-diff3a; proved; 5.8 seconds; 3.1 seconds (RCF) sin-cos-problem-diff3b; proved; 6.8 seconds sin-cos-problem-diff4a; proved; 8.4 seconds; 4.4 seconds (RCF) sin-cos-problem-diff4b; proved; 20.8 seconds; 8.4 seconds (RCF), max weight = 1096 sin-cos-problem-diff5a; proved; 12.2 seconds; 5.6 seconds (RCF), max weight = 908 sin-cos-problem-diff5b; proved; 22.3 seconds, max weight = 1211 sin-cos-problem-Kubo-weak; timed out sin-cos-problem-Kubo; timed out sin-error-analysis-1; proved; 0.2 seconds sin-error-analysis-2; proved; 0.1 seconds sin-error-analysis-3; proved; 0.1 seconds sin-error-analysis-4; proved; 0.1 seconds sin-error-analysis-5; proved; 0.1 seconds sin-error-analysis-6; proved; 0.1 seconds sin-error-analysis-7; proved; 0.3 seconds sin-error-analysis-Intel-1; proved; 0.3 seconds sin-index-2; proved; 0.6 seconds sin-index-3-weak; proved; 0.2 seconds sin-index-3; proved; 15.8 seconds sin-problem-1-weak; proved; 1.3 seconds sin-problem-10-2-sqrt-weak; proved; 54.4 seconds, max weight = 633 sin-problem-10-2-sqrt; timed out sin-problem-10-2; timed out sin-problem-10-3-cbrt-weak; proved; 16.1 seconds, max weight = 677 sin-problem-10-3-cbrt; gave up; 2.8 seconds, max weight = 1067 sin-problem-10-3; timed out sin-problem-10; proved; 2.5 seconds sin-problem-11; proved; 0.2 seconds sin-problem-13; proved; 0.0 seconds sin-problem-14; proved; 0.0 seconds sin-problem-17-nested-fun; proved; 4.0 seconds; 3.5 seconds (RCF) sin-problem-17; proved; 3.7 seconds; 3.4 seconds (RCF) sin-problem-18-weak; proved; 0.3 seconds sin-problem-18; timed out sin-problem-1; gave up; 17.7 seconds, max weight = 1996 sin-problem-2; proved; 0.0 seconds sin-problem-3; proved; 0.0 seconds sin-problem-4-weak; proved; 1.3 seconds sin-problem-4; timed out sin-problem-5-weak; proved; 1.0 seconds sin-problem-5; gave up; 6.6 seconds; 3.7 seconds (RCF), max weight = 1117 sin-problem-6; proved; 0.0 seconds sin-problem-7-weak2; proved; 6.1 seconds; 5.9 seconds (RCF) sin-problem-7-weak; timed out sin-problem-7; timed out sin-problem-8-weak; proved; 0.7 seconds sin-problem-8; timed out sin-problem-9; proved; 0.6 seconds sin-recip-1; proved; 0.2 seconds sin-recip-2; proved; 0.2 seconds sin-recip-3; proved; 0.3 seconds sin-recip-4; proved; 0.2 seconds sqrt-1mcosq-1; proved; 0.6 seconds sqrt-1mcosq-2; proved; 0.9 seconds sqrt-1mcosq-3; proved; 0.4 seconds sqrt-1mcosq-4-weak; proved; 0.9 seconds sqrt-1mcosq-4; proved; 2.1 seconds; 2.0 seconds (RCF) sqrt-1mcosq-5-weak; proved; 0.6 seconds sqrt-1mcosq-5; proved; 3.1 seconds; 2.8 seconds (RCF) sqrt-1mcosq-6; proved; 0.1 seconds sqrt-1mcosq-7-weak; timed out sqrt-1mcosq-7; timed out sqrt-1mcosq-8-weak; proved; 2.4 seconds, max weight = 610 sqrt-1mcosq-8; timed out sqrt-circles-1; proved; 0.0 seconds sqrt-circles-2; proved; 0.0 seconds sqrt-circles-3; proved; 0.0 seconds sqrt-cos-problem-1-2vars; proved; 5.2 seconds; 3.2 seconds (RCF) sqrt-cos-problem-1; proved; 37.7 seconds; 17.1 seconds (RCF), max weight = 797 sqrt-cos-problem-2-2vars; timed out sqrt-cos-problem-2; proved; 25.3 seconds sqrt-problem-10; proved; 0.1 seconds sqrt-problem-11; proved; 0.0 seconds sqrt-problem-12; proved; 17.0 seconds, max weight = 1998 sqrt-problem-12vars2; timed out sqrt-problem-12vars3; proved; 0.4 seconds sqrt-problem-13-sqrt1; proved; 0.2 seconds sqrt-problem-13-sqrt2; proved; 0.8 seconds sqrt-problem-13-sqrt3; proved; 3.7 seconds sqrt-problem-13-vars5; proved; 0.1 seconds sqrt-problem-13; proved; 0.1 seconds sqrt-problem-1; proved; 0.1 seconds sqrt-problem-2; proved; 0.0 seconds sqrt-problem-3; proved; 0.0 seconds sqrt-problem-8; proved; 0.2 seconds sqrt-problem-Melquiond-weak; proved; 8.8 seconds sqrt-problem-Melquiond2; proved; 0.3 seconds sqrt-problem-Melquiond3; proved; 0.1 seconds sqrt-problem-Melquiond; timed out tan-1-1var-pi; proved; 0.8 seconds tan-1-1var-weak; proved; 6.2 seconds; 3.7 seconds (RCF) tan-1-1var; timed out tan-1-2var; timed out tan-2-2var-weak2; timed out tan-2-2var-weak; proved; 20.2 seconds; 19.0 seconds (RCF) tan-2-2var; proved; 29.0 seconds; 28.1 seconds (RCF) tan-3428a; proved; 0.4 seconds tan-3428b; proved; 37.4 seconds; 16.9 seconds (RCF) tan-3428c; proved; 0.1 seconds tan-3428d; proved; 8.0 seconds; 6.8 seconds (RCF) tan-3428e; proved; 0.1 seconds tan-problem-1-sin-weak; proved; 1.0 seconds tan-problem-1-sin; timed out tan-problem-1-weak; proved; 1.2 seconds tan-problem-1; gave up; 1.5 seconds, max weight = 1237 tan-problem-2; proved; 0.0 seconds tan-problem-3-weak; proved; 0.1 seconds tan-problem-3; gave up; 2.0 seconds, max weight = 1995 tan-problem-4; proved; 0.1 seconds tan-problem-5-weak; timed out tan-problem-5; timed out tan-problem-6-weak; proved; 5.3 seconds; 4.5 seconds (RCF) tan-problem-6; timed out tan-problem-7-weak; proved; 0.3 seconds tan-problem-7; gave up; 3.1 seconds, max weight = 981 tan-problem-8; proved; 0.4 seconds tan-problem-9; proved; 0.2 seconds tanh-1; proved; 0.0 seconds tanh-1b; proved; 0.1 seconds tanh-2-weak; proved; 0.1 seconds tanh-2; gave up; 8.9 seconds, max weight = 1955 tanh-3-weak; proved; 0.1 seconds tanh-3610; proved; 0.4 seconds tanh-3611; proved; 0.4 seconds tanh-3; gave up; 9.9 seconds, max weight = 1741 tanh-4-weak; proved; 0.2 seconds tanh-4; gave up; 14.6 seconds, max weight = 1998 tanh-5-2var-sinh; proved; 0.2 seconds tanh-5; proved; 0.1 seconds tanh-5b; proved; 0.8 seconds tanh-6-2var; proved; 0.9 seconds, max weight = 692 tanh-7-weak; proved; 0.1 seconds tanh-7; gave up; 25.6 seconds, max weight = 1998 tanh-8-weak2; proved; 1.1 seconds tanh-8-weak; proved; 2.6 seconds tanh-8; gave up; 7.6 seconds, max weight = 1999 tanh-9-sinh; gave up; 8.8 seconds, max weight = 1999 tanh-9-weak2; proved; 0.7 seconds tanh-9-weak; proved; 28.6 seconds trig-squared1; timed out trig-squared2; timed out trig-squared3; timed out trig-squared4; timed out trig-squared5; timed out trig-squared6; timed out trigpoly-351-1a; proved; 0.3 seconds trigpoly-351-1b; proved; 0.8 seconds trigpoly-351-2a; proved; 0.2 seconds trigpoly-351-2b; proved; 0.4 seconds trigpoly-351-3a-weak; proved; 1.7 seconds trigpoly-351-3a; gave up; 4.6 seconds, max weight = 1995 trigpoly-351-3b-weak; proved; 10.9 seconds; 6.1 seconds (RCF) trigpoly-351-3b; timed out trigpoly-3510-2; proved; 0.3 seconds trigpoly-3510-3; proved; 0.7 seconds trigpoly-3510-4; proved; 2.7 seconds trigpoly-3510-5-weak; proved; 4.0 seconds trigpoly-3510-5; gave up; 11.4 seconds, max weight = 1896 trigpoly-3512-2; proved; 4.2 seconds; 3.9 seconds (RCF) trigpoly-3512-3; proved; 2.9 seconds; 2.7 seconds (RCF) trigpoly-3512-4-weak; proved; 9.4 seconds; 8.7 seconds (RCF) trigpoly-3512-4; timed out trigpoly-3512-5-weak; proved; 10.0 seconds; 9.1 seconds (RCF) trigpoly-3512-5; timed out trigpoly-3514-2; proved; 5.6 seconds; 5.1 seconds (RCF) trigpoly-3514-3; proved; 2.7 seconds; 2.2 seconds (RCF) trigpoly-3514-4; proved; 3.3 seconds; 2.2 seconds (RCF) trigpoly-3515-2; proved; 1.2 seconds trigpoly-3515-3; proved; 3.7 seconds; 2.9 seconds (RCF) trigpoly-3515-4; proved; 2.3 seconds; 1.8 seconds (RCF) trigpoly-352-1-weak; proved; 1.2 seconds trigpoly-352-1; proved; 0.8 seconds trigpoly-352-2-weak; proved; 0.5 seconds trigpoly-352-2; timed out trigpoly-355-3; proved; 0.0 seconds trigpoly-355-4; proved; 66.3 seconds, max weight = 1999 trigpoly-355-5; timed out trigpoly-355-6; timed out trigpoly-356-3a-sin2x; proved; 49.4 seconds; 42.1 seconds (RCF) trigpoly-356-3a; proved; 0.1 seconds trigpoly-356-3b-sin2x; proved; 23.5 seconds; 18.5 seconds (RCF) trigpoly-356-3b; proved; 0.1 seconds trigpoly-356-4a-sin2x; timed out trigpoly-356-4a; proved; 0.1 seconds trigpoly-356-4b-sin2x; timed out trigpoly-356-4b; proved; 0.5 seconds trigpoly-356-5a-pi; timed out trigpoly-356-5a; proved; 0.6 seconds trigpoly-356-5b-pi; timed out trigpoly-356-5b; proved; 0.8 seconds trigpoly-356-6a-pi; timed out trigpoly-356-6a; proved; 1.0 seconds trigpoly-356-6b-pi; timed out trigpoly-356-6b; proved; 0.8 seconds trigpoly-357-3-sqrt; proved; 0.4 seconds trigpoly-357-3; proved; 0.7 seconds trigpoly-357-5-sqrt; proved; 0.7 seconds trigpoly-357-5; proved; 1.0 seconds trigpoly-359-2-weak; proved; 25.3 seconds trigpoly-359-2; proved; 26.6 seconds trigpoly-359-3-weak; proved; 0.6 seconds trigpoly-359-3; timed out Tunnel-1-IL-L; proved; 0.1 seconds Tunnel-1-IL-U; proved; 0.1 seconds Tunnel-1-IL; proved; 0.1 seconds Tunnel-1-VC-L; proved; 0.1 seconds Tunnel-1-VC-U; proved; 0.1 seconds Tunnel-2-IL-L; proved; 0.6 seconds Tunnel-2-IL-U; proved; 0.1 seconds Tunnel-2-IL; proved; 0.4 seconds Tunnel-2-VC-L; proved; 0.1 seconds Tunnel-2-VC-U; proved; 0.3 seconds Tunnel-3-IL-L; proved; 0.1 seconds Tunnel-3-IL-U; proved; 0.1 seconds Tunnel-3-IL; proved; 0.1 seconds Tunnel-3-VC-L; proved; 0.1 seconds Tunnel-3-VC-U; proved; 0.1 seconds two-variable-problem-1; proved; 0.1 seconds two-variable-problem-2; proved; 0.0 seconds two-variable-problem-3-weak2; timed out two-variable-problem-3-weak; timed out two-variable-problem-3; timed out two-variable-problem-6; proved; 0.0 seconds two-variable-problem-7-weak; timed out two-variable-problem-7; timed out two-variable-problem-9; proved; 0.1 seconds X1-cosh; ERROR; 0.0 seconds X1-exp2; ERROR; 0.0 seconds X1-exp2r; ERROR; 0.0 seconds X1-exp; ERROR; 0.0 seconds X1-ln; ERROR; 0.0 seconds X1-sin2; ERROR; 0.0 seconds X1-sin; ERROR; 0.0 seconds X1-sincos; ERROR; 0.0 seconds X1-sinh; ERROR; 0.0 seconds X1-tan; ERROR; 0.0 seconds X1; gave up; 33.4 seconds, max weight = 1993 X1b-ln2; ERROR; 0.0 seconds X1b-ln; ERROR; 0.0 seconds X1s-sin2; ERROR; 0.0 seconds X1s-sin; ERROR; 0.0 seconds X1s-tan; timed out X2-cosh; ERROR; 0.0 seconds X2-exp2; ERROR; 0.0 seconds X2-exp3; ERROR; 0.0 seconds X2-exp4; ERROR; 0.0 seconds X2-exp5; ERROR; 0.0 seconds X2-exp6; ERROR; 0.0 seconds X2-exp; ERROR; 0.0 seconds X2-ln2; ERROR; 0.0 seconds X2-ln3; ERROR; 0.0 seconds X2-ln4; ERROR; 0.0 seconds X2-ln5; ERROR; 0.0 seconds X2-ln6; ERROR; 0.0 seconds X2-ln; ERROR; 0.0 seconds X2-sinh2; ERROR; 0.0 seconds X2-sinh; ERROR; 0.0 seconds X2-tan; ERROR; 0.0 seconds X2; gave up; 2.0 seconds, max weight = 1991 X2b-ln; ERROR; 0.0 seconds X3-exp2; ERROR; 0.0 seconds X3-exp; ERROR; 0.0 seconds X3; ERROR; 0.0 seconds X3a; ERROR; 0.0 seconds X3b; ERROR; 0.0 seconds Maximum weight in successful proofs: 1999 Total cputime for proofs: 2370.5; 1133.8 (RCF) Maximum cputime: 81.0 Proved 673 problems out of 887 or 75 percent Summary of failures: Gave Up, 44; Timed Out, 134; Error, 36 Elapsed time 1:04:25