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/synthesis-ptl-cmos-circuits/normalized-my_adder.opb
MD5SUM	fe8f615a95a6852516985b8e3e78bd85
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4561
Optimality of the best value was proved	NO
Number of terms in the objective function	577
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	24510
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	24510
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	577
Total number of constraints	1322
Number of constraints which are clauses	1306
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	16
Minimum length of a constraint	2
Maximum length of a constraint	17
Trace number 6346

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 04:23:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4767 boxname=wulflinc15 idbench=255 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fe8f615a95a6852516985b8e3e78bd85  /oldhome/oroussel/tmp/wulflinc15/normalized-my_adder.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-my_adder.opb /oldhome/oroussel/tmp/wulflinc15/normalized-my_adder.opb
IDLAUNCH: 4767
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        893068 kB
Buffers:         36736 kB
Cached:          83248 kB
SwapCached:       2144 kB
Active:          63552 kB
Inactive:        61488 kB
HighTotal:      131008 kB
HighFree:        43848 kB
LowTotal:       903652 kB
LowFree:        849220 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11092 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:43:59 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4767 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1322 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 |    1322     4977 |     440       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6274[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:87831     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |  241559   567026 |   80519       1        7     7.0 |  0.000 % |
c |       101 |  240957   565664 |   88570      98      760     7.8 |  0.188 % |
c |       251 |  240957   565664 |   97427     248     1805     7.3 |  0.188 % |
c |       477 |  240957   565664 |  107170     474     4058     8.6 |  0.188 % |
c |       814 |  240957   565664 |  117887     811     6048     7.5 |  0.188 % |
c |      1320 |  235231   552492 |  129676    1276    15140    11.9 |  2.276 % |
c |      2079 |  235231   552492 |  142644    2035    23739    11.7 |  2.276 % |
c |      3218 |  234974   551901 |  156908    3171    34333    10.8 |  2.374 % |
c |      4926 |  234974   551901 |  172599    4879   152629    31.3 |  2.374 % |
c |      7488 |  234974   551901 |  189859    7441   237669    31.9 |  2.374 % |
c |     11332 |  234872   551667 |  208845   11283   394121    34.9 |  2.411 % |
c ==============================================================================
c [1mFound solution: 6271[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:65180     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12271 |  401560   941554 |  133853   12222   494510    40.5 |  2.411 % |
c |     12372 |  401560   941554 |  147238   12323   497481    40.4 |  1.476 % |
c |     12522 |  401560   941554 |  161962   12473   498601    40.0 |  1.476 % |
c |     12749 |  401560   941554 |  178158   12700   500062    39.4 |  1.476 % |
c |     13086 |  401532   941489 |  195974   13035   504447    38.7 |  1.482 % |
c |     13592 |  401532   941489 |  215571   13541   511347    37.8 |  1.482 % |
c |     14353 |  401532   941489 |  237128   14302   522092    36.5 |  1.482 % |
c |     15493 |  401532   941489 |  260841   15442   536886    34.8 |  1.482 % |
c |     17201 |  401426   941247 |  286925   17147   643181    37.5 |  1.505 % |
c |     19764 |  401414   941220 |  315618   19709   726396    36.9 |  1.507 % |
c ==============================================================================
c [1mFound solution: 6270[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22065 |  406454   953722 |  135484   22010   865938    39.3 |  1.507 % |
c |     22165 |  406454   953722 |  149032   22110   867989    39.3 |  1.494 % |
c |     22317 |  406349   953486 |  163935   22261   869298    39.1 |  1.513 % |
c |     22543 |  406349   953486 |  180329   22487   870741    38.7 |  1.513 % |
c |     22882 |  406349   953486 |  198362   22826   872733    38.2 |  1.513 % |
c |     23389 |  406349   953486 |  218198   23333   886508    38.0 |  1.513 % |
c |     24148 |  406241   953243 |  240018   24089   896697    37.2 |  1.535 % |
c |     25288 |  406241   953243 |  264019   25229   906867    35.9 |  1.535 % |
c |     26997 |  406241   953243 |  290421   26938   932612    34.6 |  1.535 % |
c |     29562 |  406113   952953 |  319464   29495   975870    33.1 |  1.561 % |
c |     33406 |  406113   952953 |  351410   33339  1021754    30.6 |  1.561 % |
c |     39172 |  406066   952849 |  386551   39104  1148019    29.4 |  1.571 % |
c |     47821 |  406066   952849 |  425206   47753  1416833    29.7 |  1.571 % |
c |     60796 |  406030   952767 |  467727   60723  1796367    29.6 |  1.574 % |
c ==============================================================================
c [1mFound solution: 6254[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63610     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63729 |  573944  1345875 |  191314   63656  2364767    37.1 |  1.574 % |
c |     63829 |  573944  1345875 |  210445   63756  2365796    37.1 |  1.127 % |
c |     63988 |  573944  1345875 |  231489   63915  2366758    37.0 |  1.127 % |
c |     64213 |  573944  1345875 |  254638   64140  2370426    37.0 |  1.127 % |
c |     64551 |  573893  1345759 |  280102   64477  2372851    36.8 |  1.135 % |
c |     65057 |  573893  1345759 |  308113   64983  2381238    36.6 |  1.135 % |
c |     65818 |  573893  1345759 |  338924   65744  2389313    36.3 |  1.135 % |
c |     66957 |  573893  1345759 |  372816   66883  2401797    35.9 |  1.135 % |
c |     68665 |  573893  1345759 |  410098   68591  2432853    35.5 |  1.135 % |
c |     71227 |  573893  1345759 |  451108   71153  2601910    36.6 |  1.135 % |
c |     75072 |  573893  1345759 |  496219   74998  2686627    35.8 |  1.135 % |
c |     80839 |  573893  1345759 |  545841   80765  2925641    36.2 |  1.135 % |
c |     89488 |  573878  1345726 |  600425   89412  3145379    35.2 |  1.137 % |
c |    102462 |  573878  1345726 |  660467  102386  3480347    34.0 |  1.137 % |
c |    121923 |  573684  1345290 |  726514  121821  5130318    42.1 |  1.164 % |
c |    151115 |  573577  1345048 |  799166  151009  6549820    43.4 |  1.180 % |
#### 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.98 0.95 2/54 4955
Raw data (stat): 4955 (runsolver) R 4954 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423461223 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99987 s]
Raw data (loadavg): 0.94 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 7297 0 0 0 979 19 0 0 25 0 1 0 423461223 33189888 6829 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 6829 603 41 0 8062 0
vsize: 32412
[startup+20.0006 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 7389 0 0 0 1978 20 0 0 25 0 1 0 423461223 33599488 6921 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8203 6921 603 41 0 8162 0
vsize: 32812
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 7460 0 0 0 2977 21 0 0 25 0 1 0 423461223 33865728 6992 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8268 6992 603 41 0 8227 0
vsize: 33072
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 7582 0 0 0 3976 22 0 0 25 0 1 0 423461223 34299904 7114 4294967295 134512640 134672761 3221224560 3221223696 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8374 7114 603 41 0 8333 0
vsize: 33496
[startup+50.0021 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 7696 0 0 0 4976 22 0 0 25 0 1 0 423461223 34717696 7228 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8476 7228 603 41 0 8435 0
vsize: 33904
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 7750 0 0 0 5975 23 0 0 25 0 1 0 423461223 34983936 7282 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8541 7282 603 41 0 8500 0
vsize: 34164
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 12197 0 0 0 6964 34 0 0 25 0 1 0 423461223 59400192 11687 4294967295 134512640 134672761 3221224560 3221223700 1074733052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14502 11687 603 41 0 14461 0
vsize: 58008
[startup+80.0046 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 12266 0 0 0 7963 34 0 0 25 0 1 0 423461223 59670528 11756 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14568 11756 603 41 0 14527 0
vsize: 58272
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 12393 0 0 0 8963 35 0 0 25 0 1 0 423461223 60231680 11883 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14705 11883 603 41 0 14664 0
vsize: 58820
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 12512 0 0 0 9962 36 0 0 25 0 1 0 423461223 60637184 12002 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14804 12002 603 41 0 14763 0
vsize: 59216
[startup+110.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 12605 0 0 0 10961 36 0 0 25 0 1 0 423461223 61042688 12095 4294967295 134512640 134672761 3221224560 3221223760 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14903 12095 603 41 0 14862 0
vsize: 59612
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 12980 0 0 0 11960 37 0 0 25 0 1 0 423461223 61591552 12345 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15037 12345 603 41 0 14996 0
vsize: 60148
[startup+130.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13059 0 0 0 12959 38 0 0 25 0 1 0 423461223 61992960 12424 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15135 12424 603 41 0 15094 0
vsize: 60540
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13125 0 0 0 13959 38 0 0 25 0 1 0 423461223 62128128 12490 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15168 12490 603 41 0 15127 0
vsize: 60672
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13199 0 0 0 14959 39 0 0 25 0 1 0 423461223 62652416 12564 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15296 12564 603 41 0 15255 0
vsize: 61184
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13250 0 0 0 15958 40 0 0 25 0 1 0 423461223 62787584 12615 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15329 12615 603 41 0 15288 0
vsize: 61316
[startup+170.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13337 0 0 0 16957 40 0 0 25 0 1 0 423461223 63193088 12702 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15428 12702 603 41 0 15387 0
vsize: 61712
[startup+180.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13406 0 0 0 17957 40 0 0 25 0 1 0 423461223 63463424 12771 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15494 12771 603 41 0 15453 0
vsize: 61976
[startup+190.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13507 0 0 0 18957 41 0 0 25 0 1 0 423461223 63864832 12872 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15592 12872 603 41 0 15551 0
vsize: 62368
[startup+200.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13621 0 0 0 19956 42 0 0 25 0 1 0 423461223 64270336 12986 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15691 12986 603 41 0 15650 0
vsize: 62764
[startup+210.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13687 0 0 0 20955 42 0 0 25 0 1 0 423461223 64540672 13052 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15757 13052 603 41 0 15716 0
vsize: 63028
[startup+220.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13737 0 0 0 21955 43 0 0 25 0 1 0 423461223 64806912 13102 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15822 13102 603 41 0 15781 0
vsize: 63288
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13797 0 0 0 22954 43 0 0 25 0 1 0 423461223 64942080 13162 4294967295 134512640 134672761 3221224560 3221223760 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 13162 603 41 0 15814 0
vsize: 63420
[startup+240.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13857 0 0 0 23954 43 0 0 25 0 1 0 423461223 65204224 13222 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15919 13222 603 41 0 15878 0
vsize: 63676
[startup+250.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13913 0 0 0 24954 43 0 0 25 0 1 0 423461223 65474560 13278 4294967295 134512640 134672761 3221224560 3221223744 134559463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15985 13278 603 41 0 15944 0
vsize: 63940
[startup+260.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 13954 0 0 0 25954 43 0 0 25 0 1 0 423461223 65609728 13319 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16018 13319 603 41 0 15977 0
vsize: 64072
[startup+270.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 14123 0 0 0 26954 44 0 0 25 0 1 0 423461223 66285568 13488 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16183 13488 603 41 0 16142 0
vsize: 64732
[startup+280.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 14157 0 0 0 27954 44 0 0 25 0 1 0 423461223 66420736 13522 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16216 13522 603 41 0 16175 0
vsize: 64864
[startup+290.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 14416 0 0 0 28953 45 0 0 25 0 1 0 423461223 67502080 13781 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16480 13781 603 41 0 16439 0
vsize: 65920
[startup+300.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 15865 0 0 0 29950 49 0 0 25 0 1 0 423461223 71151616 14819 4294967295 134512640 134672761 3221224560 3221221608 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17371 14820 603 41 0 17330 0
vsize: 69484
[startup+310.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 19720 0 0 0 30940 59 0 0 25 0 1 0 423461223 86319104 18674 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21074 18674 603 41 0 21033 0
vsize: 84296
[startup+320.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 19791 0 0 0 31938 59 0 0 25 0 1 0 423461223 86589440 18745 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21140 18745 603 41 0 21099 0
vsize: 84560
[startup+330.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 19872 0 0 0 32938 59 0 0 25 0 1 0 423461223 86994944 18826 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21239 18826 603 41 0 21198 0
vsize: 84956
[startup+340.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 19985 0 0 0 33938 59 0 0 25 0 1 0 423461223 87396352 18939 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21337 18939 603 41 0 21296 0
vsize: 85348
[startup+350.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20022 0 0 0 34938 59 0 0 25 0 1 0 423461223 87531520 18976 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21370 18976 603 41 0 21329 0
vsize: 85480
[startup+360.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20051 0 0 0 35939 60 0 0 25 0 1 0 423461223 87666688 19005 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21403 19005 603 41 0 21362 0
vsize: 85612
[startup+370.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20105 0 0 0 36939 60 0 0 25 0 1 0 423461223 87801856 19059 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21436 19059 603 41 0 21395 0
vsize: 85744
[startup+380.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20166 0 0 0 37939 60 0 0 25 0 1 0 423461223 88072192 19120 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21502 19120 603 41 0 21461 0
vsize: 86008
[startup+390.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20224 0 0 0 38939 60 0 0 25 0 1 0 423461223 88207360 19178 4294967295 134512640 134672761 3221224560 3221223616 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21535 19178 603 41 0 21494 0
vsize: 86140
[startup+400.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20252 0 0 0 39939 60 0 0 25 0 1 0 423461223 88338432 19206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21567 19206 603 41 0 21526 0
vsize: 86268
[startup+410.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20306 0 0 0 40939 60 0 0 25 0 1 0 423461223 88612864 19260 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21634 19260 603 41 0 21593 0
vsize: 86536
[startup+420.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20403 0 0 0 41939 61 0 0 25 0 1 0 423461223 89018368 19357 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21733 19357 603 41 0 21692 0
vsize: 86932
[startup+430.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20465 0 0 0 42939 61 0 0 25 0 1 0 423461223 89153536 19419 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21766 19419 603 41 0 21725 0
vsize: 87064
[startup+440.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20511 0 0 0 43939 61 0 0 25 0 1 0 423461223 89419776 19465 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21831 19465 603 41 0 21790 0
vsize: 87324
[startup+450.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20599 0 0 0 44939 61 0 0 25 0 1 0 423461223 89686016 19553 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21896 19553 603 41 0 21855 0
vsize: 87584
[startup+460.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20654 0 0 0 45939 62 0 0 25 0 1 0 423461223 89956352 19608 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21962 19608 603 41 0 21921 0
vsize: 87848
[startup+470.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20707 0 0 0 46938 62 0 0 25 0 1 0 423461223 90218496 19661 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22026 19661 603 41 0 21985 0
vsize: 88104
[startup+480.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20760 0 0 0 47938 62 0 0 25 0 1 0 423461223 90353664 19714 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22059 19714 603 41 0 22018 0
vsize: 88236
[startup+490.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20805 0 0 0 48938 63 0 0 25 0 1 0 423461223 90624000 19759 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22125 19759 603 41 0 22084 0
vsize: 88500
[startup+500.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20859 0 0 0 49938 63 0 0 25 0 1 0 423461223 90755072 19813 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22157 19813 603 41 0 22116 0
vsize: 88628
[startup+510.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20894 0 0 0 50938 63 0 0 25 0 1 0 423461223 90890240 19848 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22190 19848 603 41 0 22149 0
vsize: 88760
[startup+520.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20929 0 0 0 51938 63 0 0 25 0 1 0 423461223 91025408 19883 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22223 19883 603 41 0 22182 0
vsize: 88892
[startup+530.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 20961 0 0 0 52938 63 0 0 25 0 1 0 423461223 91160576 19915 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22256 19915 603 41 0 22215 0
vsize: 89024
[startup+540.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21029 0 0 0 53938 63 0 0 25 0 1 0 423461223 91426816 19983 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22321 19983 603 41 0 22280 0
vsize: 89284
[startup+550.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21065 0 0 0 54938 63 0 0 25 0 1 0 423461223 91561984 20019 4294967295 134512640 134672761 3221224560 3221223696 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22354 20019 603 41 0 22313 0
vsize: 89416
[startup+560.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21121 0 0 0 55938 63 0 0 25 0 1 0 423461223 91828224 20075 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22419 20075 603 41 0 22378 0
vsize: 89676
[startup+570.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21178 0 0 0 56938 64 0 0 25 0 1 0 423461223 91963392 20132 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22452 20132 603 41 0 22411 0
vsize: 89808
[startup+580.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21240 0 0 0 57938 64 0 0 25 0 1 0 423461223 92233728 20194 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22518 20194 603 41 0 22477 0
vsize: 90072
[startup+590.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21352 0 0 0 58938 65 0 0 25 0 1 0 423461223 92774400 20306 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22650 20306 603 41 0 22609 0
vsize: 90600
[startup+600.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21474 0 0 0 59937 65 0 0 25 0 1 0 423461223 93175808 20428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22748 20428 603 41 0 22707 0
vsize: 90992
[startup+610.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21521 0 0 0 60938 65 0 0 25 0 1 0 423461223 93442048 20475 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22813 20475 603 41 0 22772 0
vsize: 91252
[startup+620.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21546 0 0 0 61937 65 0 0 25 0 1 0 423461223 93442048 20500 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22813 20500 603 41 0 22772 0
vsize: 91252
[startup+630.025 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21597 0 0 0 62938 65 0 0 25 0 1 0 423461223 93712384 20551 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22879 20551 603 41 0 22838 0
vsize: 91516
[startup+640.026 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21676 0 0 0 63938 66 0 0 25 0 1 0 423461223 93978624 20630 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22944 20630 603 41 0 22903 0
vsize: 91776
[startup+650.026 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21806 0 0 0 64938 66 0 0 25 0 1 0 423461223 94519296 20760 4294967295 134512640 134672761 3221224560 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23076 20760 603 41 0 23035 0
vsize: 92304
[startup+660.025 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 21937 0 0 0 65938 66 0 0 25 0 1 0 423461223 95055872 20891 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23207 20891 603 41 0 23166 0
vsize: 92828
[startup+670.025 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 22111 0 0 0 66937 67 0 0 25 0 1 0 423461223 95817728 21065 4294967295 134512640 134672761 3221224560 3221223664 134560150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23393 21065 603 41 0 23352 0
vsize: 93572
[startup+680.026 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 22286 0 0 0 67937 67 0 0 25 0 1 0 423461223 96489472 21240 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23557 21240 603 41 0 23516 0
vsize: 94228
[startup+690.026 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 22481 0 0 0 68937 68 0 0 25 0 1 0 423461223 97308672 21435 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23757 21435 603 41 0 23716 0
vsize: 95028
[startup+700.027 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 22792 0 0 0 69936 69 0 0 25 0 1 0 423461223 98521088 21746 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24053 21746 603 41 0 24012 0
vsize: 96212
[startup+710.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 22884 0 0 0 70936 69 0 0 25 0 1 0 423461223 98914304 21838 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24149 21838 603 41 0 24108 0
vsize: 96596
[startup+720.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 22938 0 0 0 71935 69 0 0 25 0 1 0 423461223 99184640 21892 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24215 21892 603 41 0 24174 0
vsize: 96860
[startup+730.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23064 0 0 0 72935 69 0 0 25 0 1 0 423461223 99717120 22018 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24345 22018 603 41 0 24304 0
vsize: 97380
[startup+740.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23139 0 0 0 73935 69 0 0 25 0 1 0 423461223 99987456 22093 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24411 22093 603 41 0 24370 0
vsize: 97644
[startup+750.029 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23209 0 0 0 74935 70 0 0 25 0 1 0 423461223 100253696 22163 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24476 22163 603 41 0 24435 0
vsize: 97904
[startup+760.028 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23250 0 0 0 75935 70 0 0 25 0 1 0 423461223 100913152 22204 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24637 22204 603 41 0 24596 0
vsize: 98548
[startup+770.029 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23332 0 0 0 76935 70 0 0 25 0 1 0 423461223 101318656 22286 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24736 22286 603 41 0 24695 0
vsize: 98944
[startup+780.029 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23375 0 0 0 77935 71 0 0 25 0 1 0 423461223 101449728 22329 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24768 22329 603 41 0 24727 0
vsize: 99072
[startup+790.029 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23455 0 0 0 78935 71 0 0 25 0 1 0 423461223 101720064 22409 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24834 22409 603 41 0 24793 0
vsize: 99336
[startup+800.03 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23522 0 0 0 79935 71 0 0 25 0 1 0 423461223 101990400 22476 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24900 22476 603 41 0 24859 0
vsize: 99600
[startup+810.031 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23645 0 0 0 80935 71 0 0 25 0 1 0 423461223 102522880 22599 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25030 22599 603 41 0 24989 0
vsize: 100120
[startup+820.03 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23890 0 0 0 81935 71 0 0 25 0 1 0 423461223 103473152 22844 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25262 22844 603 41 0 25221 0
vsize: 101048
[startup+830.03 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 23996 0 0 0 82935 72 0 0 25 0 1 0 423461223 103874560 22950 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25360 22950 603 41 0 25319 0
vsize: 101440
[startup+840.03 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24247 0 0 0 83934 73 0 0 25 0 1 0 423461223 104964096 23201 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25626 23201 603 41 0 25585 0
vsize: 102504
[startup+850.031 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24396 0 0 0 84933 73 0 0 25 0 1 0 423461223 105504768 23350 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25758 23350 603 41 0 25717 0
vsize: 103032
[startup+860.032 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24466 0 0 0 85933 74 0 0 25 0 1 0 423461223 105906176 23420 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25856 23420 603 41 0 25815 0
vsize: 103424
[startup+870.032 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24517 0 0 0 86933 74 0 0 25 0 1 0 423461223 106037248 23471 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25888 23471 603 41 0 25847 0
vsize: 103552
[startup+880.032 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24588 0 0 0 87933 74 0 0 25 0 1 0 423461223 106307584 23542 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25954 23542 603 41 0 25913 0
vsize: 103816
[startup+890.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24692 0 0 0 88932 75 0 0 25 0 1 0 423461223 106713088 23646 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26053 23646 603 41 0 26012 0
vsize: 104212
[startup+900.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24761 0 0 0 89932 75 0 0 25 0 1 0 423461223 106983424 23715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26119 23715 603 41 0 26078 0
vsize: 104476
[startup+910.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24823 0 0 0 90932 75 0 0 25 0 1 0 423461223 107249664 23777 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26184 23777 603 41 0 26143 0
vsize: 104736
[startup+920.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 24939 0 0 0 91932 76 0 0 25 0 1 0 423461223 107798528 23893 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26318 23893 603 41 0 26277 0
vsize: 105272
[startup+930.034 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 25009 0 0 0 92932 76 0 0 25 0 1 0 423461223 108064768 23963 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26383 23963 603 41 0 26342 0
vsize: 105532
[startup+940.033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 25153 0 0 0 93931 77 0 0 25 0 1 0 423461223 108601344 24107 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26514 24107 603 41 0 26473 0
vsize: 106056
[startup+950.034 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 25352 0 0 0 94931 77 0 0 25 0 1 0 423461223 109391872 24306 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26707 24306 603 41 0 26666 0
vsize: 106828
[startup+960.034 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 25541 0 0 0 95931 78 0 0 25 0 1 0 423461223 110206976 24495 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26906 24495 603 41 0 26865 0
vsize: 107624
[startup+970.034 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 25710 0 0 0 96931 78 0 0 25 0 1 0 423461223 110878720 24664 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27070 24664 603 41 0 27029 0
vsize: 108280
[startup+980.035 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 25945 0 0 0 97931 78 0 0 25 0 1 0 423461223 111800320 24899 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27295 24899 603 41 0 27254 0
vsize: 109180
[startup+990.036 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 26117 0 0 0 98930 79 0 0 25 0 1 0 423461223 112599040 25071 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27490 25071 603 41 0 27449 0
vsize: 109960
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 26287 0 0 0 99930 79 0 0 25 0 1 0 423461223 113258496 25241 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27651 25241 603 41 0 27610 0
vsize: 110604
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 26522 0 0 0 100929 80 0 0 25 0 1 0 423461223 114188288 25476 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27878 25476 603 41 0 27837 0
vsize: 111512
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 26765 0 0 0 101929 81 0 0 25 0 1 0 423461223 115232768 25719 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28133 25719 603 41 0 28092 0
vsize: 112532
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 27070 0 0 0 102928 82 0 0 25 0 1 0 423461223 116416512 26024 4294967295 134512640 134672761 3221224560 3221223664 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28422 26024 603 41 0 28381 0
vsize: 113688
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 27296 0 0 0 103928 82 0 0 25 0 1 0 423461223 117342208 26250 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28648 26250 603 41 0 28607 0
vsize: 114592
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 27520 0 0 0 104927 83 0 0 25 0 1 0 423461223 118263808 26474 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28873 26474 603 41 0 28832 0
vsize: 115492
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 27677 0 0 0 105927 83 0 0 25 0 1 0 423461223 118931456 26631 4294967295 134512640 134672761 3221224560 3221223664 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29036 26631 603 41 0 28995 0
vsize: 116144
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 27911 0 0 0 106926 84 0 0 25 0 1 0 423461223 119861248 26865 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29263 26865 603 41 0 29222 0
vsize: 117052
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 28141 0 0 0 107926 84 0 0 25 0 1 0 423461223 120807424 27095 4294967295 134512640 134672761 3221224560 3221223664 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29494 27095 603 41 0 29453 0
vsize: 117976
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 28348 0 0 0 108926 85 0 0 25 0 1 0 423461223 121606144 27302 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29689 27302 603 41 0 29648 0
vsize: 118756
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 28570 0 0 0 109926 85 0 0 25 0 1 0 423461223 122544128 27524 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29918 27524 603 41 0 29877 0
vsize: 119672
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 28837 0 0 0 110926 86 0 0 25 0 1 0 423461223 123625472 27791 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30182 27791 603 41 0 30141 0
vsize: 120728
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 29072 0 0 0 111925 86 0 0 25 0 1 0 423461223 124690432 28026 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30442 28026 603 41 0 30401 0
vsize: 121768
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 29331 0 0 0 112925 87 0 0 25 0 1 0 423461223 125636608 28285 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30673 28285 603 41 0 30632 0
vsize: 122692
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 29603 0 0 0 113924 88 0 0 25 0 1 0 423461223 126832640 28557 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30965 28557 603 41 0 30924 0
vsize: 123860
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 29848 0 0 0 114924 88 0 0 25 0 1 0 423461223 127770624 28802 4294967295 134512640 134672761 3221224560 3221223664 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31194 28802 603 41 0 31153 0
vsize: 124776
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 30120 0 0 0 115924 88 0 0 25 0 1 0 423461223 128958464 29074 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31484 29074 603 41 0 31443 0
vsize: 125936
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 30384 0 0 0 116924 88 0 0 25 0 1 0 423461223 130011136 29338 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31741 29338 603 41 0 31700 0
vsize: 126964
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 30670 0 0 0 117924 89 0 0 25 0 1 0 423461223 131248128 29624 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32043 29624 603 41 0 32002 0
vsize: 128172
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 30958 0 0 0 118924 89 0 0 25 0 1 0 423461223 132464640 29912 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32340 29912 603 41 0 32299 0
vsize: 129360
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 4955
Raw data (stat): 4955 (minisat+) R 4954 29151 29150 0 -1 0 31273 0 0 0 119923 90 0 0 25 0 1 0 423461223 133697536 30227 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32641 30227 603 41 0 32600 0
vsize: 130564
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.95 1/54 4955
Raw data (stat): 4955 (minisat+) Z 4954 29151 29150 0 -1 12 31276 0 0 0 119923 96 0 0 25 0 1 0 423461223 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.1
CPU time (s): 1200.2
CPU user time (s): 1199.24
CPU system time (s): 0.965853
CPU usage (%): 100.008
Max. virtual memory (Kb): 130564
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####