PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-sao2.b.opb
MD5SUM	3e273bcee52631aeea0b7b1138e7d68d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	25
Optimality of the best value was proved	NO
Number of terms in the objective function	373
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	373
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	373
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03784
Number of variables	372
Total number of constraints	779
Number of constraints which are clauses	772
Number of constraints which are cardinality constraints (but not clauses)	7
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 5813

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 01:58:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4209 boxname=wulflinc22 idbench=73 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3e273bcee52631aeea0b7b1138e7d68d  /oldhome/oroussel/tmp/wulflinc22/normalized-sao2.b.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-sao2.b.opb /oldhome/oroussel/tmp/wulflinc22/normalized-sao2.b.opb
IDLAUNCH: 4209
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        852668 kB
Buffers:         32752 kB
Cached:         106056 kB
SwapCached:        524 kB
Active:          49352 kB
Inactive:        92860 kB
HighTotal:      131008 kB
HighFree:        21252 kB
LowTotal:       903652 kB
LowFree:        831416 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34228 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:18:16 (client local time) WITH STATUS 10 IN 1200.11 SECONDS
stats: 4209 7 1200.11 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 644 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     644    12554 |     214       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13602     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   15535    47286 |    5178       1       29    29.0 |  0.000 % |
c |       101 |   15487    47189 |    5695      97     2496    25.7 |  1.883 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       196 |   15413    47023 |    5137     192     7103    37.0 |  1.883 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       259 |   15441    47094 |    5147     255    10092    39.6 |  1.883 % |
c |       359 |   15441    47094 |    5661     355    13245    37.3 |  2.625 % |
c |       509 |   15441    47094 |    6227     505    18777    37.2 |  2.625 % |
c |       734 |   15441    47094 |    6850     730    31718    43.4 |  2.625 % |
c |      1074 |   15441    47094 |    7535    1070    43683    40.8 |  2.625 % |
c |      1580 |   15430    47072 |    8289    1573    77504    49.3 |  2.664 % |
c |      2339 |   15430    47072 |    9118    2332    96963    41.6 |  2.664 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2799 |   15175    46472 |    5058    2685   114769    42.7 |  2.664 % |
c |      2900 |   15175    46472 |    5563    2786   122539    44.0 |  4.394 % |
c |      3050 |   15175    46472 |    6120    2936   132076    45.0 |  4.394 % |
c |      3277 |   15175    46472 |    6732    3163   143607    45.4 |  4.394 % |
c |      3615 |   15175    46472 |    7405    3501   163393    46.7 |  4.394 % |
c |      4121 |   15159    46440 |    8145    4000   186845    46.7 |  4.443 % |
c |      4883 |   15159    46440 |    8960    4762   215959    45.4 |  4.443 % |
c |      6027 |   15159    46440 |    9856    5906   285866    48.4 |  4.443 % |
c |      7735 |   15159    46440 |   10842    7614   368092    48.3 |  4.443 % |
c |     10297 |   15159    46440 |   11926   10176   490197    48.2 |  4.443 % |
c |     14144 |   15159    46440 |   13119   14023   705041    50.3 |  4.443 % |
c |     19910 |   15159    46440 |   14431   12778   641627    50.2 |  4.443 % |
c |     28562 |   15159    46440 |   15874   13578   732753    54.0 |  4.443 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28932 |   15158    46438 |    5052   13946   750111    53.8 |  4.443 % |
c |     29032 |   15158    46438 |    5557    3587   163881    45.7 |  4.594 % |
c |     29182 |   15158    46438 |    6112    3737   169215    45.3 |  4.594 % |
c |     29407 |   15158    46438 |    6724    3962   177882    44.9 |  4.594 % |
c |     29748 |   15158    46438 |    7396    4303   184608    42.9 |  4.594 % |
c |     30255 |   15158    46438 |    8136    4810   198572    41.3 |  4.594 % |
c |     31017 |   15158    46438 |    8949    5572   239108    42.9 |  4.594 % |
c |     32156 |   15158    46438 |    9844    6711   303052    45.2 |  4.594 % |
c |     33865 |   15158    46438 |   10829    8420   394373    46.8 |  4.594 % |
c |     36428 |   15158    46438 |   11912   10983   497378    45.3 |  4.594 % |
c |     40272 |   15158    46438 |   13103    7978   332911    41.7 |  4.594 % |
c |     46038 |   15158    46438 |   14413   13744   611479    44.5 |  4.594 % |
c |     54688 |   15158    46438 |   15855   14357   644922    44.9 |  4.594 % |
c |     67662 |   15158    46438 |   17440   18249   834028    45.7 |  4.594 % |
c |     87124 |   15158    46438 |   19184   19237  1089255    56.6 |  4.594 % |
c |    116316 |   15158    46438 |   21103   16290   769799    47.3 |  4.594 % |
c |    160112 |   15158    46438 |   23213   14014   499843    35.7 |  4.594 % |
c |    225796 |   15158    46438 |   25535   18118   577512    31.9 |  4.594 % |
c |    324322 |   15158    46438 |   28088   17530   556228    31.7 |  4.594 % |
c |    472115 |   15158    46438 |   30897   17995   789226    43.9 |  4.594 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.86 0.97 0.91 2/54 30966
Raw data (stat): 30966 (runsolver) R 30965 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480809237 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 1629 0 0 0 994 4 0 0 25 0 1 0 480809237 8486912 1603 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2072 1603 603 41 0 2031 0
vsize: 8288
[startup+20.0031 s]
Raw data (loadavg): 0.90 0.97 0.91 3/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 1947 0 0 0 1992 6 0 0 25 0 1 0 480809237 9838592 1921 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2402 1921 603 41 0 2361 0
vsize: 9608
[startup+30.0041 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2096 0 0 0 2990 7 0 0 25 0 1 0 480809237 10375168 2070 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2533 2070 603 41 0 2492 0
vsize: 10132
[startup+40.0039 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2096 0 0 0 3990 7 0 0 25 0 1 0 480809237 10375168 2070 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2533 2070 603 41 0 2492 0
vsize: 10132
[startup+50.0041 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2105 0 0 0 4990 7 0 0 25 0 1 0 480809237 10514432 2079 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2567 2079 603 41 0 2526 0
vsize: 10268
[startup+60.0041 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2107 0 0 0 5990 7 0 0 25 0 1 0 480809237 10514432 2081 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2567 2081 603 41 0 2526 0
vsize: 10268
[startup+70.0052 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2144 0 0 0 6990 7 0 0 25 0 1 0 480809237 10649600 2118 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2600 2118 603 41 0 2559 0
vsize: 10400
[startup+80.0054 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2189 0 0 0 7988 8 0 0 25 0 1 0 480809237 10788864 2163 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2634 2163 603 41 0 2593 0
vsize: 10536
[startup+90.0053 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2344 0 0 0 8988 8 0 0 25 0 1 0 480809237 11616256 2318 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2318 603 41 0 2795 0
vsize: 11344
[startup+100.006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 30966
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2360 0 0 0 9988 8 0 0 25 0 1 0 480809237 11616256 2334 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2836 2334 603 41 0 2795 0
vsize: 11344
[startup+110.008 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 30967
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2391 0 0 0 10988 9 0 0 25 0 1 0 480809237 11747328 2365 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2868 2365 603 41 0 2827 0
vsize: 11472
[startup+120.009 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 31019
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2509 0 0 0 11978 17 0 0 25 0 1 0 480809237 12283904 2483 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2999 2483 603 41 0 2958 0
vsize: 11996
[startup+130.009 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 31019
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2516 0 0 0 12978 17 0 0 25 0 1 0 480809237 12283904 2490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2999 2490 603 41 0 2958 0
vsize: 11996
[startup+140.009 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 31019
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2762 0 0 0 13977 18 0 0 25 0 1 0 480809237 13352960 2736 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3260 2736 603 41 0 3219 0
vsize: 13040
[startup+150.009 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 31019
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2874 0 0 0 14977 19 0 0 25 0 1 0 480809237 13758464 2848 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3359 2848 603 41 0 3318 0
vsize: 13436
[startup+160.009 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 31019
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2887 0 0 0 15977 19 0 0 25 0 1 0 480809237 13758464 2861 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3359 2861 603 41 0 3318 0
vsize: 13436
[startup+170.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 31019
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2894 0 0 0 16977 19 0 0 25 0 1 0 480809237 13897728 2868 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3393 2868 603 41 0 3352 0
vsize: 13572
[startup+180.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 31019
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2905 0 0 0 17977 19 0 0 25 0 1 0 480809237 13897728 2879 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3393 2879 603 41 0 3352 0
vsize: 13572
[startup+190.01 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2912 0 0 0 18977 19 0 0 25 0 1 0 480809237 13897728 2886 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3393 2886 603 41 0 3352 0
vsize: 13572
[startup+200.01 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2921 0 0 0 19977 19 0 0 25 0 1 0 480809237 13897728 2895 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3393 2895 603 41 0 3352 0
vsize: 13572
[startup+210.01 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2943 0 0 0 20978 19 0 0 25 0 1 0 480809237 14061568 2917 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3433 2917 603 41 0 3392 0
vsize: 13732
[startup+220.01 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2956 0 0 0 21978 19 0 0 25 0 1 0 480809237 14061568 2930 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3433 2930 603 41 0 3392 0
vsize: 13732
[startup+230.01 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2974 0 0 0 22978 19 0 0 25 0 1 0 480809237 14225408 2948 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3473 2948 603 41 0 3432 0
vsize: 13892
[startup+240.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 2981 0 0 0 23978 19 0 0 25 0 1 0 480809237 14225408 2955 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3473 2955 603 41 0 3432 0
vsize: 13892
[startup+250.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3000 0 0 0 24978 19 0 0 25 0 1 0 480809237 14389248 2974 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3513 2974 603 41 0 3472 0
vsize: 14052
[startup+260.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3001 0 0 0 25978 20 0 0 25 0 1 0 480809237 14389248 2975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3513 2975 603 41 0 3472 0
vsize: 14052
[startup+270.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3001 0 0 0 26978 20 0 0 25 0 1 0 480809237 14389248 2975 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3513 2975 603 41 0 3472 0
vsize: 14052
[startup+280.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3011 0 0 0 27978 20 0 0 25 0 1 0 480809237 14389248 2985 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3513 2985 603 41 0 3472 0
vsize: 14052
[startup+290.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3042 0 0 0 28978 20 0 0 25 0 1 0 480809237 14553088 3016 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3553 3016 603 41 0 3512 0
vsize: 14212
[startup+300.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3045 0 0 0 29978 20 0 0 25 0 1 0 480809237 14553088 3019 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3553 3019 603 41 0 3512 0
vsize: 14212
[startup+310.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3045 0 0 0 30979 20 0 0 25 0 1 0 480809237 14553088 3019 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3553 3019 603 41 0 3512 0
vsize: 14212
[startup+320.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3045 0 0 0 31979 20 0 0 25 0 1 0 480809237 14553088 3019 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3553 3019 603 41 0 3512 0
vsize: 14212
[startup+330.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3052 0 0 0 32979 20 0 0 25 0 1 0 480809237 14716928 3026 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3026 603 41 0 3552 0
vsize: 14372
[startup+340.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3071 0 0 0 33979 20 0 0 25 0 1 0 480809237 14716928 3045 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3593 3045 603 41 0 3552 0
vsize: 14372
[startup+350.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3078 0 0 0 34979 20 0 0 25 0 1 0 480809237 14880768 3052 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3052 603 41 0 3592 0
vsize: 14532
[startup+360.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3078 0 0 0 35979 20 0 0 25 0 1 0 480809237 14880768 3052 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3052 603 41 0 3592 0
vsize: 14532
[startup+370.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3078 0 0 0 36980 20 0 0 25 0 1 0 480809237 14880768 3052 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3052 603 41 0 3592 0
vsize: 14532
[startup+380.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3088 0 0 0 37980 20 0 0 25 0 1 0 480809237 14880768 3062 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3062 603 41 0 3592 0
vsize: 14532
[startup+390.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3089 0 0 0 38979 21 0 0 25 0 1 0 480809237 14880768 3063 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3063 603 41 0 3592 0
vsize: 14532
[startup+400.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3090 0 0 0 39979 21 0 0 25 0 1 0 480809237 14880768 3064 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3064 603 41 0 3592 0
vsize: 14532
[startup+410.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3092 0 0 0 40979 21 0 0 25 0 1 0 480809237 14880768 3066 4294967295 134512640 134672761 3221224560 3221223744 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3066 603 41 0 3592 0
vsize: 14532
[startup+420.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3094 0 0 0 41979 21 0 0 25 0 1 0 480809237 14880768 3068 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3068 603 41 0 3592 0
vsize: 14532
[startup+430.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3104 0 0 0 42979 22 0 0 25 0 1 0 480809237 14880768 3078 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3078 603 41 0 3592 0
vsize: 14532
[startup+440.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3105 0 0 0 43979 22 0 0 25 0 1 0 480809237 14880768 3079 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3079 603 41 0 3592 0
vsize: 14532
[startup+450.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3105 0 0 0 44979 22 0 0 25 0 1 0 480809237 14880768 3079 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3079 603 41 0 3592 0
vsize: 14532
[startup+460.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3119 0 0 0 45979 22 0 0 25 0 1 0 480809237 15077376 3093 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3093 603 41 0 3640 0
vsize: 14724
[startup+470.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31021
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3119 0 0 0 46979 22 0 0 25 0 1 0 480809237 15077376 3093 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3093 603 41 0 3640 0
vsize: 14724
[startup+480.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3124 0 0 0 47980 22 0 0 25 0 1 0 480809237 15077376 3098 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3098 603 41 0 3640 0
vsize: 14724
[startup+490.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3175 0 0 0 48980 22 0 0 25 0 1 0 480809237 15347712 3149 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3747 3149 603 41 0 3706 0
vsize: 14988
[startup+500.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3188 0 0 0 49980 22 0 0 25 0 1 0 480809237 15347712 3162 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3747 3162 603 41 0 3706 0
vsize: 14988
[startup+510.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3202 0 0 0 50980 22 0 0 25 0 1 0 480809237 15347712 3176 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3747 3176 603 41 0 3706 0
vsize: 14988
[startup+520.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3218 0 0 0 51980 22 0 0 25 0 1 0 480809237 15482880 3192 4294967295 134512640 134672761 3221224560 3221223724 134559748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3780 3192 603 41 0 3739 0
vsize: 15120
[startup+530.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3226 0 0 0 52980 22 0 0 25 0 1 0 480809237 15482880 3200 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3780 3200 603 41 0 3739 0
vsize: 15120
[startup+540.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3229 0 0 0 53980 22 0 0 25 0 1 0 480809237 15482880 3203 4294967295 134512640 134672761 3221224560 3221223664 134555084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3780 3203 603 41 0 3739 0
vsize: 15120
[startup+550.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3230 0 0 0 54980 22 0 0 25 0 1 0 480809237 15482880 3204 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3780 3204 603 41 0 3739 0
vsize: 15120
[startup+560.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3230 0 0 0 55980 23 0 0 25 0 1 0 480809237 15482880 3204 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3780 3204 603 41 0 3739 0
vsize: 15120
[startup+570.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3230 0 0 0 56981 23 0 0 25 0 1 0 480809237 15482880 3204 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3780 3204 603 41 0 3739 0
vsize: 15120
[startup+580.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3237 0 0 0 57980 23 0 0 25 0 1 0 480809237 15638528 3211 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3211 603 41 0 3777 0
vsize: 15272
[startup+590.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3256 0 0 0 58979 23 0 0 25 0 1 0 480809237 15638528 3230 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3230 603 41 0 3777 0
vsize: 15272
[startup+600.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3263 0 0 0 59979 24 0 0 25 0 1 0 480809237 15638528 3237 4294967295 134512640 134672761 3221224560 3221223744 134558943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3237 603 41 0 3777 0
vsize: 15272
[startup+610.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3276 0 0 0 60979 24 0 0 25 0 1 0 480809237 15802368 3250 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3858 3250 603 41 0 3817 0
vsize: 15432
[startup+620.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3277 0 0 0 61978 24 0 0 25 0 1 0 480809237 15802368 3251 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3858 3251 603 41 0 3817 0
vsize: 15432
[startup+630.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3288 0 0 0 62978 24 0 0 25 0 1 0 480809237 15802368 3262 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3858 3262 603 41 0 3817 0
vsize: 15432
[startup+640.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3295 0 0 0 63978 25 0 0 25 0 1 0 480809237 15802368 3269 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3858 3269 603 41 0 3817 0
vsize: 15432
[startup+650.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3302 0 0 0 64978 25 0 0 25 0 1 0 480809237 15966208 3276 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3898 3276 603 41 0 3857 0
vsize: 15592
[startup+660.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3302 0 0 0 65977 26 0 0 25 0 1 0 480809237 15966208 3276 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3898 3276 603 41 0 3857 0
vsize: 15592
[startup+670.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3308 0 0 0 66977 26 0 0 25 0 1 0 480809237 15966208 3282 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3898 3282 603 41 0 3857 0
vsize: 15592
[startup+680.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3318 0 0 0 67977 26 0 0 25 0 1 0 480809237 15966208 3292 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3898 3292 603 41 0 3857 0
vsize: 15592
[startup+690.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3410 0 0 0 68976 27 0 0 25 0 1 0 480809237 16384000 3384 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3384 603 41 0 3959 0
vsize: 16000
[startup+700.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3476 0 0 0 69976 27 0 0 25 0 1 0 480809237 16654336 3450 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3450 603 41 0 4025 0
vsize: 16264
[startup+710.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3498 0 0 0 70975 28 0 0 25 0 1 0 480809237 16809984 3472 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4104 3472 603 41 0 4063 0
vsize: 16416
[startup+720.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3500 0 0 0 71975 28 0 0 25 0 1 0 480809237 16809984 3474 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4104 3474 603 41 0 4063 0
vsize: 16416
[startup+730.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3566 0 0 0 72974 29 0 0 25 0 1 0 480809237 17080320 3540 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3540 603 41 0 4129 0
vsize: 16680
[startup+740.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3566 0 0 0 73974 29 0 0 25 0 1 0 480809237 17080320 3540 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3540 603 41 0 4129 0
vsize: 16680
[startup+750.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3579 0 0 0 74974 29 0 0 25 0 1 0 480809237 17219584 3553 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3553 603 41 0 4163 0
vsize: 16816
[startup+760.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3594 0 0 0 75973 30 0 0 25 0 1 0 480809237 17219584 3568 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3568 603 41 0 4163 0
vsize: 16816
[startup+770.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3602 0 0 0 76973 30 0 0 25 0 1 0 480809237 17219584 3576 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3576 603 41 0 4163 0
vsize: 16816
[startup+780.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3603 0 0 0 77973 31 0 0 25 0 1 0 480809237 17219584 3577 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3577 603 41 0 4163 0
vsize: 16816
[startup+790.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3611 0 0 0 78972 31 0 0 25 0 1 0 480809237 17383424 3585 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4244 3585 603 41 0 4203 0
vsize: 16976
[startup+800.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3614 0 0 0 79972 32 0 0 25 0 1 0 480809237 17383424 3588 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4244 3588 603 41 0 4203 0
vsize: 16976
[startup+810.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3639 0 0 0 80972 32 0 0 25 0 1 0 480809237 17547264 3613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4284 3613 603 41 0 4243 0
vsize: 17136
[startup+820.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3639 0 0 0 81971 32 0 0 25 0 1 0 480809237 17547264 3613 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4284 3613 603 41 0 4243 0
vsize: 17136
[startup+830.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3639 0 0 0 82971 33 0 0 25 0 1 0 480809237 17547264 3613 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4284 3613 603 41 0 4243 0
vsize: 17136
[startup+840.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3652 0 0 0 83971 33 0 0 25 0 1 0 480809237 17547264 3626 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4284 3626 603 41 0 4243 0
vsize: 17136
[startup+850.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3694 0 0 0 84970 33 0 0 25 0 1 0 480809237 17682432 3668 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4317 3668 603 41 0 4276 0
vsize: 17268
[startup+860.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3694 0 0 0 85970 34 0 0 25 0 1 0 480809237 17682432 3668 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4317 3668 603 41 0 4276 0
vsize: 17268
[startup+870.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3816 0 0 0 86969 34 0 0 25 0 1 0 480809237 18214912 3790 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4447 3790 603 41 0 4406 0
vsize: 17788
[startup+880.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3895 0 0 0 87969 35 0 0 25 0 1 0 480809237 18485248 3869 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4513 3869 603 41 0 4472 0
vsize: 18052
[startup+890.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3896 0 0 0 88969 35 0 0 25 0 1 0 480809237 18485248 3870 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4513 3870 603 41 0 4472 0
vsize: 18052
[startup+900.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3916 0 0 0 89969 35 0 0 25 0 1 0 480809237 18632704 3890 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4549 3890 603 41 0 4508 0
vsize: 18196
[startup+910.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3916 0 0 0 90968 35 0 0 25 0 1 0 480809237 18632704 3890 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4549 3890 603 41 0 4508 0
vsize: 18196
[startup+920.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3917 0 0 0 91968 36 0 0 25 0 1 0 480809237 18632704 3891 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4549 3891 603 41 0 4508 0
vsize: 18196
[startup+930.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3919 0 0 0 92968 36 0 0 25 0 1 0 480809237 18632704 3893 4294967295 134512640 134672761 3221224560 3221223664 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4549 3893 603 41 0 4508 0
vsize: 18196
[startup+940.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3975 0 0 0 93968 36 0 0 25 0 1 0 480809237 18927616 3949 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4621 3949 603 41 0 4580 0
vsize: 18484
[startup+950.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3975 0 0 0 94968 36 0 0 25 0 1 0 480809237 18927616 3949 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4621 3949 603 41 0 4580 0
vsize: 18484
[startup+960.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 3986 0 0 0 95968 36 0 0 25 0 1 0 480809237 18927616 3960 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4621 3960 603 41 0 4580 0
vsize: 18484
[startup+970.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4005 0 0 0 96968 36 0 0 25 0 1 0 480809237 19066880 3979 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4655 3979 603 41 0 4614 0
vsize: 18620
[startup+980.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4006 0 0 0 97969 36 0 0 25 0 1 0 480809237 19066880 3980 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4655 3980 603 41 0 4614 0
vsize: 18620
[startup+990.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4010 0 0 0 98969 36 0 0 25 0 1 0 480809237 19066880 3984 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4655 3984 603 41 0 4614 0
vsize: 18620
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4022 0 0 0 99969 36 0 0 25 0 1 0 480809237 19214336 3996 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 3996 603 41 0 4650 0
vsize: 18764
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4022 0 0 0 100969 36 0 0 25 0 1 0 480809237 19214336 3996 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 3996 603 41 0 4650 0
vsize: 18764
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4046 0 0 0 101969 37 0 0 25 0 1 0 480809237 19214336 4020 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 4020 603 41 0 4650 0
vsize: 18764
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4047 0 0 0 102969 37 0 0 25 0 1 0 480809237 19214336 4021 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 4021 603 41 0 4650 0
vsize: 18764
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4048 0 0 0 103969 37 0 0 25 0 1 0 480809237 19214336 4022 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 4022 603 41 0 4650 0
vsize: 18764
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4048 0 0 0 104969 37 0 0 25 0 1 0 480809237 19214336 4022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 4022 603 41 0 4650 0
vsize: 18764
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4052 0 0 0 105969 37 0 0 25 0 1 0 480809237 19361792 4026 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4727 4026 603 41 0 4686 0
vsize: 18908
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4206 0 0 0 106969 37 0 0 25 0 1 0 480809237 20025344 4180 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4889 4180 603 41 0 4848 0
vsize: 19556
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4208 0 0 0 107969 37 0 0 25 0 1 0 480809237 20025344 4182 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4889 4182 603 41 0 4848 0
vsize: 19556
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4209 0 0 0 108969 38 0 0 25 0 1 0 480809237 20025344 4183 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4889 4183 603 41 0 4848 0
vsize: 19556
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4222 0 0 0 109969 38 0 0 25 0 1 0 480809237 20205568 4196 4294967295 134512640 134672761 3221224560 3221223696 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4933 4196 603 41 0 4892 0
vsize: 19732
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4237 0 0 0 110969 38 0 0 25 0 1 0 480809237 20205568 4211 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4933 4211 603 41 0 4892 0
vsize: 19732
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4248 0 0 0 111969 38 0 0 25 0 1 0 480809237 20205568 4222 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4933 4222 603 41 0 4892 0
vsize: 19732
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4261 0 0 0 112969 38 0 0 25 0 1 0 480809237 20385792 4235 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4977 4235 603 41 0 4936 0
vsize: 19908
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4264 0 0 0 113969 38 0 0 25 0 1 0 480809237 20385792 4238 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4977 4238 603 41 0 4936 0
vsize: 19908
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4264 0 0 0 114969 38 0 0 25 0 1 0 480809237 20385792 4238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4977 4238 603 41 0 4936 0
vsize: 19908
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4265 0 0 0 115969 38 0 0 25 0 1 0 480809237 20385792 4239 4294967295 134512640 134672761 3221224560 3221223744 134558941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4977 4239 603 41 0 4936 0
vsize: 19908
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4265 0 0 0 116970 38 0 0 25 0 1 0 480809237 20385792 4239 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4977 4239 603 41 0 4936 0
vsize: 19908
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4265 0 0 0 117970 39 0 0 25 0 1 0 480809237 20385792 4239 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4977 4239 603 41 0 4936 0
vsize: 19908
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4265 0 0 0 118970 39 0 0 25 0 1 0 480809237 20385792 4239 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4977 4239 603 41 0 4936 0
vsize: 19908
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 31023
Raw data (stat): 30966 (minisat+) R 30965 26298 26297 0 -1 0 4266 0 0 0 119970 39 0 0 25 0 1 0 480809237 20385792 4240 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4977 4240 603 41 0 4936 0
vsize: 19908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 31023
Raw data (stat): 30966 (minisat+) Z 30965 26298 26297 0 -1 12 4269 0 0 0 119970 40 0 0 25 0 1 0 480809237 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.11
CPU user time (s): 1199.7
CPU system time (s): 0.400939
CPU usage (%): 100.006
Max. virtual memory (Kb): 19908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####