PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga45_43_sat_pb.cnf.cr.opb
MD5SUM	f711bed5ebfe5c735a8c12d953afb97c
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
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 numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	9.61454
Number of variables	2903
Total number of constraints	2066
Number of constraints which are clauses	1978
Number of constraints which are cardinality constraints (but not clauses)	88
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	22
Maximum length of a constraint	45
Trace number 5782

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 01:45:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4191 boxname=wulflinc13 idbench=55 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f711bed5ebfe5c735a8c12d953afb97c  /oldhome/oroussel/tmp/wulflinc13/normalized-fpga45_43_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc13/normalized-fpga45_43_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc13/normalized-fpga45_43_sat_pb.cnf.cr.opb
IDLAUNCH: 4191
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        894020 kB
Buffers:         35260 kB
Cached:          85388 kB
SwapCached:        392 kB
Active:          54748 kB
Inactive:        69156 kB
HighTotal:      131008 kB
HighFree:        41720 kB
LowTotal:       903652 kB
LowFree:        852300 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11232 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:05:21 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 4191 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2066 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  87]---> BDD-cost:   83
c ---[  86]---> BDD-cost:   83
c ---[  85]---> BDD-cost:   83
c ---[  84]---> BDD-cost:   83
c ---[  83]---> BDD-cost:   83
c ---[  82]---> BDD-cost:   83
c ---[  81]---> BDD-cost:   83
c ---[  80]---> BDD-cost:   83
c ---[  79]---> BDD-cost:   83
c ---[  78]---> BDD-cost:   83
c ---[  77]---> BDD-cost:   83
c ---[  76]---> BDD-cost:   83
c ---[  75]---> BDD-cost:   83
c ---[  74]---> BDD-cost:   83
c ---[  73]---> BDD-cost:   83
c ---[  72]---> BDD-cost:   83
c ---[  71]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   83
c ---[  69]---> BDD-cost:   83
c ---[  68]---> BDD-cost:   83
c ---[  67]---> BDD-cost:   83
c ---[  66]---> BDD-cost:   83
c ---[  65]---> BDD-cost:   83
c ---[  64]---> BDD-cost:   83
c ---[  63]---> BDD-cost:   83
c ---[  62]---> BDD-cost:   83
c ---[  61]---> BDD-cost:   83
c ---[  60]---> BDD-cost:   83
c ---[  59]---> BDD-cost:   83
c ---[  58]---> BDD-cost:   83
c ---[  57]---> BDD-cost:   83
c ---[  56]---> BDD-cost:   83
c ---[  55]---> BDD-cost:   83
c ---[  54]---> BDD-cost:   83
c ---[  53]---> BDD-cost:   83
c ---[  52]---> BDD-cost:   83
c ---[  51]---> BDD-cost:   83
c ---[  50]---> BDD-cost:   83
c ---[  49]---> BDD-cost:   83
c ---[  48]---> BDD-cost:   83
c ---[  47]---> BDD-cost:   83
c ---[  46]---> BDD-cost:   83
c ---[  45]---> BDD-cost:   83
c ---[  44]---> BDD-cost:   83
c ---[  43]---> BDD-cost:   83
c ---[  42]---> BDD-cost:   41
c ---[  41]---> BDD-cost:   41
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   41
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:   41
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:   41
c ---[  33]---> BDD-cost:   41
c ---[  32]---> BDD-cost:   41
c ---[  31]---> BDD-cost:   41
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:   41
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:   41
c ---[  24]---> BDD-cost:   41
c ---[  23]---> BDD-cost:   41
c ---[  22]---> BDD-cost:   41
c ---[  21]---> BDD-cost:   43
c ---[  20]---> BDD-cost:   43
c ---[  19]---> BDD-cost:   43
c ---[  18]---> BDD-cost:   43
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:   43
c ---[  15]---> BDD-cost:   43
c ---[  14]---> BDD-cost:   43
c ---[  13]---> BDD-cost:   43
c ---[  12]---> BDD-cost:   43
c ---[  11]---> BDD-cost:   43
c ---[  10]---> BDD-cost:   43
c ---[   9]---> BDD-cost:   43
c ---[   8]---> BDD-cost:   43
c ---[   7]---> BDD-cost:   43
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   43
c ---[   3]---> BDD-cost:   43
c ---[   2]---> BDD-cost:   43
c ---[   1]---> BDD-cost:   43
c ---[   0]---> BDD-cost:   43
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15701    81209 |    5233       0        0     nan |  0.000 % |
c |       101 |   15701    81209 |    5756     101    30091   297.9 |  1.042 % |
c |       251 |   15701    81209 |    6331     251    41172   164.0 |  1.042 % |
c |       477 |   15701    81209 |    6965     477   101249   212.3 |  1.042 % |
c |       816 |   15701    81209 |    7661     816   188784   231.4 |  1.042 % |
c |      1325 |   15701    81209 |    8427    1325   316955   239.2 |  1.042 % |
c |      2087 |   15701    81209 |    9270    2087   521561   249.9 |  1.042 % |
c |      3226 |   15701    81209 |   10197    3226   715932   221.9 |  1.042 % |
c |      4935 |   15701    81209 |   11217    4935  1355039   274.6 |  1.042 % |
c |      7498 |   15701    81209 |   12339    7498  2284715   304.7 |  1.042 % |
c |     11345 |   15701    81209 |   13573   11345  2854773   251.6 |  1.042 % |
c |     17112 |   15701    81209 |   14930   17112  5134950   300.1 |  1.042 % |
c |     25763 |   15701    81209 |   16423   17207  7147483   415.4 |  1.042 % |
c |     38737 |   15701    81209 |   18065   21578  6296769   291.8 |  1.042 % |
c |     58198 |   15701    81209 |   19872   18140 10242933   564.7 |  1.042 % |
c |     87390 |   15701    81209 |   21859   20249  6518874   321.9 |  1.042 % |
c |    131181 |   15701    81209 |   24045   16308  6553087   401.8 |  1.042 % |
c |    196872 |   15701    81209 |   26450   15779  9705190   615.1 |  1.042 % |
#### 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.86 0.95 0.90 2/54 4709
Raw data (stat): 4709 (runsolver) R 4708 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422515857 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 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.0006 s]
Raw data (loadavg): 0.88 0.95 0.90 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 3107 0 0 0 990 8 0 0 25 0 1 0 422515857 14700544 3084 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3589 3084 603 41 0 3548 0
vsize: 14356
[startup+20.0015 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 4993 0 0 0 1986 12 0 0 25 0 1 0 422515857 22396928 4970 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5468 4970 603 41 0 5427 0
vsize: 21872
[startup+30.0008 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 6234 0 0 0 2982 15 0 0 25 0 1 0 422515857 27533312 6211 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6722 6211 603 41 0 6681 0
vsize: 26888
[startup+40.0004 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 6497 0 0 0 3982 16 0 0 25 0 1 0 422515857 28618752 6474 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6987 6474 603 41 0 6946 0
vsize: 27948
[startup+50.0004 s]
Raw data (loadavg): 1.16 1.01 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 6968 0 0 0 4981 17 0 0 25 0 1 0 422515857 30515200 6945 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7450 6945 603 41 0 7409 0
vsize: 29800
[startup+60.0008 s]
Raw data (loadavg): 1.14 1.01 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 7822 0 0 0 5978 20 0 0 25 0 1 0 422515857 34029568 7799 4294967295 134512640 134672761 3221224528 3221223632 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8308 7799 603 41 0 8267 0
vsize: 33232
[startup+70.0004 s]
Raw data (loadavg): 1.12 1.01 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 8603 0 0 0 6976 22 0 0 25 0 1 0 422515857 37273600 8580 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9100 8580 603 41 0 9059 0
vsize: 36400
[startup+80.0004 s]
Raw data (loadavg): 1.10 1.01 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 8605 0 0 0 7976 22 0 0 25 0 1 0 422515857 37273600 8582 4294967295 134512640 134672761 3221224528 3221223544 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9100 8582 603 41 0 9059 0
vsize: 36400
[startup+89.9999 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 8607 0 0 0 8976 23 0 0 25 0 1 0 422515857 37150720 8567 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8567 603 41 0 9029 0
vsize: 36280
[startup+99.9994 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 8607 0 0 0 9975 23 0 0 25 0 1 0 422515857 37150720 8567 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9070 8567 603 41 0 9029 0
vsize: 36280
[startup+110 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 8607 0 0 0 10976 23 0 0 25 0 1 0 422515857 37150720 8567 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9070 8567 603 41 0 9029 0
vsize: 36280
[startup+120.001 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 8671 0 0 0 11976 23 0 0 25 0 1 0 422515857 37421056 8631 4294967295 134512640 134672761 3221224528 3221223712 134559604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9136 8631 603 41 0 9095 0
vsize: 36544
[startup+130 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 9854 0 0 0 12973 26 0 0 25 0 1 0 422515857 42291200 9814 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9814 603 41 0 10284 0
vsize: 41300
[startup+140 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 10615 0 0 0 13971 27 0 0 25 0 1 0 422515857 45395968 10575 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11083 10575 603 41 0 11042 0
vsize: 44332
[startup+150.001 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 10615 0 0 0 14972 27 0 0 25 0 1 0 422515857 45395968 10575 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11083 10575 603 41 0 11042 0
vsize: 44332
[startup+160 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 10615 0 0 0 15972 27 0 0 25 0 1 0 422515857 45395968 10575 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11083 10575 603 41 0 11042 0
vsize: 44332
[startup+170 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 11545 0 0 0 16970 30 0 0 25 0 1 0 422515857 49340416 11505 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12046 11505 603 41 0 12005 0
vsize: 48184
[startup+180 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 13063 0 0 0 17966 33 0 0 25 0 1 0 422515857 55586816 13023 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13571 13023 603 41 0 13530 0
vsize: 54284
[startup+189.999 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14128 0 0 0 18963 36 0 0 25 0 1 0 422515857 59908096 14088 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14088 603 41 0 14585 0
vsize: 58504
[startup+199.999 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14128 0 0 0 19963 36 0 0 25 0 1 0 422515857 59908096 14088 4294967295 134512640 134672761 3221224528 3221223632 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14088 603 41 0 14585 0
vsize: 58504
[startup+210 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14129 0 0 0 20964 36 0 0 25 0 1 0 422515857 59908096 14089 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+219.999 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14129 0 0 0 21964 36 0 0 25 0 1 0 422515857 59908096 14089 4294967295 134512640 134672761 3221224528 3221223696 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+229.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14129 0 0 0 22964 36 0 0 25 0 1 0 422515857 59908096 14089 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+240 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14129 0 0 0 23964 36 0 0 25 0 1 0 422515857 59908096 14089 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+249.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14129 0 0 0 24964 36 0 0 25 0 1 0 422515857 59908096 14089 4294967295 134512640 134672761 3221224528 3221223696 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+259.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 25964 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+270 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 26965 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+279.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 27965 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+289.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 28965 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+300 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 29965 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+309.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 30965 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+319.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 31965 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+329.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 32965 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+339.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 33966 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+349.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 34966 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+360 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 35966 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+369.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 36966 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+379.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 37966 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+390 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 38967 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+399.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 39967 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+410 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 40967 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223680 134542664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+420 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 41966 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+429.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 14131 0 0 0 42967 36 0 0 25 0 1 0 422515857 59908096 14091 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+440 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15869 0 0 0 43964 40 0 0 25 0 1 0 422515857 67055616 15829 4294967295 134512640 134672761 3221224528 3221222256 134565634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15829 603 41 0 16330 0
vsize: 65484
[startup+450 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15869 0 0 0 44964 40 0 0 25 0 1 0 422515857 67055616 15829 4294967295 134512640 134672761 3221224528 3221223712 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15829 603 41 0 16330 0
vsize: 65484
[startup+460 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15869 0 0 0 45964 40 0 0 25 0 1 0 422515857 67055616 15829 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15829 603 41 0 16330 0
vsize: 65484
[startup+470 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15870 0 0 0 46964 40 0 0 25 0 1 0 422515857 67055616 15830 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+480 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15870 0 0 0 47964 40 0 0 25 0 1 0 422515857 67055616 15830 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+489.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15870 0 0 0 48964 40 0 0 25 0 1 0 422515857 67055616 15830 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+499.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15870 0 0 0 49964 40 0 0 25 0 1 0 422515857 67055616 15830 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+510 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15870 0 0 0 50965 40 0 0 25 0 1 0 422515857 67055616 15830 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+519.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15870 0 0 0 51965 40 0 0 25 0 1 0 422515857 67055616 15830 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+529.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 15870 0 0 0 52965 40 0 0 25 0 1 0 422515857 67055616 15830 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+540 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 16231 0 0 0 53964 41 0 0 25 0 1 0 422515857 68460544 16191 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16714 16191 603 41 0 16673 0
vsize: 66856
[startup+549.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 16779 0 0 0 54963 42 0 0 25 0 1 0 422515857 70811648 16739 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17288 16740 603 41 0 17247 0
vsize: 69152
[startup+559.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 17353 0 0 0 55962 43 0 0 25 0 1 0 422515857 73179136 17313 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17866 17313 603 41 0 17825 0
vsize: 71464
[startup+569.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 17694 0 0 0 56962 44 0 0 25 0 1 0 422515857 74600448 17654 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+579.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 17694 0 0 0 57962 44 0 0 25 0 1 0 422515857 74600448 17654 4294967295 134512640 134672761 3221224528 3221223632 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+589.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 17694 0 0 0 58962 44 0 0 25 0 1 0 422515857 74600448 17654 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+599.997 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 17694 0 0 0 59962 44 0 0 25 0 1 0 422515857 74600448 17654 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+609.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 17694 0 0 0 60962 44 0 0 25 0 1 0 422515857 74600448 17654 4294967295 134512640 134672761 3221224528 3221223712 134559358 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+619.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 17694 0 0 0 61962 44 0 0 25 0 1 0 422515857 74600448 17654 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+629.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 17964 0 0 0 62962 45 0 0 25 0 1 0 422515857 75681792 17924 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18477 17924 603 41 0 18436 0
vsize: 73908
[startup+639.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 18420 0 0 0 63961 45 0 0 25 0 1 0 422515857 77570048 18380 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18938 18380 603 41 0 18897 0
vsize: 75752
[startup+649.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 19066 0 0 0 64960 46 0 0 25 0 1 0 422515857 80269312 19026 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19597 19026 603 41 0 19556 0
vsize: 78388
[startup+659.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 19605 0 0 0 65959 48 0 0 25 0 1 0 422515857 82444288 19565 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20128 19565 603 41 0 20087 0
vsize: 80512
[startup+669.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20041 0 0 0 66958 49 0 0 25 0 1 0 422515857 84201472 20001 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20001 603 41 0 20516 0
vsize: 82228
[startup+679.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20041 0 0 0 67958 49 0 0 25 0 1 0 422515857 84201472 20001 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20001 603 41 0 20516 0
vsize: 82228
[startup+689.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20041 0 0 0 68958 49 0 0 25 0 1 0 422515857 84201472 20001 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20001 603 41 0 20516 0
vsize: 82228
[startup+699.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20042 0 0 0 69959 49 0 0 25 0 1 0 422515857 84201472 20002 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+709.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20042 0 0 0 70959 49 0 0 25 0 1 0 422515857 84201472 20002 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+719.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20042 0 0 0 71959 49 0 0 25 0 1 0 422515857 84201472 20002 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+729.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20042 0 0 0 72959 49 0 0 25 0 1 0 422515857 84201472 20002 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+739.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20042 0 0 0 73959 49 0 0 25 0 1 0 422515857 84201472 20002 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+749.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20042 0 0 0 74960 49 0 0 25 0 1 0 422515857 84201472 20002 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+759.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20042 0 0 0 75960 49 0 0 25 0 1 0 422515857 84201472 20002 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+769.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20042 0 0 0 76960 49 0 0 25 0 1 0 422515857 84201472 20002 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+779.998 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20043 0 0 0 77960 49 0 0 25 0 1 0 422515857 84201472 20003 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20003 603 41 0 20516 0
vsize: 82228
[startup+789.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20043 0 0 0 78960 49 0 0 25 0 1 0 422515857 84201472 20003 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20003 603 41 0 20516 0
vsize: 82228
[startup+799.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20043 0 0 0 79960 49 0 0 25 0 1 0 422515857 84201472 20003 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20003 603 41 0 20516 0
vsize: 82228
[startup+810 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20044 0 0 0 80961 49 0 0 25 0 1 0 422515857 84201472 20004 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 20004 603 41 0 20516 0
vsize: 82228
[startup+820 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20394 0 0 0 81960 50 0 0 25 0 1 0 422515857 85688320 20354 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20920 20354 603 41 0 20879 0
vsize: 83680
[startup+830 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 20806 0 0 0 82959 51 0 0 25 0 1 0 422515857 87441408 20766 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21348 20766 603 41 0 21307 0
vsize: 85392
[startup+840 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 21249 0 0 0 83959 52 0 0 25 0 1 0 422515857 89194496 21209 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21776 21209 603 41 0 21735 0
vsize: 87104
[startup+850 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 21807 0 0 0 84958 53 0 0 25 0 1 0 422515857 91492352 21767 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22337 21767 603 41 0 22296 0
vsize: 89348
[startup+860 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22084 0 0 0 85957 54 0 0 25 0 1 0 422515857 92622848 22044 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+870 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22084 0 0 0 86957 54 0 0 25 0 1 0 422515857 92622848 22044 4294967295 134512640 134672761 3221224528 3221223664 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+879.999 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4709
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22084 0 0 0 87957 54 0 0 25 0 1 0 422515857 92622848 22044 4294967295 134512640 134672761 3221224528 3221223632 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+890 s]
Raw data (loadavg): 1.08 1.02 0.93 2/57 4751
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22084 0 0 0 88957 54 0 0 25 0 1 0 422515857 92622848 22044 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+899.999 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 4762
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22084 0 0 0 89957 54 0 0 25 0 1 0 422515857 92622848 22044 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+909.999 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 4762
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22084 0 0 0 90957 54 0 0 25 0 1 0 422515857 92622848 22044 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+919.999 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 4762
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22084 0 0 0 91957 54 0 0 25 0 1 0 422515857 92622848 22044 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+929.999 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 4762
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22084 0 0 0 92957 54 0 0 25 0 1 0 422515857 92622848 22044 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+939.999 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 4762
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22085 0 0 0 93957 54 0 0 25 0 1 0 422515857 92622848 22045 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22045 603 41 0 22572 0
vsize: 90452
[startup+949.999 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 4762
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22186 0 0 0 94958 54 0 0 25 0 1 0 422515857 93028352 22146 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22712 22146 603 41 0 22671 0
vsize: 90848
[startup+959.999 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 22734 0 0 0 95957 55 0 0 25 0 1 0 422515857 95375360 22694 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23285 22694 603 41 0 23244 0
vsize: 93140
[startup+969.999 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23018 0 0 0 96956 56 0 0 25 0 1 0 422515857 96595968 22978 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+979.999 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23018 0 0 0 97956 56 0 0 25 0 1 0 422515857 96595968 22978 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+990 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23018 0 0 0 98956 56 0 0 25 0 1 0 422515857 96595968 22978 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+999.999 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23018 0 0 0 99956 56 0 0 25 0 1 0 422515857 96595968 22978 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+1010 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23018 0 0 0 100956 56 0 0 25 0 1 0 422515857 96595968 22978 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+1020 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23019 0 0 0 101957 56 0 0 25 0 1 0 422515857 96595968 22979 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22979 603 41 0 23542 0
vsize: 94332
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23019 0 0 0 102957 56 0 0 25 0 1 0 422515857 96595968 22979 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22979 603 41 0 23542 0
vsize: 94332
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23019 0 0 0 103957 56 0 0 25 0 1 0 422515857 96595968 22979 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22979 603 41 0 23542 0
vsize: 94332
[startup+1050 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23022 0 0 0 104957 56 0 0 25 0 1 0 422515857 96595968 22982 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22982 603 41 0 23542 0
vsize: 94332
[startup+1060 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23025 0 0 0 105957 56 0 0 25 0 1 0 422515857 96595968 22985 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22985 603 41 0 23542 0
vsize: 94332
[startup+1070 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23025 0 0 0 106957 56 0 0 25 0 1 0 422515857 96595968 22985 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22985 603 41 0 23542 0
vsize: 94332
[startup+1080 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23026 0 0 0 107958 56 0 0 25 0 1 0 422515857 96595968 22986 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22986 603 41 0 23542 0
vsize: 94332
[startup+1090 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23026 0 0 0 108958 56 0 0 25 0 1 0 422515857 96595968 22986 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22986 603 41 0 23542 0
vsize: 94332
[startup+1100 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23027 0 0 0 109958 56 0 0 25 0 1 0 422515857 96595968 22987 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23027 0 0 0 110958 56 0 0 25 0 1 0 422515857 96595968 22987 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1120 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23027 0 0 0 111958 56 0 0 25 0 1 0 422515857 96595968 22987 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1130 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23027 0 0 0 112958 56 0 0 25 0 1 0 422515857 96595968 22987 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1140 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23027 0 0 0 113959 56 0 0 25 0 1 0 422515857 96595968 22987 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1150 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23027 0 0 0 114959 56 0 0 25 0 1 0 422515857 96595968 22987 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1160 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23027 0 0 0 115959 56 0 0 25 0 1 0 422515857 96595968 22987 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1170 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 23781 0 0 0 116957 58 0 0 25 0 1 0 422515857 99565568 23741 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24308 23741 603 41 0 24267 0
vsize: 97232
[startup+1180 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 24737 0 0 0 117955 60 0 0 25 0 1 0 422515857 103485440 24697 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25265 24697 603 41 0 25224 0
vsize: 101060
[startup+1190 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4764
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 25385 0 0 0 118954 62 0 0 25 0 1 0 422515857 106188800 25345 4294967295 134512640 134672761 3221224528 3221223632 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25925 25345 603 41 0 25884 0
vsize: 103700
[startup+1200 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4766
Raw data (stat): 4709 (minisat+) R 4708 30701 30700 0 -1 0 26017 0 0 0 119953 63 0 0 25 0 1 0 422515857 108756992 25977 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26552 25977 603 41 0 26511 0
vsize: 106208
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 4766
Raw data (stat): 4709 (minisat+) Z 4708 30701 30700 0 -1 12 26019 0 0 0 119953 68 0 0 25 0 1 0 422515857 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.05
CPU time (s): 1200.22
CPU user time (s): 1199.53
CPU system time (s): 0.687895
CPU usage (%): 100.014
Max. virtual memory (Kb): 106208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####