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-chnl35_45_pb.cnf.cr.opb
MD5SUM1f5fb3c191c2c77719f10f35e4f5f992
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 46
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.094985
Number of variables3150
Total number of constraints160
Number of constraints which are clauses90
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint45

Trace number 6148 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 03:30:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4528 boxname=wulflinc18 idbench=16 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1f5fb3c191c2c77719f10f35e4f5f992  /oldhome/oroussel/tmp/wulflinc18/normalized-chnl35_45_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc18/normalized-chnl35_45_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc18/normalized-chnl35_45_pb.cnf.cr.opb
IDLAUNCH: 4528
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        857352 kB
Buffers:         35288 kB
Cached:         105764 kB
SwapCached:        320 kB
Active:          55976 kB
Inactive:        88280 kB
HighTotal:      131008 kB
HighFree:        21280 kB
LowTotal:       903652 kB
LowFree:        836072 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27436 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:50:57 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 4528 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
c ---[  69]---> BDD-cost:   87
c ---[  68]---> BDD-cost:   87
c ---[  67]---> BDD-cost:   87
c ---[  66]---> BDD-cost:   87
c ---[  65]---> BDD-cost:   87
c ---[  64]---> BDD-cost:   87
c ---[  63]---> BDD-cost:   87
c ---[  62]---> BDD-cost:   87
c ---[  61]---> BDD-cost:   87
c ---[  60]---> BDD-cost:   87
c ---[  59]---> BDD-cost:   87
c ---[  58]---> BDD-cost:   87
c ---[  57]---> BDD-cost:   87
c ---[  56]---> BDD-cost:   87
c ---[  55]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   87
c ---[  53]---> BDD-cost:   87
c ---[  52]---> BDD-cost:   87
c ---[  51]---> BDD-cost:   87
c ---[  50]---> BDD-cost:   87
c ---[  49]---> BDD-cost:   87
c ---[  48]---> BDD-cost:   87
c ---[  47]---> BDD-cost:   87
c ---[  46]---> BDD-cost:   87
c ---[  45]---> BDD-cost:   87
c ---[  44]---> BDD-cost:   87
c ---[  43]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   87
c ---[  41]---> BDD-cost:   87
c ---[  40]---> BDD-cost:   87
c ---[  39]---> BDD-cost:   87
c ---[  38]---> BDD-cost:   87
c ---[  37]---> BDD-cost:   87
c ---[  36]---> BDD-cost:   87
c ---[  35]---> BDD-cost:   87
c ---[  34]---> BDD-cost:   87
c ---[  33]---> BDD-cost:   87
c ---[  32]---> BDD-cost:   87
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:   87
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:   87
c ---[  27]---> BDD-cost:   87
c ---[  26]---> BDD-cost:   87
c ---[  25]---> BDD-cost:   87
c ---[  24]---> BDD-cost:   87
c ---[  23]---> BDD-cost:   87
c ---[  22]---> BDD-cost:   87
c ---[  21]---> BDD-cost:   87
c ---[  20]---> BDD-cost:   87
c ---[  19]---> BDD-cost:   87
c ---[  18]---> BDD-cost:   87
c ---[  17]---> BDD-cost:   87
c ---[  16]---> BDD-cost:   87
c ---[  15]---> BDD-cost:   87
c ---[  14]---> BDD-cost:   87
c ---[  13]---> BDD-cost:   87
c ---[  12]---> BDD-cost:   87
c ---[  11]---> BDD-cost:   87
c ---[  10]---> BDD-cost:   87
c ---[   9]---> BDD-cost:   87
c ---[   8]---> BDD-cost:   87
c ---[   7]---> BDD-cost:   87
c ---[   6]---> BDD-cost:   87
c ---[   5]---> BDD-cost:   87
c ---[   4]---> BDD-cost:   87
c ---[   3]---> BDD-cost:   87
c ---[   2]---> BDD-cost:   87
c ---[   1]---> BDD-cost:   87
c ---[   0]---> BDD-cost:   87
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27180    78260 |    9060       0        0     nan |  0.000 % |
c |       101 |   26990    77690 |    9966      17       44     2.6 |  1.180 % |
c |       251 |   26680    76760 |   10962      33       79     2.4 |  1.840 % |
c |       476 |   26505    76235 |   12058     202    29636   146.7 |  2.219 % |
c |       813 |   26305    75635 |   13264     456    70688   155.0 |  2.652 % |
c |      1319 |   26045    74855 |   14591     892   147735   165.6 |  3.214 % |
c |      2079 |   26000    74720 |   16050    1632   289268   177.2 |  3.312 % |
c |      3218 |   25905    74435 |   17655    2725   618382   226.9 |  3.517 % |
c |      4930 |   25335    72725 |   19420    4203   979949   233.2 |  4.751 % |
c |      7494 |   24490    70190 |   21363    6450  1470711   228.0 |  6.580 % |
c |     11340 |   23305    66635 |   23499    9781  2324012   237.6 |  9.145 % |
c |     17107 |   21985    62675 |   25849   15034  3671659   244.2 | 12.002 % |
c |     25758 |   20690    58790 |   28434   23201  5877749   253.3 | 14.805 % |
c |     38734 |   18571    52435 |   31277   15028  4082221   271.6 | 19.394 % |
c |     58195 |   17391    48895 |   34405   34153  9326521   273.1 | 21.948 % |
c |     87388 |   16271    45535 |   37845   13504  4773717   353.5 | 24.372 % |
c |    131178 |   15536    43330 |   41630   28507  8980365   315.0 | 25.963 % |
c |    196862 |   14726    40900 |   45793   26404  7709170   292.0 | 27.716 % |
#### 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.85 0.95 0.90 2/55 29100
Raw data (stat): 29100 (runsolver) R 29099 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481359630 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.95 0.90 2/55 29100
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 2020 0 0 0 994 4 0 0 25 0 1 0 481359630 10182656 1997 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2486 1997 603 41 0 2445 0
vsize: 9944
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.96 0.91 2/55 29100
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 2481 0 0 0 1993 5 0 0 25 0 1 0 481359630 12075008 2458 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2948 2458 603 41 0 2907 0
vsize: 11792
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 29100
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 2875 0 0 0 2992 6 0 0 25 0 1 0 481359630 13692928 2852 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3343 2852 603 41 0 3302 0
vsize: 13372
[startup+40.0027 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 29100
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 3266 0 0 0 3991 7 0 0 25 0 1 0 481359630 15327232 3243 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3742 3243 603 41 0 3701 0
vsize: 14968
[startup+50.0037 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 29100
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 3950 0 0 0 4990 8 0 0 25 0 1 0 481359630 18026496 3927 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4401 3927 603 41 0 4360 0
vsize: 17604
[startup+60.0046 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 4248 0 0 0 5990 9 0 0 25 0 1 0 481359630 19238912 4225 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4225 603 41 0 4656 0
vsize: 18788
[startup+70.0055 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 4875 0 0 0 6989 10 0 0 25 0 1 0 481359630 21807104 4852 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5324 4852 603 41 0 5283 0
vsize: 21296
[startup+80.0057 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 5239 0 0 0 7988 11 0 0 25 0 1 0 481359630 23293952 5216 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5687 5216 603 41 0 5646 0
vsize: 22748
[startup+90.0066 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 5556 0 0 0 8987 12 0 0 25 0 1 0 481359630 24641536 5533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6016 5533 603 41 0 5975 0
vsize: 24064
[startup+100.007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 5959 0 0 0 9986 13 0 0 25 0 1 0 481359630 26275840 5936 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 5936 603 41 0 6374 0
vsize: 25660
[startup+110.008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 6322 0 0 0 10986 13 0 0 25 0 1 0 481359630 27758592 6299 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6777 6299 603 41 0 6736 0
vsize: 27108
[startup+120.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 6618 0 0 0 11985 14 0 0 25 0 1 0 481359630 28971008 6595 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7073 6595 603 41 0 7032 0
vsize: 28292
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 7008 0 0 0 12985 15 0 0 25 0 1 0 481359630 30588928 6985 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7468 6985 603 41 0 7427 0
vsize: 29872
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 7625 0 0 0 13983 16 0 0 25 0 1 0 481359630 33153024 7602 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8094 7602 603 41 0 8053 0
vsize: 32376
[startup+150.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 7936 0 0 0 14982 17 0 0 25 0 1 0 481359630 34369536 7913 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8391 7913 603 41 0 8350 0
vsize: 33564
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 8190 0 0 0 15982 18 0 0 25 0 1 0 481359630 35442688 8167 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8653 8167 603 41 0 8612 0
vsize: 34612
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 8245 0 0 0 16982 19 0 0 25 0 1 0 481359630 35713024 8222 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8719 8222 603 41 0 8678 0
vsize: 34876
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 8887 0 0 0 17980 20 0 0 25 0 1 0 481359630 38281216 8864 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9346 8864 603 41 0 9305 0
vsize: 37384
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 9282 0 0 0 18979 21 0 0 25 0 1 0 481359630 39895040 9259 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9740 9259 603 41 0 9699 0
vsize: 38960
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 9364 0 0 0 19979 22 0 0 25 0 1 0 481359630 40169472 9341 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9807 9341 603 41 0 9766 0
vsize: 39228
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 9560 0 0 0 20979 23 0 0 25 0 1 0 481359630 40980480 9537 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10005 9537 603 41 0 9964 0
vsize: 40020
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 9792 0 0 0 21978 23 0 0 25 0 1 0 481359630 41926656 9769 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10236 9769 603 41 0 10195 0
vsize: 40944
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 22976 25 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 23976 25 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223648 134559838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 24976 25 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 25976 26 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 26976 26 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 27976 26 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 28976 26 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 29976 26 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 30976 26 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 31977 26 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10600 0 0 0 32977 26 0 0 25 0 1 0 481359630 45297664 10577 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10577 603 41 0 11018 0
vsize: 44236
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 10798 0 0 0 33976 27 0 0 25 0 1 0 481359630 46100480 10775 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11255 10775 603 41 0 11214 0
vsize: 45020
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29102
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 11399 0 0 0 34974 29 0 0 25 0 1 0 481359630 48533504 11376 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11849 11376 603 41 0 11808 0
vsize: 47396
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 11794 0 0 0 35973 30 0 0 25 0 1 0 481359630 50282496 11771 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11771 603 41 0 12235 0
vsize: 49104
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 11970 0 0 0 36973 31 0 0 25 0 1 0 481359630 50958336 11947 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12441 11947 603 41 0 12400 0
vsize: 49764
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 11980 0 0 0 37973 31 0 0 25 0 1 0 481359630 51093504 11957 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12474 11957 603 41 0 12433 0
vsize: 49896
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12633 0 0 0 38971 33 0 0 25 0 1 0 481359630 53653504 12610 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13099 12610 603 41 0 13058 0
vsize: 52396
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12760 0 0 0 39972 33 0 0 25 0 1 0 481359630 54190080 12737 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13230 12737 603 41 0 13189 0
vsize: 52920
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12760 0 0 0 40972 33 0 0 25 0 1 0 481359630 54190080 12737 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13230 12737 603 41 0 13189 0
vsize: 52920
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12760 0 0 0 41972 33 0 0 25 0 1 0 481359630 54190080 12737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13230 12737 603 41 0 13189 0
vsize: 52920
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12760 0 0 0 42972 33 0 0 25 0 1 0 481359630 54190080 12737 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13230 12737 603 41 0 13189 0
vsize: 52920
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12760 0 0 0 43972 33 0 0 25 0 1 0 481359630 54190080 12737 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13230 12737 603 41 0 13189 0
vsize: 52920
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12760 0 0 0 44972 33 0 0 25 0 1 0 481359630 54190080 12737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13230 12737 603 41 0 13189 0
vsize: 52920
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12760 0 0 0 45973 33 0 0 25 0 1 0 481359630 54190080 12737 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13230 12737 603 41 0 13189 0
vsize: 52920
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 12760 0 0 0 46973 33 0 0 25 0 1 0 481359630 54190080 12737 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13230 12737 603 41 0 13189 0
vsize: 52920
[startup+480.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 13285 0 0 0 47971 35 0 0 25 0 1 0 481359630 56348672 13262 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13757 13262 603 41 0 13716 0
vsize: 55028
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14019 0 0 0 48970 37 0 0 25 0 1 0 481359630 59453440 13996 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14515 13996 603 41 0 14474 0
vsize: 58060
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 49968 38 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223648 134560316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 50968 38 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 51968 38 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 52968 38 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 53968 39 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 54968 39 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 55969 39 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 56969 39 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 57969 39 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 58969 39 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+600.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 14561 0 0 0 59969 39 0 0 25 0 1 0 481359630 61599744 14538 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14538 603 41 0 14998 0
vsize: 60156
[startup+610.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 15540 0 0 0 60968 41 0 0 25 0 1 0 481359630 65646592 15517 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16027 15517 603 41 0 15986 0
vsize: 64108
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16036 0 0 0 61967 42 0 0 25 0 1 0 481359630 67690496 16013 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16526 16013 603 41 0 16485 0
vsize: 66104
[startup+630.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16582 0 0 0 62965 43 0 0 25 0 1 0 481359630 69967872 16559 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16559 603 41 0 17041 0
vsize: 68328
[startup+640.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16582 0 0 0 63966 43 0 0 25 0 1 0 481359630 69967872 16559 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16559 603 41 0 17041 0
vsize: 68328
[startup+650.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29104
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16582 0 0 0 64966 43 0 0 25 0 1 0 481359630 69967872 16559 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16559 603 41 0 17041 0
vsize: 68328
[startup+660.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16582 0 0 0 65966 43 0 0 25 0 1 0 481359630 69967872 16559 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16559 603 41 0 17041 0
vsize: 68328
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16582 0 0 0 66966 43 0 0 25 0 1 0 481359630 69967872 16559 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16559 603 41 0 17041 0
vsize: 68328
[startup+680.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16582 0 0 0 67966 43 0 0 25 0 1 0 481359630 69967872 16559 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17082 16559 603 41 0 17041 0
vsize: 68328
[startup+690.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16582 0 0 0 68966 44 0 0 25 0 1 0 481359630 69967872 16559 4294967295 134512640 134672761 3221224544 3221223648 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16559 603 41 0 17041 0
vsize: 68328
[startup+700.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16582 0 0 0 69966 44 0 0 25 0 1 0 481359630 69967872 16559 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16559 603 41 0 17041 0
vsize: 68328
[startup+710.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16583 0 0 0 70966 44 0 0 25 0 1 0 481359630 69967872 16560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16560 603 41 0 17041 0
vsize: 68328
[startup+720.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16583 0 0 0 71966 44 0 0 25 0 1 0 481359630 69967872 16560 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16560 603 41 0 17041 0
vsize: 68328
[startup+730.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16583 0 0 0 72966 44 0 0 25 0 1 0 481359630 69967872 16560 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16560 603 41 0 17041 0
vsize: 68328
[startup+740.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 16583 0 0 0 73966 44 0 0 25 0 1 0 481359630 69967872 16560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16560 603 41 0 17041 0
vsize: 68328
[startup+750.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 17042 0 0 0 74965 46 0 0 25 0 1 0 481359630 71864320 17019 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17545 17019 603 41 0 17504 0
vsize: 70180
[startup+760.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 17812 0 0 0 75962 48 0 0 25 0 1 0 481359630 74973184 17789 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18304 17789 603 41 0 18263 0
vsize: 73216
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18478 0 0 0 76960 50 0 0 25 0 1 0 481359630 77787136 18455 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18991 18455 603 41 0 18950 0
vsize: 75964
[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 77960 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 78960 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 79960 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 80960 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+820.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 81960 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+830.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 82961 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+840.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 83961 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+850.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 84961 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+860.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18686 0 0 0 85961 51 0 0 25 0 1 0 481359630 78585856 18663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18663 603 41 0 19145 0
vsize: 76744
[startup+870.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 86961 51 0 0 25 0 1 0 481359630 78585856 18664 4294967295 134512640 134672761 3221224544 3221223776 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18664 603 41 0 19145 0
vsize: 76744
[startup+880.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 87961 51 0 0 25 0 1 0 481359630 78585856 18664 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 18664 603 41 0 19145 0
vsize: 76744
[startup+890.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 88961 51 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223716 134559643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+900.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 89961 51 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 90961 51 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 91962 51 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+930.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 92961 52 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 93961 52 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223728 134559422 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29106
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 94961 52 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 95961 52 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+970.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 96962 52 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+980.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 97962 52 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+990.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 98962 52 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18687 0 0 0 99962 52 0 0 25 0 1 0 481359630 78487552 18661 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18661 603 41 0 19121 0
vsize: 76648
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 18688 0 0 0 100962 52 0 0 25 0 1 0 481359630 78487552 18662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19162 18662 603 41 0 19121 0
vsize: 76648
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 19034 0 0 0 101961 53 0 0 25 0 1 0 481359630 79958016 19008 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19521 19008 603 41 0 19480 0
vsize: 78084
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 19727 0 0 0 102960 55 0 0 25 0 1 0 481359630 82796544 19701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20214 19701 603 41 0 20173 0
vsize: 80856
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20257 0 0 0 103959 56 0 0 25 0 1 0 481359630 84946944 20231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20739 20231 603 41 0 20698 0
vsize: 82956
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 104958 57 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 105958 57 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223716 134559060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 106958 57 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 107958 57 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 108959 57 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 109959 57 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 110959 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 111959 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 112959 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 113959 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 114959 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 115959 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 116959 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 117959 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 118960 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29108
Raw data (stat): 29100 (minisat+) R 29099 20024 20023 0 -1 0 20528 0 0 0 119960 58 0 0 25 0 1 0 481359630 86151168 20502 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21033 20502 603 41 0 20992 0
vsize: 84132
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 29108
Raw data (stat): 29100 (minisat+) Z 29099 20024 20023 0 -1 12 20530 0 0 0 119960 62 0 0 25 0 1 0 481359630 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.09
CPU time (s): 1200.23
CPU user time (s): 1199.6
CPU system time (s): 0.624905
CPU usage (%): 100.012
Max. virtual memory (Kb): 84132
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####