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-chnl30_35_pb.cnf.cr.opb
MD5SUM	b1c5adb5438ceaf1c654cfedb79b695e
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	36
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.06099
Number of variables	2100
Total number of constraints	130
Number of constraints which are clauses	70
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	30
Maximum length of a constraint	35
Trace number 6102

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 03:26:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4524 boxname=wulflinc25 idbench=12 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b1c5adb5438ceaf1c654cfedb79b695e  /oldhome/oroussel/tmp/wulflinc25/normalized-chnl30_35_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-chnl30_35_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc25/normalized-chnl30_35_pb.cnf.cr.opb
IDLAUNCH: 4524
/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:        871292 kB
Buffers:         34992 kB
Cached:          93696 kB
SwapCached:         36 kB
Active:          50492 kB
Inactive:        81104 kB
HighTotal:      131008 kB
HighFree:        33600 kB
LowTotal:       903652 kB
LowFree:        837692 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26240 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:46:22 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4524 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 130 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................
c ---[  59]---> BDD-cost:   67
c ---[  58]---> BDD-cost:   67
c ---[  57]---> BDD-cost:   67
c ---[  56]---> BDD-cost:   67
c ---[  55]---> BDD-cost:   67
c ---[  54]---> BDD-cost:   67
c ---[  53]---> BDD-cost:   67
c ---[  52]---> BDD-cost:   67
c ---[  51]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   67
c ---[  49]---> BDD-cost:   67
c ---[  48]---> BDD-cost:   67
c ---[  47]---> BDD-cost:   67
c ---[  46]---> BDD-cost:   67
c ---[  45]---> BDD-cost:   67
c ---[  44]---> BDD-cost:   67
c ---[  43]---> BDD-cost:   67
c ---[  42]---> BDD-cost:   67
c ---[  41]---> BDD-cost:   67
c ---[  40]---> BDD-cost:   67
c ---[  39]---> BDD-cost:   67
c ---[  38]---> BDD-cost:   67
c ---[  37]---> BDD-cost:   67
c ---[  36]---> BDD-cost:   67
c ---[  35]---> BDD-cost:   67
c ---[  34]---> BDD-cost:   67
c ---[  33]---> BDD-cost:   67
c ---[  32]---> BDD-cost:   67
c ---[  31]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   67
c ---[  29]---> BDD-cost:   67
c ---[  28]---> BDD-cost:   67
c ---[  27]---> BDD-cost:   67
c ---[  26]---> BDD-cost:   67
c ---[  25]---> BDD-cost:   67
c ---[  24]---> BDD-cost:   67
c ---[  23]---> BDD-cost:   67
c ---[  22]---> BDD-cost:   67
c ---[  21]---> BDD-cost:   67
c ---[  20]---> BDD-cost:   67
c ---[  19]---> BDD-cost:   67
c ---[  18]---> BDD-cost:   67
c ---[  17]---> BDD-cost:   67
c ---[  16]---> BDD-cost:   67
c ---[  15]---> BDD-cost:   67
c ---[  14]---> BDD-cost:   67
c ---[  13]---> BDD-cost:   67
c ---[  12]---> BDD-cost:   67
c ---[  11]---> BDD-cost:   67
c ---[  10]---> BDD-cost:   67
c ---[   9]---> BDD-cost:   67
c ---[   8]---> BDD-cost:   67
c ---[   7]---> BDD-cost:   67
c ---[   6]---> BDD-cost:   67
c ---[   5]---> BDD-cost:   67
c ---[   4]---> BDD-cost:   67
c ---[   3]---> BDD-cost:   67
c ---[   2]---> BDD-cost:   67
c ---[   1]---> BDD-cost:   67
c ---[   0]---> BDD-cost:   67
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17890    51480 |    5963       0        0     nan |  0.000 % |
c |       101 |   17860    51390 |    6559      90     9416   104.6 |  1.079 % |
c |       251 |   17595    50595 |    7215     118    10009    84.8 |  1.945 % |
c |       476 |   17070    49020 |    7936     145    10282    70.9 |  3.660 % |
c |       813 |   16870    48420 |    8730     397    47820   120.5 |  4.314 % |
c |      1319 |   16405    47025 |    9603     746   105243   141.1 |  5.834 % |
c |      2081 |   16360    46890 |   10563    1489   289449   194.4 |  5.981 % |
c |      3222 |   15900    45510 |   11620    2454   464317   189.2 |  7.484 % |
c |      4932 |   15775    45135 |   12782    4097   782352   191.0 |  7.892 % |
c |      7494 |   15535    44415 |   14060    6566  1362487   207.5 |  8.676 % |
c |     11340 |   15090    43080 |   15466   10253  2246471   219.1 | 10.131 % |
c |     17110 |   13755    39075 |   17013   15555  3496834   224.8 | 14.493 % |
c |     25759 |   12520    35370 |   18714   14341  3187665   222.3 | 18.529 % |
c |     38733 |   11730    33000 |   20585   17010  3917595   230.3 | 21.111 % |
c |     58194 |   11036    30920 |   22644   12616  3236981   256.6 | 23.382 % |
c |     87386 |   10682    29860 |   24908   13454  3615875   268.8 | 24.542 % |
c |    131175 |   10103    28125 |   27399   25955  6956664   268.0 | 26.438 % |
c |    196860 |    9740    27040 |   30139   16984  4692357   276.3 | 27.631 % |
c |    295388 |    9107    25155 |   33153   31475  7717490   245.2 | 29.722 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 1553
Raw data (stat): 1553 (runsolver) R 1552 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481349392 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99985 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 1917 0 0 0 993 4 0 0 25 0 1 0 481349392 9502720 1895 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2320 1895 603 41 0 2279 0
vsize: 9280
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 2803 0 0 0 1990 8 0 0 25 0 1 0 481349392 13176832 2781 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3217 2781 603 41 0 3176 0
vsize: 12868
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 3663 0 0 0 2987 10 0 0 25 0 1 0 481349392 16683008 3641 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4073 3641 603 41 0 4032 0
vsize: 16292
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 4191 0 0 0 3986 11 0 0 25 0 1 0 481349392 18845696 4169 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4601 4169 603 41 0 4560 0
vsize: 18404
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 4426 0 0 0 4986 12 0 0 25 0 1 0 481349392 19787776 4404 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4831 4404 603 41 0 4790 0
vsize: 19324
[startup+60.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 4737 0 0 0 5985 13 0 0 25 0 1 0 481349392 21000192 4715 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5127 4715 603 41 0 5086 0
vsize: 20508
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 4990 0 0 0 6983 15 0 0 25 0 1 0 481349392 22081536 4968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5391 4968 603 41 0 5350 0
vsize: 21564
[startup+80.0012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 5297 0 0 0 7982 15 0 0 25 0 1 0 481349392 23433216 5275 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5721 5275 603 41 0 5680 0
vsize: 22884
[startup+90.0018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 5668 0 0 0 8982 16 0 0 25 0 1 0 481349392 24907776 5646 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5646 603 41 0 6040 0
vsize: 24324
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 5668 0 0 0 9982 16 0 0 25 0 1 0 481349392 24907776 5646 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5646 603 41 0 6040 0
vsize: 24324
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 5668 0 0 0 10982 16 0 0 25 0 1 0 481349392 24907776 5646 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5646 603 41 0 6040 0
vsize: 24324
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 5668 0 0 0 11982 16 0 0 25 0 1 0 481349392 24907776 5646 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5646 603 41 0 6040 0
vsize: 24324
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 6038 0 0 0 12981 17 0 0 25 0 1 0 481349392 26382336 6016 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6441 6016 603 41 0 6400 0
vsize: 25764
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 6114 0 0 0 13981 18 0 0 25 0 1 0 481349392 26787840 6092 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6540 6092 603 41 0 6499 0
vsize: 26160
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 6114 0 0 0 14981 18 0 0 25 0 1 0 481349392 26787840 6092 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6540 6092 603 41 0 6499 0
vsize: 26160
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 6129 0 0 0 15981 18 0 0 25 0 1 0 481349392 26787840 6107 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6540 6107 603 41 0 6499 0
vsize: 26160
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 6859 0 0 0 16979 20 0 0 25 0 1 0 481349392 29757440 6837 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7265 6837 603 41 0 7224 0
vsize: 29060
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 6859 0 0 0 17979 20 0 0 25 0 1 0 481349392 29757440 6837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7265 6837 603 41 0 7224 0
vsize: 29060
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 6859 0 0 0 18979 20 0 0 25 0 1 0 481349392 29757440 6837 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7265 6837 603 41 0 7224 0
vsize: 29060
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 7300 0 0 0 19978 21 0 0 25 0 1 0 481349392 31645696 7278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7726 7278 603 41 0 7685 0
vsize: 30904
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 7683 0 0 0 20978 22 0 0 25 0 1 0 481349392 33136640 7661 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8090 7661 603 41 0 8049 0
vsize: 32360
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 7683 0 0 0 21978 22 0 0 25 0 1 0 481349392 33136640 7661 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8090 7661 603 41 0 8049 0
vsize: 32360
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 7683 0 0 0 22978 22 0 0 25 0 1 0 481349392 33136640 7661 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8090 7661 603 41 0 8049 0
vsize: 32360
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 8353 0 0 0 23977 23 0 0 25 0 1 0 481349392 35966976 8331 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8781 8331 603 41 0 8740 0
vsize: 35124
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 8628 0 0 0 24977 24 0 0 25 0 1 0 481349392 37044224 8606 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9044 8606 603 41 0 9003 0
vsize: 36176
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 8628 0 0 0 25977 24 0 0 25 0 1 0 481349392 37044224 8606 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9044 8606 603 41 0 9003 0
vsize: 36176
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 8628 0 0 0 26977 24 0 0 25 0 1 0 481349392 37044224 8606 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9044 8606 603 41 0 9003 0
vsize: 36176
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 8653 0 0 0 27977 24 0 0 25 0 1 0 481349392 37179392 8631 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9077 8631 603 41 0 9036 0
vsize: 36308
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 8653 0 0 0 28977 24 0 0 25 0 1 0 481349392 37179392 8631 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9077 8631 603 41 0 9036 0
vsize: 36308
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 8653 0 0 0 29978 24 0 0 25 0 1 0 481349392 37179392 8631 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9077 8631 603 41 0 9036 0
vsize: 36308
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 8926 0 0 0 30977 25 0 0 25 0 1 0 481349392 38256640 8904 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9340 8904 603 41 0 9299 0
vsize: 37360
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 9413 0 0 0 31976 26 0 0 25 0 1 0 481349392 40275968 9391 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9833 9391 603 41 0 9792 0
vsize: 39332
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 9413 0 0 0 32976 26 0 0 25 0 1 0 481349392 40275968 9391 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9833 9391 603 41 0 9792 0
vsize: 39332
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 9413 0 0 0 33976 26 0 0 25 0 1 0 481349392 40275968 9391 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9833 9391 603 41 0 9792 0
vsize: 39332
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 9538 0 0 0 34976 26 0 0 25 0 1 0 481349392 40816640 9516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9965 9516 603 41 0 9924 0
vsize: 39860
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 9538 0 0 0 35976 26 0 0 25 0 1 0 481349392 40816640 9516 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9965 9516 603 41 0 9924 0
vsize: 39860
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 9538 0 0 0 36977 26 0 0 25 0 1 0 481349392 40816640 9516 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9965 9516 603 41 0 9924 0
vsize: 39860
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 9538 0 0 0 37977 26 0 0 25 0 1 0 481349392 40816640 9516 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9965 9516 603 41 0 9924 0
vsize: 39860
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 9929 0 0 0 38976 28 0 0 25 0 1 0 481349392 42438656 9907 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9907 603 41 0 10320 0
vsize: 41444
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10238 0 0 0 39974 29 0 0 25 0 1 0 481349392 43646976 10216 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10656 10216 603 41 0 10615 0
vsize: 42624
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10238 0 0 0 40974 29 0 0 25 0 1 0 481349392 43646976 10216 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10216 603 41 0 10615 0
vsize: 42624
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10238 0 0 0 41974 29 0 0 25 0 1 0 481349392 43646976 10216 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10216 603 41 0 10615 0
vsize: 42624
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10238 0 0 0 42974 29 0 0 25 0 1 0 481349392 43646976 10216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10656 10216 603 41 0 10615 0
vsize: 42624
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10799 0 0 0 43972 31 0 0 25 0 1 0 481349392 45936640 10777 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11215 10777 603 41 0 11174 0
vsize: 44860
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10925 0 0 0 44972 31 0 0 25 0 1 0 481349392 46485504 10903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10903 603 41 0 11308 0
vsize: 45396
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10926 0 0 0 45972 31 0 0 25 0 1 0 481349392 46485504 10904 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10904 603 41 0 11308 0
vsize: 45396
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 46972 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 47972 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 48973 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 49973 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 50973 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+520.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 51973 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 52973 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 53973 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 54974 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+560 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 55974 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 10927 0 0 0 56974 31 0 0 25 0 1 0 481349392 46485504 10905 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11349 10905 603 41 0 11308 0
vsize: 45396
[startup+580 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 11106 0 0 0 57974 32 0 0 25 0 1 0 481349392 47161344 11084 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11514 11084 603 41 0 11473 0
vsize: 46056
[startup+590 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 11621 0 0 0 58973 33 0 0 25 0 1 0 481349392 49348608 11599 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12048 11599 603 41 0 12007 0
vsize: 48192
[startup+599.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 11621 0 0 0 59973 33 0 0 25 0 1 0 481349392 49348608 11599 4294967295 134512640 134672761 3221224544 3221223728 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12048 11599 603 41 0 12007 0
vsize: 48192
[startup+609.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 11621 0 0 0 60972 33 0 0 25 0 1 0 481349392 49348608 11599 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12048 11599 603 41 0 12007 0
vsize: 48192
[startup+619.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 11621 0 0 0 61973 33 0 0 25 0 1 0 481349392 49348608 11599 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12048 11599 603 41 0 12007 0
vsize: 48192
[startup+629.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 11621 0 0 0 62973 33 0 0 25 0 1 0 481349392 49348608 11599 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12048 11599 603 41 0 12007 0
vsize: 48192
[startup+640 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 11621 0 0 0 63973 33 0 0 25 0 1 0 481349392 49348608 11599 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12048 11599 603 41 0 12007 0
vsize: 48192
[startup+649.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 11621 0 0 0 64973 33 0 0 25 0 1 0 481349392 49348608 11599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12048 11599 603 41 0 12007 0
vsize: 48192
[startup+659.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12074 0 0 0 65972 34 0 0 25 0 1 0 481349392 51367936 12052 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12541 12052 603 41 0 12500 0
vsize: 50164
[startup+669.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12074 0 0 0 66972 34 0 0 25 0 1 0 481349392 51367936 12052 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12541 12052 603 41 0 12500 0
vsize: 50164
[startup+679.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12074 0 0 0 67973 34 0 0 25 0 1 0 481349392 51367936 12052 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12541 12052 603 41 0 12500 0
vsize: 50164
[startup+690 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12074 0 0 0 68973 34 0 0 25 0 1 0 481349392 51367936 12052 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12541 12052 603 41 0 12500 0
vsize: 50164
[startup+699.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12074 0 0 0 69973 34 0 0 25 0 1 0 481349392 51367936 12052 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12541 12052 603 41 0 12500 0
vsize: 50164
[startup+709.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12074 0 0 0 70973 34 0 0 25 0 1 0 481349392 51367936 12052 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12541 12052 603 41 0 12500 0
vsize: 50164
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12228 0 0 0 71973 34 0 0 25 0 1 0 481349392 51904512 12206 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 12206 603 41 0 12631 0
vsize: 50688
[startup+729.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12228 0 0 0 72973 34 0 0 25 0 1 0 481349392 51904512 12206 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 12206 603 41 0 12631 0
vsize: 50688
[startup+739.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12228 0 0 0 73973 34 0 0 25 0 1 0 481349392 51904512 12206 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 12206 603 41 0 12631 0
vsize: 50688
[startup+749.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12228 0 0 0 74974 34 0 0 25 0 1 0 481349392 51904512 12206 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 12206 603 41 0 12631 0
vsize: 50688
[startup+759.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12228 0 0 0 75974 34 0 0 25 0 1 0 481349392 51904512 12206 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 12206 603 41 0 12631 0
vsize: 50688
[startup+769.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12229 0 0 0 76974 34 0 0 25 0 1 0 481349392 51904512 12207 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 12207 603 41 0 12631 0
vsize: 50688
[startup+779.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12231 0 0 0 77974 34 0 0 25 0 1 0 481349392 51904512 12209 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 12209 603 41 0 12631 0
vsize: 50688
[startup+789.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12331 0 0 0 78974 35 0 0 25 0 1 0 481349392 52310016 12309 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12771 12309 603 41 0 12730 0
vsize: 51084
[startup+799.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12911 0 0 0 79973 36 0 0 25 0 1 0 481349392 54751232 12889 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13367 12889 603 41 0 13326 0
vsize: 53468
[startup+809.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12911 0 0 0 80973 36 0 0 25 0 1 0 481349392 54751232 12889 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13367 12889 603 41 0 13326 0
vsize: 53468
[startup+819.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 81974 36 0 0 25 0 1 0 481349392 54751232 12890 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13367 12890 603 41 0 13326 0
vsize: 53468
[startup+829.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 82974 36 0 0 25 0 1 0 481349392 54751232 12890 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13367 12890 603 41 0 13326 0
vsize: 53468
[startup+839.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 83974 36 0 0 25 0 1 0 481349392 54751232 12890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13367 12890 603 41 0 13326 0
vsize: 53468
[startup+849.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 84974 36 0 0 25 0 1 0 481349392 54751232 12890 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13367 12890 603 41 0 13326 0
vsize: 53468
[startup+859.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 85974 36 0 0 25 0 1 0 481349392 54751232 12890 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13367 12890 603 41 0 13326 0
vsize: 53468
[startup+869.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 86974 36 0 0 25 0 1 0 481349392 54726656 12890 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13361 12890 603 41 0 13320 0
vsize: 53444
[startup+879.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 87975 36 0 0 25 0 1 0 481349392 54726656 12890 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13361 12890 603 41 0 13320 0
vsize: 53444
[startup+889.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 88975 36 0 0 25 0 1 0 481349392 54726656 12890 4294967295 134512640 134672761 3221224544 3221223728 134558875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13361 12890 603 41 0 13320 0
vsize: 53444
[startup+899.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 89975 36 0 0 25 0 1 0 481349392 54726656 12890 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13361 12890 603 41 0 13320 0
vsize: 53444
[startup+909.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12912 0 0 0 90975 36 0 0 25 0 1 0 481349392 54726656 12890 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13361 12890 603 41 0 13320 0
vsize: 53444
[startup+919.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 12913 0 0 0 91975 36 0 0 25 0 1 0 481349392 54726656 12891 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13361 12891 603 41 0 13320 0
vsize: 53444
[startup+929.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13192 0 0 0 92974 36 0 0 25 0 1 0 481349392 55939072 13170 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 13170 603 41 0 13616 0
vsize: 54628
[startup+939.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13192 0 0 0 93974 36 0 0 25 0 1 0 481349392 55939072 13170 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 13170 603 41 0 13616 0
vsize: 54628
[startup+949.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13192 0 0 0 94974 36 0 0 25 0 1 0 481349392 55939072 13170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 13170 603 41 0 13616 0
vsize: 54628
[startup+959.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13192 0 0 0 95974 36 0 0 25 0 1 0 481349392 55939072 13170 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 13170 603 41 0 13616 0
vsize: 54628
[startup+969.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13192 0 0 0 96975 36 0 0 25 0 1 0 481349392 55939072 13170 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 13170 603 41 0 13616 0
vsize: 54628
[startup+979.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13256 0 0 0 97975 37 0 0 25 0 1 0 481349392 56209408 13234 4294967295 134512640 134672761 3221224544 3221223616 134553553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13723 13234 603 41 0 13682 0
vsize: 54892
[startup+989.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13524 0 0 0 98974 37 0 0 25 0 1 0 481349392 57286656 13502 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13502 603 41 0 13945 0
vsize: 55944
[startup+999.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13524 0 0 0 99974 37 0 0 25 0 1 0 481349392 57286656 13502 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13502 603 41 0 13945 0
vsize: 55944
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13524 0 0 0 100974 37 0 0 25 0 1 0 481349392 57286656 13502 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13502 603 41 0 13945 0
vsize: 55944
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13524 0 0 0 101974 37 0 0 25 0 1 0 481349392 57286656 13502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13502 603 41 0 13945 0
vsize: 55944
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13524 0 0 0 102975 37 0 0 25 0 1 0 481349392 57286656 13502 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13502 603 41 0 13945 0
vsize: 55944
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13524 0 0 0 103975 37 0 0 25 0 1 0 481349392 57286656 13502 4294967295 134512640 134672761 3221224544 3221223728 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13502 603 41 0 13945 0
vsize: 55944
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13525 0 0 0 104975 37 0 0 25 0 1 0 481349392 57286656 13503 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13503 603 41 0 13945 0
vsize: 55944
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13525 0 0 0 105975 37 0 0 25 0 1 0 481349392 57286656 13503 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13503 603 41 0 13945 0
vsize: 55944
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13525 0 0 0 106975 37 0 0 25 0 1 0 481349392 57286656 13503 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13503 603 41 0 13945 0
vsize: 55944
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13525 0 0 0 107976 37 0 0 25 0 1 0 481349392 57286656 13503 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13503 603 41 0 13945 0
vsize: 55944
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13525 0 0 0 108976 37 0 0 25 0 1 0 481349392 57286656 13503 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13503 603 41 0 13945 0
vsize: 55944
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13525 0 0 0 109976 37 0 0 25 0 1 0 481349392 57286656 13503 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13503 603 41 0 13945 0
vsize: 55944
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 13525 0 0 0 110976 37 0 0 25 0 1 0 481349392 57286656 13503 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13986 13503 603 41 0 13945 0
vsize: 55944
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14033 0 0 0 111975 39 0 0 25 0 1 0 481349392 59314176 14011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14481 14011 603 41 0 14440 0
vsize: 57924
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14837 0 0 0 112974 40 0 0 25 0 1 0 481349392 62693376 14815 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15306 14815 603 41 0 15265 0
vsize: 61224
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14837 0 0 0 113974 40 0 0 25 0 1 0 481349392 62693376 14815 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15306 14815 603 41 0 15265 0
vsize: 61224
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14837 0 0 0 114974 40 0 0 25 0 1 0 481349392 62693376 14815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15306 14815 603 41 0 15265 0
vsize: 61224
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14837 0 0 0 115974 40 0 0 25 0 1 0 481349392 62693376 14815 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15306 14815 603 41 0 15265 0
vsize: 61224
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14837 0 0 0 116975 40 0 0 25 0 1 0 481349392 62693376 14815 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15306 14815 603 41 0 15265 0
vsize: 61224
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14837 0 0 0 117975 40 0 0 25 0 1 0 481349392 62693376 14815 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15306 14815 603 41 0 15265 0
vsize: 61224
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14837 0 0 0 118975 40 0 0 25 0 1 0 481349392 62652416 14815 4294967295 134512640 134672761 3221224544 3221223712 134561639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15296 14815 603 41 0 15255 0
vsize: 61184
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1553
Raw data (stat): 1553 (minisat+) R 1552 28099 28098 0 -1 0 14837 0 0 0 119975 40 0 0 25 0 1 0 481349392 62652416 14815 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15296 14815 603 41 0 15255 0
vsize: 61184
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1553
Raw data (stat): 1553 (minisat+) Z 1552 28099 28098 0 -1 12 14839 0 0 0 119975 43 0 0 25 0 1 0 481349392 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.03
CPU time (s): 1200.19
CPU user time (s): 1199.76
CPU system time (s): 0.434933
CPU usage (%): 100.014
Max. virtual memory (Kb): 61224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####