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/manquinho/synthesis-ptl-cmos-circuits/normalized-my_adder.opb
MD5SUM	fe8f615a95a6852516985b8e3e78bd85
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4561
Optimality of the best value was proved	NO
Number of terms in the objective function	577
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	24510
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	24510
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	577
Total number of constraints	1322
Number of constraints which are clauses	1306
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	16
Minimum length of a constraint	2
Maximum length of a constraint	17
Trace number 5211

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-13 22:32:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3639 boxname=wulflinc19 idbench=255 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fe8f615a95a6852516985b8e3e78bd85  /oldhome/oroussel/tmp/wulflinc19/normalized-my_adder.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-my_adder.opb /oldhome/oroussel/tmp/wulflinc19/normalized-my_adder.opb
IDLAUNCH: 3639
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        891604 kB
Buffers:         33656 kB
Cached:          75836 kB
SwapCached:         56 kB
Active:          46472 kB
Inactive:        66024 kB
HighTotal:      131008 kB
HighFree:        51128 kB
LowTotal:       903652 kB
LowFree:        840476 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            24928 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:52:39 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 3639 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1322 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1322     4977 |     440       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6274[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2806   maxlim: 18236   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   20918    75008 |    6972       1        7     7.0 |  0.000 % |
c |       102 |   20530    73796 |    7669      90      323     3.6 |  1.062 % |
c |       252 |   20280    72994 |    8436     231      928     4.0 |  1.710 % |
c |       477 |   20280    72994 |    9279     456     2097     4.6 |  1.710 % |
c |       816 |   20224    72811 |   10207     793     3873     4.9 |  1.887 % |
c |      1324 |   20224    72811 |   11228    1301     7239     5.6 |  1.887 % |
c |      2083 |   20176    72650 |   12351    2059    12308     6.0 |  2.064 % |
c |      3222 |   20176    72650 |   13586    3198    81377    25.4 |  2.064 % |
c |      4931 |   20176    72650 |   14945    4907    94727    19.3 |  2.064 % |
c |      7493 |   20176    72650 |   16439    7469   185023    24.8 |  2.064 % |
c |     11337 |   20176    72650 |   18083   11313   438134    38.7 |  2.064 % |
c |     17103 |   20176    72650 |   19891   17079   858838    50.3 |  2.064 % |
c |     25752 |   20176    72650 |   21881   15430   789288    51.2 |  2.064 % |
c |     38726 |   20176    72650 |   24069   16688  1422624    85.2 |  2.064 % |
c |     58188 |   20176    72650 |   26476   23825  1902638    79.9 |  2.064 % |
c |     87380 |   20176    72650 |   29123   24949  2451372    98.3 |  2.064 % |
c |    131169 |   20176    72650 |   32036   20185  3023296   149.8 |  2.064 % |
c |    196853 |   20176    72650 |   35239   26606  3535700   132.9 |  2.064 % |
c |    295379 |   20176    72650 |   38763   17929  2499636   139.4 |  2.064 % |
c |    443171 |   20176    72650 |   42640   20217  2512190   124.3 |  2.064 % |
c |    664854 |   20176    72650 |   46904   35484  5973440   168.3 |  2.064 % |
#### 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.84 0.94 0.90 2/55 26639
Raw data (stat): 26639 (runsolver) R 26638 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479572472 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99971 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 1811 0 0 0 993 5 0 0 25 0 1 0 479572472 8970240 1789 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2190 1789 603 41 0 2149 0
vsize: 8760
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 2262 0 0 0 1991 6 0 0 25 0 1 0 479572472 10846208 2240 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2648 2240 603 41 0 2607 0
vsize: 10592
[startup+30.0003 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 2933 0 0 0 2990 7 0 0 25 0 1 0 479572472 13545472 2911 4294967295 134512640 134672761 3221224560 3221223664 134554644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3307 2911 603 41 0 3266 0
vsize: 13228
[startup+40.0002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 2933 0 0 0 3990 7 0 0 25 0 1 0 479572472 13545472 2911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3307 2911 603 41 0 3266 0
vsize: 13228
[startup+50.001 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 3283 0 0 0 4989 9 0 0 25 0 1 0 479572472 15020032 3261 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3667 3261 603 41 0 3626 0
vsize: 14668
[startup+60.0008 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 3795 0 0 0 5987 10 0 0 25 0 1 0 479572472 17174528 3773 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4193 3773 603 41 0 4152 0
vsize: 16772
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 3929 0 0 0 6987 11 0 0 25 0 1 0 479572472 17707008 3907 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4323 3907 603 41 0 4282 0
vsize: 17292
[startup+80.0015 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 3999 0 0 0 7987 11 0 0 25 0 1 0 479572472 17977344 3977 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3977 603 41 0 4348 0
vsize: 17556
[startup+90.0014 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 4544 0 0 0 8986 12 0 0 25 0 1 0 479572472 20119552 4522 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4522 603 41 0 4871 0
vsize: 19648
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 4916 0 0 0 9986 13 0 0 25 0 1 0 479572472 21725184 4894 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5304 4894 603 41 0 5263 0
vsize: 21216
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 5282 0 0 0 10985 14 0 0 25 0 1 0 479572472 23199744 5260 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5664 5260 603 41 0 5623 0
vsize: 22656
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 6217 0 0 0 11982 17 0 0 25 0 1 0 479572472 27099136 6195 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6616 6195 603 41 0 6575 0
vsize: 26464
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7020 0 0 0 12981 18 0 0 25 0 1 0 479572472 30302208 6998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7398 6998 603 41 0 7357 0
vsize: 29592
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7128 0 0 0 13980 19 0 0 25 0 1 0 479572472 30707712 7106 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7497 7106 603 41 0 7456 0
vsize: 29988
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7129 0 0 0 14981 19 0 0 25 0 1 0 479572472 30707712 7107 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7497 7107 603 41 0 7456 0
vsize: 29988
[startup+160.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7162 0 0 0 15981 19 0 0 25 0 1 0 479572472 30969856 7140 4294967295 134512640 134672761 3221224560 3221223696 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7140 603 41 0 7520 0
vsize: 30244
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7162 0 0 0 16981 19 0 0 25 0 1 0 479572472 30969856 7140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7140 603 41 0 7520 0
vsize: 30244
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7162 0 0 0 17981 19 0 0 25 0 1 0 479572472 30969856 7140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7140 603 41 0 7520 0
vsize: 30244
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7163 0 0 0 18981 19 0 0 25 0 1 0 479572472 30969856 7141 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7141 603 41 0 7520 0
vsize: 30244
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7163 0 0 0 19981 19 0 0 25 0 1 0 479572472 30969856 7141 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7141 603 41 0 7520 0
vsize: 30244
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26639
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7163 0 0 0 20981 19 0 0 25 0 1 0 479572472 30969856 7141 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7141 603 41 0 7520 0
vsize: 30244
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7163 0 0 0 21981 19 0 0 25 0 1 0 479572472 30969856 7141 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7561 7141 603 41 0 7520 0
vsize: 30244
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 22980 19 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 23980 19 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223744 134559550 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 24981 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 25982 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+270.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 26982 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 27982 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 28982 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+300.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 29983 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 30983 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 31983 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 32983 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 33983 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 34984 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 35984 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 36984 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223744 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7167 0 0 0 37984 20 0 0 25 0 1 0 479572472 30969856 7145 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7561 7145 603 41 0 7520 0
vsize: 30244
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7451 0 0 0 38983 21 0 0 25 0 1 0 479572472 32186368 7429 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7858 7429 603 41 0 7817 0
vsize: 31432
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7718 0 0 0 39983 21 0 0 25 0 1 0 479572472 33259520 7696 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8120 7696 603 41 0 8079 0
vsize: 32480
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7718 0 0 0 40982 22 0 0 25 0 1 0 479572472 33259520 7696 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7696 603 41 0 8079 0
vsize: 32480
[startup+420.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 41982 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 42982 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 43983 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 44983 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 45983 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223720 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 46983 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 47983 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 48983 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 49983 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26641
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7720 0 0 0 50984 22 0 0 25 0 1 0 479572472 33259520 7698 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7698 603 41 0 8079 0
vsize: 32480
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7725 0 0 0 51984 22 0 0 25 0 1 0 479572472 33259520 7703 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7703 603 41 0 8079 0
vsize: 32480
[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7725 0 0 0 52984 22 0 0 25 0 1 0 479572472 33259520 7703 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7703 603 41 0 8079 0
vsize: 32480
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7725 0 0 0 53984 22 0 0 25 0 1 0 479572472 33259520 7703 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8120 7703 603 41 0 8079 0
vsize: 32480
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 7919 0 0 0 54984 23 0 0 25 0 1 0 479572472 34066432 7897 4294967295 134512640 134672761 3221224560 3221223664 134560364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8317 7897 603 41 0 8276 0
vsize: 33268
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8478 0 0 0 55982 25 0 0 25 0 1 0 479572472 36339712 8456 4294967295 134512640 134672761 3221224560 3221223744 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8456 603 41 0 8831 0
vsize: 35488
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8478 0 0 0 56982 25 0 0 25 0 1 0 479572472 36339712 8456 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8456 603 41 0 8831 0
vsize: 35488
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8478 0 0 0 57982 25 0 0 25 0 1 0 479572472 36339712 8456 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8456 603 41 0 8831 0
vsize: 35488
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8478 0 0 0 58982 25 0 0 25 0 1 0 479572472 36339712 8456 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8456 603 41 0 8831 0
vsize: 35488
[startup+600.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8478 0 0 0 59982 25 0 0 25 0 1 0 479572472 36339712 8456 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8456 603 41 0 8831 0
vsize: 35488
[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8478 0 0 0 60982 25 0 0 25 0 1 0 479572472 36339712 8456 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8456 603 41 0 8831 0
vsize: 35488
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8478 0 0 0 61982 26 0 0 25 0 1 0 479572472 36339712 8456 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8456 603 41 0 8831 0
vsize: 35488
[startup+630.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8482 0 0 0 62982 26 0 0 25 0 1 0 479572472 36339712 8460 4294967295 134512640 134672761 3221224560 3221223376 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8460 603 41 0 8831 0
vsize: 35488
[startup+640.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8482 0 0 0 63983 26 0 0 25 0 1 0 479572472 36339712 8460 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8460 603 41 0 8831 0
vsize: 35488
[startup+650.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8482 0 0 0 64983 26 0 0 25 0 1 0 479572472 36339712 8460 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8460 603 41 0 8831 0
vsize: 35488
[startup+660.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8482 0 0 0 65983 26 0 0 25 0 1 0 479572472 36339712 8460 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8460 603 41 0 8831 0
vsize: 35488
[startup+670.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8482 0 0 0 66983 26 0 0 25 0 1 0 479572472 36339712 8460 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8460 603 41 0 8831 0
vsize: 35488
[startup+680.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 8555 0 0 0 67983 26 0 0 25 0 1 0 479572472 36749312 8533 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8972 8533 603 41 0 8931 0
vsize: 35888
[startup+690.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 9313 0 0 0 68981 28 0 0 25 0 1 0 479572472 39813120 9291 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9720 9291 603 41 0 9679 0
vsize: 38880
[startup+700.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 9877 0 0 0 69980 30 0 0 25 0 1 0 479572472 42094592 9855 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10277 9855 603 41 0 10236 0
vsize: 41108
[startup+710.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 70978 31 0 0 25 0 1 0 479572472 43585536 10215 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10215 603 41 0 10600 0
vsize: 42564
[startup+720.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 71978 31 0 0 25 0 1 0 479572472 43585536 10215 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10215 603 41 0 10600 0
vsize: 42564
[startup+730.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 72979 31 0 0 25 0 1 0 479572472 43585536 10215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10215 603 41 0 10600 0
vsize: 42564
[startup+740.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 73979 31 0 0 25 0 1 0 479572472 43585536 10215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10215 603 41 0 10600 0
vsize: 42564
[startup+750.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 74979 32 0 0 25 0 1 0 479572472 43585536 10215 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10215 603 41 0 10600 0
vsize: 42564
[startup+760.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 75979 32 0 0 25 0 1 0 479572472 43585536 10215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10215 603 41 0 10600 0
vsize: 42564
[startup+770.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 76979 32 0 0 25 0 1 0 479572472 43585536 10215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10215 603 41 0 10600 0
vsize: 42564
[startup+780.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 77979 32 0 0 25 0 1 0 479572472 43585536 10215 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10215 603 41 0 10600 0
vsize: 42564
[startup+790.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 78979 32 0 0 25 0 1 0 479572472 43560960 10215 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10635 10215 603 41 0 10594 0
vsize: 42540
[startup+800.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 79980 32 0 0 25 0 1 0 479572472 43560960 10215 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10635 10215 603 41 0 10594 0
vsize: 42540
[startup+810.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26643
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 80980 32 0 0 25 0 1 0 479572472 43560960 10215 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10635 10215 603 41 0 10594 0
vsize: 42540
[startup+820.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 81980 32 0 0 25 0 1 0 479572472 43560960 10215 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10635 10215 603 41 0 10594 0
vsize: 42540
[startup+830.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 82980 32 0 0 25 0 1 0 479572472 43560960 10215 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10635 10215 603 41 0 10594 0
vsize: 42540
[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 83980 32 0 0 25 0 1 0 479572472 43560960 10215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10635 10215 603 41 0 10594 0
vsize: 42540
[startup+850.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 84980 32 0 0 25 0 1 0 479572472 43532288 10215 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10628 10215 603 41 0 10587 0
vsize: 42512
[startup+860.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 85981 32 0 0 25 0 1 0 479572472 43532288 10215 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10628 10215 603 41 0 10587 0
vsize: 42512
[startup+870.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 86981 32 0 0 25 0 1 0 479572472 43532288 10215 4294967295 134512640 134672761 3221224560 3221223664 134555091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10628 10215 603 41 0 10587 0
vsize: 42512
[startup+880.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 87981 32 0 0 25 0 1 0 479572472 43532288 10215 4294967295 134512640 134672761 3221224560 3221223664 134560180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10628 10215 603 41 0 10587 0
vsize: 42512
[startup+890.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 88981 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+900.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 89981 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+910.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 90981 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+920.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 91982 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+930.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 92982 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+940.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 93982 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+950.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 94982 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+960.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 95982 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+970.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 96982 32 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+980.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10237 0 0 0 97983 33 0 0 25 0 1 0 479572472 43524096 10214 4294967295 134512640 134672761 3221224560 3221223728 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10626 10214 603 41 0 10585 0
vsize: 42504
[startup+990.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 98982 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 99982 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 100982 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 101982 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223664 134560483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 102982 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 103982 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223712 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 104982 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223744 134559594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 105982 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 106983 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10241 0 0 0 107983 33 0 0 25 0 1 0 479572472 43524096 10218 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10218 603 41 0 10585 0
vsize: 42504
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10634 0 0 0 108982 34 0 0 25 0 1 0 479572472 45256704 10611 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11049 10611 603 41 0 11008 0
vsize: 44196
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10946 0 0 0 109982 35 0 0 25 0 1 0 479572472 46460928 10923 4294967295 134512640 134672761 3221224560 3221223664 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11343 10923 603 41 0 11302 0
vsize: 45372
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26645
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10946 0 0 0 110982 35 0 0 25 0 1 0 479572472 46460928 10923 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11343 10923 603 41 0 11302 0
vsize: 45372
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10946 0 0 0 111982 35 0 0 25 0 1 0 479572472 46460928 10923 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11343 10923 603 41 0 11302 0
vsize: 45372
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10946 0 0 0 112982 35 0 0 25 0 1 0 479572472 46460928 10923 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11343 10923 603 41 0 11302 0
vsize: 45372
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 10946 0 0 0 113982 35 0 0 25 0 1 0 479572472 46460928 10923 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11343 10923 603 41 0 11302 0
vsize: 45372
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 11165 0 0 0 114982 36 0 0 25 0 1 0 479572472 47407104 11142 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11574 11142 603 41 0 11533 0
vsize: 46296
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 11865 0 0 0 115979 38 0 0 25 0 1 0 479572472 50233344 11842 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12264 11842 603 41 0 12223 0
vsize: 49056
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 12574 0 0 0 116978 40 0 0 25 0 1 0 479572472 53174272 12551 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12982 12551 603 41 0 12941 0
vsize: 51928
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 13230 0 0 0 117976 42 0 0 25 0 1 0 479572472 55869440 13207 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13640 13207 603 41 0 13599 0
vsize: 54560
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 13846 0 0 0 118975 44 0 0 25 0 1 0 479572472 58413056 13823 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14261 13823 603 41 0 14220 0
vsize: 57044
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26647
Raw data (stat): 26639 (minisat+) R 26638 22929 22928 0 -1 0 14415 0 0 0 119972 46 0 0 25 0 1 0 479572472 60817408 14392 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14848 14392 603 41 0 14807 0
vsize: 59392
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 26647
Raw data (stat): 26639 (minisat+) Z 26638 22929 22928 0 -1 12 14418 0 0 0 119973 49 0 0 25 0 1 0 479572472 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.22
CPU user time (s): 1199.73
CPU system time (s): 0.491925
CPU usage (%): 100.012
Max. virtual memory (Kb): 59392
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####