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-ii32b3.opb
MD5SUM	2998f4c8b2aa0ba71848641193ef2744
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	331
Optimality of the best value was proved	NO
Number of terms in the objective function	696
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	696
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	696
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.03984
Number of variables	696
Total number of constraints	6082
Number of constraints which are clauses	6082
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	32
Trace number 4696

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-13 20:03:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3533 boxname=wulflinc23 idbench=149 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2998f4c8b2aa0ba71848641193ef2744  /oldhome/oroussel/tmp/wulflinc23/normalized-ii32b3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-ii32b3.opb /oldhome/oroussel/tmp/wulflinc23/normalized-ii32b3.opb
IDLAUNCH: 3533
/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:        911736 kB
Buffers:         33900 kB
Cached:          46284 kB
SwapCached:        192 kB
Active:          45116 kB
Inactive:        38104 kB
HighTotal:      131008 kB
HighFree:        80836 kB
LowTotal:       903652 kB
LowFree:        830900 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34120 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:23:14 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 3533 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6082 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 |    6082    30036 |    2027       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 340[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1382   maxlim: 356   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        49 |   15709    64402 |    5236      49     1835    37.4 |  0.000 % |
c |       149 |   15709    64402 |    5759     149     4967    33.3 |  0.240 % |
c |       301 |   15709    64402 |    6335     301    11805    39.2 |  0.240 % |
c |       526 |   15709    64402 |    6969     526    24306    46.2 |  0.240 % |
c ==============================================================================
c [1mFound solution: 332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 364   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       816 |   15717    64448 |    5239     816    38233    46.9 |  0.240 % |
c |       916 |   15717    64448 |    5762     916    44260    48.3 |  0.383 % |
c |      1069 |   15717    64448 |    6339    1069    53164    49.7 |  0.383 % |
c |      1296 |   15717    64448 |    6973    1296    64784    50.0 |  0.383 % |
c |      1633 |   15717    64448 |    7670    1633    77599    47.5 |  0.383 % |
c |      2139 |   15717    64448 |    8437    2139    98112    45.9 |  0.383 % |
c |      2899 |   15717    64448 |    9281    2899   132642    45.8 |  0.383 % |
c |      4038 |   15717    64448 |   10209    4038   192743    47.7 |  0.383 % |
c |      5747 |   15717    64448 |   11230    5747   283099    49.3 |  0.383 % |
c |      8309 |   15717    64448 |   12353    8309   363820    43.8 |  0.383 % |
c |     12154 |   15717    64448 |   13588   12154   517894    42.6 |  0.383 % |
c |     17920 |   15717    64448 |   14947   11092   519311    46.8 |  0.383 % |
c |     26571 |   15717    64448 |   16442   12233   621603    50.8 |  0.383 % |
c |     39545 |   15717    64448 |   18086   16138  1327254    82.2 |  0.383 % |
c |     59008 |   15717    64448 |   19895   15997  1530170    95.7 |  0.383 % |
c |     88200 |   15717    64448 |   21884   13299  1385739   104.2 |  0.383 % |
c |    131991 |   15717    64448 |   24073   22897  2147963    93.8 |  0.383 % |
c |    197676 |   15717    64448 |   26480   24749  3102135   125.3 |  0.383 % |
c ==============================================================================
c [1mFound solution: 331[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 365   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    262913 |   15718    64458 |    5239   19426  2261157   116.4 |  0.383 % |
c |    263014 |   15718    64458 |    5762    4958   355795    71.8 |  0.431 % |
c |    263164 |   15718    64458 |    6339    5108   362784    71.0 |  0.431 % |
c |    263389 |   15718    64458 |    6973    5333   373485    70.0 |  0.431 % |
c |    263726 |   15718    64458 |    7670    5670   390379    68.8 |  0.431 % |
c |    264233 |   15718    64458 |    8437    6177   417403    67.6 |  0.431 % |
c |    264992 |   15718    64458 |    9281    6936   451073    65.0 |  0.431 % |
c |    266132 |   15718    64458 |   10209    8076   517925    64.1 |  0.431 % |
c |    267840 |   15718    64458 |   11230    9784   572872    58.6 |  0.431 % |
c |    270402 |   15718    64458 |   12353   12346   799799    64.8 |  0.431 % |
c |    274250 |   15718    64458 |   13588    9988   496427    49.7 |  0.431 % |
c |    280016 |   15718    64458 |   14947    8127   523955    64.5 |  0.431 % |
c |    288667 |   15675    64356 |   16442   16756  1355896    80.9 |  0.527 % |
c |    301643 |   15675    64356 |   18086   12935   820802    63.5 |  0.527 % |
c |    321104 |   15675    64356 |   19895   12790  1210010    94.6 |  0.527 % |
c |    350296 |   15675    64356 |   21884   20599  2215882   107.6 |  0.527 % |
c |    394087 |   15675    64356 |   24073   18362  2096705   114.2 |  0.527 % |
c |    459771 |   15624    64221 |   26480   19888  2622487   131.9 |  0.671 % |
c |    558297 |   15624    64221 |   29128   19914  2348376   117.9 |  0.671 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.88 2/54 4778
Raw data (stat): 4778 (runsolver) R 4777 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478679407 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.97 0.88 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 1326 0 0 0 993 4 0 0 25 0 1 0 478679407 6918144 1304 4294967295 134512640 134672761 3221224576 3221223760 134558435 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1689 1304 603 41 0 1648 0
vsize: 6756
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.97 0.88 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 1576 0 0 0 1992 5 0 0 25 0 1 0 478679407 7991296 1554 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1951 1554 603 41 0 1910 0
vsize: 7804
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.97 0.88 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 1989 0 0 0 2991 6 0 0 25 0 1 0 478679407 9674752 1967 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2362 1967 603 41 0 2321 0
vsize: 9448
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.97 0.88 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 2455 0 0 0 3990 7 0 0 25 0 1 0 478679407 11677696 2433 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2851 2433 603 41 0 2810 0
vsize: 11404
[startup+50.0005 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 2564 0 0 0 4990 7 0 0 25 0 1 0 478679407 12079104 2542 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2542 603 41 0 2908 0
vsize: 11796
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 2955 0 0 0 5989 9 0 0 25 0 1 0 478679407 13692928 2933 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3343 2933 603 41 0 3302 0
vsize: 13372
[startup+69.9998 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 2980 0 0 0 6988 9 0 0 25 0 1 0 478679407 13828096 2958 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3376 2958 603 41 0 3335 0
vsize: 13504
[startup+80.0004 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 2981 0 0 0 7988 9 0 0 25 0 1 0 478679407 13824000 2959 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3375 2959 603 41 0 3334 0
vsize: 13500
[startup+90.0003 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 2981 0 0 0 8988 9 0 0 25 0 1 0 478679407 13824000 2959 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3375 2959 603 41 0 3334 0
vsize: 13500
[startup+99.9997 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3221 0 0 0 9987 10 0 0 25 0 1 0 478679407 14770176 3199 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3606 3199 603 41 0 3565 0
vsize: 14424
[startup+110 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3221 0 0 0 10987 10 0 0 25 0 1 0 478679407 14770176 3199 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3606 3199 603 41 0 3565 0
vsize: 14424
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3222 0 0 0 11987 10 0 0 25 0 1 0 478679407 14770176 3200 4294967295 134512640 134672761 3221224576 3221223760 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3606 3200 603 41 0 3565 0
vsize: 14424
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 4778
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3222 0 0 0 12988 10 0 0 25 0 1 0 478679407 14770176 3200 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3606 3200 603 41 0 3565 0
vsize: 14424
[startup+140 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3223 0 0 0 13988 10 0 0 25 0 1 0 478679407 14770176 3201 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3606 3201 603 41 0 3565 0
vsize: 14424
[startup+150 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3223 0 0 0 14988 10 0 0 25 0 1 0 478679407 14770176 3201 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3606 3201 603 41 0 3565 0
vsize: 14424
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3517 0 0 0 15987 11 0 0 25 0 1 0 478679407 15974400 3495 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3900 3495 603 41 0 3859 0
vsize: 15600
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3517 0 0 0 16987 11 0 0 25 0 1 0 478679407 15974400 3495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3900 3495 603 41 0 3859 0
vsize: 15600
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3658 0 0 0 17987 11 0 0 25 0 1 0 478679407 16506880 3636 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4030 3636 603 41 0 3989 0
vsize: 16120
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3665 0 0 0 18987 11 0 0 25 0 1 0 478679407 16650240 3643 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4065 3643 603 41 0 4024 0
vsize: 16260
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 3921 0 0 0 19986 12 0 0 25 0 1 0 478679407 17580032 3899 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4292 3899 603 41 0 4251 0
vsize: 17168
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4379 0 0 0 20985 13 0 0 25 0 1 0 478679407 19460096 4357 4294967295 134512640 134672761 3221224576 3221223760 134559609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4751 4357 603 41 0 4710 0
vsize: 19004
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4379 0 0 0 21986 13 0 0 25 0 1 0 478679407 19460096 4357 4294967295 134512640 134672761 3221224576 3221223680 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4751 4357 603 41 0 4710 0
vsize: 19004
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4379 0 0 0 22986 13 0 0 25 0 1 0 478679407 19460096 4357 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4751 4357 603 41 0 4710 0
vsize: 19004
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4379 0 0 0 23986 13 0 0 25 0 1 0 478679407 19460096 4357 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4751 4357 603 41 0 4710 0
vsize: 19004
[startup+249.999 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4451 0 0 0 24986 14 0 0 25 0 1 0 478679407 19861504 4429 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4849 4429 603 41 0 4808 0
vsize: 19396
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4451 0 0 0 25986 14 0 0 25 0 1 0 478679407 19861504 4429 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4849 4429 603 41 0 4808 0
vsize: 19396
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4454 0 0 0 26986 14 0 0 25 0 1 0 478679407 19861504 4432 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4849 4432 603 41 0 4808 0
vsize: 19396
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4773 0 0 0 27985 15 0 0 25 0 1 0 478679407 21065728 4751 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5143 4751 603 41 0 5102 0
vsize: 20572
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4773 0 0 0 28984 15 0 0 25 0 1 0 478679407 21065728 4751 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5143 4751 603 41 0 5102 0
vsize: 20572
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4773 0 0 0 29984 15 0 0 25 0 1 0 478679407 21065728 4751 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5143 4751 603 41 0 5102 0
vsize: 20572
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4773 0 0 0 30984 15 0 0 25 0 1 0 478679407 21065728 4751 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5143 4751 603 41 0 5102 0
vsize: 20572
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4773 0 0 0 31984 15 0 0 25 0 1 0 478679407 21065728 4751 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5143 4751 603 41 0 5102 0
vsize: 20572
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4773 0 0 0 32984 15 0 0 25 0 1 0 478679407 21065728 4751 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5143 4751 603 41 0 5102 0
vsize: 20572
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4813 0 0 0 33985 15 0 0 25 0 1 0 478679407 21258240 4791 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5190 4791 603 41 0 5149 0
vsize: 20760
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4813 0 0 0 34985 15 0 0 25 0 1 0 478679407 21258240 4791 4294967295 134512640 134672761 3221224576 3221223680 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5190 4791 603 41 0 5149 0
vsize: 20760
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4816 0 0 0 35985 15 0 0 25 0 1 0 478679407 21397504 4794 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5224 4794 603 41 0 5183 0
vsize: 20896
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4857 0 0 0 36985 16 0 0 25 0 1 0 478679407 21528576 4835 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5256 4835 603 41 0 5215 0
vsize: 21024
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4863 0 0 0 37985 16 0 0 25 0 1 0 478679407 21528576 4841 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5256 4841 603 41 0 5215 0
vsize: 21024
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 38985 16 0 0 25 0 1 0 478679407 21798912 4894 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4894 603 41 0 5281 0
vsize: 21288
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 39985 16 0 0 25 0 1 0 478679407 21798912 4894 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4894 603 41 0 5281 0
vsize: 21288
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 40984 16 0 0 25 0 1 0 478679407 21786624 4894 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5319 4894 603 41 0 5278 0
vsize: 21276
[startup+419.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 41985 16 0 0 25 0 1 0 478679407 21721088 4894 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4894 603 41 0 5262 0
vsize: 21212
[startup+430 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 42985 16 0 0 25 0 1 0 478679407 21721088 4894 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4894 603 41 0 5262 0
vsize: 21212
[startup+440 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 43985 16 0 0 25 0 1 0 478679407 21721088 4894 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4894 603 41 0 5262 0
vsize: 21212
[startup+449.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 44985 16 0 0 25 0 1 0 478679407 21721088 4894 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4894 603 41 0 5262 0
vsize: 21212
[startup+460 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 45985 16 0 0 25 0 1 0 478679407 21721088 4894 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4894 603 41 0 5262 0
vsize: 21212
[startup+469.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 46985 16 0 0 25 0 1 0 478679407 21721088 4894 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4894 603 41 0 5262 0
vsize: 21212
[startup+479.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4916 0 0 0 47986 16 0 0 25 0 1 0 478679407 21721088 4894 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4894 603 41 0 5262 0
vsize: 21212
[startup+489.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 48986 16 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+499.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 49986 16 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+509.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 50986 16 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+519.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 51986 16 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+529.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 52986 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+539.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 53986 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+549.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 54987 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+559.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 55987 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223752 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+569.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 56987 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+579.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 57987 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+589.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 58987 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+599.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 59987 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+609.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 60988 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+619.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 61988 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+629.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 62988 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+639.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 63988 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+649.997 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 64988 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+659.998 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 65988 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+669.998 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 66989 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+679.998 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 4917 0 0 0 67989 17 0 0 25 0 1 0 478679407 21721088 4895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5303 4895 603 41 0 5262 0
vsize: 21212
[startup+689.997 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5142 0 0 0 68988 17 0 0 25 0 1 0 478679407 22663168 5120 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5533 5120 603 41 0 5492 0
vsize: 22132
[startup+699.997 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5142 0 0 0 69989 17 0 0 25 0 1 0 478679407 22663168 5120 4294967295 134512640 134672761 3221224576 3221223760 134559274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5533 5120 603 41 0 5492 0
vsize: 22132
[startup+709.998 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5142 0 0 0 70989 17 0 0 25 0 1 0 478679407 22663168 5120 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5533 5120 603 41 0 5492 0
vsize: 22132
[startup+719.997 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5212 0 0 0 71989 17 0 0 25 0 1 0 478679407 22933504 5190 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5599 5190 603 41 0 5558 0
vsize: 22396
[startup+729.999 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5212 0 0 0 72989 17 0 0 25 0 1 0 478679407 22933504 5190 4294967295 134512640 134672761 3221224576 3221223760 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5599 5190 603 41 0 5558 0
vsize: 22396
[startup+739.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5212 0 0 0 73989 17 0 0 25 0 1 0 478679407 22933504 5190 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5599 5190 603 41 0 5558 0
vsize: 22396
[startup+749.998 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5212 0 0 0 74989 17 0 0 25 0 1 0 478679407 22933504 5190 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5599 5190 603 41 0 5558 0
vsize: 22396
[startup+759.998 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5212 0 0 0 75990 17 0 0 25 0 1 0 478679407 22933504 5190 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5599 5190 603 41 0 5558 0
vsize: 22396
[startup+769.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5274 0 0 0 76989 18 0 0 25 0 1 0 478679407 23199744 5252 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5664 5252 603 41 0 5623 0
vsize: 22656
[startup+779.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5274 0 0 0 77990 18 0 0 25 0 1 0 478679407 23199744 5252 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5664 5252 603 41 0 5623 0
vsize: 22656
[startup+789.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5274 0 0 0 78990 18 0 0 25 0 1 0 478679407 23199744 5252 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5664 5252 603 41 0 5623 0
vsize: 22656
[startup+799.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5275 0 0 0 79990 18 0 0 25 0 1 0 478679407 23199744 5253 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5664 5253 603 41 0 5623 0
vsize: 22656
[startup+809.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5497 0 0 0 80988 19 0 0 25 0 1 0 478679407 24133632 5475 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5892 5475 603 41 0 5851 0
vsize: 23568
[startup+819.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5497 0 0 0 81989 19 0 0 25 0 1 0 478679407 24133632 5475 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5892 5475 603 41 0 5851 0
vsize: 23568
[startup+829.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5497 0 0 0 82989 20 0 0 25 0 1 0 478679407 24133632 5475 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5892 5475 603 41 0 5851 0
vsize: 23568
[startup+839.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5574 0 0 0 83989 20 0 0 25 0 1 0 478679407 24403968 5552 4294967295 134512640 134672761 3221224576 3221223700 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5958 5552 603 41 0 5917 0
vsize: 23832
[startup+849.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5592 0 0 0 84989 20 0 0 25 0 1 0 478679407 24535040 5570 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5570 603 41 0 5949 0
vsize: 23960
[startup+859.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5592 0 0 0 85989 20 0 0 25 0 1 0 478679407 24535040 5570 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5570 603 41 0 5949 0
vsize: 23960
[startup+869.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5592 0 0 0 86989 20 0 0 25 0 1 0 478679407 24535040 5570 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5570 603 41 0 5949 0
vsize: 23960
[startup+879.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5592 0 0 0 87990 20 0 0 25 0 1 0 478679407 24535040 5570 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5570 603 41 0 5949 0
vsize: 23960
[startup+889.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5592 0 0 0 88990 20 0 0 25 0 1 0 478679407 24535040 5570 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5570 603 41 0 5949 0
vsize: 23960
[startup+899.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5592 0 0 0 89990 20 0 0 25 0 1 0 478679407 24535040 5570 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5570 603 41 0 5949 0
vsize: 23960
[startup+909.998 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5592 0 0 0 90990 20 0 0 25 0 1 0 478679407 24535040 5570 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5570 603 41 0 5949 0
vsize: 23960
[startup+919.997 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5592 0 0 0 91990 20 0 0 25 0 1 0 478679407 24535040 5570 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5570 603 41 0 5949 0
vsize: 23960
[startup+929.997 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5595 0 0 0 92990 20 0 0 25 0 1 0 478679407 24535040 5573 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5573 603 41 0 5949 0
vsize: 23960
[startup+939.997 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5595 0 0 0 93990 20 0 0 25 0 1 0 478679407 24535040 5573 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5573 603 41 0 5949 0
vsize: 23960
[startup+949.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5595 0 0 0 94990 20 0 0 25 0 1 0 478679407 24535040 5573 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5573 603 41 0 5949 0
vsize: 23960
[startup+959.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5595 0 0 0 95990 20 0 0 25 0 1 0 478679407 24485888 5573 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5978 5573 603 41 0 5937 0
vsize: 23912
[startup+969.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5595 0 0 0 96990 20 0 0 25 0 1 0 478679407 24485888 5573 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5978 5573 603 41 0 5937 0
vsize: 23912
[startup+979.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 5595 0 0 0 97991 20 0 0 25 0 1 0 478679407 24485888 5573 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5978 5573 603 41 0 5937 0
vsize: 23912
[startup+989.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6067 0 0 0 98989 22 0 0 25 0 1 0 478679407 26497024 6045 4294967295 134512640 134672761 3221224576 3221223744 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6469 6045 603 41 0 6428 0
vsize: 25876
[startup+999.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6223 0 0 0 99988 22 0 0 25 0 1 0 478679407 27033600 6201 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6600 6201 603 41 0 6559 0
vsize: 26400
[startup+1010 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6223 0 0 0 100989 22 0 0 25 0 1 0 478679407 27033600 6201 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6600 6201 603 41 0 6559 0
vsize: 26400
[startup+1020 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6223 0 0 0 101989 22 0 0 25 0 1 0 478679407 27033600 6201 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6600 6201 603 41 0 6559 0
vsize: 26400
[startup+1030 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 102989 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1040 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 103989 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1050 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 104989 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1060 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 105989 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1070 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 106990 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1080 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 107990 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1090 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 108990 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1099.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 109990 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1110 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 110990 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223760 134559609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1120 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 111990 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1129.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 112991 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1140 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6229 0 0 0 113991 22 0 0 25 0 1 0 478679407 27193344 6207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6639 6207 603 41 0 6598 0
vsize: 26556
[startup+1150 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6447 0 0 0 114991 23 0 0 25 0 1 0 478679407 28000256 6425 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6836 6425 603 41 0 6795 0
vsize: 27344
[startup+1160 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6656 0 0 0 115990 24 0 0 25 0 1 0 478679407 28811264 6634 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7034 6634 603 41 0 6993 0
vsize: 28136
[startup+1170 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6656 0 0 0 116990 24 0 0 25 0 1 0 478679407 28811264 6634 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7034 6634 603 41 0 6993 0
vsize: 28136
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6656 0 0 0 117990 24 0 0 25 0 1 0 478679407 28811264 6634 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7034 6634 603 41 0 6993 0
vsize: 28136
[startup+1190 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6659 0 0 0 118991 24 0 0 25 0 1 0 478679407 28958720 6637 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7070 6637 603 41 0 7029 0
vsize: 28280
[startup+1200 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4780
Raw data (stat): 4778 (minisat+) R 4777 3260 3259 0 -1 0 6672 0 0 0 119991 24 0 0 25 0 1 0 478679407 28958720 6650 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7070 6650 603 41 0 7029 0
vsize: 28280
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 4780
Raw data (stat): 4778 (minisat+) Z 4777 3260 3259 0 -1 12 6675 0 0 0 119991 25 0 0 25 0 1 0 478679407 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.01
CPU time (s): 1200.17
CPU user time (s): 1199.91
CPU system time (s): 0.255961
CPU usage (%): 100.013
Max. virtual memory (Kb): 28280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####