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 4818

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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:        905924 kB
Buffers:         32464 kB
Cached:          61748 kB
SwapCached:         36 kB
Active:          43748 kB
Inactive:        53332 kB
HighTotal:      131008 kB
HighFree:        65576 kB
LowTotal:       903652 kB
LowFree:        840348 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26236 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:46:15 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 491 7 1200.25 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.83 0.91 0.89 2/54 30084
Raw data (stat): 30084 (runsolver) R 30083 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478828343 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0001 s]
Raw data (loadavg): 0.85 0.91 0.89 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 3085 0 0 0 989 9 0 0 25 0 1 0 478828343 14565376 3062 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3556 3062 603 41 0 3515 0
vsize: 14224
[startup+19.9994 s]
Raw data (loadavg): 0.88 0.91 0.89 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 4966 0 0 0 1984 13 0 0 25 0 1 0 478828343 22253568 4943 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5433 4943 603 41 0 5392 0
vsize: 21732
[startup+30.0006 s]
Raw data (loadavg): 0.89 0.91 0.89 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 6222 0 0 0 2980 17 0 0 25 0 1 0 478828343 27533312 6199 4294967295 134512640 134672761 3221224624 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6722 6199 603 41 0 6681 0
vsize: 26888
[startup+40.0009 s]
Raw data (loadavg): 0.91 0.92 0.89 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 6497 0 0 0 3980 18 0 0 25 0 1 0 478828343 28618752 6474 4294967295 134512640 134672761 3221224624 3221223792 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6987 6474 603 41 0 6946 0
vsize: 27948
[startup+50.0011 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 6973 0 0 0 4978 19 0 0 25 0 1 0 478828343 30650368 6950 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7483 6950 603 41 0 7442 0
vsize: 29932
[startup+60.0011 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 7843 0 0 0 5977 21 0 0 25 0 1 0 478828343 34164736 7820 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8341 7820 603 41 0 8300 0
vsize: 33364
[startup+70.0006 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 8603 0 0 0 6975 23 0 0 25 0 1 0 478828343 37273600 8580 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9100 8580 603 41 0 9059 0
vsize: 36400
[startup+80.001 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 8605 0 0 0 7975 23 0 0 25 0 1 0 478828343 37273600 8582 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9100 8582 603 41 0 9059 0
vsize: 36400
[startup+90.0011 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 8607 0 0 0 8975 23 0 0 25 0 1 0 478828343 37150720 8567 4294967295 134512640 134672761 3221224624 3221223624 1075350942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8567 603 41 0 9029 0
vsize: 36280
[startup+100.001 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 8607 0 0 0 9975 23 0 0 25 0 1 0 478828343 37150720 8567 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8567 603 41 0 9029 0
vsize: 36280
[startup+110.006 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 8607 0 0 0 10976 23 0 0 25 0 1 0 478828343 37150720 8567 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8567 603 41 0 9029 0
vsize: 36280
[startup+120.006 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 8757 0 0 0 11976 23 0 0 25 0 1 0 478828343 37826560 8717 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9235 8717 603 41 0 9194 0
vsize: 36940
[startup+130.006 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 9989 0 0 0 12973 26 0 0 25 0 1 0 478828343 42831872 9949 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10457 9949 603 41 0 10416 0
vsize: 41828
[startup+140.007 s]
Raw data (loadavg): 0.98 0.94 0.90 3/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 10615 0 0 0 13971 28 0 0 25 0 1 0 478828343 45395968 10575 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11083 10575 603 41 0 11042 0
vsize: 44332
[startup+150.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 10615 0 0 0 14972 28 0 0 25 0 1 0 478828343 45395968 10575 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11083 10575 603 41 0 11042 0
vsize: 44332
[startup+160.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 10615 0 0 0 15972 28 0 0 25 0 1 0 478828343 45395968 10575 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11083 10575 603 41 0 11042 0
vsize: 44332
[startup+170.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 11683 0 0 0 16968 32 0 0 25 0 1 0 478828343 49881088 11643 4294967295 134512640 134672761 3221224624 3221223728 134560013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12178 11643 603 41 0 12137 0
vsize: 48712
[startup+180.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 13305 0 0 0 17965 35 0 0 25 0 1 0 478828343 56528896 13265 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13801 13265 603 41 0 13760 0
vsize: 55204
[startup+190.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14128 0 0 0 18964 36 0 0 25 0 1 0 478828343 59908096 14088 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14088 603 41 0 14585 0
vsize: 58504
[startup+200.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14129 0 0 0 19964 36 0 0 25 0 1 0 478828343 59908096 14089 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+210.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14129 0 0 0 20964 36 0 0 25 0 1 0 478828343 59908096 14089 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+220.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14129 0 0 0 21964 36 0 0 25 0 1 0 478828343 59908096 14089 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+230.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14129 0 0 0 22965 36 0 0 25 0 1 0 478828343 59908096 14089 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+240.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14129 0 0 0 23965 36 0 0 25 0 1 0 478828343 59908096 14089 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+250.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14129 0 0 0 24965 36 0 0 25 0 1 0 478828343 59908096 14089 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14089 603 41 0 14585 0
vsize: 58504
[startup+260.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 25965 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+270.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 26965 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+280.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 27966 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+290.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 28966 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+300.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 29966 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+310.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 30966 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+320.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 31966 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+330.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 32967 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+340.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 33967 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+350.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 34967 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+360.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 35967 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+370.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 36967 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+380.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 37968 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+390.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 38968 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+400.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 39968 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 40968 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14131 0 0 0 41968 36 0 0 25 0 1 0 478828343 59908096 14091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14626 14091 603 41 0 14585 0
vsize: 58504
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 14766 0 0 0 42967 38 0 0 25 0 1 0 478828343 62468096 14726 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15251 14726 603 41 0 15210 0
vsize: 61004
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15869 0 0 0 43965 40 0 0 25 0 1 0 478828343 67055616 15829 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15829 603 41 0 16330 0
vsize: 65484
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15869 0 0 0 44965 40 0 0 25 0 1 0 478828343 67055616 15829 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15829 603 41 0 16330 0
vsize: 65484
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15870 0 0 0 45965 40 0 0 25 0 1 0 478828343 67055616 15830 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15870 0 0 0 46965 40 0 0 25 0 1 0 478828343 67055616 15830 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15870 0 0 0 47966 40 0 0 25 0 1 0 478828343 67055616 15830 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15870 0 0 0 48966 40 0 0 25 0 1 0 478828343 67055616 15830 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15870 0 0 0 49966 40 0 0 25 0 1 0 478828343 67055616 15830 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15870 0 0 0 50966 40 0 0 25 0 1 0 478828343 67055616 15830 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15870 0 0 0 51966 40 0 0 25 0 1 0 478828343 67055616 15830 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 15870 0 0 0 52966 40 0 0 25 0 1 0 478828343 67055616 15830 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15830 603 41 0 16330 0
vsize: 65484
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 16475 0 0 0 53966 41 0 0 25 0 1 0 478828343 69574656 16435 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16986 16435 603 41 0 16945 0
vsize: 67944
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 16998 0 0 0 54965 42 0 0 25 0 1 0 478828343 71680000 16958 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17500 16958 603 41 0 17459 0
vsize: 70000
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 17549 0 0 0 55964 43 0 0 25 0 1 0 478828343 74059776 17509 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18081 17509 603 41 0 18040 0
vsize: 72324
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 17694 0 0 0 56964 43 0 0 25 0 1 0 478828343 74600448 17654 4294967295 134512640 134672761 3221224624 3221223728 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 17694 0 0 0 57965 43 0 0 25 0 1 0 478828343 74600448 17654 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 17694 0 0 0 58965 43 0 0 25 0 1 0 478828343 74600448 17654 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 17694 0 0 0 59965 43 0 0 25 0 1 0 478828343 74600448 17654 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 17694 0 0 0 60965 43 0 0 25 0 1 0 478828343 74600448 17654 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 17694 0 0 0 61965 43 0 0 25 0 1 0 478828343 74600448 17654 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18213 17654 603 41 0 18172 0
vsize: 72852
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 18143 0 0 0 62965 44 0 0 25 0 1 0 478828343 76488704 18103 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18674 18103 603 41 0 18633 0
vsize: 74696
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 18725 0 0 0 63964 45 0 0 25 0 1 0 478828343 78786560 18685 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19235 18685 603 41 0 19194 0
vsize: 76940
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 19292 0 0 0 64963 46 0 0 25 0 1 0 478828343 81231872 19252 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19832 19252 603 41 0 19791 0
vsize: 79328
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 19878 0 0 0 65961 48 0 0 25 0 1 0 478828343 83525632 19838 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20392 19838 603 41 0 20351 0
vsize: 81568
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20041 0 0 0 66961 49 0 0 25 0 1 0 478828343 84201472 20001 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20001 603 41 0 20516 0
vsize: 82228
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20041 0 0 0 67961 49 0 0 25 0 1 0 478828343 84201472 20001 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20001 603 41 0 20516 0
vsize: 82228
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20041 0 0 0 68961 49 0 0 25 0 1 0 478828343 84201472 20001 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20001 603 41 0 20516 0
vsize: 82228
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20042 0 0 0 69961 49 0 0 25 0 1 0 478828343 84201472 20002 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20042 0 0 0 70962 49 0 0 25 0 1 0 478828343 84201472 20002 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20042 0 0 0 71962 49 0 0 25 0 1 0 478828343 84201472 20002 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20042 0 0 0 72962 49 0 0 25 0 1 0 478828343 84201472 20002 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20042 0 0 0 73962 49 0 0 25 0 1 0 478828343 84201472 20002 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20042 0 0 0 74962 49 0 0 25 0 1 0 478828343 84201472 20002 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20042 0 0 0 75963 49 0 0 25 0 1 0 478828343 84201472 20002 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20042 0 0 0 76963 49 0 0 25 0 1 0 478828343 84201472 20002 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20002 603 41 0 20516 0
vsize: 82228
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20043 0 0 0 77963 49 0 0 25 0 1 0 478828343 84201472 20003 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20003 603 41 0 20516 0
vsize: 82228
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20043 0 0 0 78963 49 0 0 25 0 1 0 478828343 84201472 20003 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20003 603 41 0 20516 0
vsize: 82228
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20044 0 0 0 79963 49 0 0 25 0 1 0 478828343 84201472 20004 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 20004 603 41 0 20516 0
vsize: 82228
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20284 0 0 0 80963 49 0 0 25 0 1 0 478828343 85286912 20244 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20822 20244 603 41 0 20781 0
vsize: 83288
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 20591 0 0 0 81962 50 0 0 25 0 1 0 478828343 86495232 20551 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21117 20551 603 41 0 21076 0
vsize: 84468
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 21069 0 0 0 82961 51 0 0 25 0 1 0 478828343 88522752 21029 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21612 21029 603 41 0 21571 0
vsize: 86448
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 21568 0 0 0 83960 52 0 0 25 0 1 0 478828343 90546176 21528 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22106 21528 603 41 0 22065 0
vsize: 88424
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 84960 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 85960 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 86960 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 87960 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 88960 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223856 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 89960 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223728 134560128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 90960 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 91961 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22084 0 0 0 92961 53 0 0 25 0 1 0 478828343 92622848 22044 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22044 603 41 0 22572 0
vsize: 90452
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22085 0 0 0 93961 53 0 0 25 0 1 0 478828343 92622848 22045 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22613 22045 603 41 0 22572 0
vsize: 90452
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 22526 0 0 0 94960 54 0 0 25 0 1 0 478828343 94543872 22486 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23082 22486 603 41 0 23041 0
vsize: 92328
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23017 0 0 0 95959 55 0 0 25 0 1 0 478828343 96595968 22977 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22977 603 41 0 23542 0
vsize: 94332
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23018 0 0 0 96960 55 0 0 25 0 1 0 478828343 96595968 22978 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+980.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23018 0 0 0 97960 55 0 0 25 0 1 0 478828343 96595968 22978 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23018 0 0 0 98960 55 0 0 25 0 1 0 478828343 96595968 22978 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23018 0 0 0 99960 55 0 0 25 0 1 0 478828343 96595968 22978 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23018 0 0 0 100960 55 0 0 25 0 1 0 478828343 96595968 22978 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22978 603 41 0 23542 0
vsize: 94332
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23019 0 0 0 101960 55 0 0 25 0 1 0 478828343 96595968 22979 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22979 603 41 0 23542 0
vsize: 94332
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23019 0 0 0 102961 55 0 0 25 0 1 0 478828343 96595968 22979 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22979 603 41 0 23542 0
vsize: 94332
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23021 0 0 0 103961 55 0 0 25 0 1 0 478828343 96595968 22981 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22981 603 41 0 23542 0
vsize: 94332
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23025 0 0 0 104961 55 0 0 25 0 1 0 478828343 96595968 22985 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22985 603 41 0 23542 0
vsize: 94332
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23025 0 0 0 105961 55 0 0 25 0 1 0 478828343 96595968 22985 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22985 603 41 0 23542 0
vsize: 94332
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23026 0 0 0 106962 55 0 0 25 0 1 0 478828343 96595968 22986 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22986 603 41 0 23542 0
vsize: 94332
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23026 0 0 0 107962 55 0 0 25 0 1 0 478828343 96595968 22986 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22986 603 41 0 23542 0
vsize: 94332
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23027 0 0 0 108962 55 0 0 25 0 1 0 478828343 96595968 22987 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23027 0 0 0 109962 55 0 0 25 0 1 0 478828343 96595968 22987 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23027 0 0 0 110962 55 0 0 25 0 1 0 478828343 96595968 22987 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23027 0 0 0 111962 55 0 0 25 0 1 0 478828343 96595968 22987 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23027 0 0 0 112963 55 0 0 25 0 1 0 478828343 96595968 22987 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23027 0 0 0 113963 55 0 0 25 0 1 0 478828343 96595968 22987 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23027 0 0 0 114963 55 0 0 25 0 1 0 478828343 96595968 22987 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23583 22987 603 41 0 23542 0
vsize: 94332
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 23623 0 0 0 115962 57 0 0 25 0 1 0 478828343 99024896 23583 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24176 23584 603 41 0 24135 0
vsize: 96704
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 24502 0 0 0 116960 59 0 0 25 0 1 0 478828343 102539264 24462 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25034 24462 603 41 0 24993 0
vsize: 100136
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 25215 0 0 0 117958 61 0 0 25 0 1 0 478828343 105512960 25175 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25760 25175 603 41 0 25719 0
vsize: 103040
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 26016 0 0 0 118956 63 0 0 25 0 1 0 478828343 108756992 25976 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26552 25976 603 41 0 26511 0
vsize: 106208
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30084
Raw data (stat): 30084 (minisat+) R 30083 28099 28098 0 -1 0 26017 0 0 0 119956 63 0 0 25 0 1 0 478828343 108756992 25977 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26552 25977 603 41 0 26511 0
vsize: 106208
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30084
Raw data (stat): 30084 (minisat+) Z 30083 28099 28098 0 -1 12 26019 0 0 0 119956 68 0 0 25 0 1 0 478828343 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.06
CPU time (s): 1200.25
CPU user time (s): 1199.56
CPU system time (s): 0.682896
CPU usage (%): 100.016
Max. virtual memory (Kb): 106208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####