### uname -a: Linux clpc8.cs.ox.ac.uk 2.6.34.7-56.fc13.x86_64 #1 SMP Wed Sep 15 03:36:55 UTC 2010 x86_64 x86_64 x86_64 GNU/Linux ### cat /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 0 cpu cores : 4 apicid : 0 initial apicid : 0 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5653.20 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 1 cpu cores : 4 apicid : 1 initial apicid : 1 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.19 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 2 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 2 cpu cores : 4 apicid : 2 initial apicid : 2 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.20 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 3 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 3 cpu cores : 4 apicid : 3 initial apicid : 3 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.21 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: ### cat /proc/meminfo: MemTotal: 3891428 kB MemFree: 1315584 kB Buffers: 78276 kB Cached: 2067460 kB SwapCached: 0 kB Active: 1123960 kB Inactive: 1133344 kB Active(anon): 49100 kB Inactive(anon): 108000 kB Active(file): 1074860 kB Inactive(file): 1025344 kB Unevictable: 0 kB Mlocked: 0 kB SwapTotal: 12586892 kB SwapFree: 12586892 kB Dirty: 2388 kB Writeback: 0 kB AnonPages: 111636 kB Mapped: 21012 kB Shmem: 45504 kB Slab: 179576 kB SReclaimable: 156680 kB SUnreclaim: 22896 kB KernelStack: 2168 kB PageTables: 13992 kB NFS_Unstable: 0 kB Bounce: 0 kB WritebackTmp: 0 kB CommitLimit: 14532604 kB Committed_AS: 522948 kB VmallocTotal: 34359738367 kB VmallocUsed: 385656 kB VmallocChunk: 34359345788 kB HardwareCorrupted: 0 kB HugePages_Total: 0 HugePages_Free: 0 HugePages_Rsvd: 0 HugePages_Surp: 0 Hugepagesize: 2048 kB DirectMap4k: 10236 kB DirectMap2M: 4016128 kB ### date: Thu Oct 13 20:01:28 BST 2011 ### user: mictau ### ulimit -a: core file size (blocks, -c) 0 data seg size (kbytes, -d) unlimited scheduling priority (-e) 0 file size (blocks, -f) unlimited pending signals (-i) 30273 max locked memory (kbytes, -l) 64 max memory size (kbytes, -m) unlimited open files (-n) 1024 pipe size (512 bytes, -p) 8 POSIX message queues (bytes, -q) 819200 real-time priority (-r) 0 stack size (kbytes, -s) 10240 cpu time (seconds, -t) unlimited max user processes (-u) 1024 virtual memory (kbytes, -v) 3584000 file locks (-x) unlimited ### timeout: timeout -s SIGINT 3600 ### tool version info: USAGE: ./ai .c Options: ------- GENERAL OPTIONS --help Display this message --show-symbol-table --show-goto-functions --show-cfg --function Set function f as main function --invariants Display analysis result (invariants) --print-assignments Display analysis result (effects of assignments) --block-inv-output Do not output invariants containing certain expressions ------- PREPROCESSING AND TRANSFORMATIONS --inline Inline function calls --preprocess-const-prop Preprocess CFG with constant propagation --preprocess-expr-prop Preprocess CFG with expression propagation --unwind Unwind each loop n times --remove-pointers Perform pointer analysis --unwind Unwind all loops n times ------- ANALYSIS OPTIONS --widening k Perform widening after k loop iterations --unsound-nan Ignore NaN in arithmetic, e.g. 0 * infinity = 0 --rounding-mode Set rounding mode for FP --diseq-itv Disequalities+intervals ------- ABSTRACT DOMAINS --box Apron box domain --polyhedra Apron polyhedra --octagon Apron octacgon --strict-polyhedra Apron strict polyhedra --disequality Equality/disquality domain --intervals Intervals (non-apron) --itv-arrays Intervals + arrays (default) --max-array-size Maximum size of arrays that are emulated --arr-diseq-itv Disequalities+intervals+arrays --const-prop Constant propagation domain --expr-prop Expression propagation domain ------- OTHER --proof-growing Use proof growing analysis ========== CONFLICT DRIVEN FIXED POINT LEARNING --proof-search Enable conflict driven fixed point learning --set-var-range v1,min1,max1,v2,min2,max2,... Set range of initial variables --filter-dec-vars Only use var as decision vars whose identifier contains --iteration-limit Quit after iterations --dec-heur-berkmin Berkmin + random decision heuristic --dec-heur-range-rel Split on largest range (relative to initial range) --dec-heur-range Split on largest range (relative to max type range) --dec-heur-rand Split randomly (default) --nr-splits Reduce range to 1/(2^(n-1)) at each decision --disable-learning Use clauses for backjumping but never apply unit rule --disable-backjumping No learning, no non-chronological backtracking --additional-clauses Provide additional clauses in file f (untested) ------- EXPERIMENTAL CBMC / CDFPL INTEGRATION --bmc-thresh Set range of variables at which bmc is called (switched off by default) --bmc-thresh-rel Use range relative to initial range --bmc-on-backtrack Only call BMC after backtrack ### tool command: /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/cdfpl --inline --filter-dec-vars IN --proof-search ### full command line: /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/cdfpl --inline --filter-dec-vars IN --proof-search /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/goubault-sas06/Poly.0.0.i ### expected verification result: unknown ############################################################################### file /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/goubault-sas06/Poly.0.0.i: Parsing Converting Type-checking Poly.0.0 Generating GOTO Program Function Pointer Removal got goto-program CFG has 30 nodes Obtaining loops ... done setting widening to 10 finding unnecessary nodes ... found 4 unnecessary nodes ITERATION (decision) 0 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, inf] } new dlevel: 1 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -0] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 1 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -0] } new dlevel: 2 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -1.7014117332e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 2 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -1.7014117332e+38] } new dlevel: 3 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -2.5521175491e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 3 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -2.5521175491e+38] } new dlevel: 4 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -2.9774705077e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 4 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -2.9774705077e+38] } new dlevel: 5 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.1901469871e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 5 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.1901469871e+38] } new dlevel: 6 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.2964852267e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 6 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.2964852267e+38] } new dlevel: 7 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3496543466e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 7 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3496543466e+38] } new dlevel: 8 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3762389065e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 8 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3762389065e+38] } new dlevel: 9 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3895311864e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 9 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3895311864e+38] } new dlevel: 10 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3961773264e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 10 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3961773264e+38] } new dlevel: 11 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3995003964e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 11 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3995003964e+38] } new dlevel: 12 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4011619314e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 12 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4011619314e+38] } new dlevel: 13 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4019926989e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 13 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4019926989e+38] } new dlevel: 14 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4024080826e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 14 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4024080826e+38] } new dlevel: 15 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4026157745e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 15 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4026157745e+38] } new dlevel: 16 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4027196204e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 16 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4027196204e+38] } new dlevel: 17 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4027715434e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 17 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4027715434e+38] } new dlevel: 18 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4027975049e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 18 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4027975049e+38] } new dlevel: 19 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028104856e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 19 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028104856e+38] } new dlevel: 20 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.402816976e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 20 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.402816976e+38] } new dlevel: 21 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028202212e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 21 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028202212e+38] } new dlevel: 22 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028218438e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 22 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028218438e+38] } new dlevel: 23 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028226551e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 23 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028226551e+38] } new dlevel: 24 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028230607e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 24 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028230607e+38] } new dlevel: 25 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028232636e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 25 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028232636e+38] } new dlevel: 26 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028234664e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 26 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028234664e+38] } new dlevel: 27 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -inf] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 27 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 28 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -0] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 28 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -0], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 29 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -1.7014117332e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 29 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -1.7014117332e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 30 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -2.5521175491e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 30 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -2.5521175491e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 31 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -2.9774705077e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 31 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -2.9774705077e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 32 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.1901469871e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 32 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.1901469871e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 33 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.2964852267e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 33 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.2964852267e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 34 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3496543466e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 34 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3496543466e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 35 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3762389065e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 35 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3762389065e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 36 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3895311864e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 36 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3895311864e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 37 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3961773264e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 37 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3961773264e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 38 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3995003964e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 38 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3995003964e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 39 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4011619314e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 39 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4011619314e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 40 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4019926989e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 40 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4019926989e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 41 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4024080826e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 41 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4024080826e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 42 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4026157745e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 42 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4026157745e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 43 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4027196204e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 43 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4027196204e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 44 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4027715434e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 44 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4027715434e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 45 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4027975049e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 45 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4027975049e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 46 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028104856e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 46 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028104856e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 47 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.402816976e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 47 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.402816976e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 48 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028202212e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 48 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028202212e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 49 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028218438e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 49 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028218438e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 50 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028226551e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 50 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028226551e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 51 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028230607e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 51 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028230607e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 52 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028232636e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 52 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028232636e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 53 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028234664e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 53 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028234664e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 54 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -inf] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 54 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 55 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -0] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 55 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -0], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 56 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -1.7014117332e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 56 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -1.7014117332e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 57 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -2.5521175491e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 57 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -2.5521175491e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 58 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -2.9774705077e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 58 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -2.9774705077e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 59 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.1901469871e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 59 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.1901469871e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 60 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.2964852267e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 60 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.2964852267e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 61 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3496543466e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 61 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3496543466e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 62 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3762389065e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 62 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3762389065e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 63 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3895311864e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 63 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3895311864e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 64 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3961773264e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 64 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3961773264e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 65 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3995003964e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 65 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3995003964e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 66 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4011619314e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 66 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4011619314e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 67 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4019926989e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 67 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4019926989e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 68 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4024080826e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 68 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4024080826e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 69 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4026157745e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 69 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4026157745e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 70 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4027196204e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 70 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4027196204e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 71 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4027715434e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 71 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4027715434e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 72 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4027975049e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 72 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4027975049e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 73 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028104856e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 73 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028104856e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 74 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.402816976e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 74 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.402816976e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 75 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028202212e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 75 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028202212e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 76 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028218438e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 76 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028218438e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 77 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028226551e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 77 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028226551e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 78 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028230607e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 78 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028230607e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 79 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028232636e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 79 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028232636e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 80 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028234664e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 80 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028234664e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 81 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -inf] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 81 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 82 scores: 1 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [-inf, -0] because of -1 SUCCESSFULLY PROVEN CASE Global generalization: 43 steps, 0.03s (0.000697674s/step) REASON: c::$file::__BUILTIN_DAED_FBETWEEN::1::f [-inf, -0], CONFLICT CLAUSE = { (c::$file::__BUILTIN_DAED_FBETWEEN::1::f,[1.4012984643e-45, inf]) } searching for uip (c::$file::__BUILTIN_DAED_FBETWEEN::1::f,[1.4012984643e-45, inf]) is incompatible with [-inf, -0] at level 82 using generalized lit as negated uip: (c::$file::__BUILTIN_DAED_FBETWEEN::1::f,[1.4012984643e-45, inf]) ADDED CLAUSE: (c::$file::__BUILTIN_DAED_FBETWEEN::1::f,[1.4012984643e-45, inf]) backtrack to dlevel: 0 CLAUSE IS UNIT ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, inf] because of 0 ITERATION (backtrack) 82 ================ ITERATION (decision) 83 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, inf] } new dlevel: 1 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -0] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 84 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -0] } new dlevel: 2 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -1.7014117332e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 85 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -1.7014117332e+38] } new dlevel: 3 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -2.5521175491e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 86 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -2.5521175491e+38] } new dlevel: 4 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -2.9774705077e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 87 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -2.9774705077e+38] } new dlevel: 5 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.1901469871e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 88 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.1901469871e+38] } new dlevel: 6 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.2964852267e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 89 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.2964852267e+38] } new dlevel: 7 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3496543466e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 90 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3496543466e+38] } new dlevel: 8 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3762389065e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 91 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3762389065e+38] } new dlevel: 9 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3895311864e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 92 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3895311864e+38] } new dlevel: 10 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3961773264e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 93 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3961773264e+38] } new dlevel: 11 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.3995003964e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 94 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.3995003964e+38] } new dlevel: 12 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4011619314e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 95 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4011619314e+38] } new dlevel: 13 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4019926989e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 96 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4019926989e+38] } new dlevel: 14 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4024080826e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 97 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4024080826e+38] } new dlevel: 15 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4026157745e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 98 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4026157745e+38] } new dlevel: 16 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4027196204e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 99 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4027196204e+38] } new dlevel: 17 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4027715434e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 100 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4027715434e+38] } new dlevel: 18 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4027975049e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 101 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4027975049e+38] } new dlevel: 19 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028104856e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 102 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028104856e+38] } new dlevel: 20 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.402816976e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 103 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.402816976e+38] } new dlevel: 21 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028202212e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 104 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028202212e+38] } new dlevel: 22 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028218438e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 105 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028218438e+38] } new dlevel: 23 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028226551e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 106 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028226551e+38] } new dlevel: 24 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028230607e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 107 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028230607e+38] } new dlevel: 25 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028232636e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 108 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028232636e+38] } new dlevel: 26 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -3.4028234664e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 109 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -3.4028234664e+38] } new dlevel: 27 scores: 1 1 1 1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::u to [-inf, -inf] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 110 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 28 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -0] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 111 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -0], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 29 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -1.7014117332e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 112 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -1.7014117332e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 30 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -2.5521175491e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 113 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -2.5521175491e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 31 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -2.9774705077e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 114 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -2.9774705077e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 32 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.1901469871e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 115 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.1901469871e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 33 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.2964852267e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 116 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.2964852267e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 34 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3496543466e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 117 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3496543466e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 35 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3762389065e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 118 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3762389065e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 36 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3895311864e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 119 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3895311864e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 37 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3961773264e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 120 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3961773264e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 38 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.3995003964e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 121 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.3995003964e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 39 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4011619314e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 122 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4011619314e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 40 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4019926989e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 123 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4019926989e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 41 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4024080826e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 124 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4024080826e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 42 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4026157745e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 125 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4026157745e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 43 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4027196204e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 126 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4027196204e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 44 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4027715434e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 127 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4027715434e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 45 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4027975049e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 128 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4027975049e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 46 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028104856e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 129 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028104856e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 47 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.402816976e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 130 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.402816976e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 48 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028202212e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 131 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028202212e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 49 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028218438e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 132 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028218438e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 50 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028226551e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 133 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028226551e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 51 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028230607e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 134 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028230607e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 52 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028232636e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 135 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028232636e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 53 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -3.4028234664e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 136 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -3.4028234664e+38], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 54 scores: 1 1 1 -1 ASSIGN c::$file::main::1::IN_x to [-inf, -inf] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 137 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 55 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -0] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 138 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -0], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 56 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -1.7014117332e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 139 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -1.7014117332e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 57 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -2.5521175491e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 140 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -2.5521175491e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 58 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -2.9774705077e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 141 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -2.9774705077e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 59 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.1901469871e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 142 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.1901469871e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 60 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.2964852267e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 143 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.2964852267e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 61 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3496543466e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 144 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3496543466e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 62 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3762389065e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 145 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3762389065e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 63 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3895311864e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 146 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3895311864e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 64 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3961773264e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 147 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3961773264e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 65 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.3995003964e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 148 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.3995003964e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 66 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4011619314e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 149 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4011619314e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 67 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4019926989e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 150 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4019926989e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 68 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4024080826e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 151 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4024080826e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 69 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4026157745e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 152 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4026157745e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 70 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4027196204e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 153 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4027196204e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 71 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4027715434e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 154 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4027715434e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 72 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4027975049e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 155 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4027975049e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 73 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028104856e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 156 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028104856e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 74 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.402816976e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 157 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.402816976e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 75 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028202212e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 158 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028202212e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 76 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028218438e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 159 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028218438e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 77 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028226551e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 160 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028226551e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 78 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028230607e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 161 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028230607e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 79 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028232636e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 162 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028232636e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 80 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -3.4028234664e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 163 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -3.4028234664e+38], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 81 scores: 1 1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::l to [-inf, -inf] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 164 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, inf], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 82 scores: 1 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.7014117332e+38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 165 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.7014117332e+38], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 83 scores: 0.5 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.507058666e+37] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 166 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.507058666e+37], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 84 scores: 0.25 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.253529333e+37] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 167 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.253529333e+37], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 85 scores: 0.125 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.1267646665e+37] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 168 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.1267646665e+37], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 86 scores: 0.0625 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.0633823332e+37] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 169 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.0633823332e+37], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 87 scores: 0.03125 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.3169116662e+36] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 170 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.3169116662e+36], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 88 scores: 0.015625 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.6584558331e+36] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 171 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.6584558331e+36], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 89 scores: 0.0078125 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.3292279166e+36] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 172 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.3292279166e+36], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 90 scores: 0.00390625 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.6461395828e+35] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 173 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.6461395828e+35], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 91 scores: 0.00195312 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.3230697914e+35] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 174 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.3230697914e+35], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 92 scores: 0.000976562 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.6615348957e+35] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 175 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.6615348957e+35], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 93 scores: 0.000488281 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.3076744785e+34] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 176 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.3076744785e+34], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 94 scores: 0.000244141 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.1538372392e+34] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 177 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.1538372392e+34], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 95 scores: 0.00012207 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.0769186196e+34] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 178 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.0769186196e+34], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 96 scores: 6.10352e-05 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.0384593098e+34] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 179 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.0384593098e+34], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 97 scores: 3.05176e-05 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.192296549e+33] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 180 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.192296549e+33], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 98 scores: 1.52588e-05 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.5961482745e+33] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 181 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.5961482745e+33], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 99 scores: 7.62939e-06 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2980741373e+33] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 182 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2980741373e+33], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 100 scores: 3.8147e-06 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.4903706863e+32] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 183 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.4903706863e+32], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 101 scores: 1.90735e-06 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.2451853432e+32] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 184 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.2451853432e+32], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 102 scores: 9.53674e-07 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.6225926716e+32] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 185 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.6225926716e+32], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 103 scores: 4.76837e-07 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.1129633579e+31] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 186 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.1129633579e+31], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 104 scores: 2.38419e-07 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.0564816789e+31] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 187 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.0564816789e+31], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 105 scores: 1.19209e-07 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.0282408395e+31] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 188 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.0282408395e+31], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 106 scores: 5.96046e-08 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.0141204197e+31] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 189 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.0141204197e+31], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 107 scores: 2.98023e-08 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.0706020987e+30] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 190 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.0706020987e+30], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 108 scores: 1.49012e-08 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.5353010493e+30] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 191 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.5353010493e+30], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 109 scores: 7.45058e-09 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2676505247e+30] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 192 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2676505247e+30], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 110 scores: 3.72529e-09 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.3382526234e+29] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 193 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.3382526234e+29], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 111 scores: 1.86265e-09 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.1691263117e+29] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 194 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.1691263117e+29], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 112 scores: 9.31323e-10 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.5845631558e+29] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 195 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.5845631558e+29], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 113 scores: 4.65661e-10 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.9228157792e+28] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 196 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.9228157792e+28], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 114 scores: 2.32831e-10 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.9614078896e+28] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 197 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.9614078896e+28], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 115 scores: 1.16415e-10 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.9807039448e+28] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 198 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.9807039448e+28], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 116 scores: 5.82077e-11 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.903519724e+27] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 199 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.903519724e+27], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 117 scores: 2.91038e-11 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.951759862e+27] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 200 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.951759862e+27], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 118 scores: 1.45519e-11 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.475879931e+27] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 201 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.475879931e+27], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 119 scores: 7.27596e-12 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2379399655e+27] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 202 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2379399655e+27], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 120 scores: 3.63798e-12 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.1896998275e+26] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 203 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.1896998275e+26], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 121 scores: 1.81899e-12 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.0948499137e+26] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 204 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.0948499137e+26], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 122 scores: 9.09495e-13 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.5474249569e+26] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 205 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.5474249569e+26], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 123 scores: 4.54747e-13 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.7371247844e+25] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 206 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.7371247844e+25], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 124 scores: 2.27374e-13 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.8685623922e+25] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 207 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.8685623922e+25], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 125 scores: 1.13687e-13 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.9342811961e+25] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 208 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.9342811961e+25], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 126 scores: 5.68434e-14 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.6714059805e+24] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 209 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.6714059805e+24], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 127 scores: 2.84217e-14 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.8357029902e+24] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 210 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.8357029902e+24], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 128 scores: 1.42109e-14 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.4178514951e+24] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 211 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.4178514951e+24], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 129 scores: 7.10543e-15 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2089257476e+24] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 212 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2089257476e+24], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 130 scores: 3.55271e-15 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.0446287378e+23] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 213 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.0446287378e+23], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 131 scores: 1.77636e-15 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.0223143689e+23] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 214 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.0223143689e+23], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 132 scores: 8.88178e-16 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.5111571844e+23] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 215 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.5111571844e+23], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 133 scores: 4.44089e-16 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.5557859222e+22] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 216 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.5557859222e+22], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 134 scores: 2.22045e-16 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.7778929611e+22] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 217 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.7778929611e+22], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 135 scores: 1.11022e-16 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.8889464806e+22] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 218 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.8889464806e+22], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 136 scores: 5.55112e-17 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.4447324028e+21] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 219 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.4447324028e+21], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 137 scores: 2.77556e-17 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.7223662014e+21] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 220 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.7223662014e+21], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 138 scores: 1.38778e-17 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.3611831007e+21] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 221 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.3611831007e+21], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 139 scores: 6.93889e-18 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.1805915503e+21] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 222 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.1805915503e+21], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 140 scores: 3.46945e-18 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.9029577517e+20] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 223 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.9029577517e+20], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 141 scores: 1.73472e-18 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.9514788759e+20] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 224 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.9514788759e+20], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 142 scores: 8.67362e-19 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4757394379e+20] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 225 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4757394379e+20], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 143 scores: 4.33681e-19 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.3786971897e+19] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 226 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.3786971897e+19], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 144 scores: 2.1684e-19 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.6893485948e+19] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 227 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.6893485948e+19], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 145 scores: 1.0842e-19 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.8446742974e+19] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 228 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.8446742974e+19], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 146 scores: 5.42101e-20 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.2233714871e+18] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 229 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.2233714871e+18], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 147 scores: 2.71051e-20 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.6116857435e+18] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 230 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.6116857435e+18], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 148 scores: 1.35525e-20 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.3058428718e+18] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 231 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.3058428718e+18], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 149 scores: 6.77626e-21 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.1529214359e+18] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 232 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.1529214359e+18], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 150 scores: 3.38813e-21 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.7646071794e+17] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 233 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.7646071794e+17], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 151 scores: 1.69407e-21 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.8823035897e+17] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 234 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.8823035897e+17], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 152 scores: 8.47033e-22 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4411517949e+17] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 235 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4411517949e+17], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 153 scores: 4.23516e-22 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.2057589743e+16] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 236 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.2057589743e+16], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 154 scores: 2.11758e-22 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.6028794871e+16] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 237 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.6028794871e+16], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 155 scores: 1.05879e-22 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.8014397436e+16] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 238 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.8014397436e+16], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 156 scores: 5.29396e-23 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.0071987179e+15] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 239 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.0071987179e+15], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 157 scores: 2.64698e-23 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.5035993589e+15] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 240 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.5035993589e+15], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 158 scores: 1.32349e-23 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.2517996795e+15] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 241 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.2517996795e+15], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 159 scores: 6.61744e-24 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.1258998397e+15] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 242 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.1258998397e+15], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 160 scores: 3.30872e-24 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.6294991987e+14] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 243 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.6294991987e+14], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 161 scores: 1.65436e-24 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.8147495993e+14] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 244 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.8147495993e+14], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 162 scores: 8.27181e-25 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4073747997e+14] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 245 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4073747997e+14], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 163 scores: 4.1359e-25 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.0368739983e+13] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 246 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.0368739983e+13], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 164 scores: 2.06795e-25 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.5184369992e+13] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 247 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.5184369992e+13], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 165 scores: 1.03398e-25 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.7592184996e+13] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 248 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.7592184996e+13], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 166 scores: 5.16988e-26 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.7960924979e+12] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 249 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.7960924979e+12], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 167 scores: 2.58494e-26 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.398046249e+12] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 250 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.398046249e+12], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 168 scores: 1.29247e-26 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.1990231245e+12] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 251 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.1990231245e+12], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 169 scores: 6.46235e-27 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.0995115622e+12] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 252 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.0995115622e+12], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 170 scores: 3.23117e-27 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.4975578112e+11] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 253 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.4975578112e+11], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 171 scores: 1.61559e-27 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.7487789056e+11] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 254 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.7487789056e+11], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 172 scores: 8.07794e-28 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.3743894528e+11] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 255 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.3743894528e+11], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 173 scores: 4.03897e-28 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 68719472640] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 256 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 68719472640], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 174 scores: 2.01948e-28 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 34359736320] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 257 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 34359736320], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 175 scores: 1.00974e-28 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 17179868160] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 258 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 17179868160], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 176 scores: 5.04871e-29 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8589934080] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 259 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8589934080], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 177 scores: 2.52435e-29 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4294967040] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 260 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4294967040], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 178 scores: 1.26218e-29 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2147483520] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 261 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2147483520], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 179 scores: 6.31089e-30 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1073741760] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 262 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1073741760], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 180 scores: 3.15544e-30 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 536870880] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 263 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 536870880], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 181 scores: 1.57772e-30 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 268435440] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 264 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 268435440], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 182 scores: 7.88861e-31 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 134217720] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 265 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 134217720], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 183 scores: 3.9443e-31 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 67108860] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 266 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 67108860], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 184 scores: 1.97215e-31 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 33554430] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 267 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 33554430], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 185 scores: 9.86076e-32 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 16777215] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 268 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 16777215], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 186 scores: 4.93038e-32 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8388607.5] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 269 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8388607.5], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 187 scores: 2.46519e-32 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4194303.75] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 270 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4194303.75], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 188 scores: 1.2326e-32 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2097151.875] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 271 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2097151.875], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 189 scores: 6.16298e-33 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1048575.9375] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 272 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1048575.9375], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 190 scores: 3.08149e-33 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 524287.96875] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 273 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 524287.96875], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 191 scores: 1.54074e-33 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 262143.98438] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 274 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 262143.98438], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 192 scores: 7.70372e-34 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 131071.99219] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 275 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 131071.99219], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 193 scores: 3.85186e-34 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 65535.996094] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 276 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 65535.996094], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 194 scores: 1.92593e-34 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 32767.998047] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 277 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 32767.998047], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 195 scores: 9.62965e-35 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 16383.999023] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 278 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 16383.999023], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 196 scores: 4.81482e-35 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8191.9995117] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 279 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8191.9995117], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 197 scores: 2.40741e-35 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4095.9997559] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 280 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4095.9997559], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 198 scores: 1.20371e-35 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2047.9998779] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 281 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2047.9998779], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 199 scores: 6.01853e-36 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1023.999939] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 282 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1023.999939], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 200 scores: 3.00927e-36 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 511.99996948] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 283 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 511.99996948], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 201 scores: 1.50463e-36 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 255.99998474] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 284 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 255.99998474], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 202 scores: 7.52316e-37 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 127.99999237] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 285 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 127.99999237], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 203 scores: 3.76158e-37 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 63.999996185] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 286 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 63.999996185], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 204 scores: 1.88079e-37 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 31.999998093] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 287 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 31.999998093], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 205 scores: 9.40395e-38 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 15.999999046] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 288 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 15.999999046], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 206 scores: 4.70198e-38 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.9999995232] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 289 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.9999995232], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 207 scores: 2.35099e-38 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.9999997616] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 290 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.9999997616], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 208 scores: 1.17549e-38 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.9999998808] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 291 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.9999998808], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 209 scores: 5.87747e-39 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.9999999404] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 292 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.9999999404], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 210 scores: 2.93874e-39 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.4999999702] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 293 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.4999999702], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 211 scores: 1.46937e-39 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.2499999851] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 294 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.2499999851], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 212 scores: 7.34684e-40 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.12499999255] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 295 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.12499999255], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 213 scores: 3.67342e-40 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.062499996275] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 296 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.062499996275], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 214 scores: 1.83671e-40 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.031249998137] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 297 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.031249998137], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 215 scores: 9.18355e-41 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.015624999069] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 298 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.015624999069], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 216 scores: 4.59177e-41 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.0078124995343] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 299 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.0078124995343], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 217 scores: 2.29589e-41 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.0039062497672] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 300 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.0039062497672], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 218 scores: 1.14794e-41 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.0019531248836] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 301 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.0019531248836], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 219 scores: 5.73972e-42 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.00097656244179] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 302 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.00097656244179], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 220 scores: 2.86986e-42 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.0004882812209] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 303 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.0004882812209], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 221 scores: 1.43493e-42 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.00024414061045] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 304 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.00024414061045], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 222 scores: 7.17465e-43 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 0.00012207030522] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 305 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 0.00012207030522], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 223 scores: 3.58732e-43 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.1035152612e-05] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 306 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.1035152612e-05], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 224 scores: 1.79366e-43 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.0517576306e-05] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 307 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.0517576306e-05], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 225 scores: 8.96831e-44 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.5258788153e-05] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 308 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.5258788153e-05], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 226 scores: 4.48416e-44 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.6293940765e-06] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 309 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.6293940765e-06], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 227 scores: 2.24208e-44 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.8146970383e-06] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 310 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.8146970383e-06], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 228 scores: 1.12104e-44 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.9073485191e-06] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 311 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.9073485191e-06], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 229 scores: 5.60519e-45 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.5367425956e-07] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 312 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.5367425956e-07], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 230 scores: 2.8026e-45 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.7683712978e-07] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 313 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.7683712978e-07], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 231 scores: 1.4013e-45 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.3841856489e-07] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 314 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.3841856489e-07], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 232 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.1920928245e-07] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 315 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.1920928245e-07], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 233 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.9604641223e-08] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 316 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.9604641223e-08], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 234 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.9802320611e-08] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 317 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.9802320611e-08], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 235 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4901160306e-08] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 318 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4901160306e-08], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 236 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.4505801528e-09] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 319 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.4505801528e-09], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 237 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.7252900764e-09] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 320 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.7252900764e-09], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 238 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.8626450382e-09] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 321 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.8626450382e-09], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 239 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.313225191e-10] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 322 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.313225191e-10], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 240 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.6566125955e-10] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 323 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.6566125955e-10], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 241 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.3283062978e-10] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 324 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.3283062978e-10], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 242 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.1641531489e-10] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 325 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.1641531489e-10], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 243 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.8207657444e-11] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 326 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.8207657444e-11], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 244 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.9103828722e-11] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 327 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.9103828722e-11], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 245 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4551914361e-11] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 328 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4551914361e-11], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 246 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.2759571805e-12] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 329 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.2759571805e-12], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 247 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.6379785903e-12] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 330 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.6379785903e-12], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 248 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.8189892951e-12] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 331 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.8189892951e-12], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 249 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.0949464756e-13] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 332 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.0949464756e-13], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 250 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.5474732378e-13] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 333 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.5474732378e-13], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 251 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.2737366189e-13] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 334 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.2737366189e-13], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 252 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.1368683095e-13] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 335 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.1368683095e-13], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 253 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.6843415473e-14] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 336 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.6843415473e-14], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 254 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.8421707736e-14] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 337 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.8421707736e-14], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 255 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4210853868e-14] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 338 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4210853868e-14], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 256 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.1054269341e-15] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 339 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.1054269341e-15], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 257 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.552713467e-15] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 340 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.552713467e-15], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 258 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.7763567335e-15] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 341 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.7763567335e-15], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 259 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.8817836676e-16] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 342 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.8817836676e-16], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 260 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.4408918338e-16] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 343 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.4408918338e-16], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 261 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.2204459169e-16] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 344 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.2204459169e-16], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 262 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.1102229585e-16] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 345 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.1102229585e-16], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 263 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.5511147923e-17] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 346 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.5511147923e-17], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 264 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.7755573961e-17] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 347 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.7755573961e-17], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 265 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.3877786981e-17] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 348 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.3877786981e-17], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 266 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.9388934903e-18] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 349 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.9388934903e-18], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 267 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.4694467452e-18] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 350 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.4694467452e-18], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 268 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.7347233726e-18] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 351 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.7347233726e-18], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 269 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.6736168629e-19] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 352 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.6736168629e-19], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 270 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.3368084314e-19] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 353 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.3368084314e-19], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 271 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.1684042157e-19] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 354 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.1684042157e-19], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 272 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.0842021079e-19] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 355 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.0842021079e-19], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 273 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.4210105393e-20] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 356 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.4210105393e-20], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 274 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.7105052697e-20] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 357 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.7105052697e-20], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 275 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.3552526348e-20] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 358 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.3552526348e-20], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 276 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.7762631741e-21] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 359 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.7762631741e-21], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 277 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.3881315871e-21] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 360 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.3881315871e-21], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 278 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.6940657935e-21] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 361 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.6940657935e-21], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 279 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.4703289677e-22] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 362 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.4703289677e-22], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 280 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.2351644838e-22] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 363 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.2351644838e-22], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 281 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.1175822419e-22] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 364 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.1175822419e-22], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 282 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.058791121e-22] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 365 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.058791121e-22], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 283 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.2939556048e-23] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 366 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.2939556048e-23], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 284 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.6469778024e-23] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 367 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.6469778024e-23], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 285 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.3234889012e-23] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 368 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.3234889012e-23], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 286 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.617444506e-24] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 369 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.617444506e-24], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 287 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.308722253e-24] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 370 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.308722253e-24], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 288 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.6543611265e-24] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 371 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.6543611265e-24], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 289 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.2718056325e-25] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 372 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.2718056325e-25], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 290 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.1359028162e-25] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 373 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.1359028162e-25], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 291 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.0679514081e-25] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 374 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.0679514081e-25], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 292 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.0339757041e-25] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 375 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.0339757041e-25], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 293 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.1698785203e-26] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 376 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.1698785203e-26], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 294 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.5849392602e-26] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 377 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.5849392602e-26], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 295 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2924696301e-26] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 378 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2924696301e-26], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 296 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.4623481504e-27] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 379 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.4623481504e-27], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 297 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.2311740752e-27] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 380 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.2311740752e-27], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 298 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.6155870376e-27] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 381 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.6155870376e-27], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 299 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 8.077935188e-28] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 382 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 8.077935188e-28], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 300 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.038967594e-28] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 383 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.038967594e-28], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 301 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.019483797e-28] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 384 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.019483797e-28], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 302 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.0097418985e-28] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 385 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.0097418985e-28], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 303 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.0487094925e-29] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 386 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.0487094925e-29], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 304 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.5243547462e-29] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 387 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.5243547462e-29], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 305 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2621773731e-29] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 388 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2621773731e-29], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 306 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.3108868656e-30] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 389 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.3108868656e-30], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 307 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.1554434328e-30] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 390 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.1554434328e-30], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 308 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.5777217164e-30] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 391 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.5777217164e-30], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 309 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.888608582e-31] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 392 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.888608582e-31], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 310 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.944304291e-31] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 393 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.944304291e-31], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 311 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.9721521455e-31] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 394 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.9721521455e-31], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 312 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.8607607275e-32] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 395 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.8607607275e-32], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 313 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.9303803638e-32] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 396 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.9303803638e-32], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 314 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.4651901819e-32] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 397 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.4651901819e-32], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 315 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2325950909e-32] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 398 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2325950909e-32], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 316 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.1629754547e-33] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 399 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.1629754547e-33], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 317 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.0814877273e-33] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 400 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.0814877273e-33], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 318 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.5407438637e-33] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 401 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.5407438637e-33], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 319 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.7037193184e-34] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 402 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.7037193184e-34], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 320 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.8518596592e-34] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 403 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.8518596592e-34], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 321 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.9259298296e-34] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 404 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.9259298296e-34], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 322 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.629649148e-35] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 405 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.629649148e-35], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 323 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.814824574e-35] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 406 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.814824574e-35], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 324 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.407412287e-35] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 407 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.407412287e-35], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 325 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2037061435e-35] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 408 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2037061435e-35], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 326 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 6.0185307175e-36] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 409 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 6.0185307175e-36], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 327 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.0092653587e-36] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 410 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.0092653587e-36], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 328 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.5046326794e-36] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 411 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.5046326794e-36], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 329 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.5231633968e-37] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 412 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.5231633968e-37], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 330 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.7615816984e-37] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 413 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.7615816984e-37], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 331 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.8807908492e-37] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 414 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.8807908492e-37], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 332 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.4039542461e-38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 415 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.4039542461e-38], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 333 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.7019774033e-38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 416 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.7019774033e-38], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 334 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.3509887016e-38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 417 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.3509887016e-38], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 335 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.175494491e-38] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 418 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.175494491e-38], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 336 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.8774731554e-39] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 419 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.8774731554e-39], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 337 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.9387372784e-39] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 420 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.9387372784e-39], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 338 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4693693398e-39] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 421 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4693693398e-39], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 339 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.3468537056e-40] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 422 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.3468537056e-40], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 340 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.6734338593e-40] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 423 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.6734338593e-40], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 341 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.8367239361e-40] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 424 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.8367239361e-40], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 342 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.1836897456e-41] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 425 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.1836897456e-41], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 343 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.5919149377e-41] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 426 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.5919149377e-41], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 344 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.2960275338e-41] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 427 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.2960275338e-41], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 345 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.1480838318e-41] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 428 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.1480838318e-41], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 346 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 5.7411198083e-42] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 429 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 5.7411198083e-42], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 347 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.8712605534e-42] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 430 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.8712605534e-42], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 348 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4363309259e-42] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 431 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4363309259e-42], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 349 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.188661122e-43] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 432 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.188661122e-43], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 350 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 3.6013370533e-43] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 433 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 3.6013370533e-43], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 351 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.807675019e-43] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 434 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.807675019e-43], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 352 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 9.1084400181e-44] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 435 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 9.1084400181e-44], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 353 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.6242849323e-44] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 436 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.6242849323e-44], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 354 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.3822073894e-44] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 437 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.3822073894e-44], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 355 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.2611686179e-44] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 438 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.2611686179e-44], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 356 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 7.0064923216e-45] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 439 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 7.0064923216e-45], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 357 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 4.203895393e-45] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 440 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 4.203895393e-45], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 358 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 2.8025969286e-45] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 441 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 2.8025969286e-45], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 359 scores: 0 -1 -1 -1 ASSIGN c::$file::__BUILTIN_DAED_FBETWEEN::1::f to [1.4012984643e-45, 1.4012984643e-45] because of -1 FAILURE TO PROVE CASE ITERATION (decision) 442 ================ { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4012984643e-45], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] } new dlevel: 360 scores: -1 -1 -1 -1 FAILED TO VERIFY PROGRAM Minimal unsafe element: { c::$file::__BUILTIN_DAED_FBETWEEN::1::f in FLOAT: [1.4012984643e-45, 1.4012984643e-45], c::$file::__BUILTIN_DAED_FBETWEEN::l in FLOAT: [-inf, -inf], c::$file::main::1::IN_x in FLOAT: [-inf, -inf], c::$file::__BUILTIN_DAED_FBETWEEN::u in FLOAT: [-inf, -inf] }== Procedure terminated after 443 iterations **** Verification failed Found 1 possible assertion violations ******** 25: ASSERT (double)y <= 0.500000l GOTO 26 Potential violation: __CPROVER_malloc_size == 0 && f == 0.000000f && __CPROVER_rounding_mode == 0 && l == 0.000000f && y == 1.000000f && IN_x == 0.000000f && u == 1.000000f Information over assertion variables: y == 1.000000f ############################################################################### ### exit code: 0 ### /usr/bin/time -v: Command being timed: "/home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/cdfpl --inline --filter-dec-vars IN --proof-search /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/goubault-sas06/Poly.0.0.i" User time (seconds): 0.47 System time (seconds): 0.01 Percent of CPU this job got: 99% Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.48 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 4864 Average resident set size (kbytes): 0 Major (requiring I/O) page faults: 0 Minor (reclaiming a frame) page faults: 1236 Voluntary context switches: 1 Involuntary context switches: 1 Swaps: 0 File system inputs: 0 File system outputs: 392 Socket messages sent: 0 Socket messages received: 0 Signals delivered: 0 Page size (bytes): 4096 Exit status: 0