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-f51m.b.opb
MD5SUM	4fc22abde8250807abd95442a25fac44
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	18
Optimality of the best value was proved	NO
Number of terms in the objective function	407
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	407
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	407
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.02684
Number of variables	406
Total number of constraints	538
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	18
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 4664

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-13 19:44:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3453 boxname=wulflinc4 idbench=69 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4fc22abde8250807abd95442a25fac44  /oldhome/oroussel/tmp/wulflinc4/normalized-f51m.b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc4/normalized-f51m.b.opb /oldhome/oroussel/tmp/wulflinc4/normalized-f51m.b.opb
IDLAUNCH: 3453
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 2
cpu MHz		: 451.169
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:        930160 kB
Buffers:         34052 kB
Cached:          51152 kB
SwapCached:          0 kB
Active:          49308 kB
Inactive:        38728 kB
HighTotal:      131008 kB
HighFree:        76048 kB
LowTotal:       903652 kB
LowFree:        854112 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10860 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:04:13 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3453 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 498 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 |     498    13351 |     166       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 796   maxlim: 381   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |    6026    33082 |    2008       1       18    18.0 |  0.000 % |
c |       101 |    6026    33082 |    2208     101      416     4.1 |  0.993 % |
c |       251 |    6026    33082 |    2429     251     1340     5.3 |  0.993 % |
c |       476 |    6026    33082 |    2672     476     2570     5.4 |  0.993 % |
c |       813 |    6019    33059 |    2939     808    11208    13.9 |  1.076 % |
c |      1319 |    6010    33028 |    3233    1305    35096    26.9 |  1.159 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1885 |    6008    33028 |    2002    1865    49481    26.5 |  1.159 % |
c |      1986 |    5990    32966 |    2202    1958    53905    27.5 |  1.489 % |
c |      2136 |    5990    32966 |    2422    2108    60876    28.9 |  1.488 % |
c |      2362 |    5981    32935 |    2664    2328    74214    31.9 |  1.570 % |
c |      2699 |    5981    32935 |    2931    2665    91356    34.3 |  1.570 % |
c |      3206 |    5927    32755 |    3224    1663    41615    25.0 |  2.397 % |
c |      3969 |    5927    32755 |    3546    2426   101616    41.9 |  2.397 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 383   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4454 |    5871    32544 |    1957    2861   127662    44.6 |  2.397 % |
c |      4554 |    5871    32544 |    2152    1531    36822    24.1 |  3.716 % |
c |      4706 |    5871    32544 |    2367    1683    47007    27.9 |  3.716 % |
c |      4932 |    5871    32544 |    2604    1909    60554    31.7 |  3.716 % |
c |      5270 |    5871    32544 |    2865    2247    85664    38.1 |  3.716 % |
c |      5777 |    5871    32544 |    3151    2754   118222    42.9 |  3.716 % |
c ==============================================================================
c [1mFound solution: 23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 384   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5806 |    5872    32550 |    1957    2783   119377    42.9 |  3.716 % |
c |      5906 |    5872    32550 |    2152    1492    35299    23.7 |  3.795 % |
c |      6058 |    5872    32550 |    2367    1644    42972    26.1 |  3.795 % |
c |      6284 |    5872    32550 |    2604    1870    55596    29.7 |  3.795 % |
c |      6623 |    5872    32550 |    2865    2209    83170    37.7 |  3.795 % |
c |      7130 |    5872    32550 |    3151    2716   116195    42.8 |  3.795 % |
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 385   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7473 |    5873    32555 |    1957    3059   134162    43.9 |  3.795 % |
c |      7573 |    5873    32555 |    2152    1630    41127    25.2 |  3.875 % |
c |      7723 |    5873    32555 |    2367    1780    48893    27.5 |  3.875 % |
c |      7950 |    5873    32555 |    2604    2007    60391    30.1 |  3.877 % |
c |      8291 |    5873    32555 |    2865    2348    92965    39.6 |  3.875 % |
c |      8798 |    5873    32555 |    3151    2855   136526    47.8 |  3.875 % |
c |      9559 |    5873    32555 |    3466    1904    75879    39.9 |  3.875 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 386   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10081 |    5874    32561 |    1958    2426   109676    45.2 |  3.875 % |
c |     10182 |    5874    32561 |    2153    1314    19587    14.9 |  3.954 % |
c |     10333 |    5874    32561 |    2369    1465    31015    21.2 |  3.954 % |
c |     10559 |    5874    32561 |    2606    1691    39939    23.6 |  3.954 % |
c |     10897 |    5874    32561 |    2866    2029    55593    27.4 |  3.954 % |
c |     11405 |    5874    32561 |    3153    2537    96281    38.0 |  3.954 % |
c |     12165 |    5874    32561 |    3468    1673    50378    30.1 |  3.954 % |
c |     13304 |    5874    32561 |    3815    2812   152245    54.1 |  3.954 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 387   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14693 |    5875    32565 |    1958    4201   321196    76.5 |  3.954 % |
c |     14796 |    5875    32565 |    2153    1154    21472    18.6 |  4.033 % |
c |     14947 |    5814    32350 |    2369    1293    23610    18.3 |  4.856 % |
c |     15175 |    5814    32350 |    2606    1521    34693    22.8 |  4.856 % |
c |     15513 |    5814    32350 |    2866    1859    54296    29.2 |  4.856 % |
c |     16020 |    5814    32350 |    3153    2366    91284    38.6 |  4.856 % |
c |     16783 |    5798    32298 |    3468    3124   129529    41.5 |  5.103 % |
c |     17922 |    5798    32298 |    3815    2162   105221    48.7 |  5.103 % |
c |     19630 |    5789    32267 |    4197    3862   258850    67.0 |  5.186 % |
c |     22192 |    5789    32267 |    4616    4203   296167    70.5 |  5.185 % |
c |     26038 |    5789    32267 |    5078    3070   219250    71.4 |  5.185 % |
c |     31807 |    5763    32177 |    5586    3527   238232    67.5 |  5.514 % |
c |     40456 |    5763    32177 |    6145    3313   252630    76.3 |  5.514 % |
c |     53432 |    5763    32177 |    6759    6533   507935    77.7 |  5.514 % |
c |     72893 |    5763    32177 |    7435    5041   307318    61.0 |  5.514 % |
c |    102088 |    5763    32177 |    8179    7163   519599    72.5 |  5.514 % |
c |    145877 |    5763    32177 |    8996    4438   201992    45.5 |  5.514 % |
c |    211561 |    5763    32177 |    9896    5431   289750    53.4 |  5.514 % |
c |    310091 |    5757    32157 |   10886    7343   558801    76.1 |  5.597 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 388   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    357627 |    5758    32163 |    1919   10319   696098    67.5 |  5.597 % |
c |    357728 |    5758    32163 |    2110    1391    22399    16.1 |  5.674 % |
c |    357878 |    5758    32163 |    2321    1541    29824    19.4 |  5.674 % |
c |    358103 |    5758    32163 |    2554    1766    38646    21.9 |  5.674 % |
c |    358440 |    5758    32163 |    2809    2103    61013    29.0 |  5.674 % |
c |    358946 |    5758    32163 |    3090    2609   103082    39.5 |  5.674 % |
c |    359706 |    5758    32163 |    3399    3369   166163    49.3 |  5.674 % |
c |    360848 |    5758    32163 |    3739    2633   141718    53.8 |  5.674 % |
c |    362558 |    5758    32163 |    4113    2345   106842    45.6 |  5.674 % |
c |    365123 |    5758    32163 |    4524    2768   154767    55.9 |  5.674 % |
c |    368969 |    5758    32163 |    4977    4159   294147    70.7 |  5.674 % |
c |    374737 |    5758    32163 |    5475    4605   403133    87.5 |  5.674 % |
c |    383386 |    5723    32042 |    6022    4627   263795    57.0 |  6.086 % |
c |    396360 |    5723    32042 |    6624    4785   400413    83.7 |  6.086 % |
c |    415823 |    5723    32042 |    7287    3638   142677    39.2 |  6.086 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 389   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    425303 |    5724    32047 |    1908    5554   291758    52.5 |  6.086 % |
c |    425406 |    5724    32047 |    2098    1492    23466    15.7 |  6.163 % |
c |    425556 |    5724    32047 |    2308    1642    31685    19.3 |  6.163 % |
c |    425781 |    5724    32047 |    2539    1867    47209    25.3 |  6.163 % |
c |    426119 |    5724    32047 |    2793    2205    63661    28.9 |  6.163 % |
c |    426625 |    5724    32047 |    3072    2711   100769    37.2 |  6.163 % |
c |    427384 |    5724    32047 |    3380    1867    53013    28.4 |  6.163 % |
c |    428525 |    5724    32047 |    3718    3008   141392    47.0 |  6.163 % |
c |    430234 |    5724    32047 |    4089    2658   108839    40.9 |  6.163 % |
c |    432797 |    5724    32047 |    4498    2876   147818    51.4 |  6.163 % |
c |    436642 |    5701    31968 |    4948    4340   219045    50.5 |  6.491 % |
c |    442408 |    5701    31968 |    5443    4797   201923    42.1 |  6.491 % |
c |    451057 |    5701    31968 |    5988    4845   281746    58.2 |  6.491 % |
c |    464034 |    5701    31968 |    6586    5438   297168    54.6 |  6.491 % |
c |    483496 |    5701    31968 |    7245    4429   286633    64.7 |  6.491 % |
c |    512688 |    5701    31968 |    7970    7245   474620    65.5 |  6.491 % |
c |    556477 |    5701    31968 |    8767    5440   427967    78.7 |  6.491 % |
c |    622161 |    5701    31968 |    9643    7918   624010    78.8 |  6.491 % |
c |    720688 |    5701    31968 |   10608    6909   371521    53.8 |  6.491 % |
c |    868478 |    5701    31968 |   11669    8100   520547    64.3 |  6.491 % |
c |   1090167 |    5695    31948 |   12836    9634   544019    56.5 |  6.574 % |
#### 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.84 0.94 0.69 2/54 7299
Raw data (stat): 7299 (runsolver) R 7298 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420341325 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.0004 s]
Raw data (loadavg): 0.87 0.94 0.69 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 899 0 0 0 995 2 0 0 25 0 1 0 420341325 5144576 877 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1256 877 603 41 0 1215 0
vsize: 5024
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.94 0.69 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1300 0 0 0 1994 4 0 0 25 0 1 0 420341325 6897664 1278 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1684 1278 603 41 0 1643 0
vsize: 6736
[startup+30.0024 s]
Raw data (loadavg): 0.90 0.94 0.69 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1308 0 0 0 2993 4 0 0 25 0 1 0 420341325 6897664 1286 4294967295 134512640 134672761 3221224576 3221223760 134559318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1684 1286 603 41 0 1643 0
vsize: 6736
[startup+40.0028 s]
Raw data (loadavg): 0.92 0.94 0.70 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1309 0 0 0 3993 4 0 0 25 0 1 0 420341325 6897664 1287 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1684 1287 603 41 0 1643 0
vsize: 6736
[startup+50.003 s]
Raw data (loadavg): 0.93 0.94 0.70 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1350 0 0 0 4993 4 0 0 25 0 1 0 420341325 7032832 1328 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1717 1328 603 41 0 1676 0
vsize: 6868
[startup+60.0038 s]
Raw data (loadavg): 0.94 0.95 0.70 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1390 0 0 0 5993 4 0 0 25 0 1 0 420341325 7168000 1368 4294967295 134512640 134672761 3221224576 3221223728 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1750 1368 603 41 0 1709 0
vsize: 7000
[startup+70.0044 s]
Raw data (loadavg): 0.95 0.95 0.71 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1505 0 0 0 6993 4 0 0 25 0 1 0 420341325 7749632 1483 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1892 1483 603 41 0 1851 0
vsize: 7568
[startup+80.0045 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1550 0 0 0 7993 5 0 0 25 0 1 0 420341325 7880704 1528 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1924 1528 603 41 0 1883 0
vsize: 7696
[startup+90.0053 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1590 0 0 0 8993 5 0 0 25 0 1 0 420341325 8015872 1568 4294967295 134512640 134672761 3221224576 3221223632 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1957 1568 603 41 0 1916 0
vsize: 7828
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.71 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1591 0 0 0 9993 5 0 0 25 0 1 0 420341325 8015872 1569 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1957 1569 603 41 0 1916 0
vsize: 7828
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1591 0 0 0 10994 5 0 0 25 0 1 0 420341325 8015872 1569 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1957 1569 603 41 0 1916 0
vsize: 7828
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1610 0 0 0 11994 5 0 0 25 0 1 0 420341325 8163328 1588 4294967295 134512640 134672761 3221224576 3221223712 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1993 1588 603 41 0 1952 0
vsize: 7972
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1648 0 0 0 12994 5 0 0 25 0 1 0 420341325 8298496 1626 4294967295 134512640 134672761 3221224576 3221223680 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2026 1626 603 41 0 1985 0
vsize: 8104
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1733 0 0 0 13994 5 0 0 25 0 1 0 420341325 8699904 1711 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2124 1711 603 41 0 2083 0
vsize: 8496
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1735 0 0 0 14994 5 0 0 25 0 1 0 420341325 8699904 1713 4294967295 134512640 134672761 3221224576 3221223532 1075350787 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2124 1713 603 41 0 2083 0
vsize: 8496
[startup+160.008 s]
Raw data (loadavg): 0.99 0.95 0.73 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1735 0 0 0 15994 5 0 0 25 0 1 0 420341325 8699904 1713 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2124 1713 603 41 0 2083 0
vsize: 8496
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 1973 0 0 0 16994 5 0 0 25 0 1 0 420341325 9637888 1951 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2353 1951 603 41 0 2312 0
vsize: 9412
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2196 0 0 0 17994 6 0 0 25 0 1 0 420341325 10567680 2174 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2580 2174 603 41 0 2539 0
vsize: 10320
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2196 0 0 0 18994 6 0 0 25 0 1 0 420341325 10567680 2174 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2580 2174 603 41 0 2539 0
vsize: 10320
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2222 0 0 0 19994 6 0 0 25 0 1 0 420341325 10698752 2200 4294967295 134512640 134672761 3221224576 3221222796 134566364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2200 603 41 0 2571 0
vsize: 10448
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2240 0 0 0 20995 6 0 0 25 0 1 0 420341325 10698752 2218 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2218 603 41 0 2571 0
vsize: 10448
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2241 0 0 0 21995 6 0 0 25 0 1 0 420341325 10698752 2219 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2219 603 41 0 2571 0
vsize: 10448
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2241 0 0 0 22995 6 0 0 25 0 1 0 420341325 10698752 2219 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2219 603 41 0 2571 0
vsize: 10448
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2241 0 0 0 23995 6 0 0 25 0 1 0 420341325 10698752 2219 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2219 603 41 0 2571 0
vsize: 10448
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2241 0 0 0 24995 6 0 0 25 0 1 0 420341325 10698752 2219 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2219 603 41 0 2571 0
vsize: 10448
[startup+260.018 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 25996 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 26995 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 27995 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 28996 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 29996 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 30996 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223760 134559176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 31996 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+330.021 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 32996 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 33996 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 34997 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 35997 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 36997 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 37997 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 38997 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 39998 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 40998 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 41998 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2242 0 0 0 42998 6 0 0 25 0 1 0 420341325 10698752 2220 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2220 603 41 0 2571 0
vsize: 10448
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2244 0 0 0 43998 6 0 0 25 0 1 0 420341325 10698752 2222 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2612 2222 603 41 0 2571 0
vsize: 10448
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 44998 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 45999 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 46999 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 47999 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 48999 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+500.028 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 49999 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 50999 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 51999 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2263 0 0 0 53000 7 0 0 25 0 1 0 420341325 10833920 2241 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2241 603 41 0 2604 0
vsize: 10580
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2316 0 0 0 54000 7 0 0 25 0 1 0 420341325 11104256 2294 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2711 2294 603 41 0 2670 0
vsize: 10844
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2344 0 0 0 55000 7 0 0 25 0 1 0 420341325 11243520 2322 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2745 2322 603 41 0 2704 0
vsize: 10980
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2379 0 0 0 56000 7 0 0 25 0 1 0 420341325 11378688 2357 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2357 603 41 0 2737 0
vsize: 11112
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2379 0 0 0 57000 7 0 0 25 0 1 0 420341325 11378688 2357 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2357 603 41 0 2737 0
vsize: 11112
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 58000 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 59000 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 60000 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 61000 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 62000 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+630.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 63001 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+640.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 64001 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+650.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 65001 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 66001 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 67001 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2384 0 0 0 68001 7 0 0 25 0 1 0 420341325 11378688 2362 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2362 603 41 0 2737 0
vsize: 11112
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2550 0 0 0 69001 8 0 0 25 0 1 0 420341325 12050432 2528 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2528 603 41 0 2901 0
vsize: 11768
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2550 0 0 0 70001 8 0 0 25 0 1 0 420341325 12050432 2528 4294967295 134512640 134672761 3221224576 3221223760 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2528 603 41 0 2901 0
vsize: 11768
[startup+710.035 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2551 0 0 0 71002 8 0 0 25 0 1 0 420341325 12050432 2529 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2529 603 41 0 2901 0
vsize: 11768
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2551 0 0 0 72002 8 0 0 25 0 1 0 420341325 12050432 2529 4294967295 134512640 134672761 3221224576 3221223680 134555084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2529 603 41 0 2901 0
vsize: 11768
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2562 0 0 0 73002 8 0 0 25 0 1 0 420341325 12050432 2540 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2540 603 41 0 2901 0
vsize: 11768
[startup+740.036 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2567 0 0 0 74002 8 0 0 25 0 1 0 420341325 12206080 2545 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2980 2545 603 41 0 2939 0
vsize: 11920
[startup+750.036 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2598 0 0 0 75002 8 0 0 25 0 1 0 420341325 12206080 2576 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2980 2576 603 41 0 2939 0
vsize: 11920
[startup+760.037 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2643 0 0 0 76002 8 0 0 25 0 1 0 420341325 12496896 2621 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2621 603 41 0 3010 0
vsize: 12204
[startup+770.038 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 77002 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+780.038 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 78003 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+790.038 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 79003 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+800.039 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 80003 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+810.039 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 81003 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+820.039 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 82003 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+830.039 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 83004 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223760 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+840.04 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 84004 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+850.04 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2646 0 0 0 85004 8 0 0 25 0 1 0 420341325 12496896 2624 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2624 603 41 0 3010 0
vsize: 12204
[startup+860.041 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2651 0 0 0 86004 8 0 0 25 0 1 0 420341325 12496896 2629 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2629 603 41 0 3010 0
vsize: 12204
[startup+870.041 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2651 0 0 0 87004 8 0 0 25 0 1 0 420341325 12496896 2629 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2629 603 41 0 3010 0
vsize: 12204
[startup+880.041 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2651 0 0 0 88005 8 0 0 25 0 1 0 420341325 12496896 2629 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2629 603 41 0 3010 0
vsize: 12204
[startup+890.043 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2651 0 0 0 89005 8 0 0 25 0 1 0 420341325 12496896 2629 4294967295 134512640 134672761 3221224576 3221223680 134555330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3051 2629 603 41 0 3010 0
vsize: 12204
[startup+900.043 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2652 0 0 0 90004 8 0 0 25 0 1 0 420341325 12496896 2630 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2630 603 41 0 3010 0
vsize: 12204
[startup+910.043 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2652 0 0 0 91004 8 0 0 25 0 1 0 420341325 12496896 2630 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2630 603 41 0 3010 0
vsize: 12204
[startup+920.044 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2652 0 0 0 92004 8 0 0 25 0 1 0 420341325 12496896 2630 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2630 603 41 0 3010 0
vsize: 12204
[startup+930.043 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2657 0 0 0 93004 8 0 0 25 0 1 0 420341325 12496896 2635 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3051 2635 603 41 0 3010 0
vsize: 12204
[startup+940.043 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2690 0 0 0 94004 9 0 0 25 0 1 0 420341325 12632064 2668 4294967295 134512640 134672761 3221224576 3221223712 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3084 2668 603 41 0 3043 0
vsize: 12336
[startup+950.044 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 7299
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2691 0 0 0 95005 9 0 0 25 0 1 0 420341325 12632064 2669 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3084 2669 603 41 0 3043 0
vsize: 12336
[startup+960.044 s]
Raw data (loadavg): 1.07 0.99 0.86 2/54 7352
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2695 0 0 0 96000 13 0 0 25 0 1 0 420341325 12775424 2673 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3119 2673 603 41 0 3078 0
vsize: 12476
[startup+970.044 s]
Raw data (loadavg): 1.06 0.99 0.86 2/54 7352
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2713 0 0 0 97000 13 0 0 25 0 1 0 420341325 12775424 2691 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3119 2691 603 41 0 3078 0
vsize: 12476
[startup+980.045 s]
Raw data (loadavg): 1.05 0.99 0.86 2/54 7352
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2716 0 0 0 98001 13 0 0 25 0 1 0 420341325 12775424 2694 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3119 2694 603 41 0 3078 0
vsize: 12476
[startup+990.045 s]
Raw data (loadavg): 1.04 0.99 0.86 2/54 7352
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2776 0 0 0 99001 13 0 0 25 0 1 0 420341325 13037568 2754 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3183 2754 603 41 0 3142 0
vsize: 12732
[startup+1000.05 s]
Raw data (loadavg): 1.04 0.99 0.86 2/54 7352
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2781 0 0 0 100000 13 0 0 25 0 1 0 420341325 13197312 2759 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3222 2759 603 41 0 3181 0
vsize: 12888
[startup+1010.05 s]
Raw data (loadavg): 1.03 0.99 0.86 2/54 7352
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2786 0 0 0 101000 13 0 0 25 0 1 0 420341325 13197312 2764 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3222 2764 603 41 0 3181 0
vsize: 12888
[startup+1020.05 s]
Raw data (loadavg): 1.03 0.99 0.86 2/54 7352
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 2787 0 0 0 102001 13 0 0 25 0 1 0 420341325 13197312 2765 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3222 2765 603 41 0 3181 0
vsize: 12888
[startup+1030.05 s]
Raw data (loadavg): 1.02 0.99 0.87 2/54 7352
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3063 0 0 0 103000 14 0 0 25 0 1 0 420341325 14270464 3041 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3041 603 41 0 3443 0
vsize: 13936
[startup+1040.05 s]
Raw data (loadavg): 1.02 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3063 0 0 0 104000 14 0 0 25 0 1 0 420341325 14270464 3041 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3041 603 41 0 3443 0
vsize: 13936
[startup+1050.05 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3063 0 0 0 105000 14 0 0 25 0 1 0 420341325 14270464 3041 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3041 603 41 0 3443 0
vsize: 13936
[startup+1060.05 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3063 0 0 0 106000 14 0 0 25 0 1 0 420341325 14270464 3041 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3041 603 41 0 3443 0
vsize: 13936
[startup+1070.05 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3063 0 0 0 107001 14 0 0 25 0 1 0 420341325 14270464 3041 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3041 603 41 0 3443 0
vsize: 13936
[startup+1080.05 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3063 0 0 0 108001 14 0 0 25 0 1 0 420341325 14270464 3041 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3041 603 41 0 3443 0
vsize: 13936
[startup+1090.05 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3063 0 0 0 109001 14 0 0 25 0 1 0 420341325 14270464 3041 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3041 603 41 0 3443 0
vsize: 13936
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3064 0 0 0 110001 14 0 0 25 0 1 0 420341325 14270464 3042 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3042 603 41 0 3443 0
vsize: 13936
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3064 0 0 0 111001 14 0 0 25 0 1 0 420341325 14270464 3042 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3042 603 41 0 3443 0
vsize: 13936
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3064 0 0 0 112002 14 0 0 25 0 1 0 420341325 14270464 3042 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3484 3042 603 41 0 3443 0
vsize: 13936
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3078 0 0 0 113002 14 0 0 25 0 1 0 420341325 14405632 3056 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3517 3056 603 41 0 3476 0
vsize: 14068
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3094 0 0 0 114002 14 0 0 25 0 1 0 420341325 14405632 3072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3517 3072 603 41 0 3476 0
vsize: 14068
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3137 0 0 0 115002 15 0 0 25 0 1 0 420341325 14540800 3115 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3550 3115 603 41 0 3509 0
vsize: 14200
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3137 0 0 0 116002 15 0 0 25 0 1 0 420341325 14540800 3115 4294967295 134512640 134672761 3221224576 3221223724 134559754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3550 3115 603 41 0 3509 0
vsize: 14200
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3137 0 0 0 117002 15 0 0 25 0 1 0 420341325 14540800 3115 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3550 3115 603 41 0 3509 0
vsize: 14200
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3138 0 0 0 118002 15 0 0 25 0 1 0 420341325 14540800 3116 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3550 3116 603 41 0 3509 0
vsize: 14200
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3138 0 0 0 119002 15 0 0 25 0 1 0 420341325 14540800 3116 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3550 3116 603 41 0 3509 0
vsize: 14200
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 7354
Raw data (stat): 7299 (minisat+) R 7298 5897 5896 0 -1 0 3138 0 0 0 120002 15 0 0 25 0 1 0 420341325 14540800 3116 4294967295 134512640 134672761 3221224576 3221223664 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3550 3116 603 41 0 3509 0
vsize: 14200
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.88 1/54 7354
Raw data (stat): 7299 (minisat+) Z 7298 5897 5896 0 -1 12 3141 0 0 0 120002 16 0 0 25 0 1 0 420341325 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.06
CPU time (s): 1200.19
CPU user time (s): 1200.03
CPU system time (s): 0.160975
CPU usage (%): 100.01
Max. virtual memory (Kb): 14200
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####