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/logic-synthesis/normalized-f51m.b.opb
MD5SUM	4fc22abde8250807abd95442a25fac44
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	18
Optimality of the best value was proved	NO
Number of terms in the objective function	407
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	407
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	407
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	406
Total number of constraints	538
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	18
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 4839

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        924376 kB
Buffers:         34008 kB
Cached:          56720 kB
SwapCached:        392 kB
Active:          49616 kB
Inactive:        44396 kB
HighTotal:      131008 kB
HighFree:        70364 kB
LowTotal:       903652 kB
LowFree:        854012 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10808 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:49:57 (client local time) WITH STATUS 10 IN 1200.13 SECONDS
stats: 617 7 1200.13 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 498 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 |     498    13351 |     166       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:14920     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   16604    50904 |    5534       1       18    18.0 |  0.000 % |
c |       101 |   16604    50904 |    6087     101     2898    28.7 |  0.055 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       208 |   16615    50935 |    5538     187    12825    68.6 |  0.055 % |
c |       309 |   16615    50935 |    6091     288    21975    76.3 |  0.192 % |
c |       459 |   16615    50935 |    6700     438    33909    77.4 |  0.192 % |
c |       686 |   16615    50935 |    7371     665    58415    87.8 |  0.192 % |
c |      1029 |   16615    50935 |    8108    1008    95310    94.6 |  0.192 % |
c |      1536 |   16615    50935 |    8919    1515   138105    91.2 |  0.192 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1913 |   16410    50460 |    5470    1862   174770    93.9 |  0.192 % |
c |      2013 |   16410    50460 |    6017    1962   183811    93.7 |  1.618 % |
c |      2163 |   16402    50444 |    6618    2111   189584    89.8 |  1.655 % |
c |      2388 |   16402    50444 |    7280    2336   201318    86.2 |  1.655 % |
c |      2726 |   16402    50444 |    8008    2674   217793    81.4 |  1.655 % |
c |      3232 |   16402    50444 |    8809    3180   247166    77.7 |  1.655 % |
c |      3992 |   16402    50444 |    9690    3940   279064    70.8 |  1.655 % |
c |      5131 |   16402    50444 |   10659    5079   327949    64.6 |  1.655 % |
c |      6839 |   16402    50444 |   11725    6787   409251    60.3 |  1.655 % |
c |      9401 |   16402    50444 |   12897    9349   513437    54.9 |  1.655 % |
c |     13245 |   16402    50444 |   14187   13193   698978    53.0 |  1.655 % |
c |     19011 |   16402    50444 |   15606   11519   497107    43.2 |  1.655 % |
c |     27660 |   16402    50444 |   17167   12053   609989    50.6 |  1.655 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33376 |   16414    50475 |    5471   17769   928999    52.3 |  1.655 % |
c |     33478 |   16414    50475 |    6018    4545   221744    48.8 |  1.663 % |
c |     33628 |   16414    50475 |    6619    4695   229759    48.9 |  1.663 % |
c |     33855 |   16414    50475 |    7281    4922   240660    48.9 |  1.663 % |
c |     34192 |   16414    50475 |    8010    5259   254469    48.4 |  1.663 % |
c |     34700 |   16414    50475 |    8811    5767   274708    47.6 |  1.663 % |
c |     35461 |   16414    50475 |    9692    6528   308203    47.2 |  1.663 % |
c |     36601 |   16414    50475 |   10661    7668   361716    47.2 |  1.663 % |
c |     38309 |   16414    50475 |   11727    9376   425326    45.4 |  1.663 % |
c |     40871 |   16414    50475 |   12900   11938   539786    45.2 |  1.663 % |
c |     44717 |   16414    50475 |   14190    9168   330073    36.0 |  1.663 % |
c |     50487 |   16414    50475 |   15609    7682   245410    31.9 |  1.663 % |
c |     59136 |   16414    50475 |   17170    8283   287557    34.7 |  1.663 % |
c |     72111 |   16414    50475 |   18887   12406   433973    35.0 |  1.663 % |
c |     91574 |   16414    50475 |   20776   12488   450296    36.1 |  1.663 % |
c |    120768 |   16414    50475 |   22853   20303   750005    36.9 |  1.663 % |
c |    164558 |   16414    50475 |   25139   17290   577512    33.4 |  1.663 % |
c |    230246 |   16414    50475 |   27653   18531   543896    29.4 |  1.663 % |
c |    328772 |   16414    50475 |   30418   14118   592755    42.0 |  1.663 % |
#### 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.91 0.95 0.90 2/54 964
Raw data (stat): 964 (runsolver) R 963 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420623233 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 1602 0 0 0 995 3 0 0 25 0 1 0 420623233 8617984 1576 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2104 1576 603 41 0 2063 0
vsize: 8416
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 1874 0 0 0 1993 4 0 0 25 0 1 0 420623233 9711616 1848 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2371 1848 603 41 0 2330 0
vsize: 9484
[startup+30.0033 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2130 0 0 0 2991 6 0 0 25 0 1 0 420623233 10792960 2104 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2635 2104 603 41 0 2594 0
vsize: 10540
[startup+40.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2139 0 0 0 3990 6 0 0 25 0 1 0 420623233 10792960 2113 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2635 2113 603 41 0 2594 0
vsize: 10540
[startup+50.0029 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2158 0 0 0 4990 6 0 0 25 0 1 0 420623233 10928128 2132 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2668 2132 603 41 0 2627 0
vsize: 10672
[startup+60.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2191 0 0 0 5990 6 0 0 25 0 1 0 420623233 11063296 2165 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2165 603 41 0 2660 0
vsize: 10804
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2322 0 0 0 6990 7 0 0 25 0 1 0 420623233 11603968 2296 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2833 2296 603 41 0 2792 0
vsize: 11332
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2438 0 0 0 7989 7 0 0 25 0 1 0 420623233 12120064 2412 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2959 2412 603 41 0 2918 0
vsize: 11836
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2438 0 0 0 8990 7 0 0 25 0 1 0 420623233 12120064 2412 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2959 2412 603 41 0 2918 0
vsize: 11836
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2438 0 0 0 9990 7 0 0 25 0 1 0 420623233 12120064 2412 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2959 2412 603 41 0 2918 0
vsize: 11836
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2438 0 0 0 10990 7 0 0 25 0 1 0 420623233 12120064 2412 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2959 2412 603 41 0 2918 0
vsize: 11836
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2448 0 0 0 11989 8 0 0 25 0 1 0 420623233 12259328 2422 4294967295 134512640 134672761 3221224640 3221223828 1075347063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2993 2422 603 41 0 2952 0
vsize: 11972
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2452 0 0 0 12989 8 0 0 25 0 1 0 420623233 12259328 2426 4294967295 134512640 134672761 3221224640 3221223808 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2993 2426 603 41 0 2952 0
vsize: 11972
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2459 0 0 0 13988 9 0 0 25 0 1 0 420623233 12259328 2433 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2993 2433 603 41 0 2952 0
vsize: 11972
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2459 0 0 0 14988 9 0 0 25 0 1 0 420623233 12259328 2433 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2993 2433 603 41 0 2952 0
vsize: 11972
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2489 0 0 0 15988 9 0 0 25 0 1 0 420623233 12406784 2463 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3029 2463 603 41 0 2988 0
vsize: 12116
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2491 0 0 0 16988 9 0 0 25 0 1 0 420623233 12406784 2465 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3029 2465 603 41 0 2988 0
vsize: 12116
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2495 0 0 0 17987 10 0 0 25 0 1 0 420623233 12554240 2469 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3065 2469 603 41 0 3024 0
vsize: 12260
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2500 0 0 0 18987 10 0 0 25 0 1 0 420623233 12554240 2474 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3065 2474 603 41 0 3024 0
vsize: 12260
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2507 0 0 0 19986 10 0 0 25 0 1 0 420623233 12554240 2481 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3065 2481 603 41 0 3024 0
vsize: 12260
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2548 0 0 0 20986 11 0 0 25 0 1 0 420623233 12689408 2522 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3098 2522 603 41 0 3057 0
vsize: 12392
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2586 0 0 0 21985 12 0 0 25 0 1 0 420623233 12820480 2560 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3130 2560 603 41 0 3089 0
vsize: 12520
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2598 0 0 0 22985 12 0 0 25 0 1 0 420623233 12963840 2572 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3165 2572 603 41 0 3124 0
vsize: 12660
[startup+240.005 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2605 0 0 0 23985 12 0 0 25 0 1 0 420623233 12963840 2579 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3165 2579 603 41 0 3124 0
vsize: 12660
[startup+250.006 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2621 0 0 0 24985 12 0 0 25 0 1 0 420623233 13107200 2595 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3200 2595 603 41 0 3159 0
vsize: 12800
[startup+260.006 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2621 0 0 0 25984 12 0 0 25 0 1 0 420623233 13107200 2595 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3200 2595 603 41 0 3159 0
vsize: 12800
[startup+270.006 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2629 0 0 0 26984 13 0 0 25 0 1 0 420623233 13107200 2603 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3200 2603 603 41 0 3159 0
vsize: 12800
[startup+280.006 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2629 0 0 0 27984 13 0 0 25 0 1 0 420623233 13107200 2603 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3200 2603 603 41 0 3159 0
vsize: 12800
[startup+290.007 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2629 0 0 0 28984 13 0 0 25 0 1 0 420623233 13107200 2603 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3200 2603 603 41 0 3159 0
vsize: 12800
[startup+300.008 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2655 0 0 0 29984 13 0 0 25 0 1 0 420623233 13238272 2629 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3232 2629 603 41 0 3191 0
vsize: 12928
[startup+310.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2716 0 0 0 30983 13 0 0 25 0 1 0 420623233 13373440 2690 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3265 2690 603 41 0 3224 0
vsize: 13060
[startup+320.008 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2735 0 0 0 31983 13 0 0 25 0 1 0 420623233 13516800 2709 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3300 2709 603 41 0 3259 0
vsize: 13200
[startup+330.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2746 0 0 0 32983 14 0 0 25 0 1 0 420623233 13516800 2720 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3300 2720 603 41 0 3259 0
vsize: 13200
[startup+340.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2757 0 0 0 33983 14 0 0 25 0 1 0 420623233 13680640 2731 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3340 2731 603 41 0 3299 0
vsize: 13360
[startup+350.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2758 0 0 0 34983 14 0 0 25 0 1 0 420623233 13680640 2732 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3340 2732 603 41 0 3299 0
vsize: 13360
[startup+360.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2763 0 0 0 35983 14 0 0 25 0 1 0 420623233 13680640 2737 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3340 2737 603 41 0 3299 0
vsize: 13360
[startup+370.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2763 0 0 0 36983 14 0 0 25 0 1 0 420623233 13680640 2737 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3340 2737 603 41 0 3299 0
vsize: 13360
[startup+380.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2763 0 0 0 37983 14 0 0 25 0 1 0 420623233 13680640 2737 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3340 2737 603 41 0 3299 0
vsize: 13360
[startup+390.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2784 0 0 0 38983 14 0 0 25 0 1 0 420623233 13873152 2758 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3387 2758 603 41 0 3346 0
vsize: 13548
[startup+400.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2792 0 0 0 39984 14 0 0 25 0 1 0 420623233 13873152 2766 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3387 2766 603 41 0 3346 0
vsize: 13548
[startup+410.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2802 0 0 0 40984 14 0 0 25 0 1 0 420623233 13873152 2776 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3387 2776 603 41 0 3346 0
vsize: 13548
[startup+420.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2804 0 0 0 41984 14 0 0 25 0 1 0 420623233 13873152 2778 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3387 2778 603 41 0 3346 0
vsize: 13548
[startup+430.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2839 0 0 0 42984 14 0 0 25 0 1 0 420623233 14020608 2813 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3423 2813 603 41 0 3382 0
vsize: 13692
[startup+440.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2841 0 0 0 43984 14 0 0 25 0 1 0 420623233 14020608 2815 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3423 2815 603 41 0 3382 0
vsize: 13692
[startup+450.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2853 0 0 0 44984 14 0 0 25 0 1 0 420623233 14168064 2827 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3459 2827 603 41 0 3418 0
vsize: 13836
[startup+460.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2853 0 0 0 45984 14 0 0 25 0 1 0 420623233 14168064 2827 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3459 2827 603 41 0 3418 0
vsize: 13836
[startup+470.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2892 0 0 0 46984 14 0 0 25 0 1 0 420623233 14303232 2866 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3492 2866 603 41 0 3451 0
vsize: 13968
[startup+480.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2892 0 0 0 47985 14 0 0 25 0 1 0 420623233 14303232 2866 4294967295 134512640 134672761 3221224640 3221223776 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3492 2866 603 41 0 3451 0
vsize: 13968
[startup+490.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2898 0 0 0 48985 14 0 0 25 0 1 0 420623233 14303232 2872 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3492 2872 603 41 0 3451 0
vsize: 13968
[startup+500.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2904 0 0 0 49985 14 0 0 25 0 1 0 420623233 14303232 2878 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3492 2878 603 41 0 3451 0
vsize: 13968
[startup+510.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2904 0 0 0 50985 14 0 0 25 0 1 0 420623233 14303232 2878 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3492 2878 603 41 0 3451 0
vsize: 13968
[startup+520.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2909 0 0 0 51985 14 0 0 25 0 1 0 420623233 14467072 2883 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 2883 603 41 0 3491 0
vsize: 14128
[startup+530.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2918 0 0 0 52985 14 0 0 25 0 1 0 420623233 14467072 2892 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 2892 603 41 0 3491 0
vsize: 14128
[startup+540.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2922 0 0 0 53985 14 0 0 25 0 1 0 420623233 14467072 2896 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 2896 603 41 0 3491 0
vsize: 14128
[startup+550.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2927 0 0 0 54986 14 0 0 25 0 1 0 420623233 14467072 2901 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 2901 603 41 0 3491 0
vsize: 14128
[startup+560.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2933 0 0 0 55986 14 0 0 25 0 1 0 420623233 14467072 2907 4294967295 134512640 134672761 3221224640 3221223744 134560364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 2907 603 41 0 3491 0
vsize: 14128
[startup+570.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2934 0 0 0 56986 14 0 0 25 0 1 0 420623233 14467072 2908 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 2908 603 41 0 3491 0
vsize: 14128
[startup+580.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2948 0 0 0 57986 14 0 0 25 0 1 0 420623233 14610432 2922 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3567 2922 603 41 0 3526 0
vsize: 14268
[startup+590.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2949 0 0 0 58986 14 0 0 25 0 1 0 420623233 14610432 2923 4294967295 134512640 134672761 3221224640 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3567 2923 603 41 0 3526 0
vsize: 14268
[startup+600.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2959 0 0 0 59986 14 0 0 25 0 1 0 420623233 14610432 2933 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3567 2933 603 41 0 3526 0
vsize: 14268
[startup+610.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2971 0 0 0 60986 15 0 0 25 0 1 0 420623233 14610432 2945 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3567 2945 603 41 0 3526 0
vsize: 14268
[startup+620.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2992 0 0 0 61986 15 0 0 25 0 1 0 420623233 14774272 2966 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3607 2966 603 41 0 3566 0
vsize: 14428
[startup+630.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2995 0 0 0 62986 15 0 0 25 0 1 0 420623233 14774272 2969 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3607 2969 603 41 0 3566 0
vsize: 14428
[startup+640.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3008 0 0 0 63986 15 0 0 25 0 1 0 420623233 14938112 2982 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2982 603 41 0 3606 0
vsize: 14588
[startup+650.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3008 0 0 0 64986 15 0 0 25 0 1 0 420623233 14938112 2982 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2982 603 41 0 3606 0
vsize: 14588
[startup+660.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3008 0 0 0 65987 15 0 0 25 0 1 0 420623233 14938112 2982 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2982 603 41 0 3606 0
vsize: 14588
[startup+670.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3020 0 0 0 66987 15 0 0 25 0 1 0 420623233 14938112 2994 4294967295 134512640 134672761 3221224640 3221223808 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2994 603 41 0 3606 0
vsize: 14588
[startup+680.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3021 0 0 0 67987 15 0 0 25 0 1 0 420623233 14938112 2995 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2995 603 41 0 3606 0
vsize: 14588
[startup+690.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3023 0 0 0 68987 15 0 0 25 0 1 0 420623233 14938112 2997 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2997 603 41 0 3606 0
vsize: 14588
[startup+700.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3024 0 0 0 69987 15 0 0 25 0 1 0 420623233 14938112 2998 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2998 603 41 0 3606 0
vsize: 14588
[startup+710.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3024 0 0 0 70987 15 0 0 25 0 1 0 420623233 14938112 2998 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2998 603 41 0 3606 0
vsize: 14588
[startup+720.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 71988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2999 603 41 0 3606 0
vsize: 14588
[startup+730.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 72988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2999 603 41 0 3606 0
vsize: 14588
[startup+740.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 73988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223824 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2999 603 41 0 3606 0
vsize: 14588
[startup+750.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 74988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2999 603 41 0 3606 0
vsize: 14588
[startup+760.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 75988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2999 603 41 0 3606 0
vsize: 14588
[startup+770.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 76988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2999 603 41 0 3606 0
vsize: 14588
[startup+780.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 77989 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3647 2999 603 41 0 3606 0
vsize: 14588
[startup+790.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3085 0 0 0 78988 16 0 0 25 0 1 0 420623233 15200256 3059 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3711 3059 603 41 0 3670 0
vsize: 14844
[startup+800.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3141 0 0 0 79989 16 0 0 25 0 1 0 420623233 15495168 3115 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3783 3115 603 41 0 3742 0
vsize: 15132
[startup+810.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3143 0 0 0 80989 16 0 0 25 0 1 0 420623233 15495168 3117 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3783 3117 603 41 0 3742 0
vsize: 15132
[startup+820.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3144 0 0 0 81989 16 0 0 25 0 1 0 420623233 15495168 3118 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3783 3118 603 41 0 3742 0
vsize: 15132
[startup+830.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3207 0 0 0 82988 16 0 0 25 0 1 0 420623233 15761408 3181 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3848 3181 603 41 0 3807 0
vsize: 15392
[startup+840.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3207 0 0 0 83989 16 0 0 25 0 1 0 420623233 15761408 3181 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3848 3181 603 41 0 3807 0
vsize: 15392
[startup+850.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3216 0 0 0 84989 16 0 0 25 0 1 0 420623233 15761408 3190 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3848 3190 603 41 0 3807 0
vsize: 15392
[startup+860.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3317 0 0 0 85989 16 0 0 25 0 1 0 420623233 16162816 3291 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3291 603 41 0 3905 0
vsize: 15784
[startup+870.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3452 0 0 0 86988 17 0 0 25 0 1 0 420623233 16695296 3426 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4076 3426 603 41 0 4035 0
vsize: 16304
[startup+880.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3514 0 0 0 87988 17 0 0 25 0 1 0 420623233 16965632 3488 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4142 3488 603 41 0 4101 0
vsize: 16568
[startup+890.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3527 0 0 0 88988 17 0 0 25 0 1 0 420623233 17100800 3501 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3501 603 41 0 4134 0
vsize: 16700
[startup+900.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3529 0 0 0 89989 17 0 0 25 0 1 0 420623233 17100800 3503 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3503 603 41 0 4134 0
vsize: 16700
[startup+910.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3543 0 0 0 90989 17 0 0 25 0 1 0 420623233 17100800 3517 4294967295 134512640 134672761 3221224640 3221223744 134560207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3517 603 41 0 4134 0
vsize: 16700
[startup+920.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3547 0 0 0 91989 18 0 0 25 0 1 0 420623233 17100800 3521 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3521 603 41 0 4134 0
vsize: 16700
[startup+930.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3547 0 0 0 92989 18 0 0 25 0 1 0 420623233 17100800 3521 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3521 603 41 0 4134 0
vsize: 16700
[startup+940.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3551 0 0 0 93989 18 0 0 25 0 1 0 420623233 17100800 3525 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3525 603 41 0 4134 0
vsize: 16700
[startup+950.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3553 0 0 0 94989 18 0 0 25 0 1 0 420623233 17100800 3527 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3527 603 41 0 4134 0
vsize: 16700
[startup+960.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3563 0 0 0 95989 18 0 0 25 0 1 0 420623233 17100800 3537 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3537 603 41 0 4134 0
vsize: 16700
[startup+970.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3563 0 0 0 96990 18 0 0 25 0 1 0 420623233 17100800 3537 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3537 603 41 0 4134 0
vsize: 16700
[startup+980.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3563 0 0 0 97989 18 0 0 25 0 1 0 420623233 17100800 3537 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3537 603 41 0 4134 0
vsize: 16700
[startup+990.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3563 0 0 0 98990 18 0 0 25 0 1 0 420623233 17100800 3537 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3537 603 41 0 4134 0
vsize: 16700
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3576 0 0 0 99990 18 0 0 25 0 1 0 420623233 17264640 3550 4294967295 134512640 134672761 3221224640 3221223744 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3550 603 41 0 4174 0
vsize: 16860
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3585 0 0 0 100990 18 0 0 25 0 1 0 420623233 17264640 3559 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3559 603 41 0 4174 0
vsize: 16860
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3591 0 0 0 101990 18 0 0 25 0 1 0 420623233 17264640 3565 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3565 603 41 0 4174 0
vsize: 16860
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3592 0 0 0 102990 18 0 0 25 0 1 0 420623233 17264640 3566 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3566 603 41 0 4174 0
vsize: 16860
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3594 0 0 0 103990 18 0 0 25 0 1 0 420623233 17264640 3568 4294967295 134512640 134672761 3221224640 3221223776 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3568 603 41 0 4174 0
vsize: 16860
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3594 0 0 0 104991 18 0 0 25 0 1 0 420623233 17264640 3568 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3568 603 41 0 4174 0
vsize: 16860
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3594 0 0 0 105991 18 0 0 25 0 1 0 420623233 17264640 3568 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4215 3568 603 41 0 4174 0
vsize: 16860
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3619 0 0 0 106991 18 0 0 25 0 1 0 420623233 17461248 3593 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3593 603 41 0 4222 0
vsize: 17052
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3635 0 0 0 107991 18 0 0 25 0 1 0 420623233 17461248 3609 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3609 603 41 0 4222 0
vsize: 17052
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3635 0 0 0 108991 18 0 0 25 0 1 0 420623233 17461248 3609 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3609 603 41 0 4222 0
vsize: 17052
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3635 0 0 0 109991 18 0 0 25 0 1 0 420623233 17461248 3609 4294967295 134512640 134672761 3221224640 3221223824 134559385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3609 603 41 0 4222 0
vsize: 17052
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3635 0 0 0 110991 18 0 0 25 0 1 0 420623233 17461248 3609 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3609 603 41 0 4222 0
vsize: 17052
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3641 0 0 0 111991 18 0 0 25 0 1 0 420623233 17461248 3615 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3615 603 41 0 4222 0
vsize: 17052
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3650 0 0 0 112992 18 0 0 25 0 1 0 420623233 17625088 3624 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3624 603 41 0 4262 0
vsize: 17212
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3652 0 0 0 113992 18 0 0 25 0 1 0 420623233 17625088 3626 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3626 603 41 0 4262 0
vsize: 17212
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3652 0 0 0 114992 18 0 0 25 0 1 0 420623233 17625088 3626 4294967295 134512640 134672761 3221224640 3221223808 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3626 603 41 0 4262 0
vsize: 17212
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3665 0 0 0 115992 18 0 0 25 0 1 0 420623233 17625088 3639 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3639 603 41 0 4262 0
vsize: 17212
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3666 0 0 0 116992 18 0 0 25 0 1 0 420623233 17625088 3640 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3640 603 41 0 4262 0
vsize: 17212
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3667 0 0 0 117992 18 0 0 25 0 1 0 420623233 17625088 3641 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3641 603 41 0 4262 0
vsize: 17212
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3667 0 0 0 118993 18 0 0 25 0 1 0 420623233 17625088 3641 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3641 603 41 0 4262 0
vsize: 17212
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 964
Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3667 0 0 0 119993 18 0 0 25 0 1 0 420623233 17625088 3641 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3641 603 41 0 4262 0
vsize: 17212
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 964
Raw data (stat): 964 (minisat+) Z 963 30701 30700 0 -1 12 3670 0 0 0 119993 19 0 0 25 0 1 0 420623233 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.02
CPU time (s): 1200.13
CPU user time (s): 1199.93
CPU system time (s): 0.19697
CPU usage (%): 100.009
Max. virtual memory (Kb): 17212
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####