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/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare2_1.opb
MD5SUM	375b355299c9fbf8170e172bcbc73eb2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16728
Optimality of the best value was proved	NO
Number of terms in the objective function	140
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	7340025
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	7340025
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.23
Number of variables	242
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	122
Trace number 14690

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-21 00:48:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19498 boxname=wulflinc24 idbench=1500 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  375b355299c9fbf8170e172bcbc73eb2  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2_1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2_1.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2_1.opb
IDLAUNCH: 19498
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        673236 kB
Buffers:         31624 kB
Cached:         296172 kB
SwapCached:        508 kB
Active:          57604 kB
Inactive:       272420 kB
HighTotal:      131008 kB
HighFree:          952 kB
LowTotal:       903652 kB
LowFree:        672284 kB
SwapTotal:     2097892 kB
SwapFree:      2096708 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5932 kB
Slab:            25784 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:08:31 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 19498 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  12]---> Adder-cost: 590   maxlim: 469334   bits: 20/19
c ---[  10]---> Adder-cost: 648   maxlim: 507792   bits: 20/19
c ---[   8]---> Adder-cost: 604   maxlim: 482140   bits: 20/19
c ---[   6]---> Adder-cost: 572   maxlim: 518845   bits: 20/19
c ---[   4]---> Adder-cost: 688   maxlim: 476350   bits: 20/19
c ---[   2]---> Adder-cost: 646   maxlim: 516106   bits: 20/19
c ---[   0]---> Adder-cost: 598   maxlim: 472356   bits: 20/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   30118   108219 |    9035       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4440          
c   -- var.elim.:  2000/4440          
c   -- var.elim.:  3000/4440          
c   -- var.elim.:  4000/4440          
c   -- var.elim.:  4440/4440          
c   -- var.elim.:  420/420          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  106/106          
c   -- var.elim.:  10/10          
c |         0 |   29071   103254 |      --       0       --      -- |     --   | -488/-1441
c |         0 |   29071   103254 |   11628       0        0     nan |  0.000 % |
c |       100 |   29071   103254 |   12791     100      316     3.2 |  6.847 % |
c |       250 |   29071   103254 |   14070     250     1568     6.3 |  6.847 % |
c |       476 |   29071   103254 |   15477     476     4605     9.7 |  6.847 % |
c ==============================================================================
c (current CPU-time: 1.03384 s)
c ==============================================================================
c [1mFound solution: 535232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       506 |   33744   114161 |   10123     506     4766     9.4 |  6.847 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1742          
c   -- var.elim.:  1742/1742          
c   -- var.elim.:  936/936          
c   -- subsuming                       
c   -- var.elim.:  51/51          
c   -- var.elim.:  13/13          
c |       506 |   33144   115611 |      --     506       --      -- |     --   | -600/1451
c |       506 |   33144   115611 |   13257     506     4766     9.4 |  6.847 % |
c |       607 |   33144   115611 |   14583     607    18687    30.8 |  5.783 % |
c |       759 |   33144   115611 |   16041     759    21134    27.8 |  5.783 % |
c |       984 |   33144   115611 |   17645     984    22458    22.8 |  5.783 % |
c ==============================================================================
c (current CPU-time: 1.82472 s)
c ==============================================================================
c [1mFound solution: 342957[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1262 |   33363   116225 |   10008    1262    28819    22.8 |  5.783 % |
c   -- subsuming                       
c   -- var.elim.:  385/385          
c   -- var.elim.:  238/238          
c |      1262 |   33248   116284 |      --    1262       --      -- |     --   | -115/60
c |      1262 |   33248   116284 |   13299    1262    28819    22.8 |  5.783 % |
c |      1363 |   33248   116284 |   14629    1363    30087    22.1 |  5.770 % |
c |      1513 |   33248   116284 |   16092    1513    32585    21.5 |  5.770 % |
c |      1738 |   33248   116284 |   17701    1738    34653    19.9 |  5.770 % |
c |      2075 |   33248   116284 |   19471    2075    39899    19.2 |  5.770 % |
c |      2582 |   33248   116284 |   21418    2582    48389    18.7 |  5.770 % |
c |      3341 |   33248   116284 |   23560    3341    60671    18.2 |  5.770 % |
c |      4480 |   33248   116284 |   25916    4480   108151    24.1 |  5.770 % |
c |      6188 |   33248   116284 |   28508    6188   193467    31.3 |  5.770 % |
c |      8750 |   33248   116284 |   31358    8750   290680    33.2 |  5.770 % |
c |     12595 |   33248   116284 |   34494   12595   584506    46.4 |  5.770 % |
c ==============================================================================
c (current CPU-time: 24.4483 s)
c ==============================================================================
c [1mFound solution: 330104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     18349 |   33344   116588 |   10003   18349  1569045    85.5 |  5.770 % |
c   -- subsuming                       
c   -- var.elim.:  206/206          
c   -- var.elim.:  147/147          
c |     18349 |   33295   116809 |      --   18349       --      -- |     --   | -49/222
c |     18349 |   33295   116809 |   13318   18349  1569045    85.5 |  5.770 % |
c |     18449 |   33295   116809 |   14649   12333  1317489   106.8 |  5.783 % |
c |     18599 |   33295   116809 |   16114   12483  1320273   105.8 |  5.783 % |
c |     18824 |   33295   116809 |   17726   12708  1322986   104.1 |  5.783 % |
c |     19161 |   33295   116809 |   19498   13045  1330045   102.0 |  5.783 % |
c |     19667 |   33295   116809 |   21448   13551  1342048    99.0 |  5.783 % |
c |     20428 |   33295   116809 |   23593   14312  1367257    95.5 |  5.783 % |
c |     21568 |   33295   116809 |   25953   15452  1413455    91.5 |  5.783 % |
c |     23276 |   33295   116809 |   28548   17160  1475755    86.0 |  5.783 % |
c |     25840 |   33295   116809 |   31403   19724  1582484    80.2 |  5.783 % |
c |     29684 |   33295   116809 |   34543   23568  1910865    81.1 |  5.783 % |
c |     35450 |   33295   116809 |   37997   29334  3015577   102.8 |  5.783 % |
c |     44099 |   33295   116809 |   41797   37983  3622740    95.4 |  5.783 % |
c |     57073 |   33295   116809 |   45977   22122  1384429    62.6 |  5.783 % |
c ==============================================================================
c (current CPU-time: 93.4828 s)
c ==============================================================================
c [1mFound solution: 192466[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     67906 |   33371   117061 |   10011   32955  2000322    60.7 |  5.783 % |
c   -- subsuming                       
c   -- var.elim.:  174/174          
c   -- var.elim.:  129/129          
c |     67906 |   33337   117213 |      --   32955       --      -- |     --   | -34/153
c |     67906 |   33337   117213 |   13334   32955  2000322    60.7 |  5.783 % |
c |     68006 |   33337   117213 |   14668   13592   678107    49.9 |  5.793 % |
c |     68156 |   33337   117213 |   16135   13742   680634    49.5 |  5.793 % |
c |     68381 |   33337   117213 |   17748   13967   685137    49.1 |  5.793 % |
c |     68720 |   33337   117213 |   19523   14306   696619    48.7 |  5.793 % |
c |     69227 |   33337   117213 |   21475   14813   711218    48.0 |  5.793 % |
c |     69987 |   33337   117213 |   23623   15573   739617    47.5 |  5.793 % |
c |     71128 |   33337   117213 |   25985   16714   784417    46.9 |  5.793 % |
c |     72838 |   33337   117213 |   28584   18424   864830    46.9 |  5.793 % |
c |     75401 |   33337   117213 |   31442   20987   995562    47.4 |  5.793 % |
c |     79246 |   33337   117213 |   34587   24832  1248778    50.3 |  5.793 % |
c |     85013 |   33337   117213 |   38045   30599  1713883    56.0 |  5.793 % |
c |     93664 |   33337   117213 |   41850   39250  2357369    60.1 |  5.793 % |
c |    106638 |   33337   117213 |   46035   22778  1377346    60.5 |  5.793 % |
c |    126099 |   33337   117213 |   50638   42239  2977910    70.5 |  5.793 % |
c |    155291 |   33337   117213 |   55702   34626  2503577    72.3 |  5.793 % |
c |    199081 |   33337   117213 |   61273   33689  2904713    86.2 |  5.793 % |
c |    264765 |   33275   116692 |   67274   52558  3865168    73.5 |  5.811 % |
c |    363291 |   33275   116692 |   74002   41767  5367748   128.5 |  5.811 % |
c |    511081 |   33256   116598 |   81356   70931  9247820   130.4 |  5.865 % |
c ==============================================================================
c (current CPU-time: 1071.47 s)
c ==============================================================================
c [1mFound solution: 190119[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    513828 |   33327   116849 |    9998   73678  9384219   127.4 |  5.865 % |
c   -- subsuming                       
c   -- var.elim.:  214/214          
c   -- var.elim.:  181/181          
c   -- var.elim.:  14/14          
c |    513828 |   33264   116951 |      --   73678       --      -- |     --   | -62/105
c |    513828 |   33264   116951 |   13305   73673  9383856   127.4 |  5.865 % |
c |    513928 |   33264   116951 |   14636   12876  1122994    87.2 |  5.958 % |
c |    514079 |   33264   116951 |   16099   13027  1125173    86.4 |  5.958 % |
c |    514305 |   33264   116951 |   17709   13253  1129983    85.3 |  5.958 % |
c |    514644 |   33264   116951 |   19480   13592  1136776    83.6 |  5.958 % |
c |    515150 |   33264   116951 |   21428   14098  1153131    81.8 |  5.958 % |
c |    515909 |   33264   116951 |   23571   14857  1181334    79.5 |  5.958 % |
c |    517048 |   33264   116951 |   25928   15996  1234887    77.2 |  5.958 % |
c |    518756 |   33264   116951 |   28521   17704  1340385    75.7 |  5.958 % |
c |    521318 |   33264   116951 |   31373   20266  1465595    72.3 |  5.958 % |
c |    525163 |   33264   116951 |   34511   24111  1740558    72.2 |  5.958 % |
c |    530930 |   33264   116951 |   37962   29878  2166905    72.5 |  5.958 % |
c |    539579 |   33264   116951 |   41758   #### 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.81 0.93 0.90 2/54 22575
Raw data (stat): 22575 (runsolver) R 22574 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540877353 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0006 s]
Raw data (loadavg): 0.84 0.93 0.90 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 2905 0 0 0 991 7 0 0 25 0 1 0 540877353 11485184 2317 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2804 2317 603 41 0 2763 0
vsize: 11216
[startup+20.0009 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 3628 0 0 0 1988 10 0 0 25 0 1 0 540877353 14467072 3040 4294967295 134512640 134672761 3221224528 3221223568 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 3040 603 41 0 3491 0
vsize: 14128
[startup+30.001 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 4233 0 0 0 2987 11 0 0 25 0 1 0 540877353 16363520 3509 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3995 3509 603 41 0 3954 0
vsize: 15980
[startup+40.0006 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 4746 0 0 0 3986 12 0 0 25 0 1 0 540877353 18456576 4022 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4506 4022 603 41 0 4465 0
vsize: 18024
[startup+50.001 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 5323 0 0 0 4984 14 0 0 25 0 1 0 540877353 20807680 4599 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5080 4599 603 41 0 5039 0
vsize: 20320
[startup+60.0011 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 5780 0 0 0 5983 15 0 0 25 0 1 0 540877353 22769664 5056 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5559 5056 603 41 0 5518 0
vsize: 22236
[startup+70.0017 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 6604 0 0 0 6981 17 0 0 25 0 1 0 540877353 26198016 5880 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6396 5880 603 41 0 6355 0
vsize: 25584
[startup+80.0021 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 6905 0 0 0 7981 18 0 0 25 0 1 0 540877353 27504640 6181 4294967295 134512640 134672761 3221224528 3221223712 134615796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6181 603 41 0 6674 0
vsize: 26860
[startup+90.0021 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 6905 0 0 0 8981 18 0 0 25 0 1 0 540877353 27504640 6181 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6181 603 41 0 6674 0
vsize: 26860
[startup+100.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 9980 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 10980 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223712 134615761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+120.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 11981 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 12981 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223664 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 13981 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223568 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 14981 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223712 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 15981 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 16982 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223568 134612572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+180.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7070 0 0 0 17982 18 0 0 25 0 1 0 540877353 27504640 6201 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6201 603 41 0 6674 0
vsize: 26860
[startup+190.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7073 0 0 0 18982 18 0 0 25 0 1 0 540877353 27504640 6204 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6204 603 41 0 6674 0
vsize: 26860
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7234 0 0 0 19982 19 0 0 25 0 1 0 540877353 28172288 6365 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6878 6365 603 41 0 6837 0
vsize: 27512
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7400 0 0 0 20981 19 0 0 25 0 1 0 540877353 28663808 6480 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6998 6480 603 41 0 6957 0
vsize: 27992
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7400 0 0 0 21982 19 0 0 25 0 1 0 540877353 28663808 6480 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6998 6480 603 41 0 6957 0
vsize: 27992
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7400 0 0 0 22982 19 0 0 25 0 1 0 540877353 28663808 6480 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6998 6480 603 41 0 6957 0
vsize: 27992
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7400 0 0 0 23982 19 0 0 25 0 1 0 540877353 28663808 6480 4294967295 134512640 134672761 3221224528 3221223712 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6998 6480 603 41 0 6957 0
vsize: 27992
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7400 0 0 0 24982 19 0 0 25 0 1 0 540877353 28663808 6480 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6998 6480 603 41 0 6957 0
vsize: 27992
[startup+260.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7517 0 0 0 25982 20 0 0 25 0 1 0 540877353 29188096 6597 4294967295 134512640 134672761 3221224528 3221223568 134614346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7126 6597 603 41 0 7085 0
vsize: 28504
[startup+270.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7833 0 0 0 26981 21 0 0 25 0 1 0 540877353 30273536 6887 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7391 6887 603 41 0 7350 0
vsize: 29564
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7833 0 0 0 27982 21 0 0 25 0 1 0 540877353 30273536 6887 4294967295 134512640 134672761 3221224528 3221223520 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7391 6887 603 41 0 7350 0
vsize: 29564
[startup+290.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7833 0 0 0 28982 21 0 0 25 0 1 0 540877353 30273536 6887 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7391 6887 603 41 0 7350 0
vsize: 29564
[startup+300.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7833 0 0 0 29982 21 0 0 25 0 1 0 540877353 30273536 6887 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7391 6887 603 41 0 7350 0
vsize: 29564
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7833 0 0 0 30983 21 0 0 25 0 1 0 540877353 30273536 6887 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7391 6887 603 41 0 7350 0
vsize: 29564
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 7851 0 0 0 31984 21 0 0 25 0 1 0 540877353 30408704 6905 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7424 6905 603 41 0 7383 0
vsize: 29696
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8228 0 0 0 32984 21 0 0 25 0 1 0 540877353 32002048 7282 4294967295 134512640 134672761 3221224528 3221223728 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7813 7282 603 41 0 7772 0
vsize: 31252
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8578 0 0 0 33983 22 0 0 25 0 1 0 540877353 33452032 7632 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8167 7632 603 41 0 8126 0
vsize: 32668
[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8958 0 0 0 34981 24 0 0 25 0 1 0 540877353 34619392 7951 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8452 7951 603 41 0 8411 0
vsize: 33808
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8958 0 0 0 35982 24 0 0 25 0 1 0 540877353 34619392 7951 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8452 7951 603 41 0 8411 0
vsize: 33808
[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8958 0 0 0 36982 24 0 0 25 0 1 0 540877353 34619392 7951 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8452 7951 603 41 0 8411 0
vsize: 33808
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8958 0 0 0 37982 24 0 0 25 0 1 0 540877353 34619392 7951 4294967295 134512640 134672761 3221224528 3221223728 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8452 7951 603 41 0 8411 0
vsize: 33808
[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8958 0 0 0 38982 24 0 0 25 0 1 0 540877353 34619392 7951 4294967295 134512640 134672761 3221224528 3221223728 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8452 7951 603 41 0 8411 0
vsize: 33808
[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8958 0 0 0 39982 24 0 0 25 0 1 0 540877353 34619392 7951 4294967295 134512640 134672761 3221224528 3221223664 134614814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8452 7951 603 41 0 8411 0
vsize: 33808
[startup+410.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8958 0 0 0 40982 24 0 0 25 0 1 0 540877353 34619392 7951 4294967295 134512640 134672761 3221224528 3221223568 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8452 7951 603 41 0 8411 0
vsize: 33808
[startup+420.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 8958 0 0 0 41983 24 0 0 25 0 1 0 540877353 34619392 7951 4294967295 134512640 134672761 3221224528 3221223664 134614505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8452 7951 603 41 0 8411 0
vsize: 33808
[startup+430.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9016 0 0 0 42983 24 0 0 25 0 1 0 540877353 34885632 8009 4294967295 134512640 134672761 3221224528 3221223712 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8517 8009 603 41 0 8476 0
vsize: 34068
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9512 0 0 0 43982 25 0 0 25 0 1 0 540877353 37146624 8505 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9069 8505 603 41 0 9028 0
vsize: 36276
[startup+450.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 44982 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223712 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 45982 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223568 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 46982 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 47982 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223568 134614335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 48982 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223568 134612885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 49983 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 50983 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+520.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 51983 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 52983 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 9871 0 0 0 53983 26 0 0 25 0 1 0 540877353 38268928 8795 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9343 8795 603 41 0 9302 0
vsize: 37372
[startup+550.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 10030 0 0 0 54983 26 0 0 25 0 1 0 540877353 38924288 8954 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9503 8954 603 41 0 9462 0
vsize: 38012
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 10426 0 0 0 55983 27 0 0 25 0 1 0 540877353 40665088 9350 4294967295 134512640 134672761 3221224528 3221223360 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9928 9350 603 41 0 9887 0
vsize: 39712
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 10782 0 0 0 56982 28 0 0 25 0 1 0 540877353 42131456 9706 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9706 603 41 0 10245 0
vsize: 41144
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 11282 0 0 0 57981 29 0 0 25 0 1 0 540877353 44113920 10206 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10770 10206 603 41 0 10729 0
vsize: 43080
[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 11633 0 0 0 58981 29 0 0 25 0 1 0 540877353 45568000 10557 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11125 10557 603 41 0 11084 0
vsize: 44500
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 11917 0 0 0 59980 31 0 0 25 0 1 0 540877353 46743552 10841 4294967295 134512640 134672761 3221224528 3221223520 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11412 10841 603 41 0 11371 0
vsize: 45648
[startup+610.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12218 0 0 0 60979 32 0 0 25 0 1 0 540877353 47943680 11142 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11705 11142 603 41 0 11664 0
vsize: 46820
[startup+620.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12495 0 0 0 61978 32 0 0 25 0 1 0 540877353 49135616 11419 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11996 11419 603 41 0 11955 0
vsize: 47984
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 62978 33 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 63978 33 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 64978 33 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 65978 33 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 66979 33 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223712 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+680.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 67979 33 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223568 134613120 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22575
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 68979 33 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223728 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+700.033 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 22619
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 69979 33 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223568 134612771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+710.033 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 22628
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 70978 34 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223568 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+720.034 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 22628
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 71978 34 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223728 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+730.034 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 22628
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 72978 34 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+740.034 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 22628
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 73978 35 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+750.034 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 22628
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12744 0 0 0 74978 35 0 0 25 0 1 0 540877353 49668096 11567 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11567 603 41 0 12085 0
vsize: 48504
[startup+760.034 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 22628
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12745 0 0 0 75977 36 0 0 25 0 1 0 540877353 49668096 11568 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11568 603 41 0 12085 0
vsize: 48504
[startup+770.035 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12853 0 0 0 76976 37 0 0 25 0 1 0 540877353 50196480 11676 4294967295 134512640 134672761 3221224528 3221223712 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12255 11676 603 41 0 12214 0
vsize: 49020
[startup+780.035 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 77976 37 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+790.035 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 78976 38 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+800.035 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 79976 38 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+810.035 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 80975 39 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+820.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 81975 39 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223696 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+830.037 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 82975 39 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+840.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 83975 40 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+850.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 84974 40 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+860.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 85974 41 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+870.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 86974 41 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+880.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 87974 41 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+890.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 12987 0 0 0 88974 42 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+900.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 89973 43 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+910.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 90973 43 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223568 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+920.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 91973 43 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+930.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 92973 44 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+940.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 93974 44 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+950.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 94974 44 0 0 25 0 1 0 540877353 50319360 11736 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12285 11736 603 41 0 12244 0
vsize: 49140
[startup+960.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 95973 45 0 0 25 0 1 0 540877353 50286592 11728 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 11728 603 41 0 12236 0
vsize: 49108
[startup+970.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 96974 45 0 0 25 0 1 0 540877353 50286592 11728 4294967295 134512640 134672761 3221224528 3221223712 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 11728 603 41 0 12236 0
vsize: 49108
[startup+980.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 97973 46 0 0 25 0 1 0 540877353 50286592 11728 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 11728 603 41 0 12236 0
vsize: 49108
[startup+990.058 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 98973 46 0 0 25 0 1 0 540877353 50286592 11728 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 11728 603 41 0 12236 0
vsize: 49108
[startup+1000.06 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 99973 47 0 0 25 0 1 0 540877353 50286592 11728 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 11728 603 41 0 12236 0
vsize: 49108
[startup+1010.06 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 100972 47 0 0 25 0 1 0 540877353 50286592 11728 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 11728 603 41 0 12236 0
vsize: 49108
[startup+1020.06 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 101972 48 0 0 25 0 1 0 540877353 50286592 11728 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 11728 603 41 0 12236 0
vsize: 49108
[startup+1030.06 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13061 0 0 0 102972 48 0 0 25 0 1 0 540877353 50286592 11728 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12277 11728 603 41 0 12236 0
vsize: 49108
[startup+1040.06 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13391 0 0 0 103971 49 0 0 25 0 1 0 540877353 51736576 12058 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12631 12058 603 41 0 12590 0
vsize: 50524
[startup+1050.06 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 13745 0 0 0 104970 50 0 0 25 0 1 0 540877353 53190656 12412 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12986 12412 603 41 0 12945 0
vsize: 51944
[startup+1060.06 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 22630
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 14217 0 0 0 105969 51 0 0 25 0 1 0 540877353 55050240 12884 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13440 12884 603 41 0 13399 0
vsize: 53760
[startup+1070.06 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 14661 0 0 0 106967 53 0 0 25 0 1 0 540877353 56901632 13328 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 13328 603 41 0 13851 0
vsize: 55568
[startup+1080.06 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 107966 55 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1090.06 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 108966 55 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1100.06 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 109966 55 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1110.06 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 110965 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1120.06 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 111965 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1130.06 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 112965 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1140.06 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 113965 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1150.06 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 114966 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1160.06 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 115966 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 116966 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223568 134612619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 117966 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 118966 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 22632
Raw data (stat): 22575 (minisat+) R 22574 28546 28545 0 -1 0 15049 0 0 0 119966 56 0 0 25 0 1 0 540877353 57565184 13506 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14054 13506 603 41 0 14013 0
vsize: 56216
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 22632
Raw data (stat): 22575 (minisat+) Z 22574 28546 28545 0 -1 12 15050 0 0 0 119966 59 0 0 25 0 1 0 540877353 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.09
CPU time (s): 1200.26
CPU user time (s): 1199.67
CPU system time (s): 0.594909
CPU usage (%): 100.015
Max. virtual memory (Kb): 56216
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####