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/logic-synthesis/normalized-5xp1.b.opb
MD5SUM	24a8f38e94b07e6ca192a34c96c24c6e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	12
Optimality of the best value was proved	NO
Number of terms in the objective function	465
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	465
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	465
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	464
Total number of constraints	859
Number of constraints which are clauses	845
Number of constraints which are cardinality constraints (but not clauses)	14
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	149
Trace number 6160

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 03:36:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4571 boxname=wulflinc21 idbench=59 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  24a8f38e94b07e6ca192a34c96c24c6e  /oldhome/oroussel/tmp/wulflinc21/normalized-5xp1.b.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-5xp1.b.opb /oldhome/oroussel/tmp/wulflinc21/normalized-5xp1.b.opb
IDLAUNCH: 4571
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        875232 kB
Buffers:         28484 kB
Cached:         110984 kB
SwapCached:          0 kB
Active:          37560 kB
Inactive:       104812 kB
HighTotal:      131008 kB
HighFree:        16436 kB
LowTotal:       903652 kB
LowFree:        858796 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11616 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:56:10 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4571 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 843 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 |     843    29887 |     281       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:17506     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   37540   115840 |   12513       0        0     nan |  0.000 % |
c |       101 |   37540   115840 |   13764     101      985     9.8 |  0.016 % |
c |       251 |   37519   115792 |   15140     249     3844    15.4 |  0.056 % |
c |       481 |   37519   115792 |   16654     479    13694    28.6 |  0.056 % |
c ==============================================================================
c [1mFound solution: 19[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 |       570 |   37478   115698 |   12492     568    17850    31.4 |  0.056 % |
c |       672 |   37478   115698 |   13741     670    30050    44.9 |  0.183 % |
c ==============================================================================
c [1mFound solution: 18[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 |       691 |   37506   115769 |   12502     689    31423    45.6 |  0.183 % |
c |       795 |   37506   115769 |   13752     793    38164    48.1 |  0.199 % |
c ==============================================================================
c [1mFound solution: 17[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 |       809 |   23585    83693 |    7861     719    36786    51.2 |  0.199 % |
c |       910 |   23585    83693 |    8647     820    39912    48.7 | 35.121 % |
c |      1062 |   23585    83693 |    9511     972    52044    53.5 | 35.121 % |
c |      1291 |   23553    83617 |   10462    1199    77032    64.2 | 35.216 % |
c ==============================================================================
c [1mFound solution: 16[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 |      1341 |   23577    83677 |    7859    1249    82056    65.7 | 35.216 % |
c |      1443 |   23565    83643 |    8644    1350    94916    70.3 | 35.226 % |
c |      1593 |   23561    83634 |    9509    1498   108550    72.5 | 35.234 % |
c ==============================================================================
c [1mFound solution: 15[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 |      1635 |   23537    83565 |    7845    1533   111651    72.8 | 35.234 % |
c |      1735 |   23537    83565 |    8629    1633   123819    75.8 | 35.308 % |
c |      1887 |   23521    83525 |    9492    1775   131960    74.3 | 35.355 % |
c |      2114 |   23521    83525 |   10441    2002   154132    77.0 | 35.355 % |
c |      2451 |   23521    83525 |   11485    2339   193275    82.6 | 35.355 % |
c |      2957 |   23521    83525 |   12634    2845   258724    90.9 | 35.355 % |
c |      3716 |   23513    83507 |   13897    3603   361380   100.3 | 35.371 % |
c ==============================================================================
c [1mFound solution: 14[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 |      4381 |   23534    83558 |    7844    4268   439023   102.9 | 35.371 % |
c |      4484 |   23534    83558 |    8628    4371   451930   103.4 | 35.357 % |
c |      4634 |   23534    83558 |    9491    4521   461825   102.2 | 35.357 % |
c |      4860 |   23480    83429 |   10440    4746   473701    99.8 | 35.500 % |
c |      5197 |   23480    83429 |   11484    5083   500237    98.4 | 35.500 % |
c |      5703 |   23480    83429 |   12632    5589   541839    96.9 | 35.500 % |
c |      6462 |   23480    83429 |   13896    6348   619542    97.6 | 35.500 % |
c |      7601 |   23418    83280 |   15285    7485   710524    94.9 | 35.691 % |
c |      9309 |   23418    83280 |   16814    9193   860672    93.6 | 35.691 % |
c |     11871 |   23418    83280 |   18495   11755  1037493    88.3 | 35.691 % |
c |     15717 |   23418    83280 |   20345   15601  1280532    82.1 | 35.691 % |
c |     21485 |   23414    83271 |   22379   21368  1656284    77.5 | 35.699 % |
c |     30137 |   23343    83103 |   24617   13672   922565    67.5 | 35.914 % |
c |     43113 |   23343    83103 |   27079   26648  1823847    68.4 | 35.914 % |
c |     62576 |   23267    82923 |   29787   27962  2005974    71.7 | 36.145 % |
c |     91768 |   23180    82716 |   32766   34847  2898874    83.2 | 36.399 % |
c |    135557 |   23053    82418 |   36042   27396  2096227    76.5 | 36.765 % |
c |    201248 |   23010    82318 |   39647   37764  3561616    94.3 | 36.884 % |
c |    299775 |   22895    82048 |   43611   43235  3102769    71.8 | 37.203 % |
#### 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.82 0.90 0.89 2/55 4418
Raw data (stat): 4418 (runsolver) R 4417 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 358661801 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99989 s]
Raw data (loadavg): 0.85 0.90 0.89 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 1991 0 0 0 993 5 0 0 25 0 1 0 358661801 10235904 1969 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2499 1969 603 41 0 2458 0
vsize: 9996
[startup+20.0006 s]
Raw data (loadavg): 0.87 0.90 0.89 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 2431 0 0 0 1992 6 0 0 25 0 1 0 358661801 12001280 2409 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2409 603 41 0 2889 0
vsize: 11720
[startup+30.0012 s]
Raw data (loadavg): 0.89 0.91 0.89 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 2726 0 0 0 2991 8 0 0 25 0 1 0 358661801 13197312 2704 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3222 2704 603 41 0 3181 0
vsize: 12888
[startup+40.001 s]
Raw data (loadavg): 0.91 0.91 0.89 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 2978 0 0 0 3990 9 0 0 25 0 1 0 358661801 14286848 2956 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3488 2956 603 41 0 3447 0
vsize: 13952
[startup+50.0016 s]
Raw data (loadavg): 0.92 0.91 0.89 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 3277 0 0 0 4989 10 0 0 25 0 1 0 358661801 15536128 3255 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3793 3255 603 41 0 3752 0
vsize: 15172
[startup+60.0017 s]
Raw data (loadavg): 0.93 0.91 0.89 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 3532 0 0 0 5988 11 0 0 25 0 1 0 358661801 16613376 3510 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3510 603 41 0 4015 0
vsize: 16224
[startup+70.002 s]
Raw data (loadavg): 0.94 0.92 0.89 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 3761 0 0 0 6987 12 0 0 25 0 1 0 358661801 17555456 3739 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4286 3739 603 41 0 4245 0
vsize: 17144
[startup+80.0027 s]
Raw data (loadavg): 0.95 0.92 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4008 0 0 0 7987 13 0 0 25 0 1 0 358661801 18497536 3986 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4516 3986 603 41 0 4475 0
vsize: 18064
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.92 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4080 0 0 0 8986 14 0 0 25 0 1 0 358661801 18767872 4058 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4582 4058 603 41 0 4541 0
vsize: 18328
[startup+100.002 s]
Raw data (loadavg): 0.96 0.92 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4080 0 0 0 9986 14 0 0 25 0 1 0 358661801 18767872 4058 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4582 4058 603 41 0 4541 0
vsize: 18328
[startup+110.003 s]
Raw data (loadavg): 0.97 0.92 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4080 0 0 0 10986 14 0 0 25 0 1 0 358661801 18767872 4058 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4582 4058 603 41 0 4541 0
vsize: 18328
[startup+120.004 s]
Raw data (loadavg): 0.97 0.93 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4087 0 0 0 11986 14 0 0 25 0 1 0 358661801 18919424 4065 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4619 4065 603 41 0 4578 0
vsize: 18476
[startup+130.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4115 0 0 0 12986 14 0 0 25 0 1 0 358661801 18919424 4093 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4619 4093 603 41 0 4578 0
vsize: 18476
[startup+140.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4131 0 0 0 13986 14 0 0 25 0 1 0 358661801 19083264 4109 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4109 603 41 0 4618 0
vsize: 18636
[startup+150.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4266 0 0 0 14986 15 0 0 25 0 1 0 358661801 19615744 4244 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4789 4244 603 41 0 4748 0
vsize: 19156
[startup+160.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4359 0 0 0 15986 15 0 0 25 0 1 0 358661801 20148224 4337 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4337 603 41 0 4878 0
vsize: 19676
[startup+170.005 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4359 0 0 0 16986 15 0 0 25 0 1 0 358661801 20148224 4337 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4337 603 41 0 4878 0
vsize: 19676
[startup+180.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4359 0 0 0 17986 15 0 0 25 0 1 0 358661801 20148224 4337 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4337 603 41 0 4878 0
vsize: 19676
[startup+190.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4359 0 0 0 18986 15 0 0 25 0 1 0 358661801 20148224 4337 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4337 603 41 0 4878 0
vsize: 19676
[startup+200.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4391 0 0 0 19986 15 0 0 25 0 1 0 358661801 20283392 4369 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4952 4369 603 41 0 4911 0
vsize: 19808
[startup+210.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4599 0 0 0 20985 16 0 0 25 0 1 0 358661801 21082112 4577 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5147 4577 603 41 0 5106 0
vsize: 20588
[startup+220.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4811 0 0 0 21985 17 0 0 25 0 1 0 358661801 22024192 4789 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5377 4789 603 41 0 5336 0
vsize: 21508
[startup+230.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4921 0 0 0 22985 17 0 0 25 0 1 0 358661801 22425600 4899 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5475 4899 603 41 0 5434 0
vsize: 21900
[startup+240.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4921 0 0 0 23984 18 0 0 25 0 1 0 358661801 22425600 4899 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5475 4899 603 41 0 5434 0
vsize: 21900
[startup+250.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4927 0 0 0 24984 18 0 0 25 0 1 0 358661801 22425600 4905 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5475 4905 603 41 0 5434 0
vsize: 21900
[startup+260.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4930 0 0 0 25984 18 0 0 25 0 1 0 358661801 22564864 4908 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5509 4908 603 41 0 5468 0
vsize: 22036
[startup+270.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4957 0 0 0 26984 18 0 0 25 0 1 0 358661801 22564864 4935 4294967295 134512640 134672761 3221224576 3221223744 134561272 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5509 4935 603 41 0 5468 0
vsize: 22036
[startup+280.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4974 0 0 0 27984 18 0 0 25 0 1 0 358661801 22728704 4952 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5549 4952 603 41 0 5508 0
vsize: 22196
[startup+290.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 4992 0 0 0 28984 18 0 0 25 0 1 0 358661801 22888448 4970 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5588 4970 603 41 0 5547 0
vsize: 22352
[startup+300.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5169 0 0 0 29984 19 0 0 25 0 1 0 358661801 23560192 5147 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5752 5147 603 41 0 5711 0
vsize: 23008
[startup+310.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5386 0 0 0 30983 20 0 0 25 0 1 0 358661801 24498176 5364 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5981 5364 603 41 0 5940 0
vsize: 23924
[startup+320.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5603 0 0 0 31983 21 0 0 25 0 1 0 358661801 25300992 5581 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6177 5581 603 41 0 6136 0
vsize: 24708
[startup+330.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5610 0 0 0 32982 21 0 0 25 0 1 0 358661801 25436160 5588 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6210 5588 603 41 0 6169 0
vsize: 24840
[startup+340.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5612 0 0 0 33982 21 0 0 25 0 1 0 358661801 25436160 5590 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6210 5590 603 41 0 6169 0
vsize: 24840
[startup+350.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5639 0 0 0 34982 21 0 0 25 0 1 0 358661801 25436160 5617 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6210 5617 603 41 0 6169 0
vsize: 24840
[startup+360.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5650 0 0 0 35982 22 0 0 25 0 1 0 358661801 25600000 5628 4294967295 134512640 134672761 3221224576 3221223728 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6250 5628 603 41 0 6209 0
vsize: 25000
[startup+370.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5660 0 0 0 36982 22 0 0 25 0 1 0 358661801 25600000 5638 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6250 5638 603 41 0 6209 0
vsize: 25000
[startup+380.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5670 0 0 0 37982 22 0 0 25 0 1 0 358661801 25600000 5648 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6250 5648 603 41 0 6209 0
vsize: 25000
[startup+390.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5694 0 0 0 38982 22 0 0 25 0 1 0 358661801 25796608 5672 4294967295 134512640 134672761 3221224576 3221223760 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6298 5672 603 41 0 6257 0
vsize: 25192
[startup+400.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5702 0 0 0 39982 22 0 0 25 0 1 0 358661801 25796608 5680 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6298 5680 603 41 0 6257 0
vsize: 25192
[startup+410.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5780 0 0 0 40982 23 0 0 25 0 1 0 358661801 26320896 5758 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5758 603 41 0 6385 0
vsize: 25704
[startup+420.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5784 0 0 0 41982 23 0 0 25 0 1 0 358661801 26320896 5762 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5762 603 41 0 6385 0
vsize: 25704
[startup+430.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5793 0 0 0 42982 23 0 0 25 0 1 0 358661801 26320896 5771 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5771 603 41 0 6385 0
vsize: 25704
[startup+440.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5793 0 0 0 43982 23 0 0 25 0 1 0 358661801 26320896 5771 4294967295 134512640 134672761 3221224576 3221223732 134560075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5771 603 41 0 6385 0
vsize: 25704
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5802 0 0 0 44982 23 0 0 25 0 1 0 358661801 26320896 5780 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5780 603 41 0 6385 0
vsize: 25704
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5802 0 0 0 45982 24 0 0 25 0 1 0 358661801 26320896 5780 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5780 603 41 0 6385 0
vsize: 25704
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5802 0 0 0 46981 24 0 0 25 0 1 0 358661801 26320896 5780 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5780 603 41 0 6385 0
vsize: 25704
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5813 0 0 0 47981 24 0 0 25 0 1 0 358661801 26320896 5791 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5791 603 41 0 6385 0
vsize: 25704
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5818 0 0 0 48981 24 0 0 25 0 1 0 358661801 26484736 5796 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6466 5796 603 41 0 6425 0
vsize: 25864
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 5827 0 0 0 49981 24 0 0 25 0 1 0 358661801 26484736 5805 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6466 5805 603 41 0 6425 0
vsize: 25864
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6100 0 0 0 50980 25 0 0 25 0 1 0 358661801 27570176 6078 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6731 6078 603 41 0 6690 0
vsize: 26924
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6337 0 0 0 51980 26 0 0 25 0 1 0 358661801 28635136 6315 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6991 6315 603 41 0 6950 0
vsize: 27964
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6351 0 0 0 52980 26 0 0 25 0 1 0 358661801 28635136 6329 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6991 6329 603 41 0 6950 0
vsize: 27964
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6378 0 0 0 53979 27 0 0 25 0 1 0 358661801 28778496 6356 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7026 6356 603 41 0 6985 0
vsize: 28104
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6379 0 0 0 54979 27 0 0 25 0 1 0 358661801 28778496 6357 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7026 6357 603 41 0 6985 0
vsize: 28104
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6396 0 0 0 55979 27 0 0 25 0 1 0 358661801 28778496 6374 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7026 6374 603 41 0 6985 0
vsize: 28104
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6402 0 0 0 56979 27 0 0 25 0 1 0 358661801 28942336 6380 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6380 603 41 0 7025 0
vsize: 28264
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6402 0 0 0 57979 28 0 0 25 0 1 0 358661801 28942336 6380 4294967295 134512640 134672761 3221224576 3221223760 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6380 603 41 0 7025 0
vsize: 28264
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6402 0 0 0 58979 28 0 0 25 0 1 0 358661801 28942336 6380 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6380 603 41 0 7025 0
vsize: 28264
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6402 0 0 0 59979 28 0 0 25 0 1 0 358661801 28942336 6380 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6380 603 41 0 7025 0
vsize: 28264
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6500 0 0 0 60979 28 0 0 25 0 1 0 358661801 29343744 6478 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7164 6478 603 41 0 7123 0
vsize: 28656
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6833 0 0 0 61978 29 0 0 25 0 1 0 358661801 30691328 6811 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7493 6811 603 41 0 7452 0
vsize: 29972
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6981 0 0 0 62978 30 0 0 25 0 1 0 358661801 31227904 6959 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7624 6959 603 41 0 7583 0
vsize: 30496
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6981 0 0 0 63977 30 0 0 25 0 1 0 358661801 31227904 6959 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7624 6959 603 41 0 7583 0
vsize: 30496
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6981 0 0 0 64978 30 0 0 25 0 1 0 358661801 31227904 6959 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7624 6959 603 41 0 7583 0
vsize: 30496
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 6981 0 0 0 65977 31 0 0 25 0 1 0 358661801 31227904 6959 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7624 6959 603 41 0 7583 0
vsize: 30496
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7000 0 0 0 66977 31 0 0 25 0 1 0 358661801 31379456 6978 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7661 6978 603 41 0 7620 0
vsize: 30644
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7001 0 0 0 67977 31 0 0 25 0 1 0 358661801 31379456 6979 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7661 6979 603 41 0 7620 0
vsize: 30644
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7007 0 0 0 68978 31 0 0 25 0 1 0 358661801 31379456 6985 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7661 6985 603 41 0 7620 0
vsize: 30644
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7009 0 0 0 69978 31 0 0 25 0 1 0 358661801 31379456 6987 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7661 6987 603 41 0 7620 0
vsize: 30644
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7009 0 0 0 70978 32 0 0 25 0 1 0 358661801 31379456 6987 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7661 6987 603 41 0 7620 0
vsize: 30644
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7022 0 0 0 71977 32 0 0 25 0 1 0 358661801 31543296 7000 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7701 7000 603 41 0 7660 0
vsize: 30804
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7038 0 0 0 72977 32 0 0 25 0 1 0 358661801 31543296 7016 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7701 7016 603 41 0 7660 0
vsize: 30804
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7115 0 0 0 73977 33 0 0 25 0 1 0 358661801 31809536 7093 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7766 7093 603 41 0 7725 0
vsize: 31064
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7390 0 0 0 74976 34 0 0 25 0 1 0 358661801 32923648 7368 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 7368 603 41 0 7997 0
vsize: 32152
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 75976 34 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 76976 34 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 77976 34 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 78976 34 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 79976 34 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 80976 35 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 81976 35 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 82976 35 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7468 0 0 0 83976 35 0 0 25 0 1 0 358661801 33325056 7446 4294967295 134512640 134672761 3221224576 3221223728 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7446 603 41 0 8095 0
vsize: 32544
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7469 0 0 0 84976 35 0 0 25 0 1 0 358661801 33325056 7447 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7447 603 41 0 8095 0
vsize: 32544
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7470 0 0 0 85976 35 0 0 25 0 1 0 358661801 33325056 7448 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7448 603 41 0 8095 0
vsize: 32544
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7471 0 0 0 86976 35 0 0 25 0 1 0 358661801 33325056 7449 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7449 603 41 0 8095 0
vsize: 32544
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7471 0 0 0 87976 35 0 0 25 0 1 0 358661801 33325056 7449 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7449 603 41 0 8095 0
vsize: 32544
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7471 0 0 0 88976 36 0 0 25 0 1 0 358661801 33325056 7449 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7449 603 41 0 8095 0
vsize: 32544
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7471 0 0 0 89976 36 0 0 25 0 1 0 358661801 33325056 7449 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7449 603 41 0 8095 0
vsize: 32544
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7471 0 0 0 90976 36 0 0 25 0 1 0 358661801 33325056 7449 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7449 603 41 0 8095 0
vsize: 32544
[startup+920.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7472 0 0 0 91976 36 0 0 25 0 1 0 358661801 33325056 7450 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7450 603 41 0 8095 0
vsize: 32544
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7474 0 0 0 92976 36 0 0 25 0 1 0 358661801 33325056 7452 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7452 603 41 0 8095 0
vsize: 32544
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7474 0 0 0 93976 37 0 0 25 0 1 0 358661801 33325056 7452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7452 603 41 0 8095 0
vsize: 32544
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7474 0 0 0 94976 37 0 0 25 0 1 0 358661801 33325056 7452 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7452 603 41 0 8095 0
vsize: 32544
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7474 0 0 0 95976 37 0 0 25 0 1 0 358661801 33325056 7452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7452 603 41 0 8095 0
vsize: 32544
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7474 0 0 0 96976 37 0 0 25 0 1 0 358661801 33325056 7452 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 7452 603 41 0 8095 0
vsize: 32544
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7483 0 0 0 97976 37 0 0 25 0 1 0 358661801 33476608 7461 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7461 603 41 0 8132 0
vsize: 32692
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7483 0 0 0 98976 37 0 0 25 0 1 0 358661801 33476608 7461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7461 603 41 0 8132 0
vsize: 32692
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7483 0 0 0 99976 37 0 0 25 0 1 0 358661801 33476608 7461 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7461 603 41 0 8132 0
vsize: 32692
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7483 0 0 0 100976 37 0 0 25 0 1 0 358661801 33476608 7461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7461 603 41 0 8132 0
vsize: 32692
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7483 0 0 0 101976 38 0 0 25 0 1 0 358661801 33476608 7461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7461 603 41 0 8132 0
vsize: 32692
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7484 0 0 0 102976 38 0 0 25 0 1 0 358661801 33476608 7462 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7462 603 41 0 8132 0
vsize: 32692
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7484 0 0 0 103976 38 0 0 25 0 1 0 358661801 33476608 7462 4294967295 134512640 134672761 3221224576 3221223712 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7462 603 41 0 8132 0
vsize: 32692
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7484 0 0 0 104976 38 0 0 25 0 1 0 358661801 33476608 7462 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7462 603 41 0 8132 0
vsize: 32692
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7487 0 0 0 105976 38 0 0 25 0 1 0 358661801 33476608 7465 4294967295 134512640 134672761 3221224576 3221223532 1075350119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7465 603 41 0 8132 0
vsize: 32692
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7498 0 0 0 106976 38 0 0 25 0 1 0 358661801 33476608 7476 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7476 603 41 0 8132 0
vsize: 32692
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7498 0 0 0 107976 38 0 0 25 0 1 0 358661801 33476608 7476 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7476 603 41 0 8132 0
vsize: 32692
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7507 0 0 0 108976 39 0 0 25 0 1 0 358661801 33476608 7485 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7485 603 41 0 8132 0
vsize: 32692
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7507 0 0 0 109976 39 0 0 25 0 1 0 358661801 33476608 7485 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7485 603 41 0 8132 0
vsize: 32692
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7513 0 0 0 110976 39 0 0 25 0 1 0 358661801 33476608 7491 4294967295 134512640 134672761 3221224576 3221223776 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7491 603 41 0 8132 0
vsize: 32692
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7513 0 0 0 111976 39 0 0 25 0 1 0 358661801 33476608 7491 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7491 603 41 0 8132 0
vsize: 32692
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7514 0 0 0 112976 39 0 0 25 0 1 0 358661801 33476608 7492 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7492 603 41 0 8132 0
vsize: 32692
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7523 0 0 0 113976 39 0 0 25 0 1 0 358661801 33673216 7501 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8221 7501 603 41 0 8180 0
vsize: 32884
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7524 0 0 0 114976 39 0 0 25 0 1 0 358661801 33673216 7502 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8221 7502 603 41 0 8180 0
vsize: 32884
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7551 0 0 0 115976 40 0 0 25 0 1 0 358661801 33673216 7529 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8221 7529 603 41 0 8180 0
vsize: 32884
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7552 0 0 0 116976 40 0 0 25 0 1 0 358661801 33673216 7530 4294967295 134512640 134672761 3221224576 3221223712 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8221 7530 603 41 0 8180 0
vsize: 32884
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7552 0 0 0 117976 40 0 0 25 0 1 0 358661801 33673216 7530 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8221 7530 603 41 0 8180 0
vsize: 32884
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7577 0 0 0 118976 40 0 0 25 0 1 0 358661801 33865728 7555 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8268 7555 603 41 0 8227 0
vsize: 33072
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4418
Raw data (stat): 4418 (minisat+) R 4417 30927 30926 0 -1 0 7577 0 0 0 119976 40 0 0 25 0 1 0 358661801 33865728 7555 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8268 7555 603 41 0 8227 0
vsize: 33072
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 4418
Raw data (stat): 4418 (minisat+) Z 4417 30927 30926 0 -1 12 7580 0 0 0 119976 41 0 0 25 0 1 0 358661801 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.04
CPU time (s): 1200.19
CPU user time (s): 1199.77
CPU system time (s): 0.417936
CPU usage (%): 100.012
Max. virtual memory (Kb): 33072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####