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/MIPLIB/miplib/normalized-mps-v2-20-10-lp4l.opb
MD5SUM	3c39e3c2b993ee2185e2a1a3e73b9723
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3744
Optimality of the best value was proved	NO
Number of terms in the objective function	1086
Biggest coefficient in the objective function	283
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	197191
Number of bits of the sum of numbers in the objective function	18
Biggest number in a constraint	283
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	197191
Number of bits of the biggest sum of numbers	18
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	1086
Total number of constraints	1171
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1170
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1086
Trace number 22253

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-22 02:31:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11913 boxname=wulflinc18 idbench=917 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-lp4l.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-lp4l.opb
IDLAUNCH: 11913
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        643556 kB
Buffers:         19300 kB
Cached:         348648 kB
SwapCached:        748 kB
Active:          15820 kB
Inactive:       354172 kB
HighTotal:      131008 kB
HighFree:        84168 kB
LowTotal:       903652 kB
LowFree:        559388 kB
SwapTotal:     2097892 kB
SwapFree:      2096168 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15544 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:51:15 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 11913 7 1200.28 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 169 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 168]---> Adder-cost: 592   maxlim: 2471   bits: 12/12
c ---[ 166]---> BDD-cost:   41
c ---[ 164]---> BDD-cost:   67
c ---[ 162]---> BDD-cost:   99
c ---[ 160]---> BDD-cost:   79
c ---[ 158]---> BDD-cost:   45
c ---[ 156]---> BDD-cost:   69
c ---[ 154]---> BDD-cost:   55
c ---[ 152]---> BDD-cost:   37
c ---[ 150]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   79
c ---[ 144]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   75
c ---[ 140]---> BDD-cost:   77
c ---[ 138]---> BDD-cost:   41
c ---[ 136]---> BDD-cost:   75
c ---[ 134]---> BDD-cost:  107
c ---[ 132]---> BDD-cost:   91
c ---[ 130]---> BDD-cost:  127
c ---[ 128]---> BDD-cost:  123
c ---[ 126]---> BDD-cost:   89
c ---[ 124]---> BDD-cost:   57
c ---[ 122]---> BDD-cost:   89
c ---[ 120]---> BDD-cost:   71
c ---[ 118]---> BDD-cost:  103
c ---[ 116]---> BDD-cost:  117
c ---[ 114]---> BDD-cost:  125
c ---[ 112]---> BDD-cost:   91
c ---[ 110]---> BDD-cost:   59
c ---[ 108]---> BDD-cost:   89
c ---[ 106]---> BDD-cost:   71
c ---[ 104]---> BDD-cost:  129
c ---[ 102]---> BDD-cost:  113
c ---[ 100]---> BDD-cost:  123
c ---[  98]---> BDD-cost:   89
c ---[  96]---> BDD-cost:   61
c ---[  94]---> BDD-cost:   59
c ---[  92]---> BDD-cost:   33
c ---[  90]---> BDD-cost:  123
c ---[  88]---> BDD-cost:  121
c ---[  86]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   45
c ---[  82]---> BDD-cost:   69
c ---[  80]---> BDD-cost:   59
c ---[  78]---> BDD-cost:   33
c ---[  76]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   69
c ---[  72]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   67
c ---[  68]---> BDD-cost:   95
c ---[  66]---> BDD-cost:   85
c ---[  64]---> BDD-cost:  107
c ---[  62]---> BDD-cost:   97
c ---[  60]---> BDD-cost:   33
c ---[  58]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   43
c ---[  48]---> BDD-cost:   75
c ---[  46]---> BDD-cost:  105
c ---[  44]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   63
c ---[  38]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   63
c ---[  32]---> BDD-cost:    5
c ---[  30]---> BDD-cost:  169
c ---[  28]---> BDD-cost:  155
c ---[  26]---> BDD-cost:  115
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   83
c ---[  20]---> BDD-cost:  111
c ---[  18]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  161
c ---[  14]---> BDD-cost:  151
c ---[  12]---> BDD-cost:  117
c ---[  10]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   85
c ---[   6]---> BDD-cost:   71
c ---[   4]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   37
c ---[   0]---> Adder-cost: 2160   maxlim: 1059   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   35697   111365 |   11899       0        0     nan |  0.000 % |
c |       100 |   35673   111283 |   13088      98     3550    36.2 |  1.208 % |
c |       250 |   35673   111283 |   14397     248     6872    27.7 |  1.208 % |
c |       475 |   35673   111283 |   15837     473    22930    48.5 |  1.208 % |
c |       812 |   35582   110964 |   17421     797    32292    40.5 |  1.350 % |
c |      1318 |   35228   109731 |   19163    1236    39075    31.6 |  1.930 % |
c |      2077 |   35115   109352 |   21079    1978    55328    28.0 |  2.083 % |
c |      3216 |   35106   109323 |   23187    3116   134443    43.1 |  2.102 % |
c |      4924 |   35091   109270 |   25506    4817   501813   104.2 |  2.111 % |
c ==============================================================================
c [1mFound solution: 4678[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8142   maxlim: 192513   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5808 |   91968   312356 |   30656    5701   636022   111.6 |  2.111 % |
c |      5908 |   91968   312356 |   33721    5801   638088   110.0 |  1.222 % |
c ==============================================================================
c [1mFound solution: 4381[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192810   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6012 |   91987   312479 |   30662    5905   642881   108.9 |  1.222 % |
c |      6113 |   91987   312479 |   33728    6006   643901   107.2 |  1.248 % |
c |      6263 |   91987   312479 |   37101    6156   648018   105.3 |  1.248 % |
c |      6490 |   91987   312479 |   40811    6383   655375   102.7 |  1.248 % |
c |      6828 |   91987   312479 |   44892    6721   678577   101.0 |  1.248 % |
c |      7334 |   91987   312479 |   49381    7227   710491    98.3 |  1.248 % |
c |      8093 |   91987   312479 |   54319    7986   772776    96.8 |  1.248 % |
c ==============================================================================
c [1mFound solution: 4329[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192862   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8535 |   92003   312609 |   30667    8428   796805    94.5 |  1.248 % |
c |      8635 |   91996   312585 |   33733    8527   798553    93.6 |  1.285 % |
c |      8786 |   91996   312585 |   37107    8678   799323    92.1 |  1.285 % |
c |      9015 |   91996   312585 |   40817    8907   810541    91.0 |  1.285 % |
c ==============================================================================
c [1mFound solution: 4303[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192888   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9343 |   92000   312645 |   30666    9235   872957    94.5 |  1.285 % |
c |      9447 |   92000   312645 |   33732    9339   877086    93.9 |  1.306 % |
c |      9599 |   92000   312645 |   37105    9491   896729    94.5 |  1.306 % |
c |      9825 |   91979   312575 |   40816    9711   900061    92.7 |  1.322 % |
c |     10164 |   91979   312575 |   44898   10050   962481    95.8 |  1.322 % |
c |     10673 |   91967   312533 |   49387   10550  1020834    96.8 |  1.328 % |
c |     11432 |   91967   312533 |   54326   11309  1107842    98.0 |  1.328 % |
c |     12574 |   91967   312533 |   59759   12451  1288451   103.5 |  1.328 % |
c |     14282 |   91951   312481 |   65735   14156  1567998   110.8 |  1.344 % |
c |     16846 |   91944   312457 |   72308   16718  2021257   120.9 |  1.349 % |
c |     20697 |   91944   312457 |   79539   20569  2889530   140.5 |  1.349 % |
c ==============================================================================
c [1mFound solution: 4269[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192922   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21234 |   91954   312544 |   30651   21106  2966775   140.6 |  1.349 % |
c |     21335 |   91898   312350 |   33716   21192  2969519   140.1 |  1.413 % |
c |     21485 |   91898   312350 |   37087   21342  3004545   140.8 |  1.413 % |
c |     21711 |   91785   311959 |   40796   21531  3013007   139.9 |  1.504 % |
c |     22051 |   91785   311959 |   44876   21871  3070258   140.4 |  1.504 % |
c |     22559 |   91785   311959 |   49363   22379  3176774   142.0 |  1.504 % |
c |     23320 |   91756   311856 |   54300   23120  3255681   140.8 |  1.520 % |
c |     24459 |   91756   311856 |   59730   24259  3473974   143.2 |  1.520 % |
c |     26169 |   91756   311856 |   65703   25969  3776044   145.4 |  1.520 % |
c |     28733 |   91756   311856 |   72273   28533  4179806   146.5 |  1.520 % |
c |     32579 |   91676   311577 |   79500   32345  4833206   149.4 |  1.589 % |
c |     38348 |   91676   311577 |   87450   38114  6308737   165.5 |  1.589 % |
c |     46997 |   91601   311320 |   96195   46740  8459122   181.0 |  1.643 % |
c ==============================================================================
c [1mFound solution: 4262[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192929   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59475 |   91556   311180 |   30518   59211 11444311   193.3 |  1.643 % |
c |     59575 |   91556   311180 |   33569   16951  2967034   175.0 |  1.685 % |
c |     59727 |   91556   311180 |   36926   17103  2987056   174.7 |  1.685 % |
c |     59955 |   91556   311180 |   40619   17331  3023499   174.5 |  1.685 % |
c |     60296 |   91556   311180 |   44681   17672  3059606   173.1 |  1.685 % |
c |     60802 |   91556   311180 |   49149   18178  3146794   173.1 |  1.685 % |
c |     61561 |   91556   311180 |   54064   18937  3286300   173.5 |  1.685 % |
c |     62700 |   91556   311180 |   59470   20076  3636099   181.1 |  1.685 % |
c |     64412 |   91556   311180 |   65418   21788  3877981   178.0 |  1.685 % |
c ==============================================================================
c [1mFound solution: 4219[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192972   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66546 |   91560   311241 |   30520   23922  4366619   182.5 |  1.685 % |
c |     66646 |   91560   311241 |   33572   24022  4371054   182.0 |  1.707 % |
c |     66797 |   91560   311241 |   36929   24173  4384424   181.4 |  1.707 % |
c |     67026 |   91560   311241 |   40622   24402  4398296   180.2 |  1.707 % |
c |     67363 |   91560   311241 |   44684   24739  4461698   180.4 |  1.707 % |
c |     67871 |   91560   311241 |   49152   25247  4557821   180.5 |  1.707 % |
c |     68634 |   91560   311241 |   54068   26010  4671976   179.6 |  1.707 % |
c |     69773 |   91560   311241 |   59474   27149  5037188   185.5 |  1.707 % |
c |     71481 |   91560   311241 |   65422   28857  5394646   186.9 |  1.707 % |
c |     74043 |   91535   311160 |   71964   31415  6062380   193.0 |  1.733 % |
c |     77887 |   91535   311160 |   79161   35259  6921757   196.3 |  1.733 % |
c |     83653 |   91535   311160 |   87077   41025  8057816   196.4 |  1.733 % |
c |     92304 |   91535   311160 |   95784   49676 10781790   217.0 |  1.733 % |
c ==============================================================================
c [1mFound solution: 4172[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193019   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95559 |   91542   311224 |   30514   52931 11644687   220.0 |  1.733 % |
c |     95659 |   91542   311224 |   33565   18941  3654438   192.9 |  1.754 % |
c |     95809 |   91542   311224 |   36921   19091  3658733   191.6 |  1.754 % |
c ==============================================================================
c [1mFound solution: 3944[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193247   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95994 |   91551   311287 |   30517   19276  3681560   191.0 |  1.754 % |
c |     96096 |   91551   311287 |   33568   19378  3703843   191.1 |  1.775 % |
c |     96246 |   91551   311287 |   36925   19528  3722802   190.6 |  1.775 % |
c |     96471 |   91551   311287 |   40618   19753  3810541   192.9 |  1.775 % |
c |     96811 |   91551   311287 |   44679   20093  3856602   191.9 |  1.775 % |
c |     97319 |   91551   311287 |   49147   20601  3980720   193.2 |  1.775 % |
c |     98078 |   91551   311287 |   54062   21360  4197445   196.5 |  1.775 % |
c |     99219 |   91551   311287 |   59468   22501  4443126   197.5 |  1.775 % |
c |    100927 |   91551   311287 |   65415   24209  5125900   211.7 |  1.775 % |
c |    103490 |   91551   311287 |   71957   26772  5785251   216.1 |  1.775 % |
c |    107334 |   91551   311287 |   79153   30616  7230782   236.2 |  1.775 % |
c |    113103 |   91551   311287 |   87068   36385  8775221   241.2 |  1.775 % |
c |    121753 |   91551   311287 |   95775   45035 11913321   264.5 |  1.775 % |
c |    134728 |   91506   311130 |  105352   58002 16013485   276.1 |  1.796 % |
c |    154190 |   91497   311099 |  115888   77462 23776761   306.9 |  1.802 % |
c |    183385 |   91480   311042 |  127477  106650 33287203   312.1 |  1.812 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v CO100001_bit0 -CO100002_bit0 -CO100003_bit0 -CO100004_bit0 -CO100005_bit0 -CO100006_bit0 -CO100007_bit0 -CO100008_bit0 -CO100009_bit0 -CO100010_bit0 -CO100011_bit0 -CO100012_bit0 -CO100013_bit0 -CO100014_bit0 -CO100015_bit0 -CO100016_bit0 -CO100017_bit0 -CO100018_bit0 -CO100019_bit0 -CO100020_bit0 -CO100021_bit0 -CO100022_bit0 -CO100023_bit0 -CO100024_bit0 -CO100025_bit0 -CO100026_bit0 CO100027_bit0 -CO100028_bit0 -CO100029_bit0 -CO100030_bit0 -CO100031_bit0 -CO100032_bit0 -CO100033_bit0 -CO100034_bit0 -CO100035_bit0 -CO100036_bit0 -CO100037_bit0 -CO100038_bit0 -CO100039_bit0 -CO100040_bit0 -CO100041_bit0 -CO100042_bit0 -CO100043_bit0 -CO100044_bit0 -CO100045_bit0 -CO100046_bit0 -CO100047_bit0 -CO100048_bit0 -CO100049_bit0 -CO100050_bit0 -CO100051_bit0 -CO100052_bit0 -CO100053_bit0 -CO100054_bit0 -CO100055_bit0 -CO100056_bit0 -CO100057_bit0 -CO100058_bit0 -CO100059_bit0 -CO100060_bit0 -CO100061_bit0 -CO100062_bit0 -CO100063_bit0 -CO100064_bit0 -CO100065_bit0 CO100066_bit0 -CO100067_bit0 -CO100068_bit0 -CO100069_bit0 -CO100070_bit0 -CO100071_bit0 -CO100072_bit0 -CO100073_bit0 -CO100074_bit0 -CO100075_bit0 -CO100076_bit0 -CO100077_bit0 -CO100078_bit0 -CO100079_bit0 -CO100080_bit0 CO100081_bit0 -CO100082_bit0 CO100083_bit0 -CO100084_bit0 -CO100085_bit0 -CO100086_bit0 -CO100087_bit0 -CO100088_bit0 -CO100089_bit0 -CO100090_bit0 -CO100091_bit0 -CO100092_bit0 -CO100093_bit0 -CO100094_bit0 -CO100095_bit0 -CO100096_bit0 -CO100097_bit0 -CO100098_bit0 -CO100099_bit0 CO100100_bit0 -CO100101_bit0 -CO100102_bit0 -CO100103_bit0 -CO100104_bit0 -CO100105_bit0 -CO100106_bit0 -CO100107_bit0 -CO100108_bit0 -CO100109_bit0 CO100110_bit0 -CO100111_bit0 -CO100112_bit0 -CO100113_bit0 -CO100114_bit0 -CO100115_bit0 -CO100116_bit0 -CO100117_bit0 -CO100118_bit0 -CO100119_bit0 -CO100120_bit0 -CO100121_bit0 -CO100122_bit0 -CO100123_bit0 -CO100124_bit0 -CO100125_bit0 -CO100126_bit0 -CO100127_bit0 -CO100128_bit0 -CO100129_bit0 -CO100130_bit0 -CO100131_bit0 -CO100132_bit0 -CO100133_bit0 -CO100134_bit0 CO100135_bit0 -CO100136_bit0 -CO100137_bit0 CO100138_bit0 -CO100139_bit0 -CO100140_bit0 -CO100141_bit0 -CO100142_bit0 -CO100143_bit0 -CO100144_bit0 -CO100145_bit0 -CO100146_bit0 -CO100147_bit0 -CO100148_bit0 -CO100149_bit0 -CO100150_bit0 -CO100151_bit0 -CO100152_bit0 -CO100153_bit0 -CO100154_bit0 -CO100155_bit0 -CO100156_bit0 -CO100157_bit0 -CO100158_bit0 -CO100159_bit0 -CO100160_bit0 -CO100161_bit0 -CO100162_bit0 -CO100163_bit0 -CO100164_bit0 -CO100165_bit0 CO100166_bit0 -CO100167_bit0 -CO100168_bit0 -CO100169_bit0 -CO100170_bit0 -CO100171_bit0 -CO100172_bit0 -CO100173_bit0 -CO100174_bit0 -CO100175_bit0 -CO100176_bit0 -CO100177_bit0 -CO100178_bit0 -CO100179_bit0 -CO100180_bit0 -CO100181_bit0 -CO100182_bit0 -CO100183_bit0 -CO100184_bit0 -CO100185_bit0 -CO100186_bit0 -CO100187_bit0 -CO100188_bit0 -CO100189_bit0 -CO100190_bit0 -CO100191_bit0 -CO100192_bit0 -CO100193_bit0 -CO100194_bit0 -CO100195_bit0 -CO100196_bit0 -CO100197_bit0 -CO100198_bit0 CO100199_bit0 -CO100200_bit0 -CO100201_bit0 -CO100202_bit0 -CO100203_bit0 -CO100204_bit0 -CO100205_bit0 -CO100206_bit0 -CO100207_bit0 -CO100208_bit0 -CO100209_bit0 -CO100210_bit0 -CO100211_bit0 -CO100212_bit0 -CO100213_bit0 -CO100214_bit0 -CO100215_bit0 -CO100216_bit0 -CO100217_bit0 -CO100218_bit0 -CO100219_bit0 -CO100220_bit0 -CO100221_bit0 -CO100222_bit0 -CO100223_bit0 -CO100224_bit0 -CO100225_bit0 -CO100226_bit0 -CO100227_bit0 -CO100228_bit0 -CO100229_bit0 CO100230_bit0 -CO100231_bit0 -CO100232_bit0 -CO100233_bit0 -CO100234_bit0 -CO100235_bit0 -CO100236_bit0 -CO100237_bit0 -CO100238_bit0 -CO100239_bit0 -CO100240_bit0 -CO100241_bit0 -CO100242_bit0 -CO100243_bit0 -CO100244_bit0 -CO100245_bit0 -CO100246_bit0 -CO100247_bit0 -CO100248_bit0 -CO100249_bit0 -CO100250_bit0 -CO100251_bit0 -CO100252_bit0 -CO100253_bit0 -CO100254_bit0 -CO100255_bit0 -CO100256_bit0 -CO100257_bit0 -CO100258_bit0 -CO100259_bit0 -CO100260_bit0 -CO100261_bit0 -CO100262_bit0 -CO100263_bit0 -CO100264_bit0 -CO100265_bit0 -CO100266_bit0 -CO100267_bit0 -CO100268_bit0 -CO100269_bit0 -CO100270_bit0 -CO100271_bit0 -CO100272_bit0 -CO100273_bit0 -CO100274_bit0 -CO100275_bit0 -CO100276_bit0 -CO100277_bit0 -CO100278_bit0 -CO100279_bit0 -CO100280_bit0 -CO100281_bit0 -CO100282_bit0 -CO100283_bit0 -CO100284_bit0 -CO100285_bit0 -CO100286_bit0 -CO100287_bit0 -CO100288_bit0 -CO100289_bit0 -CO100290_bit0 -CO100291_bit0 -CO100292_bit0 -CO100293_bit0 CO100294_bit0 -CO100295_bit0 -CO100296_bit0 -CO100297_bit0 -CO100298_bit0 -CO100299_bit0 -CO100300_bit0 -CO100301_bit0 -CO100302_bit0 -CO100303_bit0 -CO100304_bit0 -CO100305_bit0 -CO100306_bit0 -CO100307_bit0 -CO100308_bit0 -CO100309_bit0 -CO100310_bit0 -CO100311_bit0 -CO100312_bit0 -CO100313_bit0 -CO100314_bit0 -CO100315_bit0 -CO100316_bit0 -CO100317_bit0 -CO100318_bit0 -CO100319_bit0 -CO100320_bit0 -CO100321_bit0 -CO100322_bit0 -CO100323_bit0 -CO100324_bit0 -CO100325_bit0 -CO100326_bit0 -CO100327_bit0 -CO100328_bit0 -CO100329_bit0 -CO100330_bit0 -CO100331_bit0 -CO100332_bit0 -CO100333_bit0 -CO100334_bit0 -CO100335_bit0 -CO100336_bit0 -CO100337_bit0 -CO100338_bit0 -CO100339_bit0 -CO100340_bit0 -CO100341_bit0 -CO100342_bit0 -CO100343_bit0 -CO100344_bit0 -CO100345_bit0 -CO100346_bit0 -CO100347_bit0 -CO100348_bit0 -CO100349_bit0 -CO100350_bit0 -CO100351_bit0 -CO100352_bit0 -CO100353_bit0 -CO100354_bit0 -CO100355_bit0 -CO100356_bit0 -CO100357_bit0 -CO100358_bit0 -CO100359_bit0 -CO100360_bit0 -CO100361_bit0 -CO100362_bit0 -CO100363_bit0 -CO100364_bit0 -CO100365_bit0 -CO100366_bit0 -CO100367_bit0 -CO100368_bit0 -CO100369_bit0 -CO100370_bit0 -CO100371_bit0 -CO100372_bit0 -CO100373_bit0 -CO100374_bit0 -CO100375_bit0 -CO100376_bit0 -CO100377_bit0 -CO100378_bit0 -CO100379_bit0 -CO100380_bit0 -CO100381_bit0 -CO100382_bit0 -CO100383_bit0 -CO100384_bit0 -CO100385_bit0 -CO100386_bit0 -CO100387_bit0 -CO100388_bit0 -CO100389_bit0 -CO100390_bit0 -CO100391_bit0 -CO100392_bit0 -CO100393_bit0 -CO100394_bit0 -CO100395_bit0 -CO100396_bit0 -CO100397_bit0 -CO100398_bit0 -CO100399_bit0 -CO100400_bit0 -CO100401_bit0 -CO100402_bit0 -CO100403_bit0 -CO100404_bit0 -CO100405_bit0 -CO100406_bit0 CO100407_bit0 -CO100408_bit0 -CO100409_bit0 -CO100410_bit0 -CO100411_bit0 -CO100412_bit0 -CO100413_bit0 -CO100414_bit0 -CO100415_bit0 -CO100416_bit0 -CO100417_bit0 -CO100418_bit0 -CO100419_bit0 -CO100420_bit0 -CO100421_bit0 -CO100422_bit0 -CO100423_bit0 -CO100424_bit0 -CO100425_bit0 -CO100426_bit0 -CO100427_bit0 -CO100428_bit0 -CO100429_bit0 -CO100430_bit0 -CO100431_bit0 -CO100432_bit0 -CO100433_bit0 -CO100434_bit0 -CO100435_bit0 -CO100436_bit0 -CO100437_bit0 -CO100438_bit0 -CO100439_bit0 -CO100440_bit0 -CO100441_bit0 -CO100442_bit0 -CO100443_bit0 -CO100444_bit0 -CO100445_bit0 CO100446_bit0 -CO100447_bit0 -CO100448_bit0 -CO100449_bit0 -CO100450_bit0 -CO100451_bit0 -CO100452_bit0 -CO100453_bit0 -CO100454_bit0 -CO100455_bit0 -CO100456_bit0 -CO100457_bit0 -CO100458_bit0 -CO100459_bit0 -CO100460_bit0 -CO100461_bit0 -CO100462_bit0 -CO100463_bit0 -CO100464_bit0 -CO100465_bit0 -CO100466_bit0 -CO100467_bit0 -CO100468_bit0 -CO100469_bit0 -CO100470_bit0 -CO100471_bit0 -CO100472_bit0 -CO100473_bit0 -CO100474_bit0 -CO100475_bit0 -CO100476_bit0 -CO100477_bit0 -CO100478_bit0 -CO100479_bit0 -CO100480_bit0 -CO100481_bit0 -CO100482_bit0 -CO100483_bit0 -CO100484_bit0 -CO100485_bit0 -CO100486_bit0 -CO100487_bit0 -CO100488_bit0 -CO100489_bit0 -CO100490_bit0 -CO100491_bit0 -CO100492_bit0 -CO100493_bit0 -CO100494_bit0 -CO100495_bit0 -CO100496_bit0 -CO100497_bit0 -CO100498_bit0 -CO100499_bit0 -CO100500_bit0 -CO100501_bit0 -CO100502_bit0 -CO100503_bit0 -CO100504_bit0 -CO100505_bit0 -CO100506_bit0 -CO100507_bit0 -CO100508_bit0 -CO100509_bit0 CO100510_bit0 -CO100511_bit0 -CO100512_bit0 -CO100513_bit0 -CO100514_bit0 -CO100515_bit0 -CO100516_bit0 -CO100517_bit0 -CO100518_bit0 -CO100519_bit0 -CO100520_bit0 -CO100521_bit0 -CO100522_bit0 -CO100523_bit0 -CO100524_bit0 -CO100525_bit0 -CO100526_bit0 -CO100527_bit0 -CO100528_bit0 -CO100529_bit0 -CO100530_bit0 -CO100531_bit0 -CO100532_bit0 -CO100533_bit0 -CO100534_bit0 -CO100535_bit0 -CO100536_bit0 -CO100537_bit0 -CO100538_bit0 -CO100539_bit0 -CO100540_bit0 -CO100541_bit0 -CO100542_bit0 -CO100543_bit0 -CO100544_bit0 -CO100545_bit0 -CO100546_bit0 -CO100547_bit0 -CO100548_bit0 -CO100549_bit0 -CO100550_bit0 -CO100551_bit0 CO100552_bit0 -CO100553_bit0 -CO100554_bit0 -CO100555_bit0 -CO100556_bit0 -CO100557_bit0 -CO100558_bit0 -CO100559_bit0 -CO100560_bit0 -CO100561_bit0 -CO100562_bit0 -CO100563_bit0 -CO100564_bit0 -CO100565_bit0 -CO100566_bit0 -CO100567_bit0 -CO100568_bit0 -CO100569_bit0 -CO100570_bit0 -CO100571_bit0 -CO100572_bit0 CO100573_bit0 -CO100574_bit0 -CO100575_bit0 -CO100576_bit0 -CO100577_bit0 -CO100578_bit0 -CO100579_bit0 -CO100580_bit0 -CO100581_bit0 -CO100582_bit0 -CO100583_bit0 -CO100584_bit0 -CO100585_bit0 -CO100586_bit0 -CO100587_bit0 -CO100588_bit0 -CO100589_bit0 -CO100590_bit0 -CO100591_bit0 -CO100592_bit0 -CO100593_bit0 -CO100594_bit0 -CO100595_bit0 -CO100596_bit0 -CO100597_bit0 -CO100598_bit0 -CO100599_bit0 -CO100600_bit0 -CO100601_bit0 -CO100602_bit0 -CO100603_bit0 -CO100604_bit0 -CO100605_bit0 -CO100606_bit0 -CO100607_bit0 -CO100608_bit0 -CO100609_bit0 -CO100610_bit0 -CO100611_bit0 -CO100612_bit0 -CO100613_bit0 -CO100614_bit0 -CO100615_bit0 -CO100616_bit0 -CO100617_bit0 -CO100618_bit0 -CO100619_bit0 -CO100620_bit0 -CO100621_bit0 -CO100622_bit0 -CO100623_bit0 -CO100624_bit0 -CO100625_bit0 -CO100626_bit0 -CO100627_bit0 -CO100628_bit0 -CO100629_bit0 -CO100630_bit0 -CO100631_bit0 -CO100632_bit0 -CO100633_bit0 -CO100634_bit0 -CO100635_bit0 -CO100636_bit0 -CO100637_bit0 -CO100638_bit0 -CO100639_bit0 -CO100640_bit0 -CO100641_bit0 -CO100642_bit0 -CO100643_bit0 -CO100644_bit0 -CO100645_bit0 -CO100646_bit0 -CO100647_bit0 -CO100648_bit0 -CO100649_bit0 -CO100650_bit0 -CO100651_bit0 -CO100652_bit0 -CO100653_bit0 -CO100654_bit0 -CO100655_bit0 -CO100656_bit0 -CO100657_bit0 -CO100658_bit0 -CO100659_bit0 -CO100660_bit0 -CO100661_bit0 -CO100662_bit0 -CO100663_bit0 -CO100664_bit0 -CO100665_bit0 -CO100666_bit0 -CO100667_bit0 -CO100668_bit0 -CO100669_bit0 -CO100670_bit0 -CO100671_bit0 -CO100672_bit0 -CO100673_bit0 -CO100674_bit0 -CO100675_bit0 -CO100676_bit0 -CO100677_bit0 -CO100678_bit0 -CO100679_bit0 -CO100680_bit0 -CO100681_bit0 -CO100682_bit0 -CO100683_bit0 -CO100684_bit0 -CO100685_bit0 -CO100686_bit0 -CO100687_bit0 -CO100688_bit0 -CO100689_bit0 -CO100690_bit0 -CO100691_bit0 -CO100692_bit0 -CO100693_bit0 -CO100694_bit0 -CO100695_bit0 -CO100696_bit0 -CO100697_bit0 -CO100698_bit0 -CO100699_bit0 -CO100700_bit0 -CO100701_bit0 -CO100702_bit0 -CO100703_bit0 CO100704_bit0 -CO100705_bit0 -CO100706_bit0 -CO100707_bit0 -CO100708_bit0 -CO100709_bit0 -CO100710_bit0 -CO100711_bit0 -CO100712_bit0 -CO100713_bit0 -CO100714_bit0 -CO100715_bit0 -CO100716_bit0 -CO100717_bit0 -CO100718_bit0 -CO100719_bit0 -CO100720_bit0 -CO100721_bit0 -CO100722_bit0 -CO100723_bit0 -CO100724_bit0 -CO100725_bit0 -CO100726_bit0 -CO100727_bit0 -CO100728_bit0 -CO100729_bit0 -CO100730_bit0 -CO100731_bit0 -CO100732_bit0 -CO100733_bit0 -CO100734_bit0 -CO100735_bit0 -CO100736_bit0 -CO100737_bit0 -CO100738_bit0 -CO100739_bit0 -CO100740_bit0 -CO100741_bit0 -CO100742_bit0 -CO100743_bit0 -CO100744_bit0 -CO100745_bit0 -CO100746_bit0 -CO100747_bit0 -CO100748_bit0 -CO100749_bit0 -CO100750_bit0 CO100751_bit0 -CO100752_bit0 -CO100753_bit0 -CO100754_bit0 -CO100755_bit0 -CO100756_bit0 -CO100757_bit0 -CO100758_bit0 CO100759_bit0 -CO100760_bit0 -CO100761_bit0 -CO100762_bit0 -CO100763_bit0 -CO100764_bit0 -CO100765_bit0 -CO100766_bit0 -CO100767_bit0 -CO100768_bit0 -CO100769_bit0 -CO100770_bit0 -CO100771_bit0 -CO100772_bit0 -CO100773_bit0 -CO100774_bit0 -CO100775_bit0 -CO100776_bit0 -CO100777_bit0 -CO100778_bit0 -CO100779_bit0 -CO100780_bit0 -CO100781_bit0 -CO100782_bit0 -CO100783_bit0 -CO100784_bit0 -CO100785_bit0 -CO100786_bit0 -CO100787_bit0 -CO100788_bit0 -CO100789_bit0 -CO100790_bit0 -CO100791_bit0 -CO100792_bit0 -CO100793_bit0 -CO100794_bit0 -CO100795_bit0 -CO100796_bit0 -CO100797_bit0 -CO100798_bit0 -CO100799_bit0 -CO100800_bit0 -CO100801_bit0 -CO100802_bit0 -CO100803_bit0 -CO100804_bit0 -CO100805_bit0 -CO100806_bit0 -CO100807_bit0 -CO100808_bit0 -CO100809_bit0 -CO100810_bit0 -CO100811_bit0 -CO100812_bit0 -CO100813_bit0 -CO100814_bit0 -CO100815_bit0 -CO100816_bit0 -CO100817_bit0 -CO100818_bit0#### 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): 1.05 0.99 0.91 2/55 15146
Raw data (stat): 15146 (runsolver) R 15145 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550129565 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 2636 0 1 0 991 7 0 0 25 0 1 0 550129565 12840960 2489 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3135 2489 603 41 0 3094 0
vsize: 12540
[startup+20.0022 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 7152 0 1 0 1979 19 0 0 25 0 1 0 550129565 30240768 6252 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7383 6252 603 41 0 7342 0
vsize: 29532
[startup+30.0031 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 7555 0 1 0 2977 21 0 0 25 0 1 0 550129565 31604736 6571 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7716 6571 603 41 0 7675 0
vsize: 30864
[startup+40.0037 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 8009 0 1 0 3976 23 0 0 25 0 1 0 550129565 33492992 7025 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8177 7025 603 41 0 8136 0
vsize: 32708
[startup+50.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 8515 0 1 0 4974 25 0 0 25 0 1 0 550129565 35594240 7531 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8690 7531 603 41 0 8649 0
vsize: 34760
[startup+60.0059 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 9072 0 1 0 5972 27 0 0 25 0 1 0 550129565 37883904 8088 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9249 8088 603 41 0 9208 0
vsize: 36996
[startup+70.0064 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 9619 0 1 0 6970 29 0 0 25 0 1 0 550129565 39686144 8551 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9689 8551 603 41 0 9648 0
vsize: 38756
[startup+80.0067 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 10008 0 1 0 7968 30 0 0 25 0 1 0 550129565 41304064 8940 4294967295 134512640 134672761 3221224624 3221223792 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10084 8940 603 41 0 10043 0
vsize: 40336
[startup+90.0076 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 10470 0 1 0 8968 31 0 0 25 0 1 0 550129565 43188224 9402 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10544 9402 603 41 0 10503 0
vsize: 42176
[startup+100.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 11017 0 1 0 9966 33 0 0 25 0 1 0 550129565 45486080 9949 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11105 9949 603 41 0 11064 0
vsize: 44420
[startup+110.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 11403 0 1 0 10965 35 0 0 25 0 1 0 550129565 46944256 10335 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11461 10335 603 41 0 11420 0
vsize: 45844
[startup+120.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 11700 0 1 0 11964 35 0 0 25 0 1 0 550129565 48283648 10632 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11788 10632 603 41 0 11747 0
vsize: 47152
[startup+130.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 12144 0 1 0 12963 37 0 0 25 0 1 0 550129565 50163712 11076 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12247 11076 603 41 0 12206 0
vsize: 48988
[startup+140.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 12669 0 1 0 13961 38 0 0 25 0 1 0 550129565 52314112 11601 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12772 11601 603 41 0 12731 0
vsize: 51088
[startup+150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 13108 0 1 0 14960 39 0 0 25 0 1 0 550129565 54067200 12040 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13200 12040 603 41 0 13159 0
vsize: 52800
[startup+160.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 13544 0 1 0 15959 40 0 0 25 0 1 0 550129565 55820288 12476 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13628 12476 603 41 0 13587 0
vsize: 54512
[startup+170.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 14011 0 1 0 16958 42 0 0 25 0 1 0 550129565 57827328 12943 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14118 12943 603 41 0 14077 0
vsize: 56472
[startup+180.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 14521 0 1 0 17956 44 0 0 25 0 1 0 550129565 59842560 13453 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14610 13453 603 41 0 14569 0
vsize: 58440
[startup+190.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 14998 0 1 0 18955 45 0 0 25 0 1 0 550129565 61833216 13930 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15096 13930 603 41 0 15055 0
vsize: 60384
[startup+200.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 15352 0 1 0 19954 46 0 0 25 0 1 0 550129565 63311872 14284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15457 14284 603 41 0 15416 0
vsize: 61828
[startup+210.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 15822 0 1 0 20953 47 0 0 25 0 1 0 550129565 65183744 14754 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15914 14754 603 41 0 15873 0
vsize: 63656
[startup+220.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 16308 0 1 0 21952 49 0 0 25 0 1 0 550129565 67186688 15240 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16403 15240 603 41 0 16362 0
vsize: 65612
[startup+230.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 16773 0 1 0 22951 50 0 0 25 0 1 0 550129565 69070848 15705 4294967295 134512640 134672761 3221224624 3221223760 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16863 15705 603 41 0 16822 0
vsize: 67452
[startup+240.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 17220 0 1 0 23949 52 0 0 25 0 1 0 550129565 70909952 16152 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17312 16152 603 41 0 17271 0
vsize: 69248
[startup+250.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 17639 0 1 0 24948 53 0 0 25 0 1 0 550129565 72646656 16571 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17736 16571 603 41 0 17695 0
vsize: 70944
[startup+260.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15146
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18172 0 1 0 25947 54 0 0 25 0 1 0 550129565 74784768 17104 4294967295 134512640 134672761 3221224624 3221223792 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18258 17104 603 41 0 18217 0
vsize: 73032
[startup+270.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18498 0 1 0 26946 56 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+280.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18498 0 1 0 27946 56 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+290.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18498 0 1 0 28946 56 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+300.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 29946 56 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223808 134559199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+310.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 30944 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223728 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+320.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 31944 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+330.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 32944 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+340.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 33945 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+350.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 34945 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+360.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 35945 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+370.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 36945 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+380.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 37945 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+390.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 38945 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+400.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18540 0 1 0 39945 57 0 0 25 0 1 0 550129565 75583488 17322 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+410.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18541 0 1 0 40946 57 0 0 25 0 1 0 550129565 75583488 17323 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17323 603 41 0 18412 0
vsize: 73812
[startup+420.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18541 0 1 0 41946 57 0 0 25 0 1 0 550129565 75583488 17323 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17323 603 41 0 18412 0
vsize: 73812
[startup+430.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18541 0 1 0 42946 57 0 0 25 0 1 0 550129565 75583488 17323 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18453 17323 603 41 0 18412 0
vsize: 73812
[startup+440.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 18646 0 1 0 43946 58 0 0 25 0 1 0 550129565 76132352 17428 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18587 17428 603 41 0 18546 0
vsize: 74348
[startup+450.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 44944 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+460.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 45944 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+470.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 46944 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+480.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 47944 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+490.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 48944 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+500.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 49945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+510.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 50945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+520.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 51945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+530.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 52945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+540.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 53945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+550.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 54945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+560.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15148
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 55945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+570.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 56945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+580.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19227 0 1 0 57945 60 0 0 25 0 1 0 550129565 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+590.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19338 0 1 0 58946 61 0 0 25 0 1 0 550129565 77664256 17805 4294967295 134512640 134672761 3221224624 3221223728 134560306 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18961 17805 603 41 0 18920 0
vsize: 75844
[startup+600.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 19891 0 1 0 59945 61 0 0 25 0 1 0 550129565 79945728 18358 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19518 18358 603 41 0 19477 0
vsize: 78072
[startup+610.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 20464 0 1 0 60943 64 0 0 25 0 1 0 550129565 82227200 18931 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20075 18931 603 41 0 20034 0
vsize: 80300
[startup+620.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 20951 0 1 0 61942 65 0 0 25 0 1 0 550129565 84254720 19418 4294967295 134512640 134672761 3221224624 3221223808 134559383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20570 19418 603 41 0 20529 0
vsize: 82280
[startup+630.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 21632 0 1 0 62940 67 0 0 25 0 1 0 550129565 87056384 20099 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21254 20099 603 41 0 21213 0
vsize: 85016
[startup+640.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 22161 0 1 0 63939 68 0 0 25 0 1 0 550129565 89133056 20628 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21761 20628 603 41 0 21720 0
vsize: 87044
[startup+650.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 22663 0 1 0 64938 70 0 0 25 0 1 0 550129565 91267072 21130 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22282 21130 603 41 0 22241 0
vsize: 89128
[startup+660.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 23114 0 1 0 65937 71 0 0 25 0 1 0 550129565 93134848 21581 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22738 21581 603 41 0 22697 0
vsize: 90952
[startup+670.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 23533 0 1 0 66937 71 0 0 25 0 1 0 550129565 94752768 22000 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23133 22000 603 41 0 23092 0
vsize: 92532
[startup+680.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 24057 0 1 0 67936 73 0 0 25 0 1 0 550129565 96903168 22524 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23658 22524 603 41 0 23617 0
vsize: 94632
[startup+690.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 24705 0 1 0 68935 74 0 0 25 0 1 0 550129565 99590144 23172 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24314 23172 603 41 0 24273 0
vsize: 97256
[startup+700.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 25276 0 1 0 69933 76 0 0 25 0 1 0 550129565 101871616 23743 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24871 23743 603 41 0 24830 0
vsize: 99484
[startup+710.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 25822 0 1 0 70932 78 0 0 25 0 1 0 550129565 104112128 24289 4294967295 134512640 134672761 3221224624 3221223728 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25418 24289 603 41 0 25377 0
vsize: 101672
[startup+720.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 26222 0 1 0 71931 78 0 0 25 0 1 0 550129565 105852928 24689 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25843 24689 603 41 0 25802 0
vsize: 103372
[startup+730.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 26635 0 1 0 72930 80 0 0 25 0 1 0 550129565 107442176 25102 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26231 25102 603 41 0 26190 0
vsize: 104924
[startup+740.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 27185 0 1 0 73929 81 0 0 25 0 1 0 550129565 109957120 25652 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26845 25652 603 41 0 26804 0
vsize: 107380
[startup+750.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 27649 0 1 0 74928 82 0 0 25 0 1 0 550129565 111820800 26116 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27300 26116 603 41 0 27259 0
vsize: 109200
[startup+760.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 28115 0 1 0 75926 84 0 0 25 0 1 0 550129565 113831936 26582 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27791 26582 603 41 0 27750 0
vsize: 111164
[startup+770.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 28780 0 1 0 76924 86 0 0 25 0 1 0 550129565 116543488 27247 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28453 27247 603 41 0 28412 0
vsize: 113812
[startup+780.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 29576 0 1 0 77923 88 0 0 25 0 1 0 550129565 119779328 28043 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29243 28043 603 41 0 29202 0
vsize: 116972
[startup+790.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 30183 0 1 0 78922 89 0 0 25 0 1 0 550129565 122195968 28650 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29833 28650 603 41 0 29792 0
vsize: 119332
[startup+800.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 30677 0 1 0 79921 91 0 0 25 0 1 0 550129565 124207104 29144 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30324 29144 603 41 0 30283 0
vsize: 121296
[startup+810.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 31139 0 1 0 80920 92 0 0 25 0 1 0 550129565 126210048 29606 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30813 29606 603 41 0 30772 0
vsize: 123252
[startup+820.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 31527 0 1 0 81918 93 0 0 25 0 1 0 550129565 127688704 29994 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31174 29994 603 41 0 31133 0
vsize: 124696
[startup+830.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 31900 0 1 0 82917 94 0 0 25 0 1 0 550129565 129302528 30367 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31568 30367 603 41 0 31527 0
vsize: 126272
[startup+840.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 32296 0 1 0 83916 95 0 0 25 0 1 0 550129565 130924544 30763 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31964 30763 603 41 0 31923 0
vsize: 127856
[startup+850.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 32731 0 1 0 84915 96 0 0 25 0 1 0 550129565 132669440 31198 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32390 31198 603 41 0 32349 0
vsize: 129560
[startup+860.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15150
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 33142 0 1 0 85915 97 0 0 25 0 1 0 550129565 134275072 31609 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32782 31609 603 41 0 32741 0
vsize: 131128
[startup+870.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 33539 0 1 0 86914 98 0 0 25 0 1 0 550129565 136007680 32006 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33205 32006 603 41 0 33164 0
vsize: 132820
[startup+880.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 33909 0 1 0 87913 99 0 0 25 0 1 0 550129565 137469952 32376 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33562 32376 603 41 0 33521 0
vsize: 134248
[startup+890.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 34306 0 1 0 88912 100 0 0 25 0 1 0 550129565 139051008 32773 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33948 32773 603 41 0 33907 0
vsize: 135792
[startup+900.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 34706 0 1 0 89911 101 0 0 25 0 1 0 550129565 140775424 33173 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34369 33173 603 41 0 34328 0
vsize: 137476
[startup+910.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 35106 0 1 0 90910 102 0 0 25 0 1 0 550129565 142376960 33573 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34760 33573 603 41 0 34719 0
vsize: 139040
[startup+920.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 35532 0 1 0 91909 104 0 0 25 0 1 0 550129565 144109568 33999 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35183 33999 603 41 0 35142 0
vsize: 140732
[startup+930.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 35943 0 1 0 92908 105 0 0 25 0 1 0 550129565 145833984 34410 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35604 34410 603 41 0 35563 0
vsize: 142416
[startup+940.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 36188 0 1 0 93908 106 0 0 25 0 1 0 550129565 146776064 34655 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35834 34655 603 41 0 35793 0
vsize: 143336
[startup+950.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 36587 0 1 0 94906 107 0 0 25 0 1 0 550129565 148377600 35054 4294967295 134512640 134672761 3221224624 3221223760 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36225 35054 603 41 0 36184 0
vsize: 144900
[startup+960.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 37036 0 1 0 95905 108 0 0 25 0 1 0 550129565 150249472 35503 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36682 35503 603 41 0 36641 0
vsize: 146728
[startup+970.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 37447 0 1 0 96904 110 0 0 25 0 1 0 550129565 151859200 35914 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37075 35915 603 41 0 37034 0
vsize: 148300
[startup+980.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 37740 0 1 0 97904 110 0 0 25 0 1 0 550129565 153059328 36207 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37368 36207 603 41 0 37327 0
vsize: 149472
[startup+990.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 38159 0 1 0 98904 111 0 0 25 0 1 0 550129565 154820608 36626 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37798 36626 603 41 0 37757 0
vsize: 151192
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 38457 0 1 0 99902 112 0 0 25 0 1 0 550129565 156033024 36924 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38094 36924 603 41 0 38053 0
vsize: 152376
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 38929 0 1 0 100902 113 0 0 25 0 1 0 550129565 158027776 37396 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38581 37396 603 41 0 38540 0
vsize: 154324
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 39425 0 1 0 101902 114 0 0 25 0 1 0 550129565 160018432 37892 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39067 37892 603 41 0 39026 0
vsize: 156268
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 39770 0 1 0 102901 115 0 0 25 0 1 0 550129565 161361920 38237 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39395 38237 603 41 0 39354 0
vsize: 157580
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 40145 0 1 0 103900 116 0 0 25 0 1 0 550129565 162967552 38612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39787 38612 603 41 0 39746 0
vsize: 159148
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 40623 0 1 0 104899 117 0 0 25 0 1 0 550129565 164823040 39090 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40240 39090 603 41 0 40199 0
vsize: 160960
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 40999 0 1 0 105899 118 0 0 25 0 1 0 550129565 166424576 39466 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40631 39466 603 41 0 40590 0
vsize: 162524
[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 41232 0 1 0 106898 118 0 0 25 0 1 0 550129565 167366656 39699 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40861 39699 603 41 0 40820 0
vsize: 163444
[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 41633 0 1 0 107896 120 0 0 25 0 1 0 550129565 168976384 40100 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41254 40100 603 41 0 41213 0
vsize: 165016
[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 42073 0 1 0 108896 120 0 0 25 0 1 0 550129565 170835968 40540 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41708 40540 603 41 0 41667 0
vsize: 166832
[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 42565 0 1 0 109895 121 0 0 25 0 1 0 550129565 172822528 41032 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42193 41032 603 41 0 42152 0
vsize: 168772
[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 43041 0 1 0 110894 123 0 0 25 0 1 0 550129565 174813184 41508 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42679 41508 603 41 0 42638 0
vsize: 170716
[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 43499 0 1 0 111892 124 0 0 25 0 1 0 550129565 176693248 41966 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43138 41966 603 41 0 43097 0
vsize: 172552
[startup+1130.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 43961 0 1 0 112891 126 0 0 25 0 1 0 550129565 178561024 42428 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43594 42428 603 41 0 43553 0
vsize: 174376
[startup+1140.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 44362 0 1 0 113890 127 0 0 25 0 1 0 550129565 180154368 42829 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43983 42830 603 41 0 43942 0
vsize: 175932
[startup+1150.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 44756 0 1 0 114890 128 0 0 25 0 1 0 550129565 181735424 43223 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44369 43223 603 41 0 44328 0
vsize: 177476
[startup+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15152
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 45130 0 1 0 115889 128 0 0 25 0 1 0 550129565 183332864 43597 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44759 43597 603 41 0 44718 0
vsize: 179036
[startup+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15154
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 45563 0 1 0 116889 129 0 0 25 0 1 0 550129565 185061376 44030 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45181 44030 603 41 0 45140 0
vsize: 180724
[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15154
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 45942 0 1 0 117888 130 0 0 25 0 1 0 550129565 186662912 44409 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45572 44409 603 41 0 45531 0
vsize: 182288
[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15154
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 46306 0 1 0 118887 131 0 0 25 0 1 0 550129565 188141568 44773 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45933 44773 603 41 0 45892 0
vsize: 183732
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15154
Raw data (stat): 15146 (minisat+) R 15145 20024 20023 0 -1 0 46695 0 1 0 119886 132 0 0 25 0 1 0 550129565 189726720 45162 4294967295 134512640 134672761 3221224624 3221223792 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46320 45162 603 41 0 46279 0
vsize: 185280
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 15154
Raw data (stat): 15146 (minisat+) Z 15145 20024 20023 0 -1 12 46698 0 1 0 119887 141 0 0 25 0 1 0 550129565 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.17
CPU time (s): 1200.28
CPU user time (s): 1198.87
CPU system time (s): 1.41079
CPU usage (%): 100.009
Max. virtual memory (Kb): 185280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####