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 5790

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        834660 kB
Buffers:         35252 kB
Cached:         124520 kB
SwapCached:       2476 kB
Active:          55652 kB
Inactive:       109508 kB
HighTotal:      131008 kB
HighFree:         3388 kB
LowTotal:       903652 kB
LowFree:        831272 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29380 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:07:52 (client local time) WITH STATUS 10 IN 1200.12 SECONDS
stats: 4195 7 1200.12 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 |   19368    73043 |    6456       0        0     nan |  0.000 % |
c |       102 |   19368    73043 |    7101     102     7508    73.6 |  0.016 % |
c |       253 |   19356    73019 |    7811     251    21282    84.8 |  0.056 % |
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 |       293 |   17268    68155 |    5756     287    23635    82.4 |  0.056 % |
c |       393 |   17268    68155 |    6331     387    30443    78.7 | 11.325 % |
c |       543 |   17268    68155 |    6964     537    39041    72.7 | 11.325 % |
c |       770 |   17268    68155 |    7661     764    50110    65.6 | 11.325 % |
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 |       864 |   17261    68142 |    5753     845    54108    64.0 | 11.325 % |
c |       964 |   17261    68142 |    6328     945    61405    65.0 | 11.470 % |
c |      1115 |   17261    68142 |    6961    1096    75538    68.9 | 11.470 % |
c |      1341 |   17261    68142 |    7657    1322    87753    66.4 | 11.470 % |
c |      1678 |   17261    68142 |    8422    1659   110793    66.8 | 11.470 % |
c |      2184 |   17261    68142 |    9265    2165   155258    71.7 | 11.470 % |
c |      2943 |   17261    68142 |   10191    2924   219586    75.1 | 11.470 % |
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 |      3979 |   17273    68172 |    5757    3960   368681    93.1 | 11.470 % |
c |      4081 |   17273    68172 |    6332    4062   376314    92.6 | 11.470 % |
c |      4232 |   17273    68172 |    6965    4213   386712    91.8 | 11.470 % |
c |      4457 |   17273    68172 |    7662    4438   409455    92.3 | 11.470 % |
c |      4795 |   17273    68172 |    8428    4776   432918    90.6 | 11.470 % |
c |      5301 |   17273    68172 |    9271    5282   466487    88.3 | 11.470 % |
c |      6061 |   17273    68172 |   10198    6042   522550    86.5 | 11.470 % |
c |      7204 |   17273    68172 |   11218    7185   589528    82.0 | 11.470 % |
c |      8917 |   17273    68172 |   12340    8898   698521    78.5 | 11.470 % |
c |     11480 |   17273    68172 |   13574   11461   858013    74.9 | 11.470 % |
c |     15325 |   17273    68172 |   14932   15306  1141586    74.6 | 11.470 % |
c |     21092 |   17273    68172 |   16425   12759   938327    73.5 | 11.470 % |
c |     29741 |   17273    68172 |   18067   12053   875185    72.6 | 11.470 % |
c |     42716 |   17273    68172 |   19874   14184   867021    61.1 | 11.470 % |
c |     62178 |   17273    68172 |   21862   11498   890576    77.5 | 11.470 % |
c |     91371 |   17273    68172 |   24048   15677  1206811    77.0 | 11.470 % |
c |    135161 |   17273    68172 |   26453   20827  1226051    58.9 | 11.470 % |
c |    200848 |   17273    68172 |   29098   27816  1466699    52.7 | 11.470 % |
c |    299376 |   17273    68172 |   32008   25897  1765102    68.2 | 11.470 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.97 0.91 2/54 29018
Raw data (stat): 29018 (runsolver) R 29017 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480753407 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 1899 0 0 0 993 5 0 0 25 0 1 0 480753407 9879552 1876 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2412 1876 603 41 0 2371 0
vsize: 9648
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2228 0 0 0 1992 6 0 0 25 0 1 0 480753407 11223040 2205 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2740 2205 603 41 0 2699 0
vsize: 10960
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2596 0 0 0 2991 7 0 0 25 0 1 0 480753407 12689408 2573 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3098 2573 603 41 0 3057 0
vsize: 12392
[startup+40.0022 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2752 0 0 0 3990 7 0 0 25 0 1 0 480753407 13463552 2729 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3287 2729 603 41 0 3246 0
vsize: 13148
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2752 0 0 0 4990 7 0 0 25 0 1 0 480753407 13463552 2729 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3287 2729 603 41 0 3246 0
vsize: 13148
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2778 0 0 0 5989 8 0 0 25 0 1 0 480753407 13463552 2755 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3287 2755 603 41 0 3246 0
vsize: 13148
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2955 0 0 0 6988 9 0 0 25 0 1 0 480753407 14282752 2932 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3487 2932 603 41 0 3446 0
vsize: 13948
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2955 0 0 0 7988 9 0 0 25 0 1 0 480753407 14282752 2932 4294967295 134512640 134672761 3221224560 3221223664 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3487 2932 603 41 0 3446 0
vsize: 13948
[startup+90.0036 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3080 0 0 0 8988 10 0 0 25 0 1 0 480753407 14807040 3057 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3057 603 41 0 3574 0
vsize: 14460
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3178 0 0 0 9986 11 0 0 25 0 1 0 480753407 15204352 3155 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3155 603 41 0 3671 0
vsize: 14848
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3184 0 0 0 10986 11 0 0 25 0 1 0 480753407 15204352 3161 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3161 603 41 0 3671 0
vsize: 14848
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3249 0 0 0 11985 12 0 0 25 0 1 0 480753407 15478784 3226 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3226 603 41 0 3738 0
vsize: 15116
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3436 0 0 0 12984 13 0 0 25 0 1 0 480753407 16281600 3413 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3975 3413 603 41 0 3934 0
vsize: 15900
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3454 0 0 0 13984 13 0 0 25 0 1 0 480753407 16281600 3431 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3975 3431 603 41 0 3934 0
vsize: 15900
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3523 0 0 0 14984 13 0 0 25 0 1 0 480753407 16699392 3500 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4077 3500 603 41 0 4036 0
vsize: 16308
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3759 0 0 0 15983 14 0 0 25 0 1 0 480753407 17682432 3736 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4317 3736 603 41 0 4276 0
vsize: 17268
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3767 0 0 0 16983 15 0 0 25 0 1 0 480753407 17682432 3744 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4317 3744 603 41 0 4276 0
vsize: 17268
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3790 0 0 0 17983 15 0 0 25 0 1 0 480753407 17829888 3767 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4353 3767 603 41 0 4312 0
vsize: 17412
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3830 0 0 0 18982 15 0 0 25 0 1 0 480753407 17977344 3807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3807 603 41 0 4348 0
vsize: 17556
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3862 0 0 0 19982 16 0 0 25 0 1 0 480753407 18288640 3839 4294967295 134512640 134672761 3221224560 3221223560 1075350054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4465 3839 603 41 0 4424 0
vsize: 17860
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3864 0 0 0 20981 16 0 0 25 0 1 0 480753407 18288640 3841 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4465 3841 603 41 0 4424 0
vsize: 17860
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3876 0 0 0 21981 16 0 0 25 0 1 0 480753407 18288640 3853 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4465 3853 603 41 0 4424 0
vsize: 17860
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3880 0 0 0 22981 17 0 0 25 0 1 0 480753407 18288640 3857 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4465 3857 603 41 0 4424 0
vsize: 17860
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3888 0 0 0 23980 17 0 0 25 0 1 0 480753407 18288640 3865 4294967295 134512640 134672761 3221224560 3221223728 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4465 3865 603 41 0 4424 0
vsize: 17860
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4035 0 0 0 24980 18 0 0 25 0 1 0 480753407 18997248 4012 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4638 4012 603 41 0 4597 0
vsize: 18552
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4081 0 0 0 25979 18 0 0 25 0 1 0 480753407 19136512 4058 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4672 4058 603 41 0 4631 0
vsize: 18688
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4093 0 0 0 26979 19 0 0 25 0 1 0 480753407 19300352 4070 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4712 4070 603 41 0 4671 0
vsize: 18848
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4103 0 0 0 27979 19 0 0 25 0 1 0 480753407 19300352 4080 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4712 4080 603 41 0 4671 0
vsize: 18848
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4122 0 0 0 28978 19 0 0 25 0 1 0 480753407 19464192 4099 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4752 4099 603 41 0 4711 0
vsize: 19008
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4127 0 0 0 29977 20 0 0 25 0 1 0 480753407 19464192 4104 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4752 4104 603 41 0 4711 0
vsize: 19008
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4127 0 0 0 30977 20 0 0 25 0 1 0 480753407 19464192 4104 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4752 4104 603 41 0 4711 0
vsize: 19008
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4140 0 0 0 31976 21 0 0 25 0 1 0 480753407 19464192 4117 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4752 4117 603 41 0 4711 0
vsize: 19008
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4163 0 0 0 32976 21 0 0 25 0 1 0 480753407 19607552 4140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4787 4140 603 41 0 4746 0
vsize: 19148
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4189 0 0 0 33976 22 0 0 25 0 1 0 480753407 19755008 4166 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4166 603 41 0 4782 0
vsize: 19292
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4197 0 0 0 34975 22 0 0 25 0 1 0 480753407 19755008 4174 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4174 603 41 0 4782 0
vsize: 19292
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4198 0 0 0 35975 22 0 0 25 0 1 0 480753407 19755008 4175 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4175 603 41 0 4782 0
vsize: 19292
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4206 0 0 0 36974 23 0 0 25 0 1 0 480753407 19755008 4183 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4183 603 41 0 4782 0
vsize: 19292
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4207 0 0 0 37974 23 0 0 25 0 1 0 480753407 19755008 4184 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4184 603 41 0 4782 0
vsize: 19292
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4210 0 0 0 38974 23 0 0 25 0 1 0 480753407 19755008 4187 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4187 603 41 0 4782 0
vsize: 19292
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4210 0 0 0 39973 24 0 0 25 0 1 0 480753407 19755008 4187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4187 603 41 0 4782 0
vsize: 19292
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4218 0 0 0 40973 24 0 0 25 0 1 0 480753407 19755008 4195 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4823 4195 603 41 0 4782 0
vsize: 19292
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4221 0 0 0 41973 24 0 0 25 0 1 0 480753407 19918848 4198 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4863 4198 603 41 0 4822 0
vsize: 19452
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4221 0 0 0 42974 24 0 0 25 0 1 0 480753407 19918848 4198 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4863 4198 603 41 0 4822 0
vsize: 19452
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4235 0 0 0 43974 24 0 0 25 0 1 0 480753407 19918848 4212 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4863 4212 603 41 0 4822 0
vsize: 19452
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4236 0 0 0 44974 24 0 0 25 0 1 0 480753407 19918848 4213 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4863 4213 603 41 0 4822 0
vsize: 19452
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4255 0 0 0 45974 24 0 0 25 0 1 0 480753407 20082688 4232 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4903 4232 603 41 0 4862 0
vsize: 19612
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4256 0 0 0 46974 24 0 0 25 0 1 0 480753407 20082688 4233 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4903 4233 603 41 0 4862 0
vsize: 19612
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4256 0 0 0 47974 24 0 0 25 0 1 0 480753407 20082688 4233 4294967295 134512640 134672761 3221224560 3221223664 134555076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4903 4233 603 41 0 4862 0
vsize: 19612
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4261 0 0 0 48975 24 0 0 25 0 1 0 480753407 20082688 4238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4903 4238 603 41 0 4862 0
vsize: 19612
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4261 0 0 0 49975 24 0 0 25 0 1 0 480753407 20082688 4238 4294967295 134512640 134672761 3221224560 3221223664 134555214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4903 4238 603 41 0 4862 0
vsize: 19612
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4284 0 0 0 50975 24 0 0 25 0 1 0 480753407 20246528 4261 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4943 4261 603 41 0 4902 0
vsize: 19772
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4298 0 0 0 51975 24 0 0 25 0 1 0 480753407 20246528 4275 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4943 4275 603 41 0 4902 0
vsize: 19772
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4311 0 0 0 52975 24 0 0 25 0 1 0 480753407 20246528 4288 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4943 4288 603 41 0 4902 0
vsize: 19772
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4341 0 0 0 53975 24 0 0 25 0 1 0 480753407 20410368 4318 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4983 4318 603 41 0 4942 0
vsize: 19932
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4341 0 0 0 54975 24 0 0 25 0 1 0 480753407 20410368 4318 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4983 4318 603 41 0 4942 0
vsize: 19932
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4341 0 0 0 55975 24 0 0 25 0 1 0 480753407 20410368 4318 4294967295 134512640 134672761 3221224560 3221223696 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4983 4318 603 41 0 4942 0
vsize: 19932
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4350 0 0 0 56976 24 0 0 25 0 1 0 480753407 20606976 4327 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5031 4327 603 41 0 4990 0
vsize: 20124
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4352 0 0 0 57976 24 0 0 25 0 1 0 480753407 20606976 4329 4294967295 134512640 134672761 3221224560 3221223724 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5031 4329 603 41 0 4990 0
vsize: 20124
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4376 0 0 0 58976 24 0 0 25 0 1 0 480753407 20606976 4353 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5031 4353 603 41 0 4990 0
vsize: 20124
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 59976 24 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4369 603 41 0 5038 0
vsize: 20316
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 60976 25 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4369 603 41 0 5038 0
vsize: 20316
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 61976 25 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4369 603 41 0 5038 0
vsize: 20316
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 62976 25 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4369 603 41 0 5038 0
vsize: 20316
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 63976 25 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4369 603 41 0 5038 0
vsize: 20316
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4407 0 0 0 64976 25 0 0 25 0 1 0 480753407 20803584 4384 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4384 603 41 0 5038 0
vsize: 20316
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4408 0 0 0 65976 25 0 0 25 0 1 0 480753407 20803584 4385 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5079 4385 603 41 0 5038 0
vsize: 20316
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4419 0 0 0 66977 25 0 0 25 0 1 0 480753407 20967424 4396 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5119 4396 603 41 0 5078 0
vsize: 20476
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4428 0 0 0 67977 25 0 0 25 0 1 0 480753407 20967424 4405 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5119 4405 603 41 0 5078 0
vsize: 20476
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4429 0 0 0 68977 25 0 0 25 0 1 0 480753407 20967424 4406 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5119 4406 603 41 0 5078 0
vsize: 20476
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 69977 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5119 4413 603 41 0 5078 0
vsize: 20476
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 70977 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5119 4413 603 41 0 5078 0
vsize: 20476
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 71977 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223744 134558768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5119 4413 603 41 0 5078 0
vsize: 20476
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29018
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 72978 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5119 4413 603 41 0 5078 0
vsize: 20476
[startup+740.023 s]
Raw data (loadavg): 1.22 1.02 0.93 2/57 29067
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 73978 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5119 4413 603 41 0 5078 0
vsize: 20476
[startup+750.022 s]
Raw data (loadavg): 1.19 1.02 0.93 2/54 29071
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4588 0 0 0 74978 26 0 0 25 0 1 0 480753407 21635072 4565 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5282 4565 603 41 0 5241 0
vsize: 21128
[startup+760.022 s]
Raw data (loadavg): 1.16 1.02 0.93 2/54 29071
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4755 0 0 0 75978 26 0 0 25 0 1 0 480753407 22298624 4732 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5444 4732 603 41 0 5403 0
vsize: 21776
[startup+770.022 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 29071
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4762 0 0 0 76978 26 0 0 25 0 1 0 480753407 22437888 4739 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5478 4739 603 41 0 5437 0
vsize: 21912
[startup+780.021 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 29071
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4765 0 0 0 77978 26 0 0 25 0 1 0 480753407 22437888 4742 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5478 4742 603 41 0 5437 0
vsize: 21912
[startup+790.021 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 29071
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4771 0 0 0 78978 26 0 0 25 0 1 0 480753407 22437888 4748 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5478 4748 603 41 0 5437 0
vsize: 21912
[startup+800.021 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 29071
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4796 0 0 0 79978 26 0 0 25 0 1 0 480753407 22618112 4773 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4773 603 41 0 5481 0
vsize: 22088
[startup+810.022 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4813 0 0 0 80978 26 0 0 25 0 1 0 480753407 22618112 4790 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4790 603 41 0 5481 0
vsize: 22088
[startup+820.021 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4824 0 0 0 81978 26 0 0 25 0 1 0 480753407 22618112 4801 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4801 603 41 0 5481 0
vsize: 22088
[startup+830.021 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4826 0 0 0 82978 26 0 0 25 0 1 0 480753407 22618112 4803 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4803 603 41 0 5481 0
vsize: 22088
[startup+840.021 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4827 0 0 0 83978 26 0 0 25 0 1 0 480753407 22618112 4804 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4804 603 41 0 5481 0
vsize: 22088
[startup+850.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4829 0 0 0 84979 26 0 0 25 0 1 0 480753407 22618112 4806 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4806 603 41 0 5481 0
vsize: 22088
[startup+860.021 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4829 0 0 0 85979 26 0 0 25 0 1 0 480753407 22618112 4806 4294967295 134512640 134672761 3221224560 3221223664 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4806 603 41 0 5481 0
vsize: 22088
[startup+870.021 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4829 0 0 0 86979 26 0 0 25 0 1 0 480753407 22618112 4806 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4806 603 41 0 5481 0
vsize: 22088
[startup+880.021 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4830 0 0 0 87979 26 0 0 25 0 1 0 480753407 22618112 4807 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4807 603 41 0 5481 0
vsize: 22088
[startup+890.021 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4830 0 0 0 88979 26 0 0 25 0 1 0 480753407 22618112 4807 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5522 4807 603 41 0 5481 0
vsize: 22088
[startup+900.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4862 0 0 0 89979 26 0 0 25 0 1 0 480753407 22781952 4839 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5562 4839 603 41 0 5521 0
vsize: 22248
[startup+910.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4885 0 0 0 90978 27 0 0 25 0 1 0 480753407 22913024 4862 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5594 4862 603 41 0 5553 0
vsize: 22376
[startup+920.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5049 0 0 0 91978 27 0 0 25 0 1 0 480753407 23588864 5026 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5759 5026 603 41 0 5718 0
vsize: 23036
[startup+930.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5181 0 0 0 92978 28 0 0 25 0 1 0 480753407 24248320 5158 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5920 5158 603 41 0 5879 0
vsize: 23680
[startup+940.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5204 0 0 0 93978 28 0 0 25 0 1 0 480753407 24391680 5181 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5955 5181 603 41 0 5914 0
vsize: 23820
[startup+950.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5207 0 0 0 94978 28 0 0 25 0 1 0 480753407 24391680 5184 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5955 5184 603 41 0 5914 0
vsize: 23820
[startup+960.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5207 0 0 0 95978 28 0 0 25 0 1 0 480753407 24391680 5184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5955 5184 603 41 0 5914 0
vsize: 23820
[startup+970.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5212 0 0 0 96978 28 0 0 25 0 1 0 480753407 24391680 5189 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5955 5189 603 41 0 5914 0
vsize: 23820
[startup+980.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5350 0 0 0 97978 28 0 0 25 0 1 0 480753407 25063424 5327 4294967295 134512640 134672761 3221224560 3221223744 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6119 5327 603 41 0 6078 0
vsize: 24476
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5608 0 0 0 98977 29 0 0 25 0 1 0 480753407 26001408 5585 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6348 5585 603 41 0 6307 0
vsize: 25392
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5636 0 0 0 99977 30 0 0 25 0 1 0 480753407 26132480 5613 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6380 5613 603 41 0 6339 0
vsize: 25520
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5636 0 0 0 100977 30 0 0 25 0 1 0 480753407 26132480 5613 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6380 5613 603 41 0 6339 0
vsize: 25520
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5636 0 0 0 101977 30 0 0 25 0 1 0 480753407 26132480 5613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6380 5613 603 41 0 6339 0
vsize: 25520
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5637 0 0 0 102978 30 0 0 25 0 1 0 480753407 26132480 5614 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6380 5614 603 41 0 6339 0
vsize: 25520
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5676 0 0 0 103978 30 0 0 25 0 1 0 480753407 26304512 5653 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6422 5653 603 41 0 6381 0
vsize: 25688
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5850 0 0 0 104977 30 0 0 25 0 1 0 480753407 27107328 5827 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6618 5827 603 41 0 6577 0
vsize: 26472
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6050 0 0 0 105977 31 0 0 25 0 1 0 480753407 27934720 6027 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6820 6027 603 41 0 6779 0
vsize: 27280
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29073
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6050 0 0 0 106977 31 0 0 25 0 1 0 480753407 27934720 6027 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6820 6027 603 41 0 6779 0
vsize: 27280
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6050 0 0 0 107977 31 0 0 25 0 1 0 480753407 27934720 6027 4294967295 134512640 134672761 3221224560 3221223760 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6820 6027 603 41 0 6779 0
vsize: 27280
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6055 0 0 0 108977 31 0 0 25 0 1 0 480753407 27934720 6032 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6820 6032 603 41 0 6779 0
vsize: 27280
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6055 0 0 0 109977 31 0 0 25 0 1 0 480753407 27934720 6032 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6820 6032 603 41 0 6779 0
vsize: 27280
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6060 0 0 0 110977 31 0 0 25 0 1 0 480753407 27934720 6037 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6820 6037 603 41 0 6779 0
vsize: 27280
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6074 0 0 0 111977 31 0 0 25 0 1 0 480753407 28123136 6051 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6051 603 41 0 6825 0
vsize: 27464
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6074 0 0 0 112978 31 0 0 25 0 1 0 480753407 28123136 6051 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6051 603 41 0 6825 0
vsize: 27464
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6075 0 0 0 113978 31 0 0 25 0 1 0 480753407 28123136 6052 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6052 603 41 0 6825 0
vsize: 27464
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6085 0 0 0 114978 31 0 0 25 0 1 0 480753407 28123136 6062 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6062 603 41 0 6825 0
vsize: 27464
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6095 0 0 0 115978 31 0 0 25 0 1 0 480753407 28123136 6072 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6072 603 41 0 6825 0
vsize: 27464
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6098 0 0 0 116978 32 0 0 25 0 1 0 480753407 28123136 6075 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6075 603 41 0 6825 0
vsize: 27464
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6099 0 0 0 117978 32 0 0 25 0 1 0 480753407 28123136 6076 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6076 603 41 0 6825 0
vsize: 27464
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6099 0 0 0 118978 32 0 0 25 0 1 0 480753407 28123136 6076 4294967295 134512640 134672761 3221224560 3221223664 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6076 603 41 0 6825 0
vsize: 27464
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29075
Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6099 0 0 0 119978 32 0 0 25 0 1 0 480753407 28123136 6076 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6866 6076 603 41 0 6825 0
vsize: 27464
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 29075
Raw data (stat): 29018 (minisat+) Z 29017 22612 22611 0 -1 12 6102 0 0 0 119978 33 0 0 25 0 1 0 480753407 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.04
CPU time (s): 1200.12
CPU user time (s): 1199.79
CPU system time (s): 0.334949
CPU usage (%): 100.007
Max. virtual memory (Kb): 27464
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####