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-chnl50_51_pb.cnf.cr.opb
MD5SUM00bdc6bb9bafd4b1100d8bfa4f886626
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 52
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.156976
Number of variables5100
Total number of constraints202
Number of constraints which are clauses102
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint51

Trace number 6154 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 03:32:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4532 boxname=wulflinc9 idbench=20 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00bdc6bb9bafd4b1100d8bfa4f886626  /oldhome/oroussel/tmp/wulflinc9/normalized-chnl50_51_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc9/normalized-chnl50_51_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc9/normalized-chnl50_51_pb.cnf.cr.opb
IDLAUNCH: 4532
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        892608 kB
Buffers:         36332 kB
Cached:          85640 kB
SwapCached:        564 kB
Active:          54304 kB
Inactive:        71072 kB
HighTotal:      131008 kB
HighFree:        41496 kB
LowTotal:       903652 kB
LowFree:        851112 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11128 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:52:04 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 4532 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 202 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................
c ---[  99]---> BDD-cost:   99
c ---[  98]---> BDD-cost:   99
c ---[  97]---> BDD-cost:   99
c ---[  96]---> BDD-cost:   99
c ---[  95]---> BDD-cost:   99
c ---[  94]---> BDD-cost:   99
c ---[  93]---> BDD-cost:   99
c ---[  92]---> BDD-cost:   99
c ---[  91]---> BDD-cost:   99
c ---[  90]---> BDD-cost:   99
c ---[  89]---> BDD-cost:   99
c ---[  88]---> BDD-cost:   99
c ---[  87]---> BDD-cost:   99
c ---[  86]---> BDD-cost:   99
c ---[  85]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   99
c ---[  83]---> BDD-cost:   99
c ---[  82]---> BDD-cost:   99
c ---[  81]---> BDD-cost:   99
c ---[  80]---> BDD-cost:   99
c ---[  79]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   99
c ---[  77]---> BDD-cost:   99
c ---[  76]---> BDD-cost:   99
c ---[  75]---> BDD-cost:   99
c ---[  74]---> BDD-cost:   99
c ---[  73]---> BDD-cost:   99
c ---[  72]---> BDD-cost:   99
c ---[  71]---> BDD-cost:   99
c ---[  70]---> BDD-cost:   99
c ---[  69]---> BDD-cost:   99
c ---[  68]---> BDD-cost:   99
c ---[  67]---> BDD-cost:   99
c ---[  66]---> BDD-cost:   99
c ---[  65]---> BDD-cost:   99
c ---[  64]---> BDD-cost:   99
c ---[  63]---> BDD-cost:   99
c ---[  62]---> BDD-cost:   99
c ---[  61]---> BDD-cost:   99
c ---[  60]---> BDD-cost:   99
c ---[  59]---> BDD-cost:   99
c ---[  58]---> BDD-cost:   99
c ---[  57]---> BDD-cost:   99
c ---[  56]---> BDD-cost:   99
c ---[  55]---> BDD-cost:   99
c ---[  54]---> BDD-cost:   99
c ---[  53]---> BDD-cost:   99
c ---[  52]---> BDD-cost:   99
c ---[  51]---> BDD-cost:   99
c ---[  50]---> BDD-cost:   99
c ---[  49]---> BDD-cost:   99
c ---[  48]---> BDD-cost:   99
c ---[  47]---> BDD-cost:   99
c ---[  46]---> BDD-cost:   99
c ---[  45]---> BDD-cost:   99
c ---[  44]---> BDD-cost:   99
c ---[  43]---> BDD-cost:   99
c ---[  42]---> BDD-cost:   99
c ---[  41]---> BDD-cost:   99
c ---[  40]---> BDD-cost:   99
c ---[  39]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   99
c ---[  37]---> BDD-cost:   99
c ---[  36]---> BDD-cost:   99
c ---[  35]---> BDD-cost:   99
c ---[  34]---> BDD-cost:   99
c ---[  33]---> BDD-cost:   99
c ---[  32]---> BDD-cost:   99
c ---[  31]---> BDD-cost:   99
c ---[  30]---> BDD-cost:   99
c ---[  29]---> BDD-cost:   99
c ---[  28]---> BDD-cost:   99
c ---[  27]---> BDD-cost:   99
c ---[  26]---> BDD-cost:   99
c ---[  25]---> BDD-cost:   99
c ---[  24]---> BDD-cost:   99
c ---[  23]---> BDD-cost:   99
c ---[  22]---> BDD-cost:   99
c ---[  21]---> BDD-cost:   99
c ---[  20]---> BDD-cost:   99
c ---[  19]---> BDD-cost:   99
c ---[  18]---> BDD-cost:   99
c ---[  17]---> BDD-cost:   99
c ---[  16]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   99
c ---[  14]---> BDD-cost:   99
c ---[  13]---> BDD-cost:   99
c ---[  12]---> BDD-cost:   99
c ---[  11]---> BDD-cost:   99
c ---[  10]---> BDD-cost:   99
c ---[   9]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   99
c ---[   7]---> BDD-cost:   99
c ---[   6]---> BDD-cost:   99
c ---[   5]---> BDD-cost:   99
c ---[   4]---> BDD-cost:   99
c ---[   3]---> BDD-cost:   99
c ---[   2]---> BDD-cost:   99
c ---[   1]---> BDD-cost:   99
c ---[   0]---> BDD-cost:   99
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   44202   127400 |   14734       0        0     nan |  0.000 % |
c |       101 |   43972   126710 |   16207       6       16     2.7 |  0.973 % |
c |       251 |   43717   125945 |   17828      38      122     3.2 |  1.320 % |
c |       476 |   43157   124265 |   19610      51      153     3.0 |  2.067 % |
c |       813 |   42392   121970 |   21572     111      387     3.5 |  3.087 % |
c |      1320 |   41193   118375 |   23729     197     1001     5.1 |  4.680 % |
c |      2081 |   40693   116875 |   26102     783   154322   197.1 |  5.347 % |
c |      3225 |   39403   113005 |   28712    1496   369891   247.3 |  7.067 % |
c |      4934 |   38078   109030 |   31583    2794   793589   284.0 |  8.833 % |
c |      7499 |   35083   100045 |   34742    4410  1318582   299.0 | 12.827 % |
c |     11343 |   32993    93775 |   38216    7610  2380425   312.8 | 15.620 % |
c |     17110 |   29244    82530 |   42037   12207  3858913   316.1 | 20.613 % |
c |     25761 |   27689    77865 |   46241   20412  7306366   357.9 | 22.687 % |
c |     38736 |   26160    73280 |   50865   32921 13101749   398.0 | 24.727 % |
c |     58198 |   25412    71040 |   55952   52162 22671361   434.6 | 25.727 % |
c |     87391 |   24100    67110 |   61547   33624 15319824   455.6 | 27.480 % |
c |    131182 |   23421    65075 |   67702   23946 11598326   484.4 | 28.387 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 3524
Raw data (stat): 3524 (runsolver) R 3523 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423152683 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+10.0008 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 1512 0 0 0 994 4 0 0 25 0 1 0 423152683 7974912 1487 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1947 1487 603 41 0 1906 0
vsize: 7788
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 1925 0 0 0 1993 5 0 0 25 0 1 0 423152683 9596928 1900 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2343 1900 603 41 0 2302 0
vsize: 9372
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 2387 0 0 0 2992 6 0 0 25 0 1 0 423152683 11489280 2362 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2805 2362 603 41 0 2764 0
vsize: 11220
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 2583 0 0 0 3991 6 0 0 25 0 1 0 423152683 12300288 2558 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3003 2558 603 41 0 2962 0
vsize: 12012
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 2696 0 0 0 4991 7 0 0 25 0 1 0 423152683 12840960 2671 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3135 2671 603 41 0 3094 0
vsize: 12540
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 2922 0 0 0 5991 7 0 0 25 0 1 0 423152683 13787136 2897 4294967295 134512640 134672761 3221224544 3221223696 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3366 2897 603 41 0 3325 0
vsize: 13464
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 3451 0 0 0 6990 8 0 0 25 0 1 0 423152683 15949824 3426 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3894 3426 603 41 0 3853 0
vsize: 15576
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 3815 0 0 0 7989 9 0 0 25 0 1 0 423152683 17432576 3790 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4256 3791 603 41 0 4215 0
vsize: 17024
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 4108 0 0 0 8989 10 0 0 25 0 1 0 423152683 18644992 4083 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 4083 603 41 0 4511 0
vsize: 18208
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 4178 0 0 0 9989 10 0 0 25 0 1 0 423152683 18915328 4153 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4618 4153 603 41 0 4577 0
vsize: 18472
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 4255 0 0 0 10989 10 0 0 25 0 1 0 423152683 19177472 4230 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4682 4230 603 41 0 4641 0
vsize: 18728
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 4509 0 0 0 11988 11 0 0 25 0 1 0 423152683 20312064 4484 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4959 4484 603 41 0 4918 0
vsize: 19836
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 5044 0 0 0 12987 12 0 0 25 0 1 0 423152683 22474752 5019 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5487 5019 603 41 0 5446 0
vsize: 21948
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 5046 0 0 0 13987 12 0 0 25 0 1 0 423152683 22474752 5021 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5487 5021 603 41 0 5446 0
vsize: 21948
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 5186 0 0 0 14987 13 0 0 25 0 1 0 423152683 23015424 5161 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5619 5161 603 41 0 5578 0
vsize: 22476
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 5273 0 0 0 15987 13 0 0 25 0 1 0 423152683 23420928 5248 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5718 5248 603 41 0 5677 0
vsize: 22872
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 5374 0 0 0 16987 13 0 0 25 0 1 0 423152683 23826432 5349 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5817 5349 603 41 0 5776 0
vsize: 23268
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 5476 0 0 0 17986 14 0 0 25 0 1 0 423152683 24231936 5451 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5916 5451 603 41 0 5875 0
vsize: 23664
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 5691 0 0 0 18986 15 0 0 25 0 1 0 423152683 25042944 5666 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6114 5666 603 41 0 6073 0
vsize: 24456
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 5881 0 0 0 19986 15 0 0 25 0 1 0 423152683 25853952 5856 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6312 5856 603 41 0 6271 0
vsize: 25248
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 6193 0 0 0 20985 16 0 0 25 0 1 0 423152683 27070464 6168 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6609 6168 603 41 0 6568 0
vsize: 26436
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 6400 0 0 0 21985 16 0 0 25 0 1 0 423152683 28016640 6375 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6840 6375 603 41 0 6799 0
vsize: 27360
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 7172 0 0 0 22984 17 0 0 25 0 1 0 423152683 31121408 7147 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7598 7147 603 41 0 7557 0
vsize: 30392
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 7726 0 0 0 23982 19 0 0 25 0 1 0 423152683 33419264 7701 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8159 7701 603 41 0 8118 0
vsize: 32636
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 8181 0 0 0 24981 20 0 0 25 0 1 0 423152683 35307520 8156 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8620 8156 603 41 0 8579 0
vsize: 34480
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 8360 0 0 0 25981 21 0 0 25 0 1 0 423152683 36118528 8335 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8818 8335 603 41 0 8777 0
vsize: 35272
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 9338 0 0 0 26980 22 0 0 25 0 1 0 423152683 40034304 9313 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9774 9314 603 41 0 9733 0
vsize: 39096
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 9595 0 0 0 27979 23 0 0 25 0 1 0 423152683 41111552 9570 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10037 9570 603 41 0 9996 0
vsize: 40148
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 9607 0 0 0 28979 23 0 0 25 0 1 0 423152683 41111552 9582 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10037 9582 603 41 0 9996 0
vsize: 40148
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 10626 0 0 0 29977 26 0 0 25 0 1 0 423152683 45297664 10601 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11059 10601 603 41 0 11018 0
vsize: 44236
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 11343 0 0 0 30976 27 0 0 25 0 1 0 423152683 48271360 11318 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11785 11318 603 41 0 11744 0
vsize: 47140
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 12166 0 0 0 31974 29 0 0 25 0 1 0 423152683 51642368 12141 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12608 12141 603 41 0 12567 0
vsize: 50432
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 13223 0 0 0 32972 31 0 0 25 0 1 0 423152683 55959552 13198 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13662 13198 603 41 0 13621 0
vsize: 54648
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 13916 0 0 0 33971 33 0 0 25 0 1 0 423152683 58789888 13891 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14353 13891 603 41 0 14312 0
vsize: 57412
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 13916 0 0 0 34971 33 0 0 25 0 1 0 423152683 58789888 13891 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14353 13891 603 41 0 14312 0
vsize: 57412
[startup+360.016 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 13937 0 0 0 35971 33 0 0 25 0 1 0 423152683 58789888 13912 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14353 13912 603 41 0 14312 0
vsize: 57412
[startup+370.015 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 14071 0 0 0 36971 33 0 0 25 0 1 0 423152683 59334656 14046 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14486 14046 603 41 0 14445 0
vsize: 57944
[startup+380.016 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 14226 0 0 0 37971 34 0 0 25 0 1 0 423152683 60010496 14201 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14651 14201 603 41 0 14610 0
vsize: 58604
[startup+390.016 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 14279 0 0 0 38971 34 0 0 25 0 1 0 423152683 60280832 14254 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14717 14254 603 41 0 14676 0
vsize: 58868
[startup+400.018 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 14645 0 0 0 39971 34 0 0 25 0 1 0 423152683 61767680 14620 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15080 14620 603 41 0 15039 0
vsize: 60320
[startup+410.018 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 15035 0 0 0 40970 35 0 0 25 0 1 0 423152683 63389696 15010 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15476 15010 603 41 0 15435 0
vsize: 61904
[startup+420.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 15326 0 0 0 41970 36 0 0 25 0 1 0 423152683 64471040 15301 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15740 15301 603 41 0 15699 0
vsize: 62960
[startup+430.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 15866 0 0 0 42968 37 0 0 25 0 1 0 423152683 66891776 15841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16331 15841 603 41 0 16290 0
vsize: 65324
[startup+440.019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 16370 0 0 0 43967 38 0 0 25 0 1 0 423152683 68919296 16345 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16826 16345 603 41 0 16785 0
vsize: 67304
[startup+450.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 16486 0 0 0 44966 39 0 0 25 0 1 0 423152683 69455872 16461 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16957 16461 603 41 0 16916 0
vsize: 67828
[startup+460.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 17012 0 0 0 45966 40 0 0 25 0 1 0 423152683 71618560 16987 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17485 16987 603 41 0 17444 0
vsize: 69940
[startup+470.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 17314 0 0 0 46965 40 0 0 25 0 1 0 423152683 72826880 17289 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17780 17289 603 41 0 17739 0
vsize: 71120
[startup+480.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 17319 0 0 0 47966 40 0 0 25 0 1 0 423152683 72826880 17294 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17780 17294 603 41 0 17739 0
vsize: 71120
[startup+490.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 17321 0 0 0 48966 40 0 0 25 0 1 0 423152683 72826880 17296 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17780 17296 603 41 0 17739 0
vsize: 71120
[startup+500.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 18373 0 0 0 49964 42 0 0 25 0 1 0 423152683 77127680 18348 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18830 18348 603 41 0 18789 0
vsize: 75320
[startup+510.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 19575 0 0 0 50961 45 0 0 25 0 1 0 423152683 81989632 19550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20017 19550 603 41 0 19976 0
vsize: 80068
[startup+520.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 20560 0 0 0 51960 47 0 0 25 0 1 0 423152683 86052864 20535 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21009 20535 603 41 0 20968 0
vsize: 84036
[startup+530.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 21209 0 0 0 52958 48 0 0 25 0 1 0 423152683 88752128 21184 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21668 21184 603 41 0 21627 0
vsize: 86672
[startup+540.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 21504 0 0 0 53958 49 0 0 25 0 1 0 423152683 89968640 21479 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21965 21479 603 41 0 21924 0
vsize: 87860
[startup+550.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 22623 0 0 0 54955 52 0 0 25 0 1 0 423152683 94552064 22598 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23084 22598 603 41 0 23043 0
vsize: 92336
[startup+560.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 23817 0 0 0 55952 55 0 0 25 0 1 0 423152683 99414016 23792 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24271 23792 603 41 0 24230 0
vsize: 97084
[startup+570.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 24873 0 0 0 56950 57 0 0 25 0 1 0 423152683 103739392 24848 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25327 24848 603 41 0 25286 0
vsize: 101308
[startup+580.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 25510 0 0 0 57949 59 0 0 25 0 1 0 423152683 106295296 25485 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25951 25485 603 41 0 25910 0
vsize: 103804
[startup+590.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 25578 0 0 0 58949 59 0 0 25 0 1 0 423152683 106565632 25553 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26017 25553 603 41 0 25976 0
vsize: 104068
[startup+600.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 25888 0 0 0 59948 59 0 0 25 0 1 0 423152683 107913216 25863 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26346 25863 603 41 0 26305 0
vsize: 105384
[startup+610.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 26006 0 0 0 60947 60 0 0 25 0 1 0 423152683 108314624 25981 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26444 25981 603 41 0 26403 0
vsize: 105776
[startup+620.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 26466 0 0 0 61946 61 0 0 25 0 1 0 423152683 110202880 26441 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26905 26441 603 41 0 26864 0
vsize: 107620
[startup+630.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 27417 0 0 0 62943 64 0 0 25 0 1 0 423152683 114122752 27392 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27862 27392 603 41 0 27821 0
vsize: 111448
[startup+640.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 27973 0 0 0 63942 65 0 0 25 0 1 0 423152683 116420608 27948 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28423 27948 603 41 0 28382 0
vsize: 113692
[startup+650.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 28088 0 0 0 64941 66 0 0 25 0 1 0 423152683 116822016 28063 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28521 28063 603 41 0 28480 0
vsize: 114084
[startup+660.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29003 0 0 0 65938 69 0 0 25 0 1 0 423152683 120594432 28978 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29442 28978 603 41 0 29401 0
vsize: 117768
[startup+670.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29095 0 0 0 66937 70 0 0 25 0 1 0 423152683 120995840 29070 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29540 29070 603 41 0 29499 0
vsize: 118160
[startup+680.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29473 0 0 0 67936 71 0 0 25 0 1 0 423152683 122613760 29448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29935 29448 603 41 0 29894 0
vsize: 119740
[startup+690.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 68935 72 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+700.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 69935 72 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+710.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 70935 73 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+720.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 71934 73 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+730.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 72934 73 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+740.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 73934 74 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+750.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 74934 74 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+760.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 75934 74 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+770.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 76934 74 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+780.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 77933 75 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+790.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 78933 75 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+800.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 79933 75 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+810.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 80933 75 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+820.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 81933 75 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+830.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 82932 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+840.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 83932 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+850.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 84933 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+860.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 85933 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+870.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 86933 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134559818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+880.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 87933 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+890.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 88933 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+900.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 89934 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+910.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 90934 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+920.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 91934 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+930.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 92934 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+940.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 93934 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+950.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 94934 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+960.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 29995 0 0 0 95935 76 0 0 25 0 1 0 423152683 124641280 29970 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30430 29970 603 41 0 30389 0
vsize: 121720
[startup+970.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 30381 0 0 0 96934 77 0 0 25 0 1 0 423152683 126255104 30356 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30824 30356 603 41 0 30783 0
vsize: 123296
[startup+980.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 31216 0 0 0 97932 78 0 0 25 0 1 0 423152683 129761280 31191 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31680 31191 603 41 0 31639 0
vsize: 126720
[startup+990.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 32499 0 0 0 98929 81 0 0 25 0 1 0 423152683 135024640 32474 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32965 32474 603 41 0 32924 0
vsize: 131860
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 33542 0 0 0 99927 84 0 0 25 0 1 0 423152683 139206656 33517 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33986 33517 603 41 0 33945 0
vsize: 135944
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 33884 0 0 0 100926 85 0 0 25 0 1 0 423152683 140693504 33859 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34349 33859 603 41 0 34308 0
vsize: 137396
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 34053 0 0 0 101926 85 0 0 25 0 1 0 423152683 141373440 34028 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34515 34028 603 41 0 34474 0
vsize: 138060
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 34727 0 0 0 102925 86 0 0 25 0 1 0 423152683 144052224 34702 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35169 34702 603 41 0 35128 0
vsize: 140676
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 35446 0 0 0 103923 89 0 0 25 0 1 0 423152683 147030016 35421 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35896 35421 603 41 0 35855 0
vsize: 143584
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36218 0 0 0 104921 90 0 0 25 0 1 0 423152683 150401024 36193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36719 36193 603 41 0 36678 0
vsize: 146876
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 105922 90 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 106922 90 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 107922 90 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223716 134556664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 108922 90 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 109922 90 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 110922 90 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 111922 90 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 112922 90 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 113922 91 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 114922 91 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 115923 91 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 116923 91 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 117923 91 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 118923 91 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3524
Raw data (stat): 3524 (minisat+) R 3523 30854 30853 0 -1 0 36229 0 0 0 119923 91 0 0 25 0 1 0 423152683 150536192 36204 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36752 36204 603 41 0 36711 0
vsize: 147008
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 3524
Raw data (stat): 3524 (minisat+) Z 3523 30854 30853 0 -1 12 36231 0 0 0 119923 97 0 0 25 0 1 0 423152683 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.1
CPU time (s): 1200.22
CPU user time (s): 1199.24
CPU system time (s): 0.975851
CPU usage (%): 100.009
Max. virtual memory (Kb): 147008
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####