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-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare1_1.opb
MD5SUM	452acf9ed3adc2d2cfe293dad01c0934
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	167110
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.02
Number of variables	280
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	130
Trace number 20782

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        378616 kB
Buffers:         34328 kB
Cached:         594196 kB
SwapCached:         68 kB
Active:         175928 kB
Inactive:       455484 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        378364 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6880 kB
Slab:            18928 kB
Committed_AS:    63716 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 22:10:02 (client local time) WITH STATUS 10 IN 1200.56 SECONDS
stats: 14480 7 1200.56 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> Adder-cost: 662   maxlim: 3510008   bits: 23/22
c ---[   8]---> Adder-cost: 660   maxlim: 3759828   bits: 23/22
c ---[   6]---> Adder-cost: 770   maxlim: 3884662   bits: 23/22
c ---[   4]---> Adder-cost: 500   maxlim: 3402645   bits: 23/22
c ---[   2]---> Adder-cost: 574   maxlim: 3468109   bits: 23/22
c ---[   0]---> Adder-cost: 558   maxlim: 3462997   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   25754    92792 |    7726       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3817          
c   -- var.elim.:  2000/3817          
c   -- var.elim.:  3000/3817          
c   -- var.elim.:  3817/3817          
c   -- var.elim.:  419/419          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  126/126          
c |         0 |   24713    87653 |      --       0       --      -- |     --   | -495/-1492
c |         0 |   24713    87653 |    9885       0        0     nan |  0.000 % |
c |       100 |   24713    87653 |   10873     100      760     7.6 |  8.757 % |
c |       250 |   24713    87653 |   11961     250     2502    10.0 |  8.757 % |
c ==============================================================================
c (current CPU-time: 0.908861 s)
c ==============================================================================
c [1mFound solution: 7232502[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1725     Base: 2 2 2 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 |       433 |   29107    97922 |    8732     433     3798     8.8 |  8.757 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1650          
c   -- var.elim.:  1650/1650          
c   -- var.elim.:  915/915          
c   -- subsuming                       
c   -- var.elim.:  259/259          
c   -- var.elim.:  84/84          
c |       433 |   28444    99424 |      --     433       --      -- |     --   | -663/1503
c |       433 |   28444    99424 |   11377     433     3798     8.8 |  8.757 % |
c ==============================================================================
c (current CPU-time: 1.22981 s)
c ==============================================================================
c [1mFound solution: 2728458[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 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 |       490 |   28619    99930 |    8585     490     4662     9.5 |  8.757 % |
c   -- subsuming                       
c   -- var.elim.:  448/448          
c   -- var.elim.:  209/209          
c |       490 |   28521    99934 |      --     490       --      -- |     --   | -98/5
c |       490 |   28521    99934 |   11408     490     4662     9.5 |  8.757 % |
c |       590 |   28521    99934 |   12549     590    13685    23.2 |  7.354 % |
c |       740 |   28521    99934 |   13804     740    17306    23.4 |  7.354 % |
c |       965 |   28521    99934 |   15184     965    19812    20.5 |  7.354 % |
c |      1302 |   28521    99934 |   16703    1302    26166    20.1 |  7.354 % |
c |      1809 |   28521    99934 |   18373    1809    34813    19.2 |  7.354 % |
c |      2568 |   28521    99934 |   20210    2568    88650    34.5 |  7.354 % |
c |      3707 |   28521    99934 |   22231    3707   126056    34.0 |  7.354 % |
c ==============================================================================
c (current CPU-time: 3.47447 s)
c ==============================================================================
c [1mFound solution: 2355862[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 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 |      4923 |   28609   100213 |    8582    4923   157250    31.9 |  7.354 % |
c   -- subsuming                       
c   -- var.elim.:  196/196          
c   -- var.elim.:  135/135          
c |      4923 |   28567   100304 |      --    4923       --      -- |     --   | -42/92
c |      4923 |   28567   100304 |   11426    4923   157250    31.9 |  7.354 % |
c ==============================================================================
c (current CPU-time: 3.60345 s)
c ==============================================================================
c [1mFound solution: 1498531[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 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4965 |   28640   100551 |    8591    4965   157458    31.7 |  7.354 % |
c   -- subsuming                       
c   -- var.elim.:  172/172          
c   -- var.elim.:  124/124          
c |      4965 |   28601   100736 |      --    4965       --      -- |     --   | -39/186
c |      4965 |   28601   100736 |   11440    4965   157458    31.7 |  7.354 % |
c |      5067 |   28601   100736 |   12584    5067   169318    33.4 |  7.379 % |
c |      5217 |   28601   100736 |   13842    5217   172237    33.0 |  7.379 % |
c |      5443 |   28601   100736 |   15227    5443   174942    32.1 |  7.379 % |
c |      5782 |   28601   100736 |   16749    5782   182339    31.5 |  7.379 % |
c |      6288 |   28601   100736 |   18424    6288   197298    31.4 |  7.379 % |
c |      7047 |   28601   100736 |   20267    7047   260056    36.9 |  7.379 % |
c |      8187 |   28601   100736 |   22294    8187   318499    38.9 |  7.379 % |
c |      9895 |   28601   100736 |   24523    9895   650375    65.7 |  7.379 % |
c |     12457 |   28601   100736 |   26975   12457   785827    63.1 |  7.379 % |
c |     16303 |   28601   100736 |   29673   16303   983358    60.3 |  7.379 % |
c |     22069 |   28601   100736 |   32640   22069  1372160    62.2 |  7.379 % |
c |     30719 |   28601   100736 |   35904   30719  2184862    71.1 |  7.379 % |
c |     43694 |   28601   100736 |   39495   19866  1447887    72.9 |  7.379 % |
c |     63156 |   28601   100736 |   43444   39328  2685165    68.3 |  7.379 % |
c |     92348 |   28601   100736 |   47789   39270  2822846    71.9 |  7.379 % |
c |    136138 |   28596   100667 |   52559   46980  2562416    54.5 |  7.400 % |
c |    201822 |   28596   100667 |   57815   36813  2394421    65.0 |  7.400 % |
c ==============================================================================
c (current CPU-time: 476.257 s)
c ==============================================================================
c [1mFound solution: 1026678[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 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 |    265063 |   28582   100280 |    8574   52938  6199696   117.1 |  7.400 % |
c   -- subsuming                       
c   -- var.elim.:  192/192          
c   -- var.elim.:  172/172          
c   -- var.elim.:  12/12          
c |    265063 |   28485   100288 |      --   52938       --      -- |     --   | -69/77
c |    265063 |   28485   100288 |   11394   51474  6096850   118.4 |  7.400 % |
c |    265164 |   28485   100288 |   12533    8318   375541    45.1 |  7.622 % |
c |    265316 |   28485   100288 |   13786    8470   378541    44.7 |  7.622 % |
c |    265541 |   28485   100288 |   15165    8695   383438    44.1 |  7.622 % |
c |    265879 |   28485   100288 |   16681    9033   392130    43.4 |  7.622 % |
c |    266385 |   28485   100288 |   18350    9539   403461    42.3 |  7.622 % |
c |    267145 |   28485   100288 |   20185   10299   422560    41.0 |  7.622 % |
c ==============================================================================
c (current CPU-time: 479.796 s)
c ==============================================================================
c [1mFound solution: 883305[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 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 |    267411 |   28543   100508 |    8562   10565   454789    43.0 |  7.622 % |
c   -- subsuming                       
c   -- var.elim.:  192/192          
c   -- var.elim.:  125/125          
c   -- var.elim.:  79/79          
c   -- var.elim.:  76/76          
c   -- var.elim.:  63/63          
c   -- var.elim.:  42/42          
c |    267411 |   28440    99780 |      --   10565       --      -- |     --   | -103/-727
c |    267411 |   28440    99780 |   11376   10548   453661    43.0 |  7.622 % |
c |    267511 |   28440    99780 |   12513   10648   457704    43.0 |  7.649 % |
c |    267663 |   28440    99780 |   13764   10800   461450    42.7 |  7.649 % |
c |    267888 |   28440    99780 |   15141   11025   466563    42.3 |  7.649 % |
c |    268227 |   28440    99780 |   16655   11364   474931    41.8 |  7.649 % |
c |    268734 |   28440    99780 |   18321   11871   490291    41.3 |  7.649 % |
c |    269494 |   28440    99780 |   20153   12631   520025    41.2 |  7.649 % |
c |    270633 |   28440    99780 |   22168   13770   578966    42.0 |  7.649 % |
c |    272341 |   28440    99780 |   24385   15478   643739    41.6 |  7.649 % |
c |    274903 |   28415    99674 |   26800   18038   744157    41.3 |  7.712 % |
c |    278748 |   28415    99674 |   29480   21883   889920    40.7 |  7.712 % |
c |    284515 |   28415    99674 |   32428   27650  1223747    44.3 |  7.711 % |
c |    293164 |   28397    99592 |   35648   17775   737959    41.5 |  7.753 % |
c |    306141 |   28351    99402 |   39150   30746  1372394    44.6 |  7.898 % |
c |    325602 |   28351    99402 |   43065   22758  1653068    72.6 |  7.898 % |
c |    354794 |   28307    99245 |   47298   21863  2236603   102.3 |  8.022 % |
c |    398583 |   28307    99245 |   52027   31898  2123535    66.6 |  8.022 % |
c |    464267 |   28307    99245 |   57230   20005  1949421    97.4 |  8.022 % |
c ==============================================================================
c (current CPU-time: 862.682 s)
c ==============================================================================
c [1mFound solution: 594432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 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 |    465686 |   28376    99480 |    8512   21424  2105389    98.3 |  8.022 % |
c   -- subsuming                       
c   -- var.elim.:  238/238          
c   -- var.elim.:  163/163          
c   -- var.elim.:  17/17          
c |    465686 |   28314    99548 |      --   21424       --      -- |     --   | -62/69
c |    465686 |   28314    99548 |   11325   21424  2105389    98.3 |  8.022 % |
c |    465786 |   28314    99548 |   12458    9622   713852    74.2 |  8.060 % |
c |    465938 |   28314    99548 |   13703    9774   716923    73.4 |  8.060 % |
c |    466164 |   28314    99548 |   15074   10000   720863    72.1 |  8.060 % |
c |    466501 |   28314    99548 |   16581   10337   726985    70.3 |  8.060 % |
c |    467007 |   28314    99548 |   18239   10843   739008    68.2 |  8.060 % |
c |    467767 |   28314    99548 |   20063   11603   762536    65.7 |  8.060 % |
c |    468906 |   28314    99548 |   22070   12742   790975    62.1 |  8.060 % |
c |    470615 |   28286    99427 |   24253   14449   840091    58.1 |  8.122 % |
c |    473177 |   28286    99427 |   26678   17011   944204    55.5 |  8.122 % |
c |    477022 |   28286    99427 |   29346   20856  1109847    53.2 |  8.122 % |
c |    482792 |   28286    99427 |   32281   26626  1438085    54.0 |  8.122 % |
c |    491441 |   28286    99427 |   35509   15599   738339    47.3 |  8.122 % |
c |    504415 |   28286    99427 |   39060   28573  1452749    50.8 |  8.122 % |
c |    523879 |   28286    99427 |   42966   19338  1202720    62.2 |  8.122 % |
c ==============================================================================
c (current CPU-time: 943.616 s)
c ==============================================================================
c [1mFound solution: 365306[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 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    537797 |   28326    99566 |    8497   33255  1864919    56.1 |  8.122 % |
c   -- subsuming                       
c   -- var.elim.:  229/229          
c   -- var.elim.:  154/154          
c   -- var.elim.:  51/51          
c |    537797 |   28140    98731 |      --   33255       --      -- |     --   | -85/-473
c |    537797 |   28140    98731 |   11256   32672  1747650    53.5 |  8.122 % |
c |    537897 |   28140    98731 |   12381    8966   411631    45.9 |  8.516 % |
c |    538048 |   28140    98731 |   13619    9117   412950    45.3 |  8.516 % |
c |    538273 |   28140    98731 |   14981    9342   416686    44.6 |  8.516 % |
c |    538611 |   28140    98731 |   16479    9680   420991    43.5 |  8.516 % |
c |    539117 |   28140    98731 |   18127   10186   438971    43.1 |  8.516 % |
c |    539876 |   28140    98731 |   19940   10945#### 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.85 0.95 0.90 2/54 10554
Raw data (stat): 10554 (runsolver) R 10553 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548455861 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.0007 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 2937 0 0 0 993 5 0 0 25 0 1 0 548455861 10436608 2124 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2548 2124 603 41 0 2507 0
vsize: 10192
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 3769 0 0 0 1990 8 0 0 25 0 1 0 548455861 13828096 2956 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3376 2956 603 41 0 3335 0
vsize: 13504
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 4603 0 0 0 2988 9 0 0 25 0 1 0 548455861 17276928 3790 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4218 3790 603 41 0 4177 0
vsize: 16872
[startup+40.0097 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5185 0 0 0 3987 11 0 0 25 0 1 0 548455861 19795968 4372 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4833 4372 603 41 0 4792 0
vsize: 19332
[startup+50.0253 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5421 0 0 0 4988 11 0 0 25 0 1 0 548455861 20803584 4608 4294967295 134512640 134672761 3221224528 3221223712 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4608 603 41 0 5038 0
vsize: 20316
[startup+60.0255 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5421 0 0 0 5989 12 0 0 25 0 1 0 548455861 20803584 4608 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4608 603 41 0 5038 0
vsize: 20316
[startup+70.0255 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5421 0 0 0 6989 12 0 0 25 0 1 0 548455861 20803584 4608 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4608 603 41 0 5038 0
vsize: 20316
[startup+80.0262 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5590 0 0 0 7988 12 0 0 25 0 1 0 548455861 21458944 4777 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5239 4777 603 41 0 5198 0
vsize: 20956
[startup+90.0256 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5909 0 0 0 8987 13 0 0 25 0 1 0 548455861 22474752 5053 4294967295 134512640 134672761 3221224528 3221223728 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 5053 603 41 0 5446 0
vsize: 21948
[startup+100.026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5909 0 0 0 9987 13 0 0 25 0 1 0 548455861 22474752 5053 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 5053 603 41 0 5446 0
vsize: 21948
[startup+110.026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5909 0 0 0 10988 14 0 0 25 0 1 0 548455861 22474752 5053 4294967295 134512640 134672761 3221224528 3221223568 134612616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 5053 603 41 0 5446 0
vsize: 21948
[startup+120.026 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 5909 0 0 0 11988 14 0 0 25 0 1 0 548455861 22474752 5053 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 5053 603 41 0 5446 0
vsize: 21948
[startup+130.027 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6314 0 0 0 12986 16 0 0 25 0 1 0 548455861 24190976 5458 4294967295 134512640 134672761 3221224528 3221223712 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5906 5458 603 41 0 5865 0
vsize: 23624
[startup+140.027 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6693 0 0 0 13985 16 0 0 25 0 1 0 548455861 25686016 5819 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5819 603 41 0 6230 0
vsize: 25084
[startup+150.027 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6693 0 0 0 14985 16 0 0 25 0 1 0 548455861 25686016 5819 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5819 603 41 0 6230 0
vsize: 25084
[startup+160.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6693 0 0 0 15986 16 0 0 25 0 1 0 548455861 25686016 5819 4294967295 134512640 134672761 3221224528 3221223712 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5819 603 41 0 6230 0
vsize: 25084
[startup+170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6693 0 0 0 16986 17 0 0 25 0 1 0 548455861 25686016 5819 4294967295 134512640 134672761 3221224528 3221223712 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5819 603 41 0 6230 0
vsize: 25084
[startup+180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6693 0 0 0 17986 17 0 0 25 0 1 0 548455861 25686016 5819 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5819 603 41 0 6230 0
vsize: 25084
[startup+190.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6693 0 0 0 18987 17 0 0 25 0 1 0 548455861 25686016 5819 4294967295 134512640 134672761 3221224528 3221223712 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5819 603 41 0 6230 0
vsize: 25084
[startup+200.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6693 0 0 0 19991 17 0 0 25 0 1 0 548455861 25686016 5819 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6271 5819 603 41 0 6230 0
vsize: 25084
[startup+210.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 20991 17 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+220.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 21991 17 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+230.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 22991 17 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+240.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 23991 17 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+250.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 24992 17 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+260.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 25993 17 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+270.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 26993 17 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+280.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 27995 17 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+290.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 28996 18 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+300.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 29997 18 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223520 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+310.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 30997 18 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+320.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 31997 18 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+330.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 32997 18 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+340.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 6751 0 0 0 33998 18 0 0 25 0 1 0 548455861 25686016 5824 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5824 603 41 0 6230 0
vsize: 25084
[startup+350.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 7143 0 0 0 34997 19 0 0 25 0 1 0 548455861 27389952 6216 4294967295 134512640 134672761 3221224528 3221223712 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6687 6216 603 41 0 6646 0
vsize: 26748
[startup+360.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 7861 0 0 0 35995 22 0 0 25 0 1 0 548455861 30257152 6934 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7387 6934 603 41 0 7346 0
vsize: 29548
[startup+370.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8604 0 0 0 36993 24 0 0 25 0 1 0 548455861 33275904 7677 4294967295 134512640 134672761 3221224528 3221223584 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8124 7677 603 41 0 8083 0
vsize: 32496
[startup+380.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8613 0 0 0 37994 24 0 0 25 0 1 0 548455861 33013760 7627 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 7627 603 41 0 8019 0
vsize: 32240
[startup+390.263 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8613 0 0 0 39005 24 0 0 25 0 1 0 548455861 33013760 7627 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 7627 603 41 0 8019 0
vsize: 32240
[startup+400.263 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8613 0 0 0 40006 24 0 0 25 0 1 0 548455861 33013760 7627 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 7627 603 41 0 8019 0
vsize: 32240
[startup+410.266 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8613 0 0 0 41006 24 0 0 25 0 1 0 548455861 33013760 7627 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 7627 603 41 0 8019 0
vsize: 32240
[startup+420.266 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8613 0 0 0 42006 24 0 0 25 0 1 0 548455861 33013760 7627 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 7627 603 41 0 8019 0
vsize: 32240
[startup+430.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8613 0 0 0 43007 24 0 0 25 0 1 0 548455861 33013760 7627 4294967295 134512640 134672761 3221224528 3221223568 134612832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 7627 603 41 0 8019 0
vsize: 32240
[startup+440.285 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8613 0 0 0 44008 24 0 0 25 0 1 0 548455861 33013760 7627 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8060 7627 603 41 0 8019 0
vsize: 32240
[startup+450.284 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 8838 0 0 0 45008 25 0 0 25 0 1 0 548455861 33951744 7852 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8289 7852 603 41 0 8248 0
vsize: 33156
[startup+460.288 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 9425 0 0 0 46006 27 0 0 25 0 1 0 548455861 36450304 8439 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8899 8439 603 41 0 8858 0
vsize: 35596
[startup+470.288 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 9898 0 0 0 47005 28 0 0 25 0 1 0 548455861 38305792 8912 4294967295 134512640 134672761 3221224528 3221223712 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9352 8912 603 41 0 9311 0
vsize: 37408
[startup+480.288 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 48002 29 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223904 134620485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+490.288 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 49001 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+500.288 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 50001 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+510.288 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 51001 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+520.288 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 52001 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+530.289 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 53002 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+540.289 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 54002 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+550.289 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 55002 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+560.29 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 56001 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+570.29 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 57002 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+580.29 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 58002 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+590.29 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 59002 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+600.29 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10554
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 60002 30 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+610.29 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 10607
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 60993 39 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+620.291 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 10607
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 61993 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+630.292 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 10607
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 62993 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223568 134612578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+640.292 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 10607
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 63993 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+650.291 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 10607
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 64994 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+660.292 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 10607
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 65994 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223568 134612653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+670.292 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 10607
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 66994 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+680.294 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 67994 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+690.294 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 68994 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+700.294 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 69995 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+710.294 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 70995 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+720.293 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 71994 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+730.294 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 72995 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+740.294 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 73995 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+750.293 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 74995 40 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+760.293 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 75995 41 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+770.293 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 76995 41 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+780.293 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 77995 41 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+790.293 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 78995 41 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+800.293 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 79995 41 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+810.293 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 80995 41 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+820.293 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10501 0 0 0 81996 41 0 0 25 0 1 0 548455861 39477248 9210 4294967295 134512640 134672761 3221224528 3221223712 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9210 603 41 0 9597 0
vsize: 38552
[startup+830.294 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10513 0 0 0 82996 41 0 0 25 0 1 0 548455861 39608320 9222 4294967295 134512640 134672761 3221224528 3221223728 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9670 9222 603 41 0 9629 0
vsize: 38680
[startup+840.294 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 10882 0 0 0 83995 42 0 0 25 0 1 0 548455861 41074688 9591 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9591 603 41 0 9987 0
vsize: 40112
[startup+850.294 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11176 0 0 0 84994 43 0 0 25 0 1 0 548455861 42270720 9885 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10320 9885 603 41 0 10279 0
vsize: 41280
[startup+860.396 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11345 0 0 0 86004 44 0 0 25 0 1 0 548455861 42893312 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10472 10032 603 41 0 10431 0
vsize: 41888
[startup+870.396 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11495 0 0 0 87003 44 0 0 25 0 1 0 548455861 42893312 10033 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10472 10033 603 41 0 10431 0
vsize: 41888
[startup+880.397 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11495 0 0 0 88003 44 0 0 25 0 1 0 548455861 42893312 10033 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10472 10033 603 41 0 10431 0
vsize: 41888
[startup+890.397 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11528 0 0 0 89003 44 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+900.396 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11528 0 0 0 90003 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+910.397 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11528 0 0 0 91003 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223692 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+920.397 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11528 0 0 0 92004 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+930.398 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10609
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11569 0 0 0 93004 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+940.398 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11569 0 0 0 94004 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+950.398 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 95003 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+960.399 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 96003 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+970.399 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 97003 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+980.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 98003 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+990.401 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 99003 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1000.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 100003 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223728 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1010.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 101004 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223664 134614715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1020.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 102004 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223568 134613769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1030.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 103004 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1040.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 104004 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1050.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 105004 45 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1060.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 106005 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1070.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 107005 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1080.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 108005 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223664 134614503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1090.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 109005 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1100.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 110005 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1110.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 111006 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1120.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 112006 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1130.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 113006 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1140.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 114006 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1150.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 115006 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1160.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 116006 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1170.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 117007 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1180.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 118007 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1190.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 119007 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
[startup+1200.4 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10611
Raw data (stat): 10554 (minisat+) R 10553 22612 22611 0 -1 0 11634 0 0 0 120007 46 0 0 25 0 1 0 548455861 42889216 10032 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10471 10032 603 41 0 10430 0
vsize: 41884
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.43 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 10611
Raw data (stat): 10554 (minisat+) Z 10553 22612 22611 0 -1 12 11635 0 0 0 120007 48 0 0 25 0 1 0 548455861 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.43
CPU time (s): 1200.56
CPU user time (s): 1200.08
CPU system time (s): 0.482926
CPU usage (%): 100.011
Max. virtual memory (Kb): 41888
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####