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-count.b.opb
MD5SUM	f13ba9c997276002b5bd6db1f679a6f5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	24
Optimality of the best value was proved	NO
Number of terms in the objective function	467
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	467
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	467
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.04584
Number of variables	466
Total number of constraints	694
Number of constraints which are clauses	694
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	78
Trace number 6169

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-14 03:38:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4577 boxname=wulflinc6 idbench=65 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f13ba9c997276002b5bd6db1f679a6f5  /oldhome/oroussel/tmp/wulflinc6/normalized-count.b.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc6/normalized-count.b.opb /oldhome/oroussel/tmp/wulflinc6/normalized-count.b.opb
IDLAUNCH: 4577
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        878312 kB
Buffers:         36472 kB
Cached:          97768 kB
SwapCached:       2644 kB
Active:          54460 kB
Inactive:        85288 kB
HighTotal:      131008 kB
HighFree:        29344 kB
LowTotal:       903652 kB
LowFree:        848968 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10988 kB
Committed_AS:    63468 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:58:14 (client local time) WITH STATUS 10 IN 1200.36 SECONDS
stats: 4577 7 1200.36 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 694 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 |     694    17335 |     231       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:17658     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38073   104886 |   12691       0        0     nan |  0.000 % |
c |       100 |   37864   104411 |   13960      87      336     3.9 |  1.149 % |
c |       250 |   37864   104411 |   15356     237     2728    11.5 |  1.149 % |
c |       476 |   37848   104375 |   16891     462     8224    17.8 |  1.180 % |
c |       813 |   37599   103806 |   18580     748    10226    13.7 |  1.724 % |
c |      1320 |   37286   103096 |   20438    1061    12293    11.6 |  2.431 % |
c |      2080 |   37266   103051 |   22482    1820    33830    18.6 |  2.478 % |
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 |      2348 |   37299   103134 |   12433    2088    50743    24.3 |  2.478 % |
c |      2449 |   37299   103134 |   13676    2189    53044    24.2 |  2.483 % |
c |      2599 |   37299   103134 |   15043    2339    56157    24.0 |  2.483 % |
c |      2825 |   37077   102630 |   16548    2563    58385    22.8 |  3.003 % |
c |      3162 |   37077   102630 |   18203    2900    69771    24.1 |  3.003 % |
c |      3670 |   37077   102630 |   20023    3408    86339    25.3 |  3.003 % |
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 |      3725 |   37048   102555 |   12349    3463    87944    25.4 |  3.003 % |
c |      3825 |   37048   102555 |   13583    3563    88707    24.9 |  3.096 % |
c |      3975 |   37048   102555 |   14942    3713    96270    25.9 |  3.096 % |
c |      4200 |   36860   102130 |   16436    3920   103078    26.3 |  3.507 % |
c |      4537 |   36860   102130 |   18080    4257   108057    25.4 |  3.507 % |
c ==============================================================================
c [1mFound solution: 28[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 |      5001 |   36887   102198 |   12295    4721   130901    27.7 |  3.507 % |
c |      5102 |   36887   102198 |   13524    4822   137557    28.5 |  3.520 % |
c |      5256 |   36887   102198 |   14876    4976   148963    29.9 |  3.520 % |
c |      5482 |   36887   102198 |   16364    5202   162195    31.2 |  3.520 % |
c |      5820 |   36800   101999 |   18001    5489   165188    30.1 |  3.729 % |
c |      6327 |   36800   101999 |   19801    5996   177461    29.6 |  3.729 % |
c ==============================================================================
c [1mFound solution: 26[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 |      7074 |   36826   102064 |   12275    6743   209414    31.1 |  3.729 % |
c |      7175 |   36826   102064 |   13502    6844   213057    31.1 |  3.742 % |
c |      7326 |   36826   102064 |   14852    6995   222703    31.8 |  3.742 % |
c |      7551 |   36826   102064 |   16338    7220   232236    32.2 |  3.742 % |
c |      7888 |   36826   102064 |   17971    7557   239169    31.6 |  3.742 % |
c |      8394 |   36826   102064 |   19769    8063   266615    33.1 |  3.742 % |
c |      9153 |   36779   101959 |   21745    8815   277657    31.5 |  3.835 % |
c |     10293 |   36769   101939 |   23920    9941   322776    32.5 |  3.842 % |
c ==============================================================================
c [1mFound solution: 25[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 |     11717 |   36724   101830 |   12241   11295   390403    34.6 |  3.842 % |
c |     11818 |   36724   101830 |   13465   11396   393554    34.5 |  3.981 % |
c |     11980 |   36724   101830 |   14811   11558   398895    34.5 |  3.981 % |
c |     12209 |   36724   101830 |   16292   11787   406957    34.5 |  3.981 % |
c |     12546 |   36724   101830 |   17922   12124   424774    35.0 |  3.981 % |
c |     13054 |   36724   101830 |   19714   12632   471870    37.4 |  3.981 % |
c |     13813 |   36724   101830 |   21685   13391   504622    37.7 |  3.981 % |
c |     14954 |   36724   101830 |   23854   14532   567746    39.1 |  3.981 % |
c |     16664 |   36724   101830 |   26239   16242   654616    40.3 |  3.981 % |
c |     19231 |   36724   101830 |   28863   18809   793257    42.2 |  3.981 % |
c |     23080 |   36697   101770 |   31750   22657  1020918    45.1 |  4.035 % |
c |     28846 |   36658   101682 |   34925   28421  1308354    46.0 |  4.121 % |
c |     37496 |   36658   101682 |   38417   37071  1710815    46.1 |  4.121 % |
c ==============================================================================
c [1mFound solution: 24[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 |     48560 |   36597   101548 |   12199   22954   877826    38.2 |  4.121 % |
c |     48662 |   36597   101548 |   13418   11579   379261    32.8 |  4.334 % |
c |     48813 |   36597   101548 |   14760   11730   385670    32.9 |  4.334 % |
c |     49038 |   36597   101548 |   16236   11955   394607    33.0 |  4.334 % |
c |     49375 |   36597   101548 |   17860   12292   403831    32.9 |  4.334 % |
c |     49882 |   36597   101548 |   19646   12799   416086    32.5 |  4.334 % |
c |     50642 |   36597   101548 |   21611   13559   433522    32.0 |  4.334 % |
c |     51782 |   36597   101548 |   23772   14699   491203    33.4 |  4.334 % |
c |     53492 |   36597   101548 |   26149   16409   582056    35.5 |  4.334 % |
c |     56054 |   36597   101548 |   28764   18971   705027    37.2 |  4.334 % |
c |     59898 |   36597   101548 |   31641   22815   872206    38.2 |  4.334 % |
c |     65668 |   36597   101548 |   34805   28585  1107259    38.7 |  4.334 % |
c |     74318 |   36597   101548 |   38285   37235  1468973    39.5 |  4.334 % |
c |     87293 |   36566   101479 |   42114   23699  1036824    43.7 |  4.396 % |
c |    106754 |   36547   101437 |   46325   43159  1898344    44.0 |  4.435 % |
c |    135946 |   36427   101165 |   50958   41910  1502279    35.8 |  4.706 % |
c |    179735 |   36379   101056 |   56054   51363  1690293    32.9 |  4.822 % |
c |    245420 |   36348   100987 |   61659   39614  1170639    29.6 |  4.884 % |
#### 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.92 0.97 0.91 2/54 2792
Raw data (stat): 2792 (runsolver) R 2791 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423189154 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99962 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 1649 0 0 0 993 4 0 0 25 0 1 0 423189154 8826880 1623 4294967295 134512640 134672761 3221224576 3221223776 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2155 1623 603 41 0 2114 0
vsize: 8620
[startup+19.9999 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 1865 0 0 0 1992 5 0 0 25 0 1 0 423189154 9756672 1839 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2382 1839 603 41 0 2341 0
vsize: 9528
[startup+29.9998 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 2135 0 0 0 2990 7 0 0 25 0 1 0 423189154 10829824 2109 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2644 2109 603 41 0 2603 0
vsize: 10576
[startup+39.9989 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 2334 0 0 0 3990 8 0 0 25 0 1 0 423189154 11612160 2308 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2835 2308 603 41 0 2794 0
vsize: 11340
[startup+49.9993 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 2597 0 0 0 4989 8 0 0 25 0 1 0 423189154 12693504 2571 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3099 2571 603 41 0 3058 0
vsize: 12396
[startup+59.9992 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 2860 0 0 0 5989 9 0 0 25 0 1 0 423189154 13754368 2834 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3358 2834 603 41 0 3317 0
vsize: 13432
[startup+69.9993 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3030 0 0 0 6989 10 0 0 25 0 1 0 423189154 14426112 3004 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3522 3004 603 41 0 3481 0
vsize: 14088
[startup+79.9998 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3218 0 0 0 7988 10 0 0 25 0 1 0 423189154 15233024 3192 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3719 3192 603 41 0 3678 0
vsize: 14876
[startup+89.9997 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3395 0 0 0 8988 11 0 0 25 0 1 0 423189154 16031744 3369 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3914 3369 603 41 0 3873 0
vsize: 15656
[startup+99.9987 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3593 0 0 0 9987 12 0 0 25 0 1 0 423189154 16855040 3567 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4115 3567 603 41 0 4074 0
vsize: 16460
[startup+110 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3755 0 0 0 10986 13 0 0 25 0 1 0 423189154 17534976 3729 4294967295 134512640 134672761 3221224576 3221223744 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4281 3729 603 41 0 4240 0
vsize: 17124
[startup+119.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3811 0 0 0 11986 13 0 0 25 0 1 0 423189154 17805312 3785 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4347 3785 603 41 0 4306 0
vsize: 17388
[startup+129.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3821 0 0 0 12986 13 0 0 25 0 1 0 423189154 17805312 3795 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4347 3795 603 41 0 4306 0
vsize: 17388
[startup+139.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3834 0 0 0 13986 13 0 0 25 0 1 0 423189154 17960960 3808 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4385 3808 603 41 0 4344 0
vsize: 17540
[startup+149.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3836 0 0 0 14987 13 0 0 25 0 1 0 423189154 17960960 3810 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4385 3810 603 41 0 4344 0
vsize: 17540
[startup+159.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3836 0 0 0 15987 13 0 0 25 0 1 0 423189154 17960960 3810 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4385 3810 603 41 0 4344 0
vsize: 17540
[startup+169.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3836 0 0 0 16987 13 0 0 25 0 1 0 423189154 17960960 3810 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4385 3810 603 41 0 4344 0
vsize: 17540
[startup+179.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3842 0 0 0 17987 13 0 0 25 0 1 0 423189154 17960960 3816 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4385 3816 603 41 0 4344 0
vsize: 17540
[startup+189.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3848 0 0 0 18988 13 0 0 25 0 1 0 423189154 17960960 3822 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4385 3822 603 41 0 4344 0
vsize: 17540
[startup+199.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3854 0 0 0 19988 13 0 0 25 0 1 0 423189154 17960960 3828 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4385 3828 603 41 0 4344 0
vsize: 17540
[startup+209.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3860 0 0 0 20988 13 0 0 25 0 1 0 423189154 18124800 3834 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 3834 603 41 0 4384 0
vsize: 17700
[startup+219.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3866 0 0 0 21989 13 0 0 25 0 1 0 423189154 18124800 3840 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 3840 603 41 0 4384 0
vsize: 17700
[startup+229.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3875 0 0 0 22989 13 0 0 25 0 1 0 423189154 18124800 3849 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 3849 603 41 0 4384 0
vsize: 17700
[startup+239.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3878 0 0 0 23989 13 0 0 25 0 1 0 423189154 18124800 3852 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 3852 603 41 0 4384 0
vsize: 17700
[startup+249.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3878 0 0 0 24990 13 0 0 25 0 1 0 423189154 18124800 3852 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 3852 603 41 0 4384 0
vsize: 17700
[startup+259.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3885 0 0 0 25990 13 0 0 25 0 1 0 423189154 18124800 3859 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 3859 603 41 0 4384 0
vsize: 17700
[startup+269.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3886 0 0 0 26990 14 0 0 25 0 1 0 423189154 18124800 3860 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 3860 603 41 0 4384 0
vsize: 17700
[startup+279.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3886 0 0 0 27990 14 0 0 25 0 1 0 423189154 18124800 3860 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 3860 603 41 0 4384 0
vsize: 17700
[startup+289.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3889 0 0 0 28991 14 0 0 25 0 1 0 423189154 18272256 3863 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4461 3863 603 41 0 4420 0
vsize: 17844
[startup+299.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3893 0 0 0 29991 14 0 0 25 0 1 0 423189154 18272256 3867 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4461 3867 603 41 0 4420 0
vsize: 17844
[startup+309.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3903 0 0 0 30991 14 0 0 25 0 1 0 423189154 18272256 3877 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4461 3877 603 41 0 4420 0
vsize: 17844
[startup+319.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3911 0 0 0 31992 14 0 0 25 0 1 0 423189154 18272256 3885 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4461 3885 603 41 0 4420 0
vsize: 17844
[startup+329.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 3917 0 0 0 32992 14 0 0 25 0 1 0 423189154 18272256 3891 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4461 3891 603 41 0 4420 0
vsize: 17844
[startup+339.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4013 0 0 0 33992 14 0 0 25 0 1 0 423189154 18673664 3987 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4559 3987 603 41 0 4518 0
vsize: 18236
[startup+349.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4116 0 0 0 34991 14 0 0 25 0 1 0 423189154 19255296 4090 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4701 4090 603 41 0 4660 0
vsize: 18804
[startup+359.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4222 0 0 0 35992 15 0 0 25 0 1 0 423189154 19701760 4196 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4810 4196 603 41 0 4769 0
vsize: 19240
[startup+369.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4359 0 0 0 36992 15 0 0 25 0 1 0 423189154 20258816 4333 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4946 4333 603 41 0 4905 0
vsize: 19784
[startup+379.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4373 0 0 0 37992 15 0 0 25 0 1 0 423189154 20258816 4347 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4946 4347 603 41 0 4905 0
vsize: 19784
[startup+389.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4373 0 0 0 38992 15 0 0 25 0 1 0 423189154 20258816 4347 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4946 4347 603 41 0 4905 0
vsize: 19784
[startup+399.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4373 0 0 0 39992 15 0 0 25 0 1 0 423189154 20258816 4347 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4946 4347 603 41 0 4905 0
vsize: 19784
[startup+409.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4374 0 0 0 40993 15 0 0 25 0 1 0 423189154 20258816 4348 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4946 4348 603 41 0 4905 0
vsize: 19784
[startup+419.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4374 0 0 0 41993 15 0 0 25 0 1 0 423189154 20258816 4348 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4946 4348 603 41 0 4905 0
vsize: 19784
[startup+429.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4386 0 0 0 42993 15 0 0 25 0 1 0 423189154 20418560 4360 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4360 603 41 0 4944 0
vsize: 19940
[startup+439.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4394 0 0 0 43994 15 0 0 25 0 1 0 423189154 20418560 4368 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4368 603 41 0 4944 0
vsize: 19940
[startup+449.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4396 0 0 0 44994 15 0 0 25 0 1 0 423189154 20418560 4370 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4370 603 41 0 4944 0
vsize: 19940
[startup+459.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4397 0 0 0 45994 15 0 0 25 0 1 0 423189154 20418560 4371 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4371 603 41 0 4944 0
vsize: 19940
[startup+469.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4400 0 0 0 46995 15 0 0 25 0 1 0 423189154 20418560 4374 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4374 603 41 0 4944 0
vsize: 19940
[startup+479.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4401 0 0 0 47995 15 0 0 25 0 1 0 423189154 20418560 4375 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4985 4375 603 41 0 4944 0
vsize: 19940
[startup+489.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4413 0 0 0 48994 15 0 0 25 0 1 0 423189154 20418560 4387 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4387 603 41 0 4944 0
vsize: 19940
[startup+499.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4414 0 0 0 49995 15 0 0 25 0 1 0 423189154 20418560 4388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4388 603 41 0 4944 0
vsize: 19940
[startup+509.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4415 0 0 0 50995 15 0 0 25 0 1 0 423189154 20418560 4389 4294967295 134512640 134672761 3221224576 3221223712 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4389 603 41 0 4944 0
vsize: 19940
[startup+519.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4418 0 0 0 51995 15 0 0 25 0 1 0 423189154 20418560 4392 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4392 603 41 0 4944 0
vsize: 19940
[startup+529.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4429 0 0 0 52996 15 0 0 25 0 1 0 423189154 20582400 4403 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4403 603 41 0 4984 0
vsize: 20100
[startup+539.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4452 0 0 0 53996 15 0 0 25 0 1 0 423189154 20582400 4426 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4426 603 41 0 4984 0
vsize: 20100
[startup+549.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4452 0 0 0 54996 15 0 0 25 0 1 0 423189154 20582400 4426 4294967295 134512640 134672761 3221224576 3221223712 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4426 603 41 0 4984 0
vsize: 20100
[startup+559.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4452 0 0 0 55996 15 0 0 25 0 1 0 423189154 20582400 4426 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4426 603 41 0 4984 0
vsize: 20100
[startup+569.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4452 0 0 0 56997 15 0 0 25 0 1 0 423189154 20582400 4426 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4426 603 41 0 4984 0
vsize: 20100
[startup+579.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4452 0 0 0 57997 15 0 0 25 0 1 0 423189154 20582400 4426 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4426 603 41 0 4984 0
vsize: 20100
[startup+589.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4452 0 0 0 58997 15 0 0 25 0 1 0 423189154 20582400 4426 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4426 603 41 0 4984 0
vsize: 20100
[startup+599.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4452 0 0 0 59998 15 0 0 25 0 1 0 423189154 20582400 4426 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4426 603 41 0 4984 0
vsize: 20100
[startup+609.984 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4459 0 0 0 60998 15 0 0 25 0 1 0 423189154 20746240 4433 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5065 4433 603 41 0 5024 0
vsize: 20260
[startup+619.984 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4463 0 0 0 61998 15 0 0 25 0 1 0 423189154 20746240 4437 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5065 4437 603 41 0 5024 0
vsize: 20260
[startup+629.984 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4465 0 0 0 62999 15 0 0 25 0 1 0 423189154 20746240 4439 4294967295 134512640 134672761 3221224576 3221223776 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5065 4439 603 41 0 5024 0
vsize: 20260
[startup+639.984 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4483 0 0 0 63999 15 0 0 25 0 1 0 423189154 20746240 4457 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5065 4457 603 41 0 5024 0
vsize: 20260
[startup+649.984 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4484 0 0 0 64999 15 0 0 25 0 1 0 423189154 20746240 4458 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5065 4458 603 41 0 5024 0
vsize: 20260
[startup+659.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4485 0 0 0 65999 15 0 0 25 0 1 0 423189154 20746240 4459 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5065 4459 603 41 0 5024 0
vsize: 20260
[startup+669.984 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4486 0 0 0 67000 15 0 0 25 0 1 0 423189154 20746240 4460 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5065 4460 603 41 0 5024 0
vsize: 20260
[startup+679.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4486 0 0 0 68000 15 0 0 25 0 1 0 423189154 20746240 4460 4294967295 134512640 134672761 3221224576 3221223744 134561278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5065 4460 603 41 0 5024 0
vsize: 20260
[startup+689.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4511 0 0 0 69000 15 0 0 25 0 1 0 423189154 21008384 4485 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4485 603 41 0 5088 0
vsize: 20516
[startup+699.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4514 0 0 0 70001 15 0 0 25 0 1 0 423189154 21008384 4488 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4488 603 41 0 5088 0
vsize: 20516
[startup+709.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4516 0 0 0 71001 15 0 0 25 0 1 0 423189154 21008384 4490 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4490 603 41 0 5088 0
vsize: 20516
[startup+719.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 72001 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+729.985 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 73002 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+739.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 74002 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223712 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+749.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 75002 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+759.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 76003 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+769.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 77003 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+779.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 78003 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+789.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 79004 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+799.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4517 0 0 0 80004 15 0 0 25 0 1 0 423189154 21008384 4491 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4491 603 41 0 5088 0
vsize: 20516
[startup+809.986 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4518 0 0 0 81004 15 0 0 25 0 1 0 423189154 21008384 4492 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4492 603 41 0 5088 0
vsize: 20516
[startup+819.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4518 0 0 0 82005 15 0 0 25 0 1 0 423189154 21008384 4492 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4492 603 41 0 5088 0
vsize: 20516
[startup+829.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4527 0 0 0 83005 15 0 0 25 0 1 0 423189154 21008384 4501 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4501 603 41 0 5088 0
vsize: 20516
[startup+839.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4527 0 0 0 84005 15 0 0 25 0 1 0 423189154 21008384 4501 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4501 603 41 0 5088 0
vsize: 20516
[startup+849.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4548 0 0 0 85006 16 0 0 25 0 1 0 423189154 21172224 4522 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5169 4522 603 41 0 5128 0
vsize: 20676
[startup+859.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4552 0 0 0 86006 16 0 0 25 0 1 0 423189154 21172224 4526 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5169 4526 603 41 0 5128 0
vsize: 20676
[startup+869.987 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4574 0 0 0 87006 16 0 0 25 0 1 0 423189154 21172224 4548 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5169 4548 603 41 0 5128 0
vsize: 20676
[startup+879.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4586 0 0 0 88007 16 0 0 25 0 1 0 423189154 21336064 4560 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5209 4560 603 41 0 5168 0
vsize: 20836
[startup+889.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4596 0 0 0 89007 16 0 0 25 0 1 0 423189154 21336064 4570 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5209 4570 603 41 0 5168 0
vsize: 20836
[startup+899.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4619 0 0 0 90007 16 0 0 25 0 1 0 423189154 21565440 4593 4294967295 134512640 134672761 3221224576 3221223744 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4593 603 41 0 5224 0
vsize: 21060
[startup+909.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 91007 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+919.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 92008 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+929.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 93008 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+939.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 94008 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223712 134560652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+949.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 95009 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+959.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 96009 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+969.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 97009 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+979.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 98010 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+989.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 99010 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+999.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 100010 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 101011 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 102011 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 103011 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4620 0 0 0 104012 16 0 0 25 0 1 0 423189154 21565440 4594 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5265 4594 603 41 0 5224 0
vsize: 21060
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4652 0 0 0 105012 16 0 0 25 0 1 0 423189154 21712896 4626 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5301 4626 603 41 0 5260 0
vsize: 21204
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4708 0 0 0 106012 16 0 0 25 0 1 0 423189154 21843968 4682 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5333 4682 603 41 0 5292 0
vsize: 21332
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4823 0 0 0 107012 17 0 0 25 0 1 0 423189154 22372352 4797 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5462 4797 603 41 0 5421 0
vsize: 21848
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4860 0 0 0 108012 17 0 0 25 0 1 0 423189154 22503424 4834 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4834 603 41 0 5453 0
vsize: 21976
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4863 0 0 0 109012 17 0 0 25 0 1 0 423189154 22503424 4837 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4837 603 41 0 5453 0
vsize: 21976
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4866 0 0 0 110013 17 0 0 25 0 1 0 423189154 22503424 4840 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4840 603 41 0 5453 0
vsize: 21976
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4871 0 0 0 111013 17 0 0 25 0 1 0 423189154 22503424 4845 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4845 603 41 0 5453 0
vsize: 21976
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4871 0 0 0 112013 17 0 0 25 0 1 0 423189154 22503424 4845 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4845 603 41 0 5453 0
vsize: 21976
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4871 0 0 0 113014 17 0 0 25 0 1 0 423189154 22503424 4845 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4845 603 41 0 5453 0
vsize: 21976
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4871 0 0 0 114014 17 0 0 25 0 1 0 423189154 22503424 4845 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4845 603 41 0 5453 0
vsize: 21976
[startup+1149.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4873 0 0 0 115014 17 0 0 25 0 1 0 423189154 22503424 4847 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4847 603 41 0 5453 0
vsize: 21976
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4873 0 0 0 116015 17 0 0 25 0 1 0 423189154 22503424 4847 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4847 603 41 0 5453 0
vsize: 21976
[startup+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4880 0 0 0 117015 17 0 0 25 0 1 0 423189154 22503424 4854 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4854 603 41 0 5453 0
vsize: 21976
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4880 0 0 0 118016 17 0 0 25 0 1 0 423189154 22503424 4854 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4854 603 41 0 5453 0
vsize: 21976
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4880 0 0 0 119016 17 0 0 25 0 1 0 423189154 22503424 4854 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4854 603 41 0 5453 0
vsize: 21976
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2792
Raw data (stat): 2792 (minisat+) R 2791 29653 29652 0 -1 0 4880 0 0 0 120016 17 0 0 25 0 1 0 423189154 22503424 4854 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4854 603 41 0 5453 0
vsize: 21976
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2792
Raw data (stat): 2792 (minisat+) Z 2791 29653 29652 0 -1 12 4883 0 0 0 120016 18 0 0 25 0 1 0 423189154 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.01
CPU time (s): 1200.36
CPU user time (s): 1200.17
CPU system time (s): 0.186971
CPU usage (%): 100.029
Max. virtual memory (Kb): 21976
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####