PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cm42a.opb
MD5SUM	62b75258091a8b1382fa8b1c633d9511
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	694
Optimality of the best value was proved	NO
Number of terms in the objective function	99
Biggest coefficient in the objective function	60
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	4087
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	60
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	4087
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.168973
Number of variables	99
Total number of constraints	185
Number of constraints which are clauses	185
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	20
Trace number 6337

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-14 04:22:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4764 boxname=wulflinc31 idbench=252 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  62b75258091a8b1382fa8b1c633d9511  /oldhome/oroussel/tmp/wulflinc31/normalized-cm42a.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc31/normalized-cm42a.opb /oldhome/oroussel/tmp/wulflinc31/normalized-cm42a.opb
IDLAUNCH: 4764
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        888384 kB
Buffers:         36364 kB
Cached:          71296 kB
SwapCached:        392 kB
Active:          53368 kB
Inactive:        57452 kB
HighTotal:      131008 kB
HighFree:        56028 kB
LowTotal:       903652 kB
LowFree:        832356 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29876 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:39:16 (client local time) WITH STATUS 30 IN 991.917 SECONDS
stats: 4764 0 991.917 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 185 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 |     185      626 |      61       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 939[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 8480     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23406    55077 |    7802       0        0     nan |  0.000 % |
c |       100 |   23259    54744 |    8582      97      829     8.5 |  0.441 % |
c |       251 |   23048    54266 |    9440     245     2188     8.9 |  1.116 % |
c |       478 |   23048    54266 |   10384     472     8022    17.0 |  1.116 % |
c |       817 |   22732    53545 |   11422     788    17489    22.2 |  2.128 % |
c |      1323 |   22732    53545 |   12565    1294    39857    30.8 |  2.128 % |
c |      2086 |   22732    53545 |   13821    2057    59435    28.9 |  2.128 % |
c |      3227 |   22732    53545 |   15203    3198    85918    26.9 |  2.128 % |
c |      4936 |   22732    53545 |   16724    4907   130921    26.7 |  2.128 % |
c |      7501 |   22732    53545 |   18396    7472   232997    31.2 |  2.128 % |
c ==============================================================================
c [1mFound solution: 932[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6776     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9749 |   40300    94757 |   13433    9720   307975    31.7 |  2.128 % |
c |      9849 |   40300    94757 |   14776    9820   310180    31.6 |  1.226 % |
c |     10000 |   40300    94757 |   16253    9971   313662    31.5 |  1.226 % |
c ==============================================================================
c [1mFound solution: 894[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10090 |   40987    96462 |   13662   10061   317034    31.5 |  1.226 % |
c |     10190 |   40987    96462 |   15028   10161   320676    31.6 |  1.217 % |
c |     10341 |   40987    96462 |   16531   10312   328401    31.8 |  1.217 % |
c |     10566 |   40987    96462 |   18184   10537   331270    31.4 |  1.217 % |
c |     10903 |   40987    96462 |   20002   10874   337761    31.1 |  1.218 % |
c ==============================================================================
c [1mFound solution: 839[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11008 |   41093    96754 |   13697   10979   339286    30.9 |  1.218 % |
c |     11108 |   41093    96754 |   15066   11079   340249    30.7 |  1.223 % |
c |     11261 |   41093    96754 |   16573   11232   343737    30.6 |  1.223 % |
c |     11486 |   41093    96754 |   18230   11457   347415    30.3 |  1.223 % |
c |     11823 |   41093    96754 |   20053   11794   352229    29.9 |  1.223 % |
c ==============================================================================
c [1mFound solution: 732[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11825 |   41147    96898 |   13715   11796   352255    29.9 |  1.223 % |
c ==============================================================================
c [1mFound solution: 723[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11847 |   41187    97004 |   13729   11818   353824    29.9 |  1.223 % |
c |     11947 |   41187    97004 |   15101   11918   357596    30.0 |  1.236 % |
c |     12097 |   41187    97004 |   16612   12068   359829    29.8 |  1.236 % |
c |     12322 |   41187    97004 |   18273   12293   362973    29.5 |  1.236 % |
c |     12660 |   41116    96843 |   20100   12449   367122    29.5 |  1.368 % |
c ==============================================================================
c [1mFound solution: 721[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13164 |   41275    97230 |   13758   12953   377118    29.1 |  1.368 % |
c |     13266 |   41275    97230 |   15133   13055   379004    29.0 |  1.370 % |
c |     13416 |   41129    96900 |   16647   13077   379153    29.0 |  1.640 % |
c |     13641 |   41129    96900 |   18311   13302   386701    29.1 |  1.640 % |
c |     13978 |   41129    96900 |   20143   13639   396611    29.1 |  1.640 % |
c |     14485 |   41129    96900 |   22157   14146   414564    29.3 |  1.640 % |
c |     15244 |   41129    96900 |   24373   14905   439537    29.5 |  1.640 % |
c |     16385 |   41129    96900 |   26810   16046   476862    29.7 |  1.640 % |
c |     18093 |   41129    96900 |   29491   17754   527249    29.7 |  1.640 % |
c |     20655 |   41129    96900 |   32440   20316   585109    28.8 |  1.640 % |
c |     24500 |   41129    96900 |   35684   24161   710776    29.4 |  1.640 % |
c ==============================================================================
c [1mFound solution: 705[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24800 |   41140    96927 |   13713   24461   722932    29.6 |  1.640 % |
c |     24901 |   41140    96927 |   15084   12332   327509    26.6 |  1.647 % |
c |     25052 |   41140    96927 |   16592   12483   331383    26.5 |  1.647 % |
c |     25278 |   41140    96927 |   18252   12709   338176    26.6 |  1.647 % |
c ==============================================================================
c [1mFound solution: 696[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25608 |   41151    96954 |   13717   13039   348212    26.7 |  1.647 % |
c |     25708 |   41151    96954 |   15088   13139   352338    26.8 |  1.654 % |
c |     25858 |   41151    96954 |   16597   13289   355588    26.8 |  1.654 % |
c |     26087 |   41151    96954 |   18257   13518   361018    26.7 |  1.654 % |
c |     26424 |   41151    96954 |   20083   13855   373145    26.9 |  1.654 % |
c |     26930 |   41151    96954 |   22091   14361   389084    27.1 |  1.654 % |
c |     27689 |   41151    96954 |   24300   15120   410924    27.2 |  1.654 % |
c |     28829 |   41151    96954 |   26730   16260   451684    27.8 |  1.654 % |
c |     30537 |   41067    96763 |   29403   17031   469444    27.6 |  1.829 % |
c |     33100 |   41067    96763 |   32343   19594   535964    27.4 |  1.829 % |
c |     36945 |   41067    96763 |   35578   23439   716294    30.6 |  1.829 % |
c |     42712 |   41067    96763 |   39136   29206   911598    31.2 |  1.829 % |
c |     51361 |   41067    96763 |   43049   37855  1220947    32.3 |  1.829 % |
c |     64335 |   41067    96763 |   47354   21853   643793    29.5 |  1.829 % |
c ==============================================================================
c [1mFound solution: 694[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79468 |   41096    96842 |   13698   36986  1181605    31.9 |  1.829 % |
c |     79569 |   41096    96842 |   15067    8705   213360    24.5 |  1.835 % |
c |     79719 |   41096    96842 |   16574    8855   216964    24.5 |  1.835 % |
c |     79945 |   41096    96842 |   18232    9081   223366    24.6 |  1.835 % |
c |     80283 |   41096    96842 |   20055    9419   233185    24.8 |  1.835 % |
c |     80793 |   41096    96842 |   22060    9929   244916    24.7 |  1.835 % |
c |     81553 |   41096    96842 |   24266   10689   267932    25.1 |  1.836 % |
c |     82694 |   41096    96842 |   26693   11830   308711    26.1 |  1.835 % |
c |     84403 |   41096    96842 |   29362   13539   370707    27.4 |  1.835 % |
c |     86970 |   41096    96842 |   32299   16106   488040    30.3 |  1.835 % |
c |     90817 |   41096    96842 |   35529   19953   632804    31.7 |  1.835 % |
c |     96587 |   41096    96842 |   39081   25723   819441    31.9 |  1.835 % |
c |    105237 |   41096    96842 |   42990   34373  1184187    34.5 |  1.835 % |
c |    118211 |   41096    96842 |   47289   19674   633676    32.2 |  1.835 % |
c |    137672 |   41096    96842 |   52018   39135  1370458    35.0 |  1.835 % |
c |    166865 |   41096    96842 |   57219   32960  1077775    32.7 |  1.835 % |
c |    210654 |   40900    96368 |   62941   11068   335573    30.3 |  2.207 % |
c ==============================================================================
c [1mOptimal solution: 694[0m
s OPTIMUM FOUND
v -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 x12 x13 x14 x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 x28 -x29 -x30 x31 x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 x41 -x42 -x43 x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 x74 -x75 x76 -x77 x78 -x79 x80 -x81 x82 -x83 x84 -x85 x86 -x87 x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99
c _______________________________________________________________________________
c 
c restarts              : 76
c conflicts             : 243412         (245 /sec)
c decisions             : 340728         (344 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 991.752 s
c _______________________________________________________________________________
#### 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.87 0.95 0.93 1/54 31237
Raw data (stat): 31237 (runsolver) D 31236 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 481665332 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.89 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 1212 0 0 0 993 3 0 0 25 0 1 0 481665332 6664192 1189 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1627 1189 603 41 0 1586 0
vsize: 6508
[startup+20.0013 s]
Raw data (loadavg): 0.91 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 1899 0 0 0 1990 5 0 0 25 0 1 0 481665332 9539584 1876 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2329 1876 603 41 0 2288 0
vsize: 9316
[startup+30.0023 s]
Raw data (loadavg): 0.92 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2000 0 0 0 2990 5 0 0 25 0 1 0 481665332 9965568 1977 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2433 1977 603 41 0 2392 0
vsize: 9732
[startup+40.0025 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2146 0 0 0 3989 6 0 0 25 0 1 0 481665332 10547200 2123 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2575 2123 603 41 0 2534 0
vsize: 10300
[startup+50.0031 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2272 0 0 0 4989 6 0 0 25 0 1 0 481665332 11079680 2249 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2705 2249 603 41 0 2664 0
vsize: 10820
[startup+60.0032 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2392 0 0 0 5989 7 0 0 25 0 1 0 481665332 11612160 2369 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2835 2369 603 41 0 2794 0
vsize: 11340
[startup+70.0033 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2425 0 0 0 6988 7 0 0 25 0 1 0 481665332 11665408 2402 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2848 2402 603 41 0 2807 0
vsize: 11392
[startup+80.0502 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2453 0 0 0 7992 7 0 0 25 0 1 0 481665332 11808768 2430 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2883 2430 603 41 0 2842 0
vsize: 11532
[startup+90.0498 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2456 0 0 0 8993 7 0 0 25 0 1 0 481665332 11808768 2433 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2883 2433 603 41 0 2842 0
vsize: 11532
[startup+100.051 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2458 0 0 0 9993 7 0 0 25 0 1 0 481665332 11808768 2435 4294967295 134512640 134672761 3221224576 3221223712 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2883 2435 603 41 0 2842 0
vsize: 11532
[startup+110.052 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2543 0 0 0 10993 7 0 0 25 0 1 0 481665332 12218368 2520 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2983 2520 603 41 0 2942 0
vsize: 11932
[startup+120.052 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2648 0 0 0 11993 8 0 0 25 0 1 0 481665332 12619776 2625 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3081 2625 603 41 0 3040 0
vsize: 12324
[startup+130.052 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2764 0 0 0 12992 8 0 0 25 0 1 0 481665332 13160448 2741 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3213 2741 603 41 0 3172 0
vsize: 12852
[startup+140.052 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2867 0 0 0 13992 8 0 0 25 0 1 0 481665332 13557760 2844 4294967295 134512640 134672761 3221224576 3221223712 134560645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3310 2844 603 41 0 3269 0
vsize: 13240
[startup+150.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 2967 0 0 0 14993 8 0 0 25 0 1 0 481665332 14213120 2944 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3470 2944 603 41 0 3429 0
vsize: 13880
[startup+160.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3082 0 0 0 15992 9 0 0 25 0 1 0 481665332 14610432 3059 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3567 3059 603 41 0 3526 0
vsize: 14268
[startup+170.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3208 0 0 0 16992 9 0 0 25 0 1 0 481665332 15147008 3185 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3698 3185 603 41 0 3657 0
vsize: 14792
[startup+180.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3323 0 0 0 17992 9 0 0 25 0 1 0 481665332 15540224 3300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3794 3300 603 41 0 3753 0
vsize: 15176
[startup+190.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3421 0 0 0 18992 10 0 0 25 0 1 0 481665332 15945728 3398 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3893 3398 603 41 0 3852 0
vsize: 15572
[startup+200.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3484 0 0 0 19992 10 0 0 25 0 1 0 481665332 16211968 3461 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3958 3461 603 41 0 3917 0
vsize: 15832
[startup+210.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3491 0 0 0 20992 10 0 0 25 0 1 0 481665332 16351232 3468 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3468 603 41 0 3951 0
vsize: 15968
[startup+220.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3497 0 0 0 21992 10 0 0 25 0 1 0 481665332 16351232 3474 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3474 603 41 0 3951 0
vsize: 15968
[startup+230.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3497 0 0 0 22992 10 0 0 25 0 1 0 481665332 16351232 3474 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3474 603 41 0 3951 0
vsize: 15968
[startup+240.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3498 0 0 0 23992 10 0 0 25 0 1 0 481665332 16351232 3475 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3475 603 41 0 3951 0
vsize: 15968
[startup+250.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3505 0 0 0 24993 10 0 0 25 0 1 0 481665332 16351232 3482 4294967295 134512640 134672761 3221224576 3221223712 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3482 603 41 0 3951 0
vsize: 15968
[startup+260.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3508 0 0 0 25993 10 0 0 25 0 1 0 481665332 16351232 3485 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3485 603 41 0 3951 0
vsize: 15968
[startup+270.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3511 0 0 0 26993 10 0 0 25 0 1 0 481665332 16351232 3488 4294967295 134512640 134672761 3221224576 3221223680 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3488 603 41 0 3951 0
vsize: 15968
[startup+280.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3522 0 0 0 27993 10 0 0 25 0 1 0 481665332 16498688 3499 4294967295 134512640 134672761 3221224576 3221223760 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3499 603 41 0 3987 0
vsize: 16112
[startup+290.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3533 0 0 0 28993 10 0 0 25 0 1 0 481665332 16498688 3510 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3510 603 41 0 3987 0
vsize: 16112
[startup+300.055 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3533 0 0 0 29993 10 0 0 25 0 1 0 481665332 16498688 3510 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3510 603 41 0 3987 0
vsize: 16112
[startup+310.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3533 0 0 0 30993 10 0 0 25 0 1 0 481665332 16498688 3510 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3510 603 41 0 3987 0
vsize: 16112
[startup+320.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3533 0 0 0 31994 10 0 0 25 0 1 0 481665332 16498688 3510 4294967295 134512640 134672761 3221224576 3221223776 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3510 603 41 0 3987 0
vsize: 16112
[startup+330.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3534 0 0 0 32994 10 0 0 25 0 1 0 481665332 16498688 3511 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3511 603 41 0 3987 0
vsize: 16112
[startup+340.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3534 0 0 0 33994 10 0 0 25 0 1 0 481665332 16498688 3511 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3511 603 41 0 3987 0
vsize: 16112
[startup+350.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3538 0 0 0 34994 10 0 0 25 0 1 0 481665332 16498688 3515 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3515 603 41 0 3987 0
vsize: 16112
[startup+360.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3541 0 0 0 35994 10 0 0 25 0 1 0 481665332 16498688 3518 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3518 603 41 0 3987 0
vsize: 16112
[startup+370.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3542 0 0 0 36995 10 0 0 25 0 1 0 481665332 16498688 3519 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3519 603 41 0 3987 0
vsize: 16112
[startup+380.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3542 0 0 0 37995 10 0 0 25 0 1 0 481665332 16498688 3519 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3519 603 41 0 3987 0
vsize: 16112
[startup+390.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3558 0 0 0 38995 10 0 0 25 0 1 0 481665332 16498688 3535 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3535 603 41 0 3987 0
vsize: 16112
[startup+400.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3558 0 0 0 39995 10 0 0 25 0 1 0 481665332 16498688 3535 4294967295 134512640 134672761 3221224576 3221223712 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3535 603 41 0 3987 0
vsize: 16112
[startup+410.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3561 0 0 0 40995 10 0 0 25 0 1 0 481665332 16695296 3538 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4076 3538 603 41 0 4035 0
vsize: 16304
[startup+420.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3661 0 0 0 41995 11 0 0 25 0 1 0 481665332 17141760 3638 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4185 3638 603 41 0 4144 0
vsize: 16740
[startup+430.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3703 0 0 0 42995 11 0 0 25 0 1 0 481665332 17272832 3680 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3680 603 41 0 4176 0
vsize: 16868
[startup+440.064 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3703 0 0 0 43995 11 0 0 25 0 1 0 481665332 17272832 3680 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3680 603 41 0 4176 0
vsize: 16868
[startup+450.064 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3703 0 0 0 44996 11 0 0 25 0 1 0 481665332 17272832 3680 4294967295 134512640 134672761 3221224576 3221223760 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3680 603 41 0 4176 0
vsize: 16868
[startup+460.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3703 0 0 0 45996 11 0 0 25 0 1 0 481665332 17272832 3680 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3680 603 41 0 4176 0
vsize: 16868
[startup+470.065 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3704 0 0 0 46996 11 0 0 25 0 1 0 481665332 17272832 3681 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3681 603 41 0 4176 0
vsize: 16868
[startup+480.065 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3704 0 0 0 47996 11 0 0 25 0 1 0 481665332 17272832 3681 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3681 603 41 0 4176 0
vsize: 16868
[startup+490.065 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3713 0 0 0 48996 11 0 0 25 0 1 0 481665332 17272832 3690 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4217 3690 603 41 0 4176 0
vsize: 16868
[startup+500.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3722 0 0 0 49996 11 0 0 25 0 1 0 481665332 17440768 3699 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4258 3699 603 41 0 4217 0
vsize: 17032
[startup+510.067 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3744 0 0 0 50997 11 0 0 25 0 1 0 481665332 17440768 3721 4294967295 134512640 134672761 3221224576 3221223744 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4258 3721 603 41 0 4217 0
vsize: 17032
[startup+520.067 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3745 0 0 0 51997 11 0 0 25 0 1 0 481665332 17440768 3722 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4258 3722 603 41 0 4217 0
vsize: 17032
[startup+530.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3747 0 0 0 52997 11 0 0 25 0 1 0 481665332 17440768 3724 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4258 3724 603 41 0 4217 0
vsize: 17032
[startup+540.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3768 0 0 0 53997 11 0 0 25 0 1 0 481665332 17637376 3745 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4306 3745 603 41 0 4265 0
vsize: 17224
[startup+550.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3768 0 0 0 54998 11 0 0 25 0 1 0 481665332 17637376 3745 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4306 3745 603 41 0 4265 0
vsize: 17224
[startup+560.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3845 0 0 0 55998 11 0 0 25 0 1 0 481665332 18046976 3822 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4406 3822 603 41 0 4365 0
vsize: 17624
[startup+570.071 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 3919 0 0 0 56998 11 0 0 25 0 1 0 481665332 18309120 3896 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4470 3896 603 41 0 4429 0
vsize: 17880
[startup+580.071 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4010 0 0 0 57997 12 0 0 25 0 1 0 481665332 18571264 3987 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4534 3987 603 41 0 4493 0
vsize: 18136
[startup+590.071 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4111 0 0 0 58997 12 0 0 25 0 1 0 481665332 19095552 4088 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4662 4088 603 41 0 4621 0
vsize: 18648
[startup+600.071 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4188 0 0 0 59997 12 0 0 25 0 1 0 481665332 19357696 4165 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4726 4165 603 41 0 4685 0
vsize: 18904
[startup+610.072 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4188 0 0 0 60997 12 0 0 25 0 1 0 481665332 19357696 4165 4294967295 134512640 134672761 3221224576 3221223712 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4726 4165 603 41 0 4685 0
vsize: 18904
[startup+620.072 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4189 0 0 0 61997 12 0 0 25 0 1 0 481665332 19357696 4166 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4726 4166 603 41 0 4685 0
vsize: 18904
[startup+630.072 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4200 0 0 0 62998 12 0 0 25 0 1 0 481665332 19492864 4177 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4177 603 41 0 4718 0
vsize: 19036
[startup+640.072 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4200 0 0 0 63998 12 0 0 25 0 1 0 481665332 19492864 4177 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4177 603 41 0 4718 0
vsize: 19036
[startup+650.073 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4200 0 0 0 64998 12 0 0 25 0 1 0 481665332 19492864 4177 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4177 603 41 0 4718 0
vsize: 19036
[startup+660.073 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4201 0 0 0 65998 12 0 0 25 0 1 0 481665332 19492864 4178 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4178 603 41 0 4718 0
vsize: 19036
[startup+670.073 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4205 0 0 0 66998 13 0 0 25 0 1 0 481665332 19492864 4182 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4759 4182 603 41 0 4718 0
vsize: 19036
[startup+680.074 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4205 0 0 0 67997 13 0 0 25 0 1 0 481665332 19492864 4182 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4182 603 41 0 4718 0
vsize: 19036
[startup+690.075 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4221 0 0 0 68997 13 0 0 25 0 1 0 481665332 19492864 4198 4294967295 134512640 134672761 3221224576 3221223712 134565121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4198 603 41 0 4718 0
vsize: 19036
[startup+700.076 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4227 0 0 0 69998 13 0 0 25 0 1 0 481665332 19492864 4204 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4204 603 41 0 4718 0
vsize: 19036
[startup+710.077 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4228 0 0 0 70998 13 0 0 25 0 1 0 481665332 19492864 4205 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4205 603 41 0 4718 0
vsize: 19036
[startup+720.077 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4228 0 0 0 71998 13 0 0 25 0 1 0 481665332 19492864 4205 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4205 603 41 0 4718 0
vsize: 19036
[startup+730.077 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4228 0 0 0 72998 13 0 0 25 0 1 0 481665332 19492864 4205 4294967295 134512640 134672761 3221224576 3221223744 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4205 603 41 0 4718 0
vsize: 19036
[startup+740.078 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4246 0 0 0 73998 13 0 0 25 0 1 0 481665332 19755008 4223 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4223 603 41 0 4782 0
vsize: 19292
[startup+750.078 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4247 0 0 0 74999 13 0 0 25 0 1 0 481665332 19755008 4224 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4224 603 41 0 4782 0
vsize: 19292
[startup+760.079 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4306 0 0 0 75999 13 0 0 25 0 1 0 481665332 20017152 4283 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4887 4283 603 41 0 4846 0
vsize: 19548
[startup+770.078 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4419 0 0 0 76998 14 0 0 25 0 1 0 481665332 20414464 4396 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4984 4396 603 41 0 4943 0
vsize: 19936
[startup+780.079 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4529 0 0 0 77998 14 0 0 25 0 1 0 481665332 20807680 4506 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5080 4506 603 41 0 5039 0
vsize: 20320
[startup+790.079 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 78998 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+800.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 79998 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+810.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 80999 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+820.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 81999 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+830.082 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 82999 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+840.083 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 83999 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+850.083 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 84999 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+860.084 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 86000 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223760 134558700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+870.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 86999 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+880.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 87999 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+890.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 89000 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+900.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 90000 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+910.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4575 0 0 0 91000 14 0 0 25 0 1 0 481665332 21069824 4552 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+920.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4577 0 0 0 92000 14 0 0 25 0 1 0 481665332 21069824 4554 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4554 603 41 0 5103 0
vsize: 20576
[startup+930.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4577 0 0 0 93000 14 0 0 25 0 1 0 481665332 21069824 4554 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4554 603 41 0 5103 0
vsize: 20576
[startup+940.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4577 0 0 0 94000 14 0 0 25 0 1 0 481665332 21069824 4554 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4554 603 41 0 5103 0
vsize: 20576
[startup+950.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4586 0 0 0 95001 14 0 0 25 0 1 0 481665332 21069824 4563 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4563 603 41 0 5103 0
vsize: 20576
[startup+960.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4587 0 0 0 96001 14 0 0 25 0 1 0 481665332 21069824 4564 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4564 603 41 0 5103 0
vsize: 20576
[startup+970.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4587 0 0 0 97001 14 0 0 25 0 1 0 481665332 21069824 4564 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4564 603 41 0 5103 0
vsize: 20576
[startup+980.088 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4587 0 0 0 98001 14 0 0 25 0 1 0 481665332 21069824 4564 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4564 603 41 0 5103 0
vsize: 20576
[startup+990.089 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4588 0 0 0 99001 14 0 0 25 0 1 0 481665332 21069824 4565 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4565 603 41 0 5103 0
vsize: 20576
[startup+991.84 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 31237
Raw data (stat): 31237 (minisat+) R 31236 23176 23175 0 -1 0 4588 0 0 0 99001 14 0 0 25 0 1 0 481665332 21069824 4565 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4565 603 41 0 5103 0
vsize: 0

Child status: 30
Real time (s): 991.839
CPU time (s): 991.917
CPU user time (s): 991.757
CPU system time (s): 0.159975
CPU usage (%): 100.008
Max. virtual memory (Kb): 20576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	694
#### END VERIFIER DATA ####