Name | submitted/aloul/FPGA_SAT05/normalized-fpga35_35_sat_pb.cnf.cr.opb |
MD5SUM | 022f43a9cfc62e9c9c77f51c14f8e5bf |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 36 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.83772 |
Number of variables | 1838 |
Total number of constraints | 1330 |
Number of constraints which are clauses | 1260 |
Number of constraints which are cardinality constraints (but not clauses) | 70 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 17 |
Maximum length of a constraint | 35 |
LAUNCH ON wulflinc24 THE 2005-09-18 12:41:08 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2401 boxname=wulflinc24 idbench=57 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 022f43a9cfc62e9c9c77f51c14f8e5bf /oldhome/oroussel/tmp/wulflinc24/normalized-fpga35_35_sat_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-fpga35_35_sat_pb.cnf.cr.opb IDLAUNCH: 2401 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 941992 kB Buffers: 34356 kB Cached: 30384 kB SwapCached: 744 kB Active: 54336 kB Inactive: 13072 kB HighTotal: 131008 kB HighFree: 96964 kB LowTotal: 903652 kB LowFree: 845028 kB SwapTotal: 2097892 kB SwapFree: 2096644 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5736 kB Slab: 19524 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 12:46:11 (client local time) WITH STATUS 10 IN 302.752 SECONDS stats: 2401 7 302.752 10
c Parsing PB file... c Converting 1330 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ---[ 69]---> BDD-cost: 67 c ---[ 68]---> BDD-cost: 67 c ---[ 67]---> BDD-cost: 67 c ---[ 66]---> BDD-cost: 67 c ---[ 65]---> BDD-cost: 67 c ---[ 64]---> BDD-cost: 67 c ---[ 63]---> BDD-cost: 67 c ---[ 62]---> BDD-cost: 67 c ---[ 61]---> BDD-cost: 67 c ---[ 60]---> BDD-cost: 67 c ---[ 59]---> BDD-cost: 67 c ---[ 58]---> BDD-cost: 67 c ---[ 57]---> BDD-cost: 67 c ---[ 56]---> BDD-cost: 67 c ---[ 55]---> BDD-cost: 67 c ---[ 54]---> BDD-cost: 67 c ---[ 53]---> BDD-cost: 67 c ---[ 52]---> BDD-cost: 67 c ---[ 51]---> BDD-cost: 67 c ---[ 50]---> BDD-cost: 67 c ---[ 49]---> BDD-cost: 67 c ---[ 48]---> BDD-cost: 67 c ---[ 47]---> BDD-cost: 67 c ---[ 46]---> BDD-cost: 67 c ---[ 45]---> BDD-cost: 67 c ---[ 44]---> BDD-cost: 67 c ---[ 43]---> BDD-cost: 67 c ---[ 42]---> BDD-cost: 67 c ---[ 41]---> BDD-cost: 67 c ---[ 40]---> BDD-cost: 67 c ---[ 39]---> BDD-cost: 67 c ---[ 38]---> BDD-cost: 67 c ---[ 37]---> BDD-cost: 67 c ---[ 36]---> BDD-cost: 67 c ---[ 35]---> BDD-cost: 67 c ---[ 34]---> BDD-cost: 31 c ---[ 33]---> BDD-cost: 31 c ---[ 32]---> BDD-cost: 31 c ---[ 31]---> BDD-cost: 31 c ---[ 30]---> BDD-cost: 31 c ---[ 29]---> BDD-cost: 31 c ---[ 28]---> BDD-cost: 31 c ---[ 27]---> BDD-cost: 31 c ---[ 26]---> BDD-cost: 31 c ---[ 25]---> BDD-cost: 31 c ---[ 24]---> BDD-cost: 31 c ---[ 23]---> BDD-cost: 31 c ---[ 22]---> BDD-cost: 31 c ---[ 21]---> BDD-cost: 31 c ---[ 20]---> BDD-cost: 31 c ---[ 19]---> BDD-cost: 31 c ---[ 18]---> BDD-cost: 31 c ---[ 17]---> BDD-cost: 33 c ---[ 16]---> BDD-cost: 33 c ---[ 15]---> BDD-cost: 33 c ---[ 14]---> BDD-cost: 33 c ---[ 13]---> BDD-cost: 33 c ---[ 12]---> BDD-cost: 33 c ---[ 11]---> BDD-cost: 33 c ---[ 10]---> BDD-cost: 33 c ---[ 9]---> BDD-cost: 33 c ---[ 8]---> BDD-cost: 33 c ---[ 7]---> BDD-cost: 33 c ---[ 6]---> BDD-cost: 33 c ---[ 5]---> BDD-cost: 33 c ---[ 4]---> BDD-cost: 33 c ---[ 3]---> BDD-cost: 33 c ---[ 2]---> BDD-cost: 33 c ---[ 1]---> BDD-cost: 33 c ---[ 0]---> BDD-cost: 33 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 9820 46189 | 3273 0 0 nan | 0.000 % | c | 101 | 9820 46189 | 3600 101 24521 242.8 | 1.320 % | c | 251 | 9820 46189 | 3960 251 42348 168.7 | 1.320 % | c | 476 | 9820 46189 | 4356 476 96992 203.8 | 1.320 % | c | 813 | 9820 46189 | 4791 813 173301 213.2 | 1.320 % | c | 1319 | 9820 46189 | 5271 1319 272714 206.8 | 1.320 % | c | 2079 | 9820 46189 | 5798 2079 451841 217.3 | 1.320 % | c | 3218 | 9820 46189 | 6378 3218 752263 233.8 | 1.320 % | c | 4929 | 9820 46189 | 7015 4929 920697 186.8 | 1.320 % | c | 7491 | 9820 46189 | 7717 7491 1888626 252.1 | 1.320 % | c | 11336 | 9820 46189 | 8489 6138 1768390 288.1 | 1.320 % | c | 17102 | 9820 46189 | 9338 11904 2508414 210.7 | 1.320 % | c | 25753 | 9820 46189 | 10272 8274 2738490 331.0 | 1.320 % | c | 38727 | 9820 46189 | 11299 13759 2064632 150.1 | 1.320 % | c | 58188 | 9820 46189 | 12429 11713 3413655 291.4 | 1.320 % | c | 87381 | 9820 46189 | 13672 15700 1625682 103.5 | 1.320 % | c | 131171 | 9820 46189 | 15039 9930 4050630 407.9 | 1.320 % | c ============================================================================== c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE v c _______________________________________________________________________________ c c restarts : 17 c conflicts : 132529 (439 /sec) c decisions : 192840 (638 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 302.074 s c _______________________________________________________________________________
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/23475/stat): 23475 (minisat+_script) R 23474 23475 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841332832 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/23475/statm): 174 3 169 147 0 27 0 [pid=23475] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=23476 New process pid=23477 New process pid=23478 execve syscall for /bin/sed executable One traced child (pid=23477) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=23478) exited with status: 0 One traced child (pid=23476) exited with status: 0 New process pid=23479 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-fpga35_35_sat_pb.cnf.cr.opb [startup+10.0039 s] Raw data (loadavg): 0.94 1.00 0.99 1/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) T 23475 23475 20728 0 -1 0 2702 0 0 0 961 15 0 0 25 0 1 0 1841332837 11304960 2689 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/23479/statm): 2760 2689 145 145 0 2615 0 [pid=23479] vsize: 11040 Current children cumulated CPU time (s) 9.78 Current children cumulated vsize (Kb) 13164 [startup+20.0057 s] Raw data (loadavg): 0.95 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 3414 0 0 0 1951 18 0 0 25 0 1 0 1841332837 14241792 3401 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23479/statm): 3477 3401 145 145 0 3332 0 [pid=23479] vsize: 13908 Current children cumulated CPU time (s) 19.71 Current children cumulated vsize (Kb) 16032 [startup+30.0063 s] Raw data (loadavg): 0.95 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 3448 0 0 0 2950 19 0 0 25 0 1 0 1841332837 14381056 3435 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23479/statm): 3511 3435 145 145 0 3366 0 [pid=23479] vsize: 14044 Current children cumulated CPU time (s) 29.71 Current children cumulated vsize (Kb) 16168 [startup+40.007 s] Raw data (loadavg): 0.96 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 3951 0 0 0 3942 23 0 0 25 0 1 0 1841332837 16461824 3938 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 4019 3938 145 145 0 3874 0 [pid=23479] vsize: 16076 Current children cumulated CPU time (s) 39.67 Current children cumulated vsize (Kb) 18200 [startup+50.0077 s] Raw data (loadavg): 0.97 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5050 0 0 0 4927 29 0 0 25 0 1 0 1841332837 20955136 5037 4294967295 134512640 135094434 3221224432 3221223024 134557531 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5116 5037 145 145 0 4971 0 [pid=23479] vsize: 20464 Current children cumulated CPU time (s) 49.58 Current children cumulated vsize (Kb) 22588 [startup+60.0084 s] Raw data (loadavg): 0.97 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5050 0 0 0 5927 29 0 0 25 0 1 0 1841332837 20955136 5037 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23479/statm): 5116 5037 145 145 0 4971 0 [pid=23479] vsize: 20464 Current children cumulated CPU time (s) 59.58 Current children cumulated vsize (Kb) 22588 [startup+70.0101 s] Raw data (loadavg): 0.97 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5050 0 0 0 6926 30 0 0 25 0 1 0 1841332837 20955136 5037 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23479/statm): 5116 5037 145 145 0 4971 0 [pid=23479] vsize: 20464 Current children cumulated CPU time (s) 69.58 Current children cumulated vsize (Kb) 22588 [startup+80.0108 s] Raw data (loadavg): 0.98 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5050 0 0 0 7926 30 0 0 25 0 1 0 1841332837 20955136 5037 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5116 5037 145 145 0 4971 0 [pid=23479] vsize: 20464 Current children cumulated CPU time (s) 79.58 Current children cumulated vsize (Kb) 22588 [startup+90.0115 s] Raw data (loadavg): 0.98 1.00 0.99 1/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) T 23475 23475 20728 0 -1 0 5316 0 0 0 8922 32 0 0 25 0 1 0 1841332837 22052864 5303 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5384 5303 145 145 0 5239 0 [pid=23479] vsize: 21536 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 23660 [startup+100.012 s] Raw data (loadavg): 0.98 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5595 0 0 0 9918 33 0 0 25 0 1 0 1841332837 23236608 5582 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5673 5582 145 145 0 5528 0 [pid=23479] vsize: 22692 Current children cumulated CPU time (s) 99.53 Current children cumulated vsize (Kb) 24816 [startup+110.014 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5644 0 0 0 10919 33 0 0 25 0 1 0 1841332837 23498752 5631 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5737 5631 145 145 0 5592 0 [pid=23479] vsize: 22948 Current children cumulated CPU time (s) 109.54 Current children cumulated vsize (Kb) 25072 [startup+120.015 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5810 0 0 0 11917 34 0 0 25 0 1 0 1841332837 24207360 5797 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5910 5797 145 145 0 5765 0 [pid=23479] vsize: 23640 Current children cumulated CPU time (s) 119.53 Current children cumulated vsize (Kb) 25764 [startup+130.015 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5811 0 0 0 12917 34 0 0 25 0 1 0 1841332837 24207360 5798 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5910 5798 145 145 0 5765 0 [pid=23479] vsize: 23640 Current children cumulated CPU time (s) 129.53 Current children cumulated vsize (Kb) 25764 [startup+140.016 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5811 0 0 0 13917 34 0 0 25 0 1 0 1841332837 24207360 5798 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5910 5798 145 145 0 5765 0 [pid=23479] vsize: 23640 Current children cumulated CPU time (s) 139.53 Current children cumulated vsize (Kb) 25764 [startup+150.017 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5811 0 0 0 14917 34 0 0 25 0 1 0 1841332837 24207360 5798 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5910 5798 145 145 0 5765 0 [pid=23479] vsize: 23640 Current children cumulated CPU time (s) 149.53 Current children cumulated vsize (Kb) 25764 [startup+160.017 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5811 0 0 0 15917 34 0 0 25 0 1 0 1841332837 24207360 5798 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5910 5798 145 145 0 5765 0 [pid=23479] vsize: 23640 Current children cumulated CPU time (s) 159.53 Current children cumulated vsize (Kb) 25764 [startup+170.018 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5811 0 0 0 16917 35 0 0 25 0 1 0 1841332837 24207360 5798 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 5910 5798 145 145 0 5765 0 [pid=23479] vsize: 23640 Current children cumulated CPU time (s) 169.54 Current children cumulated vsize (Kb) 25764 [startup+180.018 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 5963 0 0 0 17914 36 0 0 25 0 1 0 1841332837 24834048 5950 4294967295 134512640 135094434 3221224432 3221223104 134555771 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 6063 5950 145 145 0 5918 0 [pid=23479] vsize: 24252 Current children cumulated CPU time (s) 179.52 Current children cumulated vsize (Kb) 26376 [startup+190.02 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) T 23475 23475 20728 0 -1 0 7112 0 0 0 18896 45 0 0 25 0 1 0 1841332837 29552640 7099 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/23479/statm): 7215 7099 145 145 0 7070 0 [pid=23479] vsize: 28860 Current children cumulated CPU time (s) 189.43 Current children cumulated vsize (Kb) 30984 [startup+200.02 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 7364 0 0 0 19892 47 0 0 25 0 1 0 1841332837 30588928 7351 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 7468 7351 145 145 0 7323 0 [pid=23479] vsize: 29872 Current children cumulated CPU time (s) 199.41 Current children cumulated vsize (Kb) 31996 [startup+210.021 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 7364 0 0 0 20892 47 0 0 25 0 1 0 1841332837 30588928 7351 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 7468 7351 145 145 0 7323 0 [pid=23479] vsize: 29872 Current children cumulated CPU time (s) 209.41 Current children cumulated vsize (Kb) 31996 [startup+220.022 s] Raw data (loadavg): 0.99 1.00 0.99 1/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) T 23475 23475 20728 0 -1 0 7928 0 0 0 21883 50 0 0 25 0 1 0 1841332837 32940032 7915 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/23479/statm): 8042 7915 145 145 0 7897 0 [pid=23479] vsize: 32168 Current children cumulated CPU time (s) 219.35 Current children cumulated vsize (Kb) 34292 [startup+230.022 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 8272 0 0 0 22878 52 0 0 25 0 1 0 1841332837 34361344 8259 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 8389 8259 145 145 0 8244 0 [pid=23479] vsize: 33556 Current children cumulated CPU time (s) 229.32 Current children cumulated vsize (Kb) 35680 [startup+240.023 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 8272 0 0 0 23878 52 0 0 25 0 1 0 1841332837 34361344 8259 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 8389 8259 145 145 0 8244 0 [pid=23479] vsize: 33556 Current children cumulated CPU time (s) 239.32 Current children cumulated vsize (Kb) 35680 [startup+250.024 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 8307 0 0 0 24878 53 0 0 25 0 1 0 1841332837 34533376 8294 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 8431 8294 145 145 0 8286 0 [pid=23479] vsize: 33724 Current children cumulated CPU time (s) 249.33 Current children cumulated vsize (Kb) 35848 [startup+260.024 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 9325 0 0 0 25862 59 0 0 25 0 1 0 1841332837 38760448 9312 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 9463 9312 145 145 0 9318 0 [pid=23479] vsize: 37852 Current children cumulated CPU time (s) 259.23 Current children cumulated vsize (Kb) 39976 [startup+270.025 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 9356 0 0 0 26862 59 0 0 25 0 1 0 1841332837 38887424 9343 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 9494 9343 145 145 0 9349 0 [pid=23479] vsize: 37976 Current children cumulated CPU time (s) 269.23 Current children cumulated vsize (Kb) 40100 [startup+280.026 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 9356 0 0 0 27862 59 0 0 25 0 1 0 1841332837 38887424 9343 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 9494 9343 145 145 0 9349 0 [pid=23479] vsize: 37976 Current children cumulated CPU time (s) 279.23 Current children cumulated vsize (Kb) 40100 [startup+290.027 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 9356 0 0 0 28863 59 0 0 25 0 1 0 1841332837 38887424 9343 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 9494 9343 145 145 0 9349 0 [pid=23479] vsize: 37976 Current children cumulated CPU time (s) 289.24 Current children cumulated vsize (Kb) 40100 [startup+300.028 s] Raw data (loadavg): 0.99 1.00 0.99 2/57 23479 Raw data (/proc/23475/stat): 23475 (minisat+_script) S 23474 23475 20728 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841332832 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23475/statm): 531 226 485 147 0 384 0 [pid=23475] vsize: 2124 Raw data (/proc/23479/stat): 23479 (minisat+_64-bit) R 23475 23475 20728 0 -1 0 9782 0 0 0 29856 62 0 0 25 0 1 0 1841332837 40689664 9769 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23479/statm): 9934 9769 145 145 0 9789 0 [pid=23479] vsize: 39736 Current children cumulated CPU time (s) 299.2 Current children cumulated vsize (Kb) 41860 One traced child (pid=23479) exited with status: 10 One traced child (pid=23475) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 303.565 CPU time (s): 302.752 CPU user time (s): 302.083 CPU system time (s): 0.668898 CPU usage (%): 99.7323 Max. virtual memory (cumulated for all children) (Kb): 41860
ERROR: no interpretation found !