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 4917

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        912352 kB
Buffers:         34556 kB
Cached:          49372 kB
SwapCached:        392 kB
Active:          45536 kB
Inactive:        41632 kB
HighTotal:      131008 kB
HighFree:        77924 kB
LowTotal:       903652 kB
LowFree:        834428 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29512 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:10:16 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 1481 7 1200.17 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.84 0.94 0.90 2/54 25612
Raw data (stat): 25612 (runsolver) R 25611 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478950079 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 2177 0 0 0 993 4 0 0 25 0 1 0 478950079 11087872 2089 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2707 2089 603 41 0 2666 0
vsize: 10828
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 2444 0 0 0 1992 5 0 0 25 0 1 0 478950079 12165120 2356 4294967295 134512640 134672761 3221224640 3221223744 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2970 2356 603 41 0 2929 0
vsize: 11880
[startup+30.0028 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 2696 0 0 0 2990 6 0 0 25 0 1 0 478950079 13234176 2608 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3231 2608 603 41 0 3190 0
vsize: 12924
[startup+40.0034 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 2999 0 0 0 3988 8 0 0 25 0 1 0 478950079 14512128 2911 4294967295 134512640 134672761 3221224640 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3543 2911 603 41 0 3502 0
vsize: 14172
[startup+50.004 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3263 0 0 0 4987 9 0 0 25 0 1 0 478950079 15581184 3175 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3804 3175 603 41 0 3763 0
vsize: 15216
[startup+60.0043 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3499 0 0 0 5986 10 0 0 25 0 1 0 478950079 16510976 3411 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4031 3411 603 41 0 3990 0
vsize: 16124
[startup+70.0042 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3692 0 0 0 6986 11 0 0 25 0 1 0 478950079 17305600 3604 4294967295 134512640 134672761 3221224640 3221223824 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4225 3604 603 41 0 4184 0
vsize: 16900
[startup+80.0049 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3883 0 0 0 7985 11 0 0 25 0 1 0 478950079 18100224 3795 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4419 3795 603 41 0 4378 0
vsize: 17676
[startup+90.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3883 0 0 0 8986 11 0 0 25 0 1 0 478950079 18100224 3795 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4419 3795 603 41 0 4378 0
vsize: 17676
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3886 0 0 0 9986 11 0 0 25 0 1 0 478950079 18100224 3798 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4419 3798 603 41 0 4378 0
vsize: 17676
[startup+110.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3887 0 0 0 10986 11 0 0 25 0 1 0 478950079 18100224 3799 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4419 3799 603 41 0 4378 0
vsize: 17676
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3890 0 0 0 11986 11 0 0 25 0 1 0 478950079 18100224 3802 4294967295 134512640 134672761 3221224640 3221223744 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4419 3802 603 41 0 4378 0
vsize: 17676
[startup+130.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 3975 0 0 0 12986 11 0 0 25 0 1 0 478950079 18497536 3887 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4516 3887 603 41 0 4475 0
vsize: 18064
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4141 0 0 0 13984 13 0 0 25 0 1 0 478950079 19161088 4053 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4678 4053 603 41 0 4637 0
vsize: 18712
[startup+150.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4298 0 0 0 14984 13 0 0 25 0 1 0 478950079 19963904 4210 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4210 603 41 0 4833 0
vsize: 19496
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4445 0 0 0 15984 14 0 0 25 0 1 0 478950079 20635648 4357 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4357 603 41 0 4997 0
vsize: 20152
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4446 0 0 0 16984 14 0 0 25 0 1 0 478950079 20635648 4358 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4358 603 41 0 4997 0
vsize: 20152
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4447 0 0 0 17984 14 0 0 25 0 1 0 478950079 20635648 4359 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4359 603 41 0 4997 0
vsize: 20152
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4460 0 0 0 18984 14 0 0 25 0 1 0 478950079 20635648 4372 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4372 603 41 0 4997 0
vsize: 20152
[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4467 0 0 0 19984 14 0 0 25 0 1 0 478950079 20635648 4379 4294967295 134512640 134672761 3221224640 3221223824 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4379 603 41 0 4997 0
vsize: 20152
[startup+210.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4476 0 0 0 20985 14 0 0 25 0 1 0 478950079 20635648 4388 4294967295 134512640 134672761 3221224640 3221223744 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5038 4388 603 41 0 4997 0
vsize: 20152
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4486 0 0 0 21985 14 0 0 25 0 1 0 478950079 20783104 4398 4294967295 134512640 134672761 3221224640 3221223808 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4398 603 41 0 5033 0
vsize: 20296
[startup+230.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4494 0 0 0 22985 14 0 0 25 0 1 0 478950079 20783104 4406 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4406 603 41 0 5033 0
vsize: 20296
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4502 0 0 0 23985 14 0 0 25 0 1 0 478950079 20783104 4414 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4414 603 41 0 5033 0
vsize: 20296
[startup+250.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4502 0 0 0 24985 14 0 0 25 0 1 0 478950079 20783104 4414 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4414 603 41 0 5033 0
vsize: 20296
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4502 0 0 0 25985 14 0 0 25 0 1 0 478950079 20783104 4414 4294967295 134512640 134672761 3221224640 3221223776 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4414 603 41 0 5033 0
vsize: 20296
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4502 0 0 0 26986 14 0 0 25 0 1 0 478950079 20783104 4414 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4414 603 41 0 5033 0
vsize: 20296
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4502 0 0 0 27986 14 0 0 25 0 1 0 478950079 20783104 4414 4294967295 134512640 134672761 3221224640 3221223744 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4414 603 41 0 5033 0
vsize: 20296
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4502 0 0 0 28986 14 0 0 25 0 1 0 478950079 20783104 4414 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4414 603 41 0 5033 0
vsize: 20296
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4507 0 0 0 29986 14 0 0 25 0 1 0 478950079 20783104 4419 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4419 603 41 0 5033 0
vsize: 20296
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4508 0 0 0 30986 14 0 0 25 0 1 0 478950079 20783104 4420 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5074 4420 603 41 0 5033 0
vsize: 20296
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4514 0 0 0 31987 14 0 0 25 0 1 0 478950079 20946944 4426 4294967295 134512640 134672761 3221224640 3221223736 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5114 4426 603 41 0 5073 0
vsize: 20456
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4630 0 0 0 32986 14 0 0 25 0 1 0 478950079 21344256 4542 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5211 4542 603 41 0 5170 0
vsize: 20844
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4678 0 0 0 33986 15 0 0 25 0 1 0 478950079 21475328 4590 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5243 4590 603 41 0 5202 0
vsize: 20972
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4680 0 0 0 34986 15 0 0 25 0 1 0 478950079 21614592 4592 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5277 4592 603 41 0 5236 0
vsize: 21108
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4683 0 0 0 35987 15 0 0 25 0 1 0 478950079 21614592 4595 4294967295 134512640 134672761 3221224640 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5277 4595 603 41 0 5236 0
vsize: 21108
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4691 0 0 0 36987 15 0 0 25 0 1 0 478950079 21614592 4603 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5277 4603 603 41 0 5236 0
vsize: 21108
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4709 0 0 0 37987 15 0 0 25 0 1 0 478950079 21753856 4621 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5311 4621 603 41 0 5270 0
vsize: 21244
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4711 0 0 0 38987 15 0 0 25 0 1 0 478950079 21753856 4623 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5311 4623 603 41 0 5270 0
vsize: 21244
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4729 0 0 0 39987 15 0 0 25 0 1 0 478950079 21753856 4641 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5311 4641 603 41 0 5270 0
vsize: 21244
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4740 0 0 0 40987 15 0 0 25 0 1 0 478950079 21909504 4652 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5349 4652 603 41 0 5308 0
vsize: 21396
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4796 0 0 0 41987 15 0 0 25 0 1 0 478950079 22040576 4708 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5381 4708 603 41 0 5340 0
vsize: 21524
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4918 0 0 0 42987 16 0 0 25 0 1 0 478950079 22568960 4830 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5510 4830 603 41 0 5469 0
vsize: 22040
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4918 0 0 0 43987 16 0 0 25 0 1 0 478950079 22568960 4830 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5510 4830 603 41 0 5469 0
vsize: 22040
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4920 0 0 0 44987 16 0 0 25 0 1 0 478950079 22568960 4832 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5510 4832 603 41 0 5469 0
vsize: 22040
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4920 0 0 0 45988 16 0 0 25 0 1 0 478950079 22568960 4832 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5510 4832 603 41 0 5469 0
vsize: 22040
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4920 0 0 0 46988 16 0 0 25 0 1 0 478950079 22568960 4832 4294967295 134512640 134672761 3221224640 3221223776 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5510 4832 603 41 0 5469 0
vsize: 22040
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4931 0 0 0 47988 16 0 0 25 0 1 0 478950079 22712320 4843 4294967295 134512640 134672761 3221224640 3221223744 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5545 4843 603 41 0 5504 0
vsize: 22180
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4931 0 0 0 48987 16 0 0 25 0 1 0 478950079 22712320 4843 4294967295 134512640 134672761 3221224640 3221223776 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5545 4843 603 41 0 5504 0
vsize: 22180
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 4932 0 0 0 49988 16 0 0 25 0 1 0 478950079 22712320 4844 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5545 4844 603 41 0 5504 0
vsize: 22180
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5066 0 0 0 50988 16 0 0 25 0 1 0 478950079 23244800 4978 4294967295 134512640 134672761 3221224640 3221223776 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5675 4978 603 41 0 5634 0
vsize: 22700
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5224 0 0 0 51987 17 0 0 25 0 1 0 478950079 23912448 5136 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5838 5136 603 41 0 5797 0
vsize: 23352
[startup+530.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5392 0 0 0 52987 17 0 0 25 0 1 0 478950079 24580096 5304 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6001 5304 603 41 0 5960 0
vsize: 24004
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5418 0 0 0 53987 17 0 0 25 0 1 0 478950079 24580096 5330 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6001 5330 603 41 0 5960 0
vsize: 24004
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5418 0 0 0 54987 17 0 0 25 0 1 0 478950079 24580096 5330 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6001 5330 603 41 0 5960 0
vsize: 24004
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5421 0 0 0 55987 17 0 0 25 0 1 0 478950079 24727552 5333 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6037 5333 603 41 0 5996 0
vsize: 24148
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5428 0 0 0 56988 17 0 0 25 0 1 0 478950079 24727552 5340 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6037 5340 603 41 0 5996 0
vsize: 24148
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25612
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5428 0 0 0 57988 17 0 0 25 0 1 0 478950079 24727552 5340 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6037 5340 603 41 0 5996 0
vsize: 24148
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 25615
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5432 0 0 0 58988 17 0 0 25 0 1 0 478950079 24727552 5344 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6037 5344 603 41 0 5996 0
vsize: 24148
[startup+600.03 s]
Raw data (loadavg): 1.23 1.02 0.93 2/54 25665
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5432 0 0 0 59988 17 0 0 25 0 1 0 478950079 24727552 5344 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6037 5344 603 41 0 5996 0
vsize: 24148
[startup+610.03 s]
Raw data (loadavg): 1.19 1.02 0.93 2/54 25665
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5448 0 0 0 60988 17 0 0 25 0 1 0 478950079 24727552 5360 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6037 5360 603 41 0 5996 0
vsize: 24148
[startup+620.03 s]
Raw data (loadavg): 1.16 1.02 0.93 2/54 25665
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5457 0 0 0 61989 17 0 0 25 0 1 0 478950079 24887296 5369 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6076 5369 603 41 0 6035 0
vsize: 24304
[startup+630.031 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 25665
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5464 0 0 0 62989 17 0 0 25 0 1 0 478950079 24887296 5376 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6076 5376 603 41 0 6035 0
vsize: 24304
[startup+640.031 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 25665
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5591 0 0 0 63989 17 0 0 25 0 1 0 478950079 25419776 5503 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6206 5503 603 41 0 6165 0
vsize: 24824
[startup+650.032 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 25665
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5662 0 0 0 64989 18 0 0 25 0 1 0 478950079 25681920 5574 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5574 603 41 0 6229 0
vsize: 25080
[startup+660.033 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 25665
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5668 0 0 0 65989 18 0 0 25 0 1 0 478950079 25681920 5580 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5580 603 41 0 6229 0
vsize: 25080
[startup+670.033 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5668 0 0 0 66989 18 0 0 25 0 1 0 478950079 25681920 5580 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5580 603 41 0 6229 0
vsize: 25080
[startup+680.033 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5669 0 0 0 67989 18 0 0 25 0 1 0 478950079 25681920 5581 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5581 603 41 0 6229 0
vsize: 25080
[startup+690.033 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5669 0 0 0 68990 18 0 0 25 0 1 0 478950079 25681920 5581 4294967295 134512640 134672761 3221224640 3221223824 134558918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5581 603 41 0 6229 0
vsize: 25080
[startup+700.033 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5670 0 0 0 69990 18 0 0 25 0 1 0 478950079 25681920 5582 4294967295 134512640 134672761 3221224640 3221223792 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5582 603 41 0 6229 0
vsize: 25080
[startup+710.033 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5670 0 0 0 70990 18 0 0 25 0 1 0 478950079 25681920 5582 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5582 603 41 0 6229 0
vsize: 25080
[startup+720.033 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5676 0 0 0 71990 18 0 0 25 0 1 0 478950079 25681920 5588 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5588 603 41 0 6229 0
vsize: 25080
[startup+730.034 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5676 0 0 0 72990 18 0 0 25 0 1 0 478950079 25681920 5588 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5588 603 41 0 6229 0
vsize: 25080
[startup+740.033 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5676 0 0 0 73990 18 0 0 25 0 1 0 478950079 25681920 5588 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5588 603 41 0 6229 0
vsize: 25080
[startup+750.034 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5683 0 0 0 74990 18 0 0 25 0 1 0 478950079 25829376 5595 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6306 5595 603 41 0 6265 0
vsize: 25224
[startup+760.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5685 0 0 0 75990 18 0 0 25 0 1 0 478950079 25829376 5597 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6306 5597 603 41 0 6265 0
vsize: 25224
[startup+770.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5687 0 0 0 76990 18 0 0 25 0 1 0 478950079 25829376 5599 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6306 5599 603 41 0 6265 0
vsize: 25224
[startup+780.035 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5736 0 0 0 77991 18 0 0 25 0 1 0 478950079 25960448 5648 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6338 5648 603 41 0 6297 0
vsize: 25352
[startup+790.035 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5736 0 0 0 78991 18 0 0 25 0 1 0 478950079 25960448 5648 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6338 5648 603 41 0 6297 0
vsize: 25352
[startup+800.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5738 0 0 0 79991 18 0 0 25 0 1 0 478950079 25960448 5650 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6338 5650 603 41 0 6297 0
vsize: 25352
[startup+810.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5749 0 0 0 80991 18 0 0 25 0 1 0 478950079 25960448 5661 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6338 5661 603 41 0 6297 0
vsize: 25352
[startup+820.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5762 0 0 0 81991 18 0 0 25 0 1 0 478950079 26157056 5674 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6386 5674 603 41 0 6345 0
vsize: 25544
[startup+830.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5762 0 0 0 82991 18 0 0 25 0 1 0 478950079 26157056 5674 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6386 5674 603 41 0 6345 0
vsize: 25544
[startup+840.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5762 0 0 0 83992 18 0 0 25 0 1 0 478950079 26157056 5674 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6386 5674 603 41 0 6345 0
vsize: 25544
[startup+850.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5762 0 0 0 84992 18 0 0 25 0 1 0 478950079 26157056 5674 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6386 5674 603 41 0 6345 0
vsize: 25544
[startup+860.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5763 0 0 0 85992 18 0 0 25 0 1 0 478950079 26157056 5675 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6386 5675 603 41 0 6345 0
vsize: 25544
[startup+870.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5770 0 0 0 86992 18 0 0 25 0 1 0 478950079 26157056 5682 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6386 5682 603 41 0 6345 0
vsize: 25544
[startup+880.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5781 0 0 0 87992 18 0 0 25 0 1 0 478950079 26157056 5693 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6386 5693 603 41 0 6345 0
vsize: 25544
[startup+890.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25667
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5803 0 0 0 88992 18 0 0 25 0 1 0 478950079 26320896 5715 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6426 5715 603 41 0 6385 0
vsize: 25704
[startup+900.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5825 0 0 0 89993 18 0 0 25 0 1 0 478950079 26464256 5737 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5737 603 41 0 6420 0
vsize: 25844
[startup+910.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5830 0 0 0 90993 18 0 0 25 0 1 0 478950079 26464256 5742 4294967295 134512640 134672761 3221224640 3221223744 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5742 603 41 0 6420 0
vsize: 25844
[startup+920.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5831 0 0 0 91993 18 0 0 25 0 1 0 478950079 26464256 5743 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5743 603 41 0 6420 0
vsize: 25844
[startup+930.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5833 0 0 0 92993 18 0 0 25 0 1 0 478950079 26464256 5745 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5745 603 41 0 6420 0
vsize: 25844
[startup+940.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5839 0 0 0 93993 18 0 0 25 0 1 0 478950079 26464256 5751 4294967295 134512640 134672761 3221224640 3221223744 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5751 603 41 0 6420 0
vsize: 25844
[startup+950.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5839 0 0 0 94993 18 0 0 25 0 1 0 478950079 26464256 5751 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5751 603 41 0 6420 0
vsize: 25844
[startup+960.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5839 0 0 0 95994 18 0 0 25 0 1 0 478950079 26464256 5751 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5751 603 41 0 6420 0
vsize: 25844
[startup+970.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5841 0 0 0 96994 18 0 0 25 0 1 0 478950079 26464256 5753 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5753 603 41 0 6420 0
vsize: 25844
[startup+980.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5841 0 0 0 97994 18 0 0 25 0 1 0 478950079 26464256 5753 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5753 603 41 0 6420 0
vsize: 25844
[startup+990.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5841 0 0 0 98994 18 0 0 25 0 1 0 478950079 26464256 5753 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5753 603 41 0 6420 0
vsize: 25844
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5841 0 0 0 99994 18 0 0 25 0 1 0 478950079 26464256 5753 4294967295 134512640 134672761 3221224640 3221223888 134562680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6461 5753 603 41 0 6420 0
vsize: 25844
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5856 0 0 0 100994 18 0 0 25 0 1 0 478950079 26628096 5768 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6501 5768 603 41 0 6460 0
vsize: 26004
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5873 0 0 0 101994 18 0 0 25 0 1 0 478950079 26628096 5785 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6501 5785 603 41 0 6460 0
vsize: 26004
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5899 0 0 0 102995 18 0 0 25 0 1 0 478950079 26759168 5811 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5811 603 41 0 6492 0
vsize: 26132
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5900 0 0 0 103995 18 0 0 25 0 1 0 478950079 26759168 5812 4294967295 134512640 134672761 3221224640 3221223744 134559824 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5812 603 41 0 6492 0
vsize: 26132
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5900 0 0 0 104995 18 0 0 25 0 1 0 478950079 26759168 5812 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5812 603 41 0 6492 0
vsize: 26132
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5900 0 0 0 105995 18 0 0 25 0 1 0 478950079 26759168 5812 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5812 603 41 0 6492 0
vsize: 26132
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5900 0 0 0 106995 18 0 0 25 0 1 0 478950079 26759168 5812 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5812 603 41 0 6492 0
vsize: 26132
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5900 0 0 0 107995 18 0 0 25 0 1 0 478950079 26759168 5812 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5812 603 41 0 6492 0
vsize: 26132
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5909 0 0 0 108996 18 0 0 25 0 1 0 478950079 26759168 5821 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5821 603 41 0 6492 0
vsize: 26132
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5910 0 0 0 109996 18 0 0 25 0 1 0 478950079 26759168 5822 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5822 603 41 0 6492 0
vsize: 26132
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5911 0 0 0 110996 18 0 0 25 0 1 0 478950079 26759168 5823 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5823 603 41 0 6492 0
vsize: 26132
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5911 0 0 0 111996 18 0 0 25 0 1 0 478950079 26759168 5823 4294967295 134512640 134672761 3221224640 3221223824 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5823 603 41 0 6492 0
vsize: 26132
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5911 0 0 0 112996 18 0 0 25 0 1 0 478950079 26759168 5823 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5823 603 41 0 6492 0
vsize: 26132
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5928 0 0 0 113996 18 0 0 25 0 1 0 478950079 26918912 5840 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6572 5840 603 41 0 6531 0
vsize: 26288
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5940 0 0 0 114996 18 0 0 25 0 1 0 478950079 26918912 5852 4294967295 134512640 134672761 3221224640 3221223792 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6572 5852 603 41 0 6531 0
vsize: 26288
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5945 0 0 0 115996 18 0 0 25 0 1 0 478950079 26918912 5857 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6572 5857 603 41 0 6531 0
vsize: 26288
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5995 0 0 0 116996 19 0 0 25 0 1 0 478950079 27185152 5907 4294967295 134512640 134672761 3221224640 3221223744 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6637 5907 603 41 0 6596 0
vsize: 26548
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5995 0 0 0 117996 19 0 0 25 0 1 0 478950079 27185152 5907 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6637 5907 603 41 0 6596 0
vsize: 26548
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 5995 0 0 0 118996 19 0 0 25 0 1 0 478950079 27185152 5907 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6637 5907 603 41 0 6596 0
vsize: 26548
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25669
Raw data (stat): 25612 (minisat+) R 25611 23176 23175 0 -1 0 6000 0 0 0 119996 19 0 0 25 0 1 0 478950079 27185152 5912 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6637 5912 603 41 0 6596 0
vsize: 26548
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 25669
Raw data (stat): 25612 (minisat+) Z 25611 23176 23175 0 -1 12 6003 0 0 0 119996 20 0 0 25 0 1 0 478950079 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.17
CPU user time (s): 1199.97
CPU system time (s): 0.202969
CPU usage (%): 100.01
Max. virtual memory (Kb): 26548
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####