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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl30_40_pb.cnf.cr.opb
MD5SUM6a0000bd3257094a387dbf208b4df8cf
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.073987
Number of variables2400
Total number of constraints140
Number of constraints which are clauses80
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint30
Maximum length of a constraint40

Trace number 6124 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-14 03:27:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4525 boxname=wulflinc20 idbench=13 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6a0000bd3257094a387dbf208b4df8cf  /oldhome/oroussel/tmp/wulflinc20/normalized-chnl30_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc20/normalized-chnl30_40_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc20/normalized-chnl30_40_pb.cnf.cr.opb
IDLAUNCH: 4525
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        876416 kB
Buffers:         35232 kB
Cached:          87396 kB
SwapCached:       2628 kB
Active:          49892 kB
Inactive:        78200 kB
HighTotal:      131008 kB
HighFree:        39900 kB
LowTotal:       903652 kB
LowFree:        836516 kB
SwapTotal:     2097892 kB
SwapFree:      2095264 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24540 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:47:02 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 4525 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20600    59280 |    6866       0        0     nan |  0.000 % |
c |       101 |   20505    58995 |    7552      65     7410   114.0 |  1.126 % |
c |       251 |   20235    58185 |    8307     106     7914    74.7 |  1.895 % |
c |       476 |   19995    57465 |    9138     229    22059    96.3 |  2.593 % |
c |       814 |   19950    57330 |   10052     546    80651   147.7 |  2.707 % |
c |      1320 |   19940    57300 |   11057    1049   208801   199.0 |  2.735 % |
c |      2079 |   19860    57060 |   12163    1756   387394   220.6 |  2.963 % |
c |      3219 |   19705    56595 |   13379    2821   610374   216.4 |  3.405 % |
c |      4927 |   19605    56295 |   14717    4475   920129   205.6 |  3.689 % |
c |      7489 |   19355    55545 |   16189    6909  1507697   218.2 |  4.416 % |
c |     11333 |   18600    53280 |   17808   10439  2130541   204.1 |  6.553 % |
c |     17099 |   17995    51465 |   19589   15926  3305671   207.6 |  8.276 % |
c |     25751 |   16845    48015 |   21548   13887  2702808   194.6 | 11.553 % |
c |     38726 |   16025    45555 |   23703   15333  3156134   205.8 | 13.889 % |
c |     58190 |   14900    42180 |   26073   20896  4514696   216.1 | 17.094 % |
c |     87383 |   14290    40350 |   28680   14528  3138381   216.0 | 18.832 % |
c |    131173 |   13181    37025 |   31549   19874  4411829   222.0 | 21.994 % |
c |    196859 |   12141    33905 |   34703   18380  4740841   257.9 | 24.957 % |
c |    295385 |   11346    31520 |   38174   36440  9260157   254.1 | 27.222 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 2665
Raw data (stat): 2665 (runsolver) R 2664 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481342977 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99964 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 2328 0 0 0 993 5 0 0 25 0 1 0 481342977 11194368 2306 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2733 2306 603 41 0 2692 0
vsize: 10932
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 2998 0 0 0 1991 8 0 0 25 0 1 0 481342977 14024704 2976 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3424 2976 603 41 0 3383 0
vsize: 13696
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 3356 0 0 0 2990 9 0 0 25 0 1 0 481342977 15372288 3334 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3753 3334 603 41 0 3712 0
vsize: 15012
[startup+40.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 3962 0 0 0 3988 10 0 0 25 0 1 0 481342977 17915904 3940 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4374 3940 603 41 0 4333 0
vsize: 17496
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 4559 0 0 0 4987 12 0 0 25 0 1 0 481342977 20332544 4537 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4964 4537 603 41 0 4923 0
vsize: 19856
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 4966 0 0 0 5985 14 0 0 25 0 1 0 481342977 22044672 4944 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5382 4944 603 41 0 5341 0
vsize: 21528
[startup+70.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 5302 0 0 0 6985 15 0 0 25 0 1 0 481342977 23396352 5280 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5712 5280 603 41 0 5671 0
vsize: 22848
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 5856 0 0 0 7982 17 0 0 25 0 1 0 481342977 25686016 5834 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5834 603 41 0 6230 0
vsize: 25084
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 5856 0 0 0 8982 18 0 0 25 0 1 0 481342977 25686016 5834 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5834 603 41 0 6230 0
vsize: 25084
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 5856 0 0 0 9982 18 0 0 25 0 1 0 481342977 25686016 5834 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5834 603 41 0 6230 0
vsize: 25084
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 5856 0 0 0 10982 18 0 0 25 0 1 0 481342977 25686016 5834 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6271 5834 603 41 0 6230 0
vsize: 25084
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 6237 0 0 0 11980 20 0 0 25 0 1 0 481342977 27295744 6215 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6664 6215 603 41 0 6623 0
vsize: 26656
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 6366 0 0 0 12980 21 0 0 25 0 1 0 481342977 27836416 6344 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6796 6344 603 41 0 6755 0
vsize: 27184
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 6366 0 0 0 13979 21 0 0 25 0 1 0 481342977 27836416 6344 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6796 6344 603 41 0 6755 0
vsize: 27184
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 6366 0 0 0 14979 21 0 0 25 0 1 0 481342977 27836416 6344 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6796 6344 603 41 0 6755 0
vsize: 27184
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 6366 0 0 0 15979 22 0 0 25 0 1 0 481342977 27836416 6344 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6796 6344 603 41 0 6755 0
vsize: 27184
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 6851 0 0 0 16977 24 0 0 25 0 1 0 481342977 29720576 6829 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7256 6829 603 41 0 7215 0
vsize: 29024
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 7300 0 0 0 17974 26 0 0 25 0 1 0 481342977 31608832 7278 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7717 7278 603 41 0 7676 0
vsize: 30868
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 7300 0 0 0 18974 27 0 0 25 0 1 0 481342977 31608832 7278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7717 7278 603 41 0 7676 0
vsize: 30868
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 7300 0 0 0 19974 27 0 0 25 0 1 0 481342977 31608832 7278 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7717 7278 603 41 0 7676 0
vsize: 30868
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 7300 0 0 0 20973 28 0 0 25 0 1 0 481342977 31608832 7278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7717 7278 603 41 0 7676 0
vsize: 30868
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 7468 0 0 0 21973 28 0 0 25 0 1 0 481342977 32288768 7446 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7883 7446 603 41 0 7842 0
vsize: 31532
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 7868 0 0 0 22972 29 0 0 25 0 1 0 481342977 33914880 7846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8280 7846 603 41 0 8239 0
vsize: 33120
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8408 0 0 0 23970 31 0 0 25 0 1 0 481342977 36208640 8386 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8840 8386 603 41 0 8799 0
vsize: 35360
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8463 0 0 0 24969 32 0 0 25 0 1 0 481342977 36343808 8441 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8873 8441 603 41 0 8832 0
vsize: 35492
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8463 0 0 0 25969 32 0 0 25 0 1 0 481342977 36343808 8441 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8873 8441 603 41 0 8832 0
vsize: 35492
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8463 0 0 0 26969 33 0 0 25 0 1 0 481342977 36343808 8441 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8873 8441 603 41 0 8832 0
vsize: 35492
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8463 0 0 0 27969 33 0 0 25 0 1 0 481342977 36343808 8441 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8873 8441 603 41 0 8832 0
vsize: 35492
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8463 0 0 0 28968 33 0 0 25 0 1 0 481342977 36343808 8441 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8873 8441 603 41 0 8832 0
vsize: 35492
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8637 0 0 0 29967 35 0 0 25 0 1 0 481342977 37158912 8615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9072 8615 603 41 0 9031 0
vsize: 36288
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8810 0 0 0 30966 35 0 0 25 0 1 0 481342977 37822464 8788 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9234 8788 603 41 0 9193 0
vsize: 36936
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8810 0 0 0 31967 35 0 0 25 0 1 0 481342977 37822464 8788 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9234 8788 603 41 0 9193 0
vsize: 36936
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8810 0 0 0 32966 36 0 0 25 0 1 0 481342977 37822464 8788 4294967295 134512640 134672761 3221224544 3221223616 134553553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9234 8788 603 41 0 9193 0
vsize: 36936
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8810 0 0 0 33966 36 0 0 25 0 1 0 481342977 37822464 8788 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9234 8788 603 41 0 9193 0
vsize: 36936
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 8810 0 0 0 34966 36 0 0 25 0 1 0 481342977 37822464 8788 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9234 8788 603 41 0 9193 0
vsize: 36936
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9114 0 0 0 35965 37 0 0 25 0 1 0 481342977 39034880 9092 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9530 9092 603 41 0 9489 0
vsize: 38120
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 36964 39 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 37964 39 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 38963 39 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 39963 39 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 40963 40 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 41963 40 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 42963 41 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 43962 41 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 44962 41 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9371 0 0 0 45962 41 0 0 25 0 1 0 481342977 40112128 9349 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9793 9349 603 41 0 9752 0
vsize: 39172
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 9891 0 0 0 46960 44 0 0 25 0 1 0 481342977 42270720 9869 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10320 9869 603 41 0 10279 0
vsize: 41280
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10389 0 0 0 47958 46 0 0 25 0 1 0 481342977 44310528 10367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10818 10367 603 41 0 10777 0
vsize: 43272
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10630 0 0 0 48957 47 0 0 25 0 1 0 481342977 45518848 10608 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11113 10608 603 41 0 11072 0
vsize: 44452
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10630 0 0 0 49957 47 0 0 25 0 1 0 481342977 45518848 10608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11113 10608 603 41 0 11072 0
vsize: 44452
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10630 0 0 0 50957 47 0 0 25 0 1 0 481342977 45518848 10608 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11113 10608 603 41 0 11072 0
vsize: 44452
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10630 0 0 0 51957 47 0 0 25 0 1 0 481342977 45518848 10608 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11113 10608 603 41 0 11072 0
vsize: 44452
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10630 0 0 0 52957 47 0 0 25 0 1 0 481342977 45518848 10608 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11113 10608 603 41 0 11072 0
vsize: 44452
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10630 0 0 0 53958 47 0 0 25 0 1 0 481342977 45518848 10608 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11113 10608 603 41 0 11072 0
vsize: 44452
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10631 0 0 0 54958 47 0 0 25 0 1 0 481342977 45518848 10609 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11113 10609 603 41 0 11072 0
vsize: 44452
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 10996 0 0 0 55956 48 0 0 25 0 1 0 481342977 47013888 10974 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11478 10974 603 41 0 11437 0
vsize: 45912
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11023 0 0 0 56957 49 0 0 25 0 1 0 481342977 47013888 11001 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11478 11001 603 41 0 11437 0
vsize: 45912
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11023 0 0 0 57957 49 0 0 25 0 1 0 481342977 47013888 11001 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11478 11001 603 41 0 11437 0
vsize: 45912
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11023 0 0 0 58957 49 0 0 25 0 1 0 481342977 47013888 11001 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11478 11001 603 41 0 11437 0
vsize: 45912
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11023 0 0 0 59957 49 0 0 25 0 1 0 481342977 47013888 11001 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11478 11001 603 41 0 11437 0
vsize: 45912
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11023 0 0 0 60957 49 0 0 25 0 1 0 481342977 47013888 11001 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11478 11001 603 41 0 11437 0
vsize: 45912
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11023 0 0 0 61957 49 0 0 25 0 1 0 481342977 47013888 11001 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11478 11001 603 41 0 11437 0
vsize: 45912
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11300 0 0 0 62957 50 0 0 25 0 1 0 481342977 48230400 11278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11775 11278 603 41 0 11734 0
vsize: 47100
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11620 0 0 0 63956 50 0 0 25 0 1 0 481342977 49438720 11598 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12070 11598 603 41 0 12029 0
vsize: 48280
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11620 0 0 0 64957 50 0 0 25 0 1 0 481342977 49438720 11598 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12070 11598 603 41 0 12029 0
vsize: 48280
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11620 0 0 0 65956 50 0 0 25 0 1 0 481342977 49438720 11598 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12070 11598 603 41 0 12029 0
vsize: 48280
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11621 0 0 0 66956 50 0 0 25 0 1 0 481342977 49438720 11599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12070 11599 603 41 0 12029 0
vsize: 48280
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11621 0 0 0 67956 50 0 0 25 0 1 0 481342977 49438720 11599 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12070 11599 603 41 0 12029 0
vsize: 48280
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 11621 0 0 0 68956 50 0 0 25 0 1 0 481342977 49438720 11599 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12070 11599 603 41 0 12029 0
vsize: 48280
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 12177 0 0 0 69955 51 0 0 25 0 1 0 481342977 51736576 12155 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12631 12155 603 41 0 12590 0
vsize: 50524
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 12935 0 0 0 70954 53 0 0 25 0 1 0 481342977 54996992 12913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12913 603 41 0 13386 0
vsize: 53708
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13067 0 0 0 71954 53 0 0 25 0 1 0 481342977 55537664 13045 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13559 13045 603 41 0 13518 0
vsize: 54236
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13067 0 0 0 72954 53 0 0 25 0 1 0 481342977 55537664 13045 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13559 13045 603 41 0 13518 0
vsize: 54236
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13067 0 0 0 73954 53 0 0 25 0 1 0 481342977 55537664 13045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13559 13045 603 41 0 13518 0
vsize: 54236
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13067 0 0 0 74954 53 0 0 25 0 1 0 481342977 55537664 13045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13559 13045 603 41 0 13518 0
vsize: 54236
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13067 0 0 0 75955 53 0 0 25 0 1 0 481342977 55537664 13045 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13559 13045 603 41 0 13518 0
vsize: 54236
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13067 0 0 0 76955 53 0 0 25 0 1 0 481342977 55537664 13045 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13559 13045 603 41 0 13518 0
vsize: 54236
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13067 0 0 0 77954 53 0 0 25 0 1 0 481342977 55537664 13045 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13559 13045 603 41 0 13518 0
vsize: 54236
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13181 0 0 0 78953 53 0 0 25 0 1 0 481342977 55939072 13159 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 13159 603 41 0 13616 0
vsize: 54628
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13660 0 0 0 79952 55 0 0 25 0 1 0 481342977 57950208 13638 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13638 603 41 0 14107 0
vsize: 56592
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13660 0 0 0 80952 55 0 0 25 0 1 0 481342977 57950208 13638 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13638 603 41 0 14107 0
vsize: 56592
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13660 0 0 0 81953 55 0 0 25 0 1 0 481342977 57950208 13638 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13638 603 41 0 14107 0
vsize: 56592
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13660 0 0 0 82953 55 0 0 25 0 1 0 481342977 57950208 13638 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13638 603 41 0 14107 0
vsize: 56592
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13660 0 0 0 83953 55 0 0 25 0 1 0 481342977 57950208 13638 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13638 603 41 0 14107 0
vsize: 56592
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13660 0 0 0 84953 55 0 0 25 0 1 0 481342977 57950208 13638 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13638 603 41 0 14107 0
vsize: 56592
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 13660 0 0 0 85953 55 0 0 25 0 1 0 481342977 57950208 13638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13638 603 41 0 14107 0
vsize: 56592
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 86953 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 87953 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 88953 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 89953 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 90954 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 91954 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223648 134559899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 92954 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 93954 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14150 0 0 0 94954 55 0 0 25 0 1 0 481342977 59977728 14128 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 14128 603 41 0 14602 0
vsize: 58572
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14359 0 0 0 95953 56 0 0 25 0 1 0 481342977 60788736 14337 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14841 14337 603 41 0 14800 0
vsize: 59364
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14598 0 0 0 96953 56 0 0 25 0 1 0 481342977 61874176 14576 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14576 603 41 0 15065 0
vsize: 60424
[startup+980.022 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14598 0 0 0 97953 56 0 0 25 0 1 0 481342977 61874176 14576 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14576 603 41 0 15065 0
vsize: 60424
[startup+990.021 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14598 0 0 0 98954 56 0 0 25 0 1 0 481342977 61874176 14576 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14576 603 41 0 15065 0
vsize: 60424
[startup+1000.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14598 0 0 0 99954 56 0 0 25 0 1 0 481342977 61874176 14576 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14576 603 41 0 15065 0
vsize: 60424
[startup+1010.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14598 0 0 0 100954 56 0 0 25 0 1 0 481342977 61874176 14576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14576 603 41 0 15065 0
vsize: 60424
[startup+1020.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14598 0 0 0 101954 56 0 0 25 0 1 0 481342977 61874176 14576 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14576 603 41 0 15065 0
vsize: 60424
[startup+1030.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14600 0 0 0 102954 56 0 0 25 0 1 0 481342977 61874176 14578 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14578 603 41 0 15065 0
vsize: 60424
[startup+1040.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14600 0 0 0 103954 56 0 0 25 0 1 0 481342977 61874176 14578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14578 603 41 0 15065 0
vsize: 60424
[startup+1050.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14600 0 0 0 104955 56 0 0 25 0 1 0 481342977 61779968 14578 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14578 603 41 0 15042 0
vsize: 60332
[startup+1060.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14600 0 0 0 105955 56 0 0 25 0 1 0 481342977 61779968 14578 4294967295 134512640 134672761 3221224544 3221223648 134555126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14578 603 41 0 15042 0
vsize: 60332
[startup+1070.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14600 0 0 0 106955 56 0 0 25 0 1 0 481342977 61779968 14578 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14578 603 41 0 15042 0
vsize: 60332
[startup+1080.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14601 0 0 0 107955 56 0 0 25 0 1 0 481342977 61779968 14579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14579 603 41 0 15042 0
vsize: 60332
[startup+1090.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14602 0 0 0 108955 56 0 0 25 0 1 0 481342977 61779968 14580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14580 603 41 0 15042 0
vsize: 60332
[startup+1100.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14602 0 0 0 109956 56 0 0 25 0 1 0 481342977 61779968 14580 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14580 603 41 0 15042 0
vsize: 60332
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14602 0 0 0 110956 56 0 0 25 0 1 0 481342977 61779968 14580 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14580 603 41 0 15042 0
vsize: 60332
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14602 0 0 0 111956 56 0 0 25 0 1 0 481342977 61779968 14580 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14580 603 41 0 15042 0
vsize: 60332
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14602 0 0 0 112956 56 0 0 25 0 1 0 481342977 61779968 14580 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14580 603 41 0 15042 0
vsize: 60332
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14603 0 0 0 113956 56 0 0 25 0 1 0 481342977 61779968 14581 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14581 603 41 0 15042 0
vsize: 60332
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14603 0 0 0 114956 56 0 0 25 0 1 0 481342977 61779968 14581 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14581 603 41 0 15042 0
vsize: 60332
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14604 0 0 0 115956 56 0 0 25 0 1 0 481342977 61779968 14582 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14582 603 41 0 15042 0
vsize: 60332
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14604 0 0 0 116957 56 0 0 25 0 1 0 481342977 61779968 14582 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14582 603 41 0 15042 0
vsize: 60332
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14604 0 0 0 117957 56 0 0 25 0 1 0 481342977 61779968 14582 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14582 603 41 0 15042 0
vsize: 60332
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14604 0 0 0 118957 56 0 0 25 0 1 0 481342977 61779968 14582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14582 603 41 0 15042 0
vsize: 60332
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2665
Raw data (stat): 2665 (minisat+) R 2664 27565 27564 0 -1 0 14604 0 0 0 119957 56 0 0 25 0 1 0 481342977 61779968 14582 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15083 14582 603 41 0 15042 0
vsize: 60332
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 2665
Raw data (stat): 2665 (minisat+) Z 2664 27565 27564 0 -1 12 14606 0 0 0 119957 59 0 0 25 0 1 0 481342977 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: 0
Real time (s): 1200.05
CPU time (s): 1200.18
CPU user time (s): 1199.58
CPU system time (s): 0.596909
CPU usage (%): 100.01
Max. virtual memory (Kb): 60424
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####