PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32b2.opb
MD5SUM	4c322f6b4009d273fbdff10efcd1c54f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	244
Optimality of the best value was proved	NO
Number of terms in the objective function	522
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	522
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	522
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03184
Number of variables	522
Total number of constraints	2819
Number of constraints which are clauses	2819
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 4692

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-13 19:52:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3532 boxname=wulflinc32 idbench=148 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4c322f6b4009d273fbdff10efcd1c54f  /oldhome/oroussel/tmp/wulflinc32/normalized-ii32b2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc32/normalized-ii32b2.opb /oldhome/oroussel/tmp/wulflinc32/normalized-ii32b2.opb
IDLAUNCH: 3532
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        753812 kB
Buffers:         33680 kB
Cached:         135856 kB
SwapCached:       1212 kB
Active:         137876 kB
Inactive:       112048 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        753556 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2244 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25100 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:12:42 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 3532 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2819 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 |    2819    12591 |     939       0        0     nan |  0.000 % |
c |       100 |    2819    12591 |    1032     100     3244    32.4 |  0.017 % |
c |       254 |    2819    12591 |    1136     254     8804    34.7 |  0.000 % |
c |       479 |    2819    12591 |    1249     479    18626    38.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 257[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1038   maxlim: 265   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       686 |   10020    38284 |    3340     686    29611    43.2 |  0.000 % |
c |       788 |   10020    38284 |    3674     788    34495    43.8 |  0.192 % |
c |       940 |   10020    38284 |    4041     940    42139    44.8 |  0.192 % |
c |      1166 |   10020    38284 |    4445    1166    52566    45.1 |  0.192 % |
c |      1504 |   10020    38284 |    4890    1504    64767    43.1 |  0.192 % |
c ==============================================================================
c [1mFound solution: 254[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 268   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1984 |   10026    38316 |    3342    1984    84067    42.4 |  0.192 % |
c ==============================================================================
c [1mFound solution: 253[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 269   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1998 |   10027    38326 |    3342    1998    84850    42.5 |  0.192 % |
c |      2099 |   10027    38326 |    3676    2099    89974    42.9 |  0.383 % |
c |      2249 |   10027    38326 |    4043    2249    93907    41.8 |  0.383 % |
c |      2480 |   10027    38326 |    4448    2480   104190    42.0 |  0.383 % |
c |      2818 |   10027    38326 |    4893    2818   119295    42.3 |  0.383 % |
c |      3325 |   10027    38326 |    5382    3325   141969    42.7 |  0.383 % |
c |      4085 |   10027    38326 |    5920    4085   172717    42.3 |  0.383 % |
c |      5225 |   10027    38326 |    6512    5225   257251    49.2 |  0.383 % |
c |      6933 |   10027    38326 |    7163    6933   344302    49.7 |  0.383 % |
c ==============================================================================
c [1mFound solution: 245[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 277   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8571 |   10032    38358 |    3344    4953   232946    47.0 |  0.383 % |
c |      8673 |   10032    38358 |    3678    2579    90659    35.2 |  0.574 % |
c |      8823 |   10032    38358 |    4046    2729    95398    35.0 |  0.574 % |
c |      9048 |   10032    38358 |    4450    2954   106663    36.1 |  0.574 % |
c |      9385 |   10032    38358 |    4895    3291   124673    37.9 |  0.574 % |
c |      9892 |   10032    38358 |    5385    3798   149818    39.4 |  0.574 % |
c |     10657 |   10032    38358 |    5924    4563   192755    42.2 |  0.574 % |
c |     11799 |   10032    38358 |    6516    5705   263492    46.2 |  0.574 % |
c |     13507 |   10032    38358 |    7168    4109   160139    39.0 |  0.574 % |
c |     16070 |   10032    38358 |    7884    6672   340127    51.0 |  0.574 % |
c |     19914 |   10032    38358 |    8673    6534   470931    72.1 |  0.574 % |
c |     25681 |   10032    38358 |    9540    7623   737141    96.7 |  0.574 % |
c |     34331 |   10032    38358 |   10494    5539   530027    95.7 |  0.574 % |
c |     47305 |   10032    38358 |   11544    7399   645610    87.3 |  0.574 % |
c |     66766 |   10032    38358 |   12698    8672   329878    38.0 |  0.574 % |
c |     95958 |   10032    38358 |   13968   10823  1229807   113.6 |  0.574 % |
c ==============================================================================
c [1mFound solution: 244[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 278   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117373 |   10037    38385 |    3345    9831  1051749   107.0 |  0.574 % |
c |    117473 |   10037    38385 |    3679    2558   129896    50.8 |  0.637 % |
c |    117623 |   10037    38385 |    4047    2708   134506    49.7 |  0.637 % |
c |    117849 |   10037    38385 |    4452    2934   145727    49.7 |  0.637 % |
c |    118187 |   10037    38385 |    4897    3272   157328    48.1 |  0.637 % |
c |    118694 |   10037    38385 |    5387    3779   182293    48.2 |  0.637 % |
c |    119453 |   10037    38385 |    5925    4538   234245    51.6 |  0.637 % |
c |    120592 |   10037    38385 |    6518    5677   276882    48.8 |  0.637 % |
c |    122300 |   10037    38385 |    7170    3783   144612    38.2 |  0.637 % |
c |    124862 |   10037    38385 |    7887    6345   275754    43.5 |  0.637 % |
c |    128706 |   10037    38385 |    8676    5668   412579    72.8 |  0.637 % |
c |    134472 |   10037    38385 |    9543    6540   571674    87.4 |  0.637 % |
c |    143122 |   10037    38385 |   10498    9812   922204    94.0 |  0.637 % |
c |    156096 |   10037    38385 |   11547    6190   330794    53.4 |  0.637 % |
c |    175557 |   10037    38385 |   12702    7321   631649    86.3 |  0.637 % |
c |    204751 |   10037    38385 |   13972    9010   814435    90.4 |  0.637 % |
c |    248540 |    9989    38243 |   15370   14909  1575339   105.7 |  0.892 % |
c |    314224 |    9989    38243 |   16907   15046  1380391    91.7 |  0.892 % |
c |    412751 |    9989    38243 |   18597   15360  1611667   104.9 |  0.892 % |
c |    560541 |    9989    38243 |   20457   17356  1700246    98.0 |  0.892 % |
c |    782225 |    9989    38243 |   22503   15047  1439213    95.6 |  0.892 % |
#### 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.92 0.95 0.76 2/53 10794
Raw data (stat): 10794 (runsolver) R 10793 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478612851 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.96 0.76 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 1070 0 0 0 995 2 0 0 25 0 1 0 478612851 5967872 1048 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1457 1048 603 41 0 1416 0
vsize: 5828
[startup+20.0026 s]
Raw data (loadavg): 0.94 0.96 0.76 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 1699 0 0 0 1993 5 0 0 25 0 1 0 478612851 8527872 1677 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2082 1677 603 41 0 2041 0
vsize: 8328
[startup+30.0031 s]
Raw data (loadavg): 0.95 0.96 0.76 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 1750 0 0 0 2993 5 0 0 25 0 1 0 478612851 8658944 1728 4294967295 134512640 134672761 3221224576 3221223584 1075349729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2114 1728 603 41 0 2073 0
vsize: 8456
[startup+40.0041 s]
Raw data (loadavg): 0.96 0.96 0.76 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 1754 0 0 0 3993 5 0 0 25 0 1 0 478612851 8658944 1732 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2114 1732 603 41 0 2073 0
vsize: 8456
[startup+50.0048 s]
Raw data (loadavg): 0.96 0.96 0.77 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 1820 0 0 0 4993 5 0 0 25 0 1 0 478612851 8925184 1798 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2179 1798 603 41 0 2138 0
vsize: 8716
[startup+60.0054 s]
Raw data (loadavg): 0.97 0.96 0.77 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 1821 0 0 0 5992 6 0 0 25 0 1 0 478612851 8925184 1799 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2179 1799 603 41 0 2138 0
vsize: 8716
[startup+70.0064 s]
Raw data (loadavg): 0.97 0.96 0.77 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2082 0 0 0 6991 7 0 0 25 0 1 0 478612851 10129408 2060 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2473 2060 603 41 0 2432 0
vsize: 9892
[startup+80.0071 s]
Raw data (loadavg): 0.98 0.96 0.77 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2195 0 0 0 7991 7 0 0 25 0 1 0 478612851 10534912 2173 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2173 603 41 0 2531 0
vsize: 10288
[startup+90.0079 s]
Raw data (loadavg): 0.98 0.96 0.77 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2424 0 0 0 8990 8 0 0 25 0 1 0 478612851 11472896 2402 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2801 2402 603 41 0 2760 0
vsize: 11204
[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.78 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2424 0 0 0 9991 8 0 0 25 0 1 0 478612851 11472896 2402 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2801 2402 603 41 0 2760 0
vsize: 11204
[startup+110.009 s]
Raw data (loadavg): 0.98 0.97 0.78 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 10990 8 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.78 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 11990 8 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.78 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 12991 8 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223716 134560629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.78 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 13991 8 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+150.012 s]
Raw data (loadavg): 0.99 0.97 0.79 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 14991 8 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.79 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 15991 8 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 16992 8 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.79 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 17992 8 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 18991 9 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223040 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.80 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 19991 9 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.80 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 20991 9 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223488 1075352446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.80 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2462 0 0 0 21991 9 0 0 25 0 1 0 478612851 11608064 2440 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2440 603 41 0 2793 0
vsize: 11336
[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.80 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2539 0 0 0 22992 9 0 0 25 0 1 0 478612851 11874304 2517 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2899 2517 603 41 0 2858 0
vsize: 11596
[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.80 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2810 0 0 0 23991 9 0 0 25 0 1 0 478612851 13168640 2788 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3215 2788 603 41 0 3174 0
vsize: 12860
[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.81 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2810 0 0 0 24992 10 0 0 25 0 1 0 478612851 13168640 2788 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3215 2788 603 41 0 3174 0
vsize: 12860
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.81 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2810 0 0 0 25992 10 0 0 25 0 1 0 478612851 13168640 2788 4294967295 134512640 134672761 3221224576 3221223680 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3215 2788 603 41 0 3174 0
vsize: 12860
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.81 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2810 0 0 0 26992 10 0 0 25 0 1 0 478612851 13168640 2788 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3215 2788 603 41 0 3174 0
vsize: 12860
[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.81 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2810 0 0 0 27992 10 0 0 25 0 1 0 478612851 13168640 2788 4294967295 134512640 134672761 3221224576 3221223680 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3215 2788 603 41 0 3174 0
vsize: 12860
[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.81 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2856 0 0 0 28992 10 0 0 25 0 1 0 478612851 13303808 2834 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3248 2834 603 41 0 3207 0
vsize: 12992
[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2863 0 0 0 29993 10 0 0 25 0 1 0 478612851 13303808 2841 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3248 2841 603 41 0 3207 0
vsize: 12992
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.82 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2863 0 0 0 30993 10 0 0 25 0 1 0 478612851 13303808 2841 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3248 2841 603 41 0 3207 0
vsize: 12992
[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.82 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2864 0 0 0 31993 10 0 0 25 0 1 0 478612851 13303808 2842 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3248 2842 603 41 0 3207 0
vsize: 12992
[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.82 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2865 0 0 0 32993 10 0 0 25 0 1 0 478612851 13303808 2843 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3248 2843 603 41 0 3207 0
vsize: 12992
[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.82 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2865 0 0 0 33993 10 0 0 25 0 1 0 478612851 13303808 2843 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3248 2843 603 41 0 3207 0
vsize: 12992
[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.82 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 2865 0 0 0 34993 10 0 0 25 0 1 0 478612851 13303808 2843 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3248 2843 603 41 0 3207 0
vsize: 12992
[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.82 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3269 0 0 0 35992 11 0 0 25 0 1 0 478612851 15040512 3247 4294967295 134512640 134672761 3221224576 3221223760 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3672 3247 603 41 0 3631 0
vsize: 14688
[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.82 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3269 0 0 0 36992 11 0 0 25 0 1 0 478612851 15040512 3247 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3672 3247 603 41 0 3631 0
vsize: 14688
[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.82 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3480 0 0 0 37992 12 0 0 25 0 1 0 478612851 15851520 3458 4294967295 134512640 134672761 3221224576 3221223760 134559367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3458 603 41 0 3829 0
vsize: 15480
[startup+390.031 s]
Raw data (loadavg): 0.99 0.97 0.83 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3480 0 0 0 38992 12 0 0 25 0 1 0 478612851 15851520 3458 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3458 603 41 0 3829 0
vsize: 15480
[startup+400.032 s]
Raw data (loadavg): 0.99 0.97 0.83 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3480 0 0 0 39992 12 0 0 25 0 1 0 478612851 15851520 3458 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3458 603 41 0 3829 0
vsize: 15480
[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.83 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3480 0 0 0 40993 12 0 0 25 0 1 0 478612851 15851520 3458 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3458 603 41 0 3829 0
vsize: 15480
[startup+420.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3480 0 0 0 41993 12 0 0 25 0 1 0 478612851 15851520 3458 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3458 603 41 0 3829 0
vsize: 15480
[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.83 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3480 0 0 0 42993 12 0 0 25 0 1 0 478612851 15851520 3458 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3458 603 41 0 3829 0
vsize: 15480
[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.83 2/53 10794
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3480 0 0 0 43993 12 0 0 25 0 1 0 478612851 15851520 3458 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3870 3458 603 41 0 3829 0
vsize: 15480
[startup+450.035 s]
Raw data (loadavg): 1.07 0.99 0.84 2/53 10847
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3481 0 0 0 44993 12 0 0 25 0 1 0 478612851 15851520 3459 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3459 603 41 0 3829 0
vsize: 15480
[startup+460.036 s]
Raw data (loadavg): 1.06 0.99 0.84 2/53 10847
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3481 0 0 0 45993 12 0 0 25 0 1 0 478612851 15851520 3459 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3459 603 41 0 3829 0
vsize: 15480
[startup+470.037 s]
Raw data (loadavg): 1.05 0.99 0.84 2/53 10847
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3481 0 0 0 46993 12 0 0 25 0 1 0 478612851 15851520 3459 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3459 603 41 0 3829 0
vsize: 15480
[startup+480.037 s]
Raw data (loadavg): 1.04 0.99 0.84 2/53 10847
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3481 0 0 0 47993 12 0 0 25 0 1 0 478612851 15851520 3459 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3459 603 41 0 3829 0
vsize: 15480
[startup+490.038 s]
Raw data (loadavg): 1.04 0.99 0.84 2/53 10847
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3481 0 0 0 48994 12 0 0 25 0 1 0 478612851 15851520 3459 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3459 603 41 0 3829 0
vsize: 15480
[startup+500.039 s]
Raw data (loadavg): 1.03 0.99 0.84 2/53 10847
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3481 0 0 0 49994 12 0 0 25 0 1 0 478612851 15851520 3459 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3459 603 41 0 3829 0
vsize: 15480
[startup+510.039 s]
Raw data (loadavg): 1.03 0.99 0.84 2/53 10847
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3483 0 0 0 50994 12 0 0 25 0 1 0 478612851 15851520 3461 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3461 603 41 0 3829 0
vsize: 15480
[startup+520.04 s]
Raw data (loadavg): 1.02 0.99 0.84 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3483 0 0 0 51994 12 0 0 25 0 1 0 478612851 15851520 3461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3461 603 41 0 3829 0
vsize: 15480
[startup+530.041 s]
Raw data (loadavg): 1.02 0.99 0.84 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3483 0 0 0 52995 12 0 0 25 0 1 0 478612851 15851520 3461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3461 603 41 0 3829 0
vsize: 15480
[startup+540.041 s]
Raw data (loadavg): 1.01 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3604 0 0 0 53994 13 0 0 25 0 1 0 478612851 16384000 3582 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3582 603 41 0 3959 0
vsize: 16000
[startup+550.042 s]
Raw data (loadavg): 1.01 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3612 0 0 0 54995 13 0 0 25 0 1 0 478612851 16384000 3590 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3590 603 41 0 3959 0
vsize: 16000
[startup+560.042 s]
Raw data (loadavg): 1.01 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3612 0 0 0 55995 13 0 0 25 0 1 0 478612851 16384000 3590 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3590 603 41 0 3959 0
vsize: 16000
[startup+570.043 s]
Raw data (loadavg): 1.01 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3612 0 0 0 56995 13 0 0 25 0 1 0 478612851 16384000 3590 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3590 603 41 0 3959 0
vsize: 16000
[startup+580.044 s]
Raw data (loadavg): 1.01 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3625 0 0 0 57995 13 0 0 25 0 1 0 478612851 16519168 3603 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4033 3603 603 41 0 3992 0
vsize: 16132
[startup+590.044 s]
Raw data (loadavg): 1.00 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3625 0 0 0 58995 13 0 0 25 0 1 0 478612851 16519168 3603 4294967295 134512640 134672761 3221224576 3221223760 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4033 3603 603 41 0 3992 0
vsize: 16132
[startup+600.044 s]
Raw data (loadavg): 1.00 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3659 0 0 0 59995 13 0 0 25 0 1 0 478612851 16654336 3637 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3637 603 41 0 4025 0
vsize: 16264
[startup+610.045 s]
Raw data (loadavg): 1.00 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3659 0 0 0 60996 13 0 0 25 0 1 0 478612851 16654336 3637 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3637 603 41 0 4025 0
vsize: 16264
[startup+620.046 s]
Raw data (loadavg): 1.00 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3659 0 0 0 61996 13 0 0 25 0 1 0 478612851 16654336 3637 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3637 603 41 0 4025 0
vsize: 16264
[startup+630.047 s]
Raw data (loadavg): 1.00 0.99 0.85 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3663 0 0 0 62996 13 0 0 25 0 1 0 478612851 16654336 3641 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3641 603 41 0 4025 0
vsize: 16264
[startup+640.046 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3663 0 0 0 63996 13 0 0 25 0 1 0 478612851 16654336 3641 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3641 603 41 0 4025 0
vsize: 16264
[startup+650.047 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3663 0 0 0 64997 13 0 0 25 0 1 0 478612851 16654336 3641 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3641 603 41 0 4025 0
vsize: 16264
[startup+660.048 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3665 0 0 0 65996 13 0 0 25 0 1 0 478612851 16654336 3643 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3643 603 41 0 4025 0
vsize: 16264
[startup+670.05 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3665 0 0 0 66996 13 0 0 25 0 1 0 478612851 16654336 3643 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3643 603 41 0 4025 0
vsize: 16264
[startup+680.05 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3665 0 0 0 67996 13 0 0 25 0 1 0 478612851 16654336 3643 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3643 603 41 0 4025 0
vsize: 16264
[startup+690.05 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3665 0 0 0 68996 13 0 0 25 0 1 0 478612851 16654336 3643 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3643 603 41 0 4025 0
vsize: 16264
[startup+700.051 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3665 0 0 0 69997 13 0 0 25 0 1 0 478612851 16654336 3643 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3643 603 41 0 4025 0
vsize: 16264
[startup+710.052 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3720 0 0 0 70996 14 0 0 25 0 1 0 478612851 16916480 3698 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3698 603 41 0 4089 0
vsize: 16520
[startup+720.053 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3798 0 0 0 71996 14 0 0 25 0 1 0 478612851 17186816 3776 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3776 603 41 0 4155 0
vsize: 16784
[startup+730.053 s]
Raw data (loadavg): 1.00 0.99 0.86 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3823 0 0 0 72996 14 0 0 25 0 1 0 478612851 17317888 3801 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4228 3801 603 41 0 4187 0
vsize: 16912
[startup+740.053 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3823 0 0 0 73997 14 0 0 25 0 1 0 478612851 17317888 3801 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4228 3801 603 41 0 4187 0
vsize: 16912
[startup+750.054 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3823 0 0 0 74997 14 0 0 25 0 1 0 478612851 17297408 3801 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3801 603 41 0 4182 0
vsize: 16892
[startup+760.054 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3823 0 0 0 75997 14 0 0 25 0 1 0 478612851 17297408 3801 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3801 603 41 0 4182 0
vsize: 16892
[startup+770.055 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3823 0 0 0 76997 14 0 0 25 0 1 0 478612851 17297408 3801 4294967295 134512640 134672761 3221224576 3221223736 134559749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3801 603 41 0 4182 0
vsize: 16892
[startup+780.056 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3823 0 0 0 77998 14 0 0 25 0 1 0 478612851 17297408 3801 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3801 603 41 0 4182 0
vsize: 16892
[startup+790.057 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3823 0 0 0 78998 14 0 0 25 0 1 0 478612851 17281024 3801 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4219 3801 603 41 0 4178 0
vsize: 16876
[startup+800.058 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3823 0 0 0 79998 14 0 0 25 0 1 0 478612851 17281024 3801 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4219 3801 603 41 0 4178 0
vsize: 16876
[startup+810.058 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10849
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3962 0 0 0 80998 15 0 0 25 0 1 0 478612851 17813504 3940 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4349 3940 603 41 0 4308 0
vsize: 17396
[startup+820.059 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3967 0 0 0 81998 15 0 0 25 0 1 0 478612851 17973248 3945 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3945 603 41 0 4347 0
vsize: 17552
[startup+830.06 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3968 0 0 0 82998 15 0 0 25 0 1 0 478612851 17973248 3946 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3946 603 41 0 4347 0
vsize: 17552
[startup+840.06 s]
Raw data (loadavg): 1.00 0.99 0.87 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3973 0 0 0 83998 15 0 0 25 0 1 0 478612851 17973248 3951 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3951 603 41 0 4347 0
vsize: 17552
[startup+850.06 s]
Raw data (loadavg): 1.00 0.99 0.88 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3974 0 0 0 84998 15 0 0 25 0 1 0 478612851 17973248 3952 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3952 603 41 0 4347 0
vsize: 17552
[startup+860.061 s]
Raw data (loadavg): 1.00 0.99 0.88 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3974 0 0 0 85999 15 0 0 25 0 1 0 478612851 17973248 3952 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3952 603 41 0 4347 0
vsize: 17552
[startup+870.062 s]
Raw data (loadavg): 1.00 0.99 0.88 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3974 0 0 0 86999 15 0 0 25 0 1 0 478612851 17973248 3952 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3952 603 41 0 4347 0
vsize: 17552
[startup+880.063 s]
Raw data (loadavg): 1.00 0.99 0.88 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3974 0 0 0 87999 15 0 0 25 0 1 0 478612851 17973248 3952 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3952 603 41 0 4347 0
vsize: 17552
[startup+890.062 s]
Raw data (loadavg): 1.00 0.99 0.88 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3974 0 0 0 88999 15 0 0 25 0 1 0 478612851 17973248 3952 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3952 603 41 0 4347 0
vsize: 17552
[startup+900.063 s]
Raw data (loadavg): 1.00 0.99 0.88 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3975 0 0 0 90000 15 0 0 25 0 1 0 478612851 17973248 3953 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3953 603 41 0 4347 0
vsize: 17552
[startup+910.064 s]
Raw data (loadavg): 1.00 0.99 0.88 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3975 0 0 0 91000 15 0 0 25 0 1 0 478612851 17973248 3953 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3953 603 41 0 4347 0
vsize: 17552
[startup+920.065 s]
Raw data (loadavg): 1.00 0.99 0.88 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3976 0 0 0 92000 15 0 0 25 0 1 0 478612851 17973248 3954 4294967295 134512640 134672761 3221224576 3221223664 134565868 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3954 603 41 0 4347 0
vsize: 17552
[startup+930.065 s]
Raw data (loadavg): 1.08 1.00 0.89 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3976 0 0 0 93000 15 0 0 25 0 1 0 478612851 17973248 3954 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3954 603 41 0 4347 0
vsize: 17552
[startup+940.065 s]
Raw data (loadavg): 1.14 1.02 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3977 0 0 0 94001 15 0 0 25 0 1 0 478612851 17973248 3955 4294967295 134512640 134672761 3221224576 3221223740 134560077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3955 603 41 0 4347 0
vsize: 17552
[startup+950.066 s]
Raw data (loadavg): 1.12 1.02 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3977 0 0 0 95001 15 0 0 25 0 1 0 478612851 17973248 3955 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3955 603 41 0 4347 0
vsize: 17552
[startup+960.067 s]
Raw data (loadavg): 1.10 1.02 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3977 0 0 0 96001 15 0 0 25 0 1 0 478612851 17973248 3955 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3955 603 41 0 4347 0
vsize: 17552
[startup+970.068 s]
Raw data (loadavg): 1.08 1.02 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3977 0 0 0 97001 15 0 0 25 0 1 0 478612851 17973248 3955 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3955 603 41 0 4347 0
vsize: 17552
[startup+980.069 s]
Raw data (loadavg): 1.07 1.02 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3977 0 0 0 98002 15 0 0 25 0 1 0 478612851 17973248 3955 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3955 603 41 0 4347 0
vsize: 17552
[startup+990.069 s]
Raw data (loadavg): 1.06 1.01 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3977 0 0 0 99002 15 0 0 25 0 1 0 478612851 17973248 3955 4294967295 134512640 134672761 3221224576 3221223680 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3955 603 41 0 4347 0
vsize: 17552
[startup+1000.07 s]
Raw data (loadavg): 1.05 1.01 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3977 0 0 0 100002 15 0 0 25 0 1 0 478612851 17973248 3955 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3955 603 41 0 4347 0
vsize: 17552
[startup+1010.07 s]
Raw data (loadavg): 1.04 1.01 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3977 0 0 0 101002 15 0 0 25 0 1 0 478612851 17973248 3955 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3955 603 41 0 4347 0
vsize: 17552
[startup+1020.07 s]
Raw data (loadavg): 1.04 1.01 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3978 0 0 0 102002 15 0 0 25 0 1 0 478612851 17973248 3956 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3956 603 41 0 4347 0
vsize: 17552
[startup+1030.07 s]
Raw data (loadavg): 1.03 1.01 0.90 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3979 0 0 0 103002 15 0 0 25 0 1 0 478612851 17973248 3957 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3957 603 41 0 4347 0
vsize: 17552
[startup+1040.07 s]
Raw data (loadavg): 1.02 1.01 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3979 0 0 0 104002 15 0 0 25 0 1 0 478612851 17973248 3957 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3957 603 41 0 4347 0
vsize: 17552
[startup+1050.07 s]
Raw data (loadavg): 1.02 1.01 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3980 0 0 0 105002 15 0 0 25 0 1 0 478612851 17973248 3958 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3958 603 41 0 4347 0
vsize: 17552
[startup+1060.07 s]
Raw data (loadavg): 1.02 1.01 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3980 0 0 0 106002 15 0 0 25 0 1 0 478612851 17973248 3958 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3958 603 41 0 4347 0
vsize: 17552
[startup+1070.08 s]
Raw data (loadavg): 1.01 1.01 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3980 0 0 0 107003 15 0 0 25 0 1 0 478612851 17973248 3958 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3958 603 41 0 4347 0
vsize: 17552
[startup+1080.08 s]
Raw data (loadavg): 1.01 1.01 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3980 0 0 0 108003 15 0 0 25 0 1 0 478612851 17973248 3958 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3958 603 41 0 4347 0
vsize: 17552
[startup+1090.08 s]
Raw data (loadavg): 1.01 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3987 0 0 0 109003 15 0 0 25 0 1 0 478612851 17973248 3965 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3965 603 41 0 4347 0
vsize: 17552
[startup+1100.08 s]
Raw data (loadavg): 1.01 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 3992 0 0 0 110003 15 0 0 25 0 1 0 478612851 17973248 3970 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3970 603 41 0 4347 0
vsize: 17552
[startup+1110.08 s]
Raw data (loadavg): 1.01 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4086 0 0 0 111003 15 0 0 25 0 1 0 478612851 18378752 4064 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4487 4064 603 41 0 4446 0
vsize: 17948
[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4089 0 0 0 112004 15 0 0 25 0 1 0 478612851 18378752 4067 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4487 4067 603 41 0 4446 0
vsize: 17948
[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4146 0 0 0 113004 16 0 0 25 0 1 0 478612851 18644992 4124 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4124 603 41 0 4511 0
vsize: 18208
[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4151 0 0 0 114004 16 0 0 25 0 1 0 478612851 18644992 4129 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4129 603 41 0 4511 0
vsize: 18208
[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4378 0 0 0 115003 17 0 0 25 0 1 0 478612851 19578880 4356 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4780 4356 603 41 0 4739 0
vsize: 19120
[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4378 0 0 0 116003 17 0 0 25 0 1 0 478612851 19578880 4356 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4780 4356 603 41 0 4739 0
vsize: 19120
[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4440 0 0 0 117003 17 0 0 25 0 1 0 478612851 19845120 4418 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 4418 603 41 0 4804 0
vsize: 19380
[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4445 0 0 0 118004 17 0 0 25 0 1 0 478612851 19845120 4423 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 4423 603 41 0 4804 0
vsize: 19380
[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4446 0 0 0 119004 17 0 0 25 0 1 0 478612851 19845120 4424 4294967295 134512640 134672761 3221224576 3221222144 134565812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 4424 603 41 0 4804 0
vsize: 19380
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.91 2/53 10851
Raw data (stat): 10794 (minisat+) R 10793 7987 7986 0 -1 0 4446 0 0 0 120004 17 0 0 25 0 1 0 478612851 19845120 4424 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 4424 603 41 0 4804 0
vsize: 19380
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.91 1/53 10851
Raw data (stat): 10794 (minisat+) Z 10793 7987 7986 0 -1 12 4449 0 0 0 120004 18 0 0 25 0 1 0 478612851 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.23
CPU user time (s): 1200.05
CPU system time (s): 0.183972
CPU usage (%): 100.011
Max. virtual memory (Kb): 19380
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####