PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a2.opb
MD5SUM	6005a01d3f2ae55b0ca9c19f876c5827
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	139
Optimality of the best value was proved	NO
Number of terms in the objective function	360
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	360
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	360
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	360
Total number of constraints	980
Number of constraints which are clauses	980
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 4735

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 20:07:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3548 boxname=wulflinc20 idbench=164 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6005a01d3f2ae55b0ca9c19f876c5827  /oldhome/oroussel/tmp/wulflinc20/normalized-ii8a2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-ii8a2.opb /oldhome/oroussel/tmp/wulflinc20/normalized-ii8a2.opb
IDLAUNCH: 3548
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        897192 kB
Buffers:         32748 kB
Cached:          69404 kB
SwapCached:       2636 kB
Active:          43440 kB
Inactive:        64236 kB
HighTotal:      131008 kB
HighFree:        57876 kB
LowTotal:       903652 kB
LowFree:        839316 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24244 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:27:19 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3548 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 980 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     980     2412 |     326       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 150[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 712   maxlim: 210   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |    5921    20042 |    1973       3       20     6.7 |  0.000 % |
c |       103 |    5921    20042 |    2170     103     1129    11.0 |  0.464 % |
c |       253 |    5921    20042 |    2387     253     2753    10.9 |  0.464 % |
c |       478 |    5921    20042 |    2626     478     5430    11.4 |  0.464 % |
c |       816 |    5921    20042 |    2888     816    14979    18.4 |  0.464 % |
c |      1322 |    5921    20042 |    3177    1322    24939    18.9 |  0.464 % |
c |      2081 |    5921    20042 |    3495    2081    47351    22.8 |  0.464 % |
c |      3220 |    5921    20042 |    3844    3220    78132    24.3 |  0.464 % |
c |      4929 |    5921    20042 |    4229    2829    68983    24.4 |  0.464 % |
c |      7491 |    5921    20042 |    4652    3124    81798    26.2 |  0.464 % |
c |     11336 |    5921    20042 |    5117    4335   191066    44.1 |  0.464 % |
c |     17102 |    5921    20042 |    5629    4449   273111    61.4 |  0.464 % |
c |     25751 |    5921    20042 |    6192    4039   142903    35.4 |  0.466 % |
c |     38726 |    5921    20042 |    6811    6859   519188    75.7 |  0.464 % |
c ==============================================================================
c [1mFound solution: 149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 211   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55689 |    5922    20050 |    1974    5551   291947    52.6 |  0.464 % |
c |     55790 |    5922    20050 |    2171    1489    27859    18.7 |  0.559 % |
c |     55941 |    5922    20050 |    2388    1640    31243    19.1 |  0.557 % |
c |     56167 |    5922    20050 |    2627    1866    36654    19.6 |  0.557 % |
c |     56504 |    5922    20050 |    2890    2203    44163    20.0 |  0.557 % |
c |     57011 |    5922    20050 |    3179    2710    54832    20.2 |  0.557 % |
c |     57770 |    5922    20050 |    3497    3469    82189    23.7 |  0.557 % |
c |     58911 |    5922    20050 |    3846    2564    84320    32.9 |  0.557 % |
c |     60619 |    5922    20050 |    4231    4272   152528    35.7 |  0.557 % |
c |     63182 |    5922    20050 |    4654    4699   219384    46.7 |  0.557 % |
c |     67026 |    5922    20050 |    5120    3538   199432    56.4 |  0.557 % |
c |     72792 |    5922    20050 |    5632    3530   154742    43.8 |  0.557 % |
c |     81442 |    5922    20050 |    6195    5925   365894    61.8 |  0.557 % |
c |     94417 |    5922    20050 |    6814    5362   341438    63.7 |  0.557 % |
c |    113879 |    5922    20050 |    7496    6418   474860    74.0 |  0.557 % |
c |    143071 |    5922    20050 |    8245    4015   168711    42.0 |  0.557 % |
c |    186860 |    5922    20050 |    9070    8574   600083    70.0 |  0.557 % |
c |    252545 |    5922    20050 |    9977    7775   459180    59.1 |  0.557 % |
c ==============================================================================
c [1mFound solution: 148[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 212   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    304933 |    5925    20066 |    1975    7474   570819    76.4 |  0.557 % |
c |    305034 |    5925    20066 |    2172    1970    56579    28.7 |  0.651 % |
c |    305185 |    5925    20066 |    2389    2121    58387    27.5 |  0.649 % |
c |    305411 |    5925    20066 |    2628    2347    63138    26.9 |  0.649 % |
c |    305748 |    5925    20066 |    2891    1354    16103    11.9 |  0.649 % |
c |    306255 |    5925    20066 |    3180    1861    31824    17.1 |  0.649 % |
c |    307014 |    5925    20066 |    3498    2620    54104    20.7 |  0.651 % |
c |    308154 |    5925    20066 |    3848    1970    34953    17.7 |  0.649 % |
c |    309862 |    5925    20066 |    4233    3678    91083    24.8 |  0.649 % |
c |    312425 |    5925    20066 |    4656    3984   124424    31.2 |  0.649 % |
c |    316270 |    5925    20066 |    5122    2660    72988    27.4 |  0.652 % |
c |    322036 |    5925    20066 |    5634    2906   111951    38.5 |  0.649 % |
c |    330685 |    5925    20066 |    6198    5583   237865    42.6 |  0.649 % |
c |    343660 |    5925    20066 |    6818    5488   243623    44.4 |  0.649 % |
c |    363121 |    5925    20066 |    7500    6619   435109    65.7 |  0.649 % |
c |    392313 |    5925    20066 |    8250    7637   626777    82.1 |  0.649 % |
c |    436103 |    5925    20066 |    9075    6945   359210    51.7 |  0.649 % |
c |    501787 |    5925    20066 |    9982    6362   365411    57.4 |  0.649 % |
c |    600313 |    5925    20066 |   10980    5893   341547    58.0 |  0.649 % |
c ==============================================================================
c [1mFound solution: 147[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 213   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    602510 |    5926    20075 |    1975    8090   446855    55.2 |  0.649 % |
c |    602611 |    5926    20075 |    2172    1113     6706     6.0 |  0.741 % |
c |    602761 |    5926    20075 |    2389    1263     8786     7.0 |  0.741 % |
c |    602986 |    5926    20075 |    2628    1488    11103     7.5 |  0.741 % |
c |    603324 |    5926    20075 |    2891    1826    18007     9.9 |  0.741 % |
c |    603830 |    5926    20075 |    3180    2332    30524    13.1 |  0.741 % |
c |    604590 |    5926    20075 |    3498    3092    73543    23.8 |  0.741 % |
c |    605729 |    5926    20075 |    3848    2354    46628    19.8 |  0.741 % |
c |    607437 |    5926    20075 |    4233    4062   118537    29.2 |  0.741 % |
c |    609999 |    5926    20075 |    4656    4456   141875    31.8 |  0.741 % |
c |    613844 |    5926    20075 |    5122    3319   122792    37.0 |  0.741 % |
c |    619610 |    5926    20075 |    5634    3436   171803    50.0 |  0.741 % |
c |    628259 |    5926    20075 |    6198    5897   327891    55.6 |  0.742 % |
c |    641236 |    5926    20075 |    6818    6055   243007    40.1 |  0.741 % |
c |    660697 |    5926    20075 |    7500    7145   437237    61.2 |  0.741 % |
c |    689890 |    5926    20075 |    8250    8033   465714    58.0 |  0.741 % |
c |    733679 |    5926    20075 |    9075    4561   126454    27.7 |  0.741 % |
c |    799365 |    5926    20075 |    9982    7577   481056    63.5 |  0.741 % |
c |    897894 |    5926    20075 |   10980    5624   352301    62.6 |  0.741 % |
c |   1045684 |    5926    20075 |   12078    8369   553484    66.1 |  0.741 % |
c |   1267367 |    5926    20075 |   13286    9191   635478    69.1 |  0.741 % |
#### 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.93 0.97 0.87 2/54 30277
Raw data (stat): 30277 (runsolver) R 30276 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478704311 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.94 0.97 0.87 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 845 0 0 0 995 2 0 0 25 0 1 0 478704311 4997120 823 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1220 823 603 41 0 1179 0
vsize: 4880
[startup+20.0018 s]
Raw data (loadavg): 0.95 0.97 0.87 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1096 0 0 0 1994 3 0 0 25 0 1 0 478704311 6074368 1074 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1483 1074 603 41 0 1442 0
vsize: 5932
[startup+30.0024 s]
Raw data (loadavg): 0.95 0.97 0.87 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1096 0 0 0 2994 4 0 0 25 0 1 0 478704311 6074368 1074 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1483 1074 603 41 0 1442 0
vsize: 5932
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.97 0.87 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1096 0 0 0 3994 4 0 0 25 0 1 0 478704311 6074368 1074 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1483 1074 603 41 0 1442 0
vsize: 5932
[startup+50.0019 s]
Raw data (loadavg): 0.97 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1124 0 0 0 4994 4 0 0 25 0 1 0 478704311 6074368 1102 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1483 1102 603 41 0 1442 0
vsize: 5932
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1238 0 0 0 5994 4 0 0 25 0 1 0 478704311 6610944 1216 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1614 1216 603 41 0 1573 0
vsize: 6456
[startup+70.002 s]
Raw data (loadavg): 0.97 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1273 0 0 0 6994 4 0 0 25 0 1 0 478704311 6742016 1251 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1646 1251 603 41 0 1605 0
vsize: 6584
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1293 0 0 0 7994 5 0 0 25 0 1 0 478704311 6926336 1271 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1691 1271 603 41 0 1650 0
vsize: 6764
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1370 0 0 0 8993 5 0 0 25 0 1 0 478704311 7192576 1348 4294967295 134512640 134672761 3221224576 3221223680 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1756 1348 603 41 0 1715 0
vsize: 7024
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1395 0 0 0 9993 5 0 0 25 0 1 0 478704311 7323648 1373 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1788 1373 603 41 0 1747 0
vsize: 7152
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1443 0 0 0 10993 6 0 0 25 0 1 0 478704311 7458816 1421 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1821 1421 603 41 0 1780 0
vsize: 7284
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1556 0 0 0 11993 6 0 0 25 0 1 0 478704311 7999488 1534 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1953 1534 603 41 0 1912 0
vsize: 7812
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1556 0 0 0 12993 6 0 0 25 0 1 0 478704311 7999488 1534 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1953 1534 603 41 0 1912 0
vsize: 7812
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1556 0 0 0 13993 6 0 0 25 0 1 0 478704311 7999488 1534 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1953 1534 603 41 0 1912 0
vsize: 7812
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1556 0 0 0 14994 6 0 0 25 0 1 0 478704311 7999488 1534 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1953 1534 603 41 0 1912 0
vsize: 7812
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1666 0 0 0 15994 6 0 0 25 0 1 0 478704311 8404992 1644 4294967295 134512640 134672761 3221224576 3221223760 134559422 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2052 1644 603 41 0 2011 0
vsize: 8208
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1780 0 0 0 16994 6 0 0 25 0 1 0 478704311 8802304 1758 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2149 1758 603 41 0 2108 0
vsize: 8596
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1880 0 0 0 17993 7 0 0 25 0 1 0 478704311 9203712 1858 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2247 1858 603 41 0 2206 0
vsize: 8988
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1880 0 0 0 18993 7 0 0 25 0 1 0 478704311 9203712 1858 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2247 1858 603 41 0 2206 0
vsize: 8988
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 19993 7 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 20992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 21991 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 22991 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 23992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 24992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 25992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 26992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 27992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134555222 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 28992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 29992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 30992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 31992 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 32993 8 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 33993 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 34993 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 35993 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 36993 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 37993 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 38993 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 39994 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 40994 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 41994 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 42994 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 43994 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 44994 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223760 134558941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 45994 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 46994 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223680 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1890 0 0 0 47995 9 0 0 25 0 1 0 478704311 9338880 1868 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1868 603 41 0 2239 0
vsize: 9120
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1891 0 0 0 48995 9 0 0 25 0 1 0 478704311 9338880 1869 4294967295 134512640 134672761 3221224576 3221223760 134558957 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1869 603 41 0 2239 0
vsize: 9120
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1913 0 0 0 49995 9 0 0 25 0 1 0 478704311 9338880 1891 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2280 1891 603 41 0 2239 0
vsize: 9120
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1917 0 0 0 50995 10 0 0 25 0 1 0 478704311 9482240 1895 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2315 1895 603 41 0 2274 0
vsize: 9260
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 1936 0 0 0 51995 10 0 0 25 0 1 0 478704311 9482240 1914 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2315 1914 603 41 0 2274 0
vsize: 9260
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2102 0 0 0 52994 11 0 0 25 0 1 0 478704311 10153984 2080 4294967295 134512640 134672761 3221224576 3221223760 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2479 2080 603 41 0 2438 0
vsize: 9916
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2177 0 0 0 53994 11 0 0 25 0 1 0 478704311 10420224 2155 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2544 2155 603 41 0 2503 0
vsize: 10176
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2190 0 0 0 54994 11 0 0 25 0 1 0 478704311 10551296 2168 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2576 2168 603 41 0 2535 0
vsize: 10304
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2223 0 0 0 55994 11 0 0 25 0 1 0 478704311 10682368 2201 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2608 2201 603 41 0 2567 0
vsize: 10432
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2223 0 0 0 56994 11 0 0 25 0 1 0 478704311 10682368 2201 4294967295 134512640 134672761 3221224576 3221223760 134559611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2608 2201 603 41 0 2567 0
vsize: 10432
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2223 0 0 0 57995 11 0 0 25 0 1 0 478704311 10682368 2201 4294967295 134512640 134672761 3221224576 3221223740 134564515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2608 2201 603 41 0 2567 0
vsize: 10432
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2223 0 0 0 58995 11 0 0 25 0 1 0 478704311 10682368 2201 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2608 2201 603 41 0 2567 0
vsize: 10432
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2265 0 0 0 59995 12 0 0 25 0 1 0 478704311 10817536 2243 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2641 2243 603 41 0 2600 0
vsize: 10564
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2266 0 0 0 60995 12 0 0 25 0 1 0 478704311 10817536 2244 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2641 2244 603 41 0 2600 0
vsize: 10564
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2266 0 0 0 61995 12 0 0 25 0 1 0 478704311 10817536 2244 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2641 2244 603 41 0 2600 0
vsize: 10564
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2266 0 0 0 62995 12 0 0 25 0 1 0 478704311 10817536 2244 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2641 2244 603 41 0 2600 0
vsize: 10564
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2266 0 0 0 63995 12 0 0 25 0 1 0 478704311 10817536 2244 4294967295 134512640 134672761 3221224576 3221223760 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2641 2244 603 41 0 2600 0
vsize: 10564
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2266 0 0 0 64995 12 0 0 25 0 1 0 478704311 10817536 2244 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2641 2244 603 41 0 2600 0
vsize: 10564
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2273 0 0 0 65995 12 0 0 25 0 1 0 478704311 10817536 2251 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2641 2251 603 41 0 2600 0
vsize: 10564
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2273 0 0 0 66995 12 0 0 25 0 1 0 478704311 10817536 2251 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2641 2251 603 41 0 2600 0
vsize: 10564
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2288 0 0 0 67995 12 0 0 25 0 1 0 478704311 10952704 2266 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2674 2266 603 41 0 2633 0
vsize: 10696
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2288 0 0 0 68996 12 0 0 25 0 1 0 478704311 10936320 2266 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2670 2266 603 41 0 2629 0
vsize: 10680
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2288 0 0 0 69996 12 0 0 25 0 1 0 478704311 10915840 2266 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2665 2266 603 41 0 2624 0
vsize: 10660
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2288 0 0 0 70996 12 0 0 25 0 1 0 478704311 10907648 2266 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2663 2266 603 41 0 2622 0
vsize: 10652
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2310 0 0 0 71996 13 0 0 25 0 1 0 478704311 11042816 2288 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2696 2288 603 41 0 2655 0
vsize: 10784
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2310 0 0 0 72996 13 0 0 25 0 1 0 478704311 11042816 2288 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2696 2288 603 41 0 2655 0
vsize: 10784
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2311 0 0 0 73996 13 0 0 25 0 1 0 478704311 11042816 2289 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2696 2289 603 41 0 2655 0
vsize: 10784
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2311 0 0 0 74996 13 0 0 25 0 1 0 478704311 11042816 2289 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2696 2289 603 41 0 2655 0
vsize: 10784
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2311 0 0 0 75996 13 0 0 25 0 1 0 478704311 11042816 2289 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2696 2289 603 41 0 2655 0
vsize: 10784
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2311 0 0 0 76996 13 0 0 25 0 1 0 478704311 11042816 2289 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2696 2289 603 41 0 2655 0
vsize: 10784
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2324 0 0 0 77996 13 0 0 25 0 1 0 478704311 11042816 2302 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2696 2302 603 41 0 2655 0
vsize: 10784
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2397 0 0 0 78996 14 0 0 25 0 1 0 478704311 11313152 2375 4294967295 134512640 134672761 3221224576 3221223680 134559771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2762 2375 603 41 0 2721 0
vsize: 11048
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2403 0 0 0 79996 14 0 0 25 0 1 0 478704311 11444224 2381 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2794 2381 603 41 0 2753 0
vsize: 11176
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2418 0 0 0 80996 14 0 0 25 0 1 0 478704311 11444224 2396 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2794 2396 603 41 0 2753 0
vsize: 11176
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2431 0 0 0 81996 14 0 0 25 0 1 0 478704311 11591680 2409 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2830 2409 603 41 0 2789 0
vsize: 11320
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2439 0 0 0 82996 14 0 0 25 0 1 0 478704311 11591680 2417 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2830 2417 603 41 0 2789 0
vsize: 11320
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2444 0 0 0 83996 14 0 0 25 0 1 0 478704311 11591680 2422 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2830 2422 603 41 0 2789 0
vsize: 11320
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2459 0 0 0 84996 14 0 0 25 0 1 0 478704311 11591680 2437 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2830 2437 603 41 0 2789 0
vsize: 11320
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2463 0 0 0 85996 14 0 0 25 0 1 0 478704311 11726848 2441 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2441 603 41 0 2822 0
vsize: 11452
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2463 0 0 0 86997 14 0 0 25 0 1 0 478704311 11726848 2441 4294967295 134512640 134672761 3221224576 3221223776 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2441 603 41 0 2822 0
vsize: 11452
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2463 0 0 0 87997 14 0 0 25 0 1 0 478704311 11726848 2441 4294967295 134512640 134672761 3221224576 3221223760 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2441 603 41 0 2822 0
vsize: 11452
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2463 0 0 0 88997 14 0 0 25 0 1 0 478704311 11726848 2441 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2441 603 41 0 2822 0
vsize: 11452
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2463 0 0 0 89997 14 0 0 25 0 1 0 478704311 11726848 2441 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2441 603 41 0 2822 0
vsize: 11452
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2463 0 0 0 90997 14 0 0 25 0 1 0 478704311 11726848 2441 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2441 603 41 0 2822 0
vsize: 11452
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2463 0 0 0 91997 15 0 0 25 0 1 0 478704311 11726848 2441 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2441 603 41 0 2822 0
vsize: 11452
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2463 0 0 0 92997 15 0 0 25 0 1 0 478704311 11726848 2441 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2863 2441 603 41 0 2822 0
vsize: 11452
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2465 0 0 0 93997 15 0 0 25 0 1 0 478704311 11726848 2443 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2863 2443 603 41 0 2822 0
vsize: 11452
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2465 0 0 0 94996 16 0 0 25 0 1 0 478704311 11726848 2443 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2863 2443 603 41 0 2822 0
vsize: 11452
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2484 0 0 0 95996 16 0 0 25 0 1 0 478704311 11726848 2462 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2863 2462 603 41 0 2822 0
vsize: 11452
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2515 0 0 0 96996 16 0 0 25 0 1 0 478704311 11862016 2493 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2896 2493 603 41 0 2855 0
vsize: 11584
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2575 0 0 0 97996 17 0 0 25 0 1 0 478704311 12128256 2553 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2961 2553 603 41 0 2920 0
vsize: 11844
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2608 0 0 0 98995 17 0 0 25 0 1 0 478704311 12263424 2586 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2586 603 41 0 2953 0
vsize: 11976
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2611 0 0 0 99995 18 0 0 25 0 1 0 478704311 12263424 2589 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2589 603 41 0 2953 0
vsize: 11976
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2611 0 0 0 100995 18 0 0 25 0 1 0 478704311 12263424 2589 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2994 2589 603 41 0 2953 0
vsize: 11976
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 101994 19 0 0 25 0 1 0 478704311 12529664 2634 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3059 2634 603 41 0 3018 0
vsize: 12236
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 102995 19 0 0 25 0 1 0 478704311 12521472 2634 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3057 2634 603 41 0 3016 0
vsize: 12228
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 103994 19 0 0 25 0 1 0 478704311 12521472 2634 4294967295 134512640 134672761 3221224576 3221223680 134559778 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3057 2634 603 41 0 3016 0
vsize: 12228
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 104994 19 0 0 25 0 1 0 478704311 12517376 2634 4294967295 134512640 134672761 3221224576 3221223760 134558903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3056 2634 603 41 0 3015 0
vsize: 12224
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 105994 20 0 0 25 0 1 0 478704311 12517376 2634 4294967295 134512640 134672761 3221224576 3221223760 134559599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3056 2634 603 41 0 3015 0
vsize: 12224
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 106994 20 0 0 25 0 1 0 478704311 12517376 2634 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3056 2634 603 41 0 3015 0
vsize: 12224
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 107994 20 0 0 25 0 1 0 478704311 12517376 2634 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3056 2634 603 41 0 3015 0
vsize: 12224
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 108994 20 0 0 25 0 1 0 478704311 12517376 2634 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3056 2634 603 41 0 3015 0
vsize: 12224
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2656 0 0 0 109994 20 0 0 25 0 1 0 478704311 12517376 2634 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3056 2634 603 41 0 3015 0
vsize: 12224
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2666 0 0 0 110995 20 0 0 25 0 1 0 478704311 12517376 2644 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3056 2644 603 41 0 3015 0
vsize: 12224
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2710 0 0 0 111995 21 0 0 25 0 1 0 478704311 12652544 2688 4294967295 134512640 134672761 3221224576 3221223760 134558918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3089 2688 603 41 0 3048 0
vsize: 12356
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2721 0 0 0 112995 21 0 0 25 0 1 0 478704311 12783616 2699 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3121 2699 603 41 0 3080 0
vsize: 12484
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2725 0 0 0 113995 21 0 0 25 0 1 0 478704311 12783616 2703 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3121 2703 603 41 0 3080 0
vsize: 12484
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2730 0 0 0 114995 21 0 0 25 0 1 0 478704311 12783616 2708 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3121 2708 603 41 0 3080 0
vsize: 12484
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2730 0 0 0 115995 21 0 0 25 0 1 0 478704311 12783616 2708 4294967295 134512640 134672761 3221224576 3221223680 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3121 2708 603 41 0 3080 0
vsize: 12484
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2730 0 0 0 116995 21 0 0 25 0 1 0 478704311 12783616 2708 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3121 2708 603 41 0 3080 0
vsize: 12484
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2730 0 0 0 117995 21 0 0 25 0 1 0 478704311 12783616 2708 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3121 2708 603 41 0 3080 0
vsize: 12484
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2730 0 0 0 118995 21 0 0 25 0 1 0 478704311 12783616 2708 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3121 2708 603 41 0 3080 0
vsize: 12484
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 27565 27564 0 -1 0 2730 0 0 0 119995 21 0 0 25 0 1 0 478704311 12783616 2708 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3121 2708 603 41 0 3080 0
vsize: 12484
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30277
Raw data (stat): 30277 (minisat+) Z 30276 27565 27564 0 -1 12 2733 0 0 0 119995 22 0 0 25 0 1 0 478704311 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.18
CPU user time (s): 1199.96
CPU system time (s): 0.224965
CPU usage (%): 100.012
Max. virtual memory (Kb): 12484
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####