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/primes-dimacs-cnf/normalized-ii8a3.opb
MD5SUM	a430664a9b4f203a5896b33ca2b0e0e5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	528
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	528
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	528
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02384
Number of variables	528
Total number of constraints	1816
Number of constraints which are clauses	1816
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 5888

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-14 02:11:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4301 boxname=wulflinc23 idbench=165 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a430664a9b4f203a5896b33ca2b0e0e5  /oldhome/oroussel/tmp/wulflinc23/normalized-ii8a3.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-ii8a3.opb /oldhome/oroussel/tmp/wulflinc23/normalized-ii8a3.opb
IDLAUNCH: 4301
/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:        893608 kB
Buffers:         34880 kB
Cached:          63324 kB
SwapCached:        192 kB
Active:          52984 kB
Inactive:        48252 kB
HighTotal:      131008 kB
HighFree:        63924 kB
LowTotal:       903652 kB
LowFree:        829684 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34208 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:31:24 (client local time) WITH STATUS 10 IN 1200.04 SECONDS
stats: 4301 7 1200.04 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1816 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 |    1816     4536 |     605       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23592     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   29165    68520 |    9721       3       16     5.3 |  0.000 % |
c ==============================================================================
c [1mFound solution: 210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        59 |   29396    69141 |    9798      58      792    13.7 |  0.000 % |
c |       159 |   29373    69094 |   10777     157     5757    36.7 |  0.383 % |
c |       309 |   29326    68997 |   11855     305    12018    39.4 |  0.516 % |
c |       534 |   28837    67952 |   13041     517    17976    34.8 |  1.995 % |
c ==============================================================================
c [1mFound solution: 204[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       621 |   28880    68089 |    9626     588    18176    30.9 |  1.995 % |
c |       721 |   28880    68089 |   10588     688    22308    32.4 |  2.200 % |
c |       871 |   28524    67303 |   11647     827    25164    30.4 |  3.340 % |
c |      1097 |   28524    67303 |   12812    1053    42619    40.5 |  3.340 % |
c |      1435 |   28524    67303 |   14093    1391    53572    38.5 |  3.340 % |
c ==============================================================================
c [1mFound solution: 199[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1910 |   28602    67526 |    9534    1866    63598    34.1 |  3.340 % |
c |      2010 |   28318    66912 |   10487    1959    66161    33.8 |  4.209 % |
c |      2161 |   28233    66721 |   11536    2108    68666    32.6 |  4.489 % |
c |      2387 |   28233    66721 |   12689    2334    80278    34.4 |  4.489 % |
c |      2726 |   28092    66412 |   13958    2670    97944    36.7 |  4.933 % |
c |      3232 |   27650    65426 |   15354    3164   139189    44.0 |  6.371 % |
c |      3992 |   27650    65426 |   16890    3924   180674    46.0 |  6.371 % |
c |      5136 |   27551    65211 |   18579    5065   211969    41.8 |  6.673 % |
c ==============================================================================
c [1mFound solution: 192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6518 |   27558    65253 |    9186    6436   265899    41.3 |  6.673 % |
c |      6619 |   27519    65166 |   10104    6536   269336    41.2 |  7.104 % |
c |      6769 |   27415    64938 |   11115    6684   274644    41.1 |  7.431 % |
c |      6994 |   27379    64854 |   12226    6897   277613    40.3 |  7.557 % |
c |      7331 |   27379    64854 |   13449    7234   295109    40.8 |  7.557 % |
c |      7838 |   27325    64734 |   14794    7535   302474    40.1 |  7.721 % |
c |      8597 |   27274    64621 |   16273    8293   341703    41.2 |  7.884 % |
c |      9736 |   27274    64621 |   17900    9432   369370    39.2 |  7.884 % |
c |     11444 |   27232    64533 |   19691   11138   486622    43.7 |  8.005 % |
c |     14007 |   27151    64356 |   21660   13694   628930    45.9 |  8.253 % |
c |     17851 |   27151    64356 |   23826   17538   912902    52.1 |  8.253 % |
c |     23619 |   27118    64281 |   26208   23271  1310002    56.3 |  8.364 % |
c |     32268 |   27118    64281 |   28829   16325   870814    53.3 |  8.364 % |
c |     45244 |   27118    64281 |   31712   29301  1724772    58.9 |  8.364 % |
c |     64705 |   27024    64061 |   34883   29562  1535665    51.9 |  8.696 % |
c |     93897 |   27024    64061 |   38372   36552  1736312    47.5 |  8.696 % |
c |    137686 |   27024    64061 |   42209   32006  1723902    53.9 |  8.696 % |
c |    203370 |   26915    63818 |   46430   41295  2182791    52.9 |  9.043 % |
c |    301896 |   26810    63575 |   51073   47594  2455983    51.6 |  9.407 % |
#### 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.91 0.95 0.90 2/54 7470
Raw data (stat): 7470 (runsolver) R 7469 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480888810 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 2152 0 0 0 994 4 0 0 25 0 1 0 480888810 11112448 2069 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2713 2069 603 41 0 2672 0
vsize: 10852
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 2418 0 0 0 1993 5 0 0 25 0 1 0 480888810 12103680 2335 4294967295 134512640 134672761 3221224560 3221223664 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2955 2335 603 41 0 2914 0
vsize: 11820
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 2671 0 0 0 2991 6 0 0 25 0 1 0 480888810 13160448 2588 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3213 2588 603 41 0 3172 0
vsize: 12852
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 2967 0 0 0 3990 8 0 0 25 0 1 0 480888810 14442496 2884 4294967295 134512640 134672761 3221224560 3221223728 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3526 2884 603 41 0 3485 0
vsize: 14104
[startup+50.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3228 0 0 0 4988 10 0 0 25 0 1 0 480888810 15503360 3145 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3785 3145 603 41 0 3744 0
vsize: 15140
[startup+60.0037 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3464 0 0 0 5986 11 0 0 25 0 1 0 480888810 16433152 3381 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4012 3381 603 41 0 3971 0
vsize: 16048
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3653 0 0 0 6985 12 0 0 25 0 1 0 480888810 17227776 3570 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4206 3570 603 41 0 4165 0
vsize: 16824
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3859 0 0 0 7984 14 0 0 25 0 1 0 480888810 18026496 3776 4294967295 134512640 134672761 3221224560 3221223664 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4401 3776 603 41 0 4360 0
vsize: 17604
[startup+90.0046 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3859 0 0 0 8984 14 0 0 25 0 1 0 480888810 18026496 3776 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4401 3776 603 41 0 4360 0
vsize: 17604
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3859 0 0 0 9984 14 0 0 25 0 1 0 480888810 18026496 3776 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4401 3776 603 41 0 4360 0
vsize: 17604
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3859 0 0 0 10983 14 0 0 25 0 1 0 480888810 18026496 3776 4294967295 134512640 134672761 3221224560 3221223712 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4401 3776 603 41 0 4360 0
vsize: 17604
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3859 0 0 0 11983 15 0 0 25 0 1 0 480888810 18026496 3776 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4401 3776 603 41 0 4360 0
vsize: 17604
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 3916 0 0 0 12983 15 0 0 25 0 1 0 480888810 18288640 3833 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4465 3833 603 41 0 4424 0
vsize: 17860
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4088 0 0 0 13982 16 0 0 25 0 1 0 480888810 18948096 4005 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4626 4005 603 41 0 4585 0
vsize: 18504
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4264 0 0 0 14981 16 0 0 25 0 1 0 480888810 19877888 4181 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4853 4181 603 41 0 4812 0
vsize: 19412
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4411 0 0 0 15980 18 0 0 25 0 1 0 480888810 20406272 4328 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4982 4328 603 41 0 4941 0
vsize: 19928
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4421 0 0 0 16980 18 0 0 25 0 1 0 480888810 20537344 4338 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5014 4338 603 41 0 4973 0
vsize: 20056
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4421 0 0 0 17979 18 0 0 25 0 1 0 480888810 20537344 4338 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5014 4338 603 41 0 4973 0
vsize: 20056
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4433 0 0 0 18979 18 0 0 25 0 1 0 480888810 20537344 4350 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5014 4350 603 41 0 4973 0
vsize: 20056
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4434 0 0 0 19979 18 0 0 25 0 1 0 480888810 20537344 4351 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5014 4351 603 41 0 4973 0
vsize: 20056
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4440 0 0 0 20978 19 0 0 25 0 1 0 480888810 20672512 4357 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5047 4357 603 41 0 5006 0
vsize: 20188
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4448 0 0 0 21978 19 0 0 25 0 1 0 480888810 20672512 4365 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5047 4365 603 41 0 5006 0
vsize: 20188
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4459 0 0 0 22978 19 0 0 25 0 1 0 480888810 20672512 4376 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5047 4376 603 41 0 5006 0
vsize: 20188
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4472 0 0 0 23978 20 0 0 25 0 1 0 480888810 20815872 4389 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4389 603 41 0 5041 0
vsize: 20328
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4472 0 0 0 24977 20 0 0 25 0 1 0 480888810 20815872 4389 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4389 603 41 0 5041 0
vsize: 20328
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4472 0 0 0 25977 20 0 0 25 0 1 0 480888810 20815872 4389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4389 603 41 0 5041 0
vsize: 20328
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4472 0 0 0 26976 21 0 0 25 0 1 0 480888810 20815872 4389 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4389 603 41 0 5041 0
vsize: 20328
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4472 0 0 0 27976 21 0 0 25 0 1 0 480888810 20815872 4389 4294967295 134512640 134672761 3221224560 3221223568 1075351041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4389 603 41 0 5041 0
vsize: 20328
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4472 0 0 0 28976 21 0 0 25 0 1 0 480888810 20815872 4389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4389 603 41 0 5041 0
vsize: 20328
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4472 0 0 0 29975 22 0 0 25 0 1 0 480888810 20815872 4389 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4389 603 41 0 5041 0
vsize: 20328
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4482 0 0 0 30975 22 0 0 25 0 1 0 480888810 20815872 4399 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4399 603 41 0 5041 0
vsize: 20328
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4488 0 0 0 31974 23 0 0 25 0 1 0 480888810 20815872 4405 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5082 4405 603 41 0 5041 0
vsize: 20328
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4530 0 0 0 32974 23 0 0 25 0 1 0 480888810 20946944 4447 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5114 4447 603 41 0 5073 0
vsize: 20456
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4651 0 0 0 33973 24 0 0 25 0 1 0 480888810 21471232 4568 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5242 4568 603 41 0 5201 0
vsize: 20968
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4651 0 0 0 34973 24 0 0 25 0 1 0 480888810 21471232 4568 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5242 4568 603 41 0 5201 0
vsize: 20968
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4654 0 0 0 35972 25 0 0 25 0 1 0 480888810 21471232 4571 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5242 4571 603 41 0 5201 0
vsize: 20968
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4659 0 0 0 36972 25 0 0 25 0 1 0 480888810 21471232 4576 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5242 4576 603 41 0 5201 0
vsize: 20968
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4677 0 0 0 37971 26 0 0 25 0 1 0 480888810 21610496 4594 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5276 4594 603 41 0 5235 0
vsize: 21104
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4682 0 0 0 38971 26 0 0 25 0 1 0 480888810 21610496 4599 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5276 4599 603 41 0 5235 0
vsize: 21104
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4687 0 0 0 39971 26 0 0 25 0 1 0 480888810 21610496 4604 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5276 4604 603 41 0 5235 0
vsize: 21104
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4715 0 0 0 40970 27 0 0 25 0 1 0 480888810 21753856 4632 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5311 4632 603 41 0 5270 0
vsize: 21244
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4716 0 0 0 41970 27 0 0 25 0 1 0 480888810 21753856 4633 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5311 4633 603 41 0 5270 0
vsize: 21244
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4828 0 0 0 42969 28 0 0 25 0 1 0 480888810 22282240 4745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5440 4745 603 41 0 5399 0
vsize: 21760
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4891 0 0 0 43968 29 0 0 25 0 1 0 480888810 22544384 4808 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5504 4808 603 41 0 5463 0
vsize: 22016
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4894 0 0 0 44968 29 0 0 25 0 1 0 480888810 22544384 4811 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5504 4811 603 41 0 5463 0
vsize: 22016
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4894 0 0 0 45968 29 0 0 25 0 1 0 480888810 22544384 4811 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5504 4811 603 41 0 5463 0
vsize: 22016
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4895 0 0 0 46968 30 0 0 25 0 1 0 480888810 22544384 4812 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5504 4812 603 41 0 5463 0
vsize: 22016
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4905 0 0 0 47968 30 0 0 25 0 1 0 480888810 22544384 4822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5504 4822 603 41 0 5463 0
vsize: 22016
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4906 0 0 0 48967 31 0 0 25 0 1 0 480888810 22544384 4823 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5504 4823 603 41 0 5463 0
vsize: 22016
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4906 0 0 0 49967 31 0 0 25 0 1 0 480888810 22544384 4823 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5504 4823 603 41 0 5463 0
vsize: 22016
[startup+510.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 4917 0 0 0 50966 31 0 0 25 0 1 0 480888810 22675456 4834 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5536 4834 603 41 0 5495 0
vsize: 22144
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5078 0 0 0 51965 32 0 0 25 0 1 0 480888810 23343104 4995 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5699 4995 603 41 0 5658 0
vsize: 22796
[startup+530.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5239 0 0 0 52964 33 0 0 25 0 1 0 480888810 24006656 5156 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5861 5156 603 41 0 5820 0
vsize: 23444
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5398 0 0 0 53963 34 0 0 25 0 1 0 480888810 24539136 5315 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5315 603 41 0 5950 0
vsize: 23964
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5398 0 0 0 54963 34 0 0 25 0 1 0 480888810 24539136 5315 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5315 603 41 0 5950 0
vsize: 23964
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5398 0 0 0 55963 34 0 0 25 0 1 0 480888810 24539136 5315 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5315 603 41 0 5950 0
vsize: 23964
[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5404 0 0 0 56963 35 0 0 25 0 1 0 480888810 24678400 5321 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6025 5321 603 41 0 5984 0
vsize: 24100
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5407 0 0 0 57963 35 0 0 25 0 1 0 480888810 24678400 5324 4294967295 134512640 134672761 3221224560 3221223744 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6025 5324 603 41 0 5984 0
vsize: 24100
[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5407 0 0 0 58963 35 0 0 25 0 1 0 480888810 24678400 5324 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6025 5324 603 41 0 5984 0
vsize: 24100
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5411 0 0 0 59962 35 0 0 25 0 1 0 480888810 24678400 5328 4294967295 134512640 134672761 3221224560 3221223664 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6025 5328 603 41 0 5984 0
vsize: 24100
[startup+610.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5411 0 0 0 60962 36 0 0 25 0 1 0 480888810 24678400 5328 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6025 5328 603 41 0 5984 0
vsize: 24100
[startup+620.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5424 0 0 0 61961 36 0 0 25 0 1 0 480888810 24678400 5341 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6025 5341 603 41 0 5984 0
vsize: 24100
[startup+630.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5434 0 0 0 62961 36 0 0 25 0 1 0 480888810 24825856 5351 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6061 5351 603 41 0 6020 0
vsize: 24244
[startup+640.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5439 0 0 0 63961 36 0 0 25 0 1 0 480888810 24825856 5356 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6061 5356 603 41 0 6020 0
vsize: 24244
[startup+650.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5569 0 0 0 64961 37 0 0 25 0 1 0 480888810 25350144 5486 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6189 5486 603 41 0 6148 0
vsize: 24756
[startup+660.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5640 0 0 0 65961 37 0 0 25 0 1 0 480888810 25612288 5557 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5557 603 41 0 6212 0
vsize: 25012
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5645 0 0 0 66960 38 0 0 25 0 1 0 480888810 25612288 5562 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5562 603 41 0 6212 0
vsize: 25012
[startup+680.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5645 0 0 0 67960 38 0 0 25 0 1 0 480888810 25612288 5562 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5562 603 41 0 6212 0
vsize: 25012
[startup+690.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5646 0 0 0 68959 38 0 0 25 0 1 0 480888810 25612288 5563 4294967295 134512640 134672761 3221224560 3221223744 134558371 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5563 603 41 0 6212 0
vsize: 25012
[startup+700.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5646 0 0 0 69959 39 0 0 25 0 1 0 480888810 25612288 5563 4294967295 134512640 134672761 3221224560 3221223744 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5563 603 41 0 6212 0
vsize: 25012
[startup+710.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5646 0 0 0 70959 39 0 0 25 0 1 0 480888810 25612288 5563 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5563 603 41 0 6212 0
vsize: 25012
[startup+720.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5646 0 0 0 71959 39 0 0 25 0 1 0 480888810 25612288 5563 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5563 603 41 0 6212 0
vsize: 25012
[startup+730.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5651 0 0 0 72958 40 0 0 25 0 1 0 480888810 25612288 5568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5568 603 41 0 6212 0
vsize: 25012
[startup+740.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5651 0 0 0 73958 40 0 0 25 0 1 0 480888810 25612288 5568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5568 603 41 0 6212 0
vsize: 25012
[startup+750.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5651 0 0 0 74957 41 0 0 25 0 1 0 480888810 25612288 5568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6253 5568 603 41 0 6212 0
vsize: 25012
[startup+760.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5657 0 0 0 75957 41 0 0 25 0 1 0 480888810 25772032 5574 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6292 5574 603 41 0 6251 0
vsize: 25168
[startup+770.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5659 0 0 0 76957 42 0 0 25 0 1 0 480888810 25772032 5576 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6292 5576 603 41 0 6251 0
vsize: 25168
[startup+780.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5661 0 0 0 77956 42 0 0 25 0 1 0 480888810 25772032 5578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6292 5578 603 41 0 6251 0
vsize: 25168
[startup+790.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5710 0 0 0 78955 43 0 0 25 0 1 0 480888810 25903104 5627 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6324 5627 603 41 0 6283 0
vsize: 25296
[startup+800.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5710 0 0 0 79955 43 0 0 25 0 1 0 480888810 25903104 5627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6324 5627 603 41 0 6283 0
vsize: 25296
[startup+810.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5712 0 0 0 80955 43 0 0 25 0 1 0 480888810 25903104 5629 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6324 5629 603 41 0 6283 0
vsize: 25296
[startup+820.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5721 0 0 0 81954 44 0 0 25 0 1 0 480888810 25903104 5638 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6324 5638 603 41 0 6283 0
vsize: 25296
[startup+830.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5735 0 0 0 82954 44 0 0 25 0 1 0 480888810 26095616 5652 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5652 603 41 0 6330 0
vsize: 25484
[startup+840.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5736 0 0 0 83954 44 0 0 25 0 1 0 480888810 26095616 5653 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5653 603 41 0 6330 0
vsize: 25484
[startup+850.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5736 0 0 0 84954 44 0 0 25 0 1 0 480888810 26095616 5653 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5653 603 41 0 6330 0
vsize: 25484
[startup+860.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5736 0 0 0 85953 45 0 0 25 0 1 0 480888810 26095616 5653 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5653 603 41 0 6330 0
vsize: 25484
[startup+870.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5736 0 0 0 86953 45 0 0 25 0 1 0 480888810 26095616 5653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5653 603 41 0 6330 0
vsize: 25484
[startup+880.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5737 0 0 0 87952 46 0 0 25 0 1 0 480888810 26095616 5654 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5654 603 41 0 6330 0
vsize: 25484
[startup+890.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5749 0 0 0 88952 46 0 0 25 0 1 0 480888810 26095616 5666 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5666 603 41 0 6330 0
vsize: 25484
[startup+900.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5758 0 0 0 89952 46 0 0 25 0 1 0 480888810 26095616 5675 4294967295 134512640 134672761 3221224560 3221223736 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6371 5675 603 41 0 6330 0
vsize: 25484
[startup+910.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5793 0 0 0 90952 46 0 0 25 0 1 0 480888810 26361856 5710 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5710 603 41 0 6395 0
vsize: 25744
[startup+920.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5799 0 0 0 91951 47 0 0 25 0 1 0 480888810 26361856 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5716 603 41 0 6395 0
vsize: 25744
[startup+930.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5804 0 0 0 92951 47 0 0 25 0 1 0 480888810 26361856 5721 4294967295 134512640 134672761 3221224560 3221223728 134561278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5721 603 41 0 6395 0
vsize: 25744
[startup+940.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5806 0 0 0 93951 47 0 0 25 0 1 0 480888810 26361856 5723 4294967295 134512640 134672761 3221224560 3221223752 134554697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5723 603 41 0 6395 0
vsize: 25744
[startup+950.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5807 0 0 0 94950 47 0 0 25 0 1 0 480888810 26361856 5724 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5724 603 41 0 6395 0
vsize: 25744
[startup+960.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5812 0 0 0 95950 48 0 0 25 0 1 0 480888810 26361856 5729 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6436 5729 603 41 0 6395 0
vsize: 25744
[startup+970.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5812 0 0 0 96950 48 0 0 25 0 1 0 480888810 26361856 5729 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5729 603 41 0 6395 0
vsize: 25744
[startup+980.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5813 0 0 0 97951 48 0 0 25 0 1 0 480888810 26361856 5730 4294967295 134512640 134672761 3221224560 3221223744 134559351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5730 603 41 0 6395 0
vsize: 25744
[startup+990.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5814 0 0 0 98951 48 0 0 25 0 1 0 480888810 26361856 5731 4294967295 134512640 134672761 3221224560 3221223744 134558658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5731 603 41 0 6395 0
vsize: 25744
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5815 0 0 0 99951 48 0 0 25 0 1 0 480888810 26361856 5732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5732 603 41 0 6395 0
vsize: 25744
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5815 0 0 0 100951 48 0 0 25 0 1 0 480888810 26361856 5732 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5732 603 41 0 6395 0
vsize: 25744
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5815 0 0 0 101952 48 0 0 25 0 1 0 480888810 26361856 5732 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5732 603 41 0 6395 0
vsize: 25744
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5829 0 0 0 102952 48 0 0 25 0 1 0 480888810 26497024 5746 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6469 5746 603 41 0 6428 0
vsize: 25876
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5870 0 0 0 103952 48 0 0 25 0 1 0 480888810 26628096 5787 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6501 5787 603 41 0 6460 0
vsize: 26004
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5874 0 0 0 104952 48 0 0 25 0 1 0 480888810 26628096 5791 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6501 5791 603 41 0 6460 0
vsize: 26004
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5874 0 0 0 105952 48 0 0 25 0 1 0 480888810 26628096 5791 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6501 5791 603 41 0 6460 0
vsize: 26004
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5874 0 0 0 106952 48 0 0 25 0 1 0 480888810 26628096 5791 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6501 5791 603 41 0 6460 0
vsize: 26004
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5874 0 0 0 107952 48 0 0 25 0 1 0 480888810 26628096 5791 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6501 5791 603 41 0 6460 0
vsize: 26004
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5874 0 0 0 108953 48 0 0 25 0 1 0 480888810 26628096 5791 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6501 5791 603 41 0 6460 0
vsize: 26004
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5879 0 0 0 109953 48 0 0 25 0 1 0 480888810 26775552 5796 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6537 5796 603 41 0 6496 0
vsize: 26148
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5882 0 0 0 110953 48 0 0 25 0 1 0 480888810 26775552 5799 4294967295 134512640 134672761 3221224560 3221223728 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6537 5799 603 41 0 6496 0
vsize: 26148
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5883 0 0 0 111953 48 0 0 25 0 1 0 480888810 26775552 5800 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6537 5800 603 41 0 6496 0
vsize: 26148
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5885 0 0 0 112953 48 0 0 25 0 1 0 480888810 26775552 5802 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6537 5802 603 41 0 6496 0
vsize: 26148
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5885 0 0 0 113954 48 0 0 25 0 1 0 480888810 26775552 5802 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6537 5802 603 41 0 6496 0
vsize: 26148
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5888 0 0 0 114954 48 0 0 25 0 1 0 480888810 26775552 5805 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6537 5805 603 41 0 6496 0
vsize: 26148
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5901 0 0 0 115953 48 0 0 25 0 1 0 480888810 26775552 5818 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6537 5818 603 41 0 6496 0
vsize: 26148
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5916 0 0 0 116953 48 0 0 25 0 1 0 480888810 26955776 5833 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6581 5833 603 41 0 6540 0
vsize: 26324
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5928 0 0 0 117953 48 0 0 25 0 1 0 480888810 26955776 5845 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6581 5845 603 41 0 6540 0
vsize: 26324
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5967 0 0 0 118953 48 0 0 25 0 1 0 480888810 27086848 5884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6613 5884 603 41 0 6572 0
vsize: 26452
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7470
Raw data (stat): 7470 (minisat+) R 7469 3260 3259 0 -1 0 5967 0 0 0 119953 48 0 0 25 0 1 0 480888810 27086848 5884 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6613 5884 603 41 0 6572 0
vsize: 26452
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7470
Raw data (stat): 7470 (minisat+) Z 7469 3260 3259 0 -1 12 5970 0 0 0 119954 49 0 0 25 0 1 0 480888810 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: 10
Real time (s): 1200.06
CPU time (s): 1200.04
CPU user time (s): 1199.54
CPU system time (s): 0.499924
CPU usage (%): 99.9983
Max. virtual memory (Kb): 26452
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####