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/synthesis-ptl-cmos-circuits/normalized-cc.opb
MD5SUM	0493ba9e257fafbb54efa7af2eeb7bf2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1567
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	60
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	5699
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	60
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	5699
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.134979
Number of variables	133
Total number of constraints	229
Number of constraints which are clauses	229
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	31
Trace number 5207

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-13 22:29:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3635 boxname=wulflinc23 idbench=251 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0493ba9e257fafbb54efa7af2eeb7bf2  /oldhome/oroussel/tmp/wulflinc23/normalized-cc.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-cc.opb /oldhome/oroussel/tmp/wulflinc23/normalized-cc.opb
IDLAUNCH: 3635
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        899644 kB
Buffers:         34224 kB
Cached:          58064 kB
SwapCached:        192 kB
Active:          48160 kB
Inactive:        47148 kB
HighTotal:      131008 kB
HighFree:        69104 kB
LowTotal:       903652 kB
LowFree:        830540 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34064 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:49:41 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3635 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 199 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 |     197      772 |      65       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1846[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 650   maxlim: 3853   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4684    16784 |    1561       0        0     nan |  0.000 % |
c |       100 |    4684    16784 |    1717     100      469     4.7 |  2.282 % |
c |       250 |    4684    16784 |    1888     250     1350     5.4 |  2.282 % |
c |       475 |    4684    16784 |    2077     475     5835    12.3 |  2.282 % |
c |       812 |    4684    16784 |    2285     812    16871    20.8 |  2.282 % |
c |      1318 |    4684    16784 |    2514    1318    32723    24.8 |  2.282 % |
c |      2078 |    4684    16784 |    2765    2078    60817    29.3 |  2.282 % |
c |      3217 |    4684    16784 |    3041    1727    50667    29.3 |  2.282 % |
c |      4925 |    4684    16784 |    3346    1783    47876    26.9 |  2.282 % |
c |      7487 |    4684    16784 |    3680    2573    84622    32.9 |  2.282 % |
c |     11331 |    4684    16784 |    4048    2541    86706    34.1 |  2.282 % |
c |     17097 |    4684    16784 |    4453    4072   180675    44.4 |  2.282 % |
c |     25746 |    4678    16767 |    4899    3517   119560    34.0 |  2.408 % |
c |     38720 |    4678    16767 |    5388    3787   152973    40.4 |  2.408 % |
c |     58181 |    4678    16767 |    5927    3902   135991    34.9 |  2.408 % |
c ==============================================================================
c [1mFound solution: 1829[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3870   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75444 |    4692    16857 |    1564    5825   258397    44.4 |  2.408 % |
c |     75545 |    4692    16857 |    1720    1558    38219    24.5 |  3.015 % |
c |     75695 |    4692    16857 |    1892    1708    41622    24.4 |  3.015 % |
c |     75920 |    4692    16857 |    2081    1933    47922    24.8 |  3.015 % |
c |     76257 |    4692    16857 |    2289    1167    16753    14.4 |  3.015 % |
c |     76764 |    4692    16857 |    2518    1674    38143    22.8 |  3.015 % |
c |     77523 |    4692    16857 |    2770    2433    66386    27.3 |  3.015 % |
c |     78664 |    4692    16857 |    3047    2121    55521    26.2 |  3.015 % |
c |     80372 |    4692    16857 |    3352    2173    64253    29.6 |  3.015 % |
c |     82934 |    4692    16857 |    3687    2900   119003    41.0 |  3.015 % |
c |     86778 |    4692    16857 |    4056    2894    94980    32.8 |  3.015 % |
c |     92545 |    4692    16857 |    4462    2377    73757    31.0 |  3.015 % |
c |    101194 |    4692    16857 |    4908    4024   148689    37.0 |  3.015 % |
c |    114169 |    4692    16857 |    5399    4222   151500    35.9 |  3.015 % |
c |    133631 |    4692    16857 |    5939    4302   155625    36.2 |  3.015 % |
c |    162824 |    4692    16857 |    6533    6071   238347    39.3 |  3.015 % |
c |    206614 |    4692    16857 |    7186    6348   257170    40.5 |  3.015 % |
c |    272299 |    4692    16857 |    7905    5968   239685    40.2 |  3.015 % |
c |    370825 |    4692    16857 |    8695    7760   388420    50.1 |  3.015 % |
c ==============================================================================
c [1mFound solution: 1813[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3886   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    381439 |    4702    16927 |    1567    5081   199217    39.2 |  3.015 % |
c |    381540 |    4702    16927 |    1723    1372    20628    15.0 |  3.607 % |
c |    381693 |    4702    16927 |    1896    1525    24489    16.1 |  3.607 % |
c |    381918 |    4702    16927 |    2085    1750    27455    15.7 |  3.607 % |
c |    382256 |    4702    16927 |    2294    2088    39211    18.8 |  3.607 % |
c |    382763 |    4702    16927 |    2523    1383    24013    17.4 |  3.607 % |
c |    383523 |    4702    16927 |    2776    2143    51248    23.9 |  3.607 % |
c |    384664 |    4702    16927 |    3053    1765    43817    24.8 |  3.607 % |
c |    386372 |    4702    16927 |    3359    1841    54480    29.6 |  3.607 % |
c |    388938 |    4702    16927 |    3694    2658    80686    30.4 |  3.607 % |
c |    392782 |    4702    16927 |    4064    2609    83462    32.0 |  3.607 % |
c |    398549 |    4702    16927 |    4470    4081   184736    45.3 |  3.607 % |
c |    407198 |    4702    16927 |    4917    3394   137501    40.5 |  3.607 % |
c |    420172 |    4702    16927 |    5409    3685   145464    39.5 |  3.607 % |
c |    439634 |    4702    16927 |    5950    3575   130875    36.6 |  3.607 % |
c |    468826 |    4702    16927 |    6545    5260   204351    38.9 |  3.607 % |
c |    512615 |    4702    16927 |    7200    5324   189411    35.6 |  3.607 % |
c |    578299 |    4702    16927 |    7920    4488   197054    43.9 |  3.607 % |
c ==============================================================================
c [1mFound solution: 1800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3899   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    597226 |    4706    16962 |    1568    7146   343418    48.1 |  3.607 % |
c |    597326 |    4706    16962 |    1724     994     9648     9.7 |  3.961 % |
c |    597476 |    4706    16962 |    1897    1144    12507    10.9 |  3.961 % |
c |    597701 |    4706    16962 |    2087    1369    17559    12.8 |  3.961 % |
c |    598038 |    4706    16962 |    2295    1706    27157    15.9 |  3.961 % |
c |    598545 |    4706    16962 |    2525    2213    46017    20.8 |  3.961 % |
c |    599304 |    4706    16962 |    2777    1590    37130    23.4 |  3.961 % |
c |    600443 |    4706    16962 |    3055    2729    88701    32.5 |  3.961 % |
c |    602154 |    4706    16962 |    3361    2810    89895    32.0 |  3.961 % |
c |    604716 |    4706    16962 |    3697    3547   148415    41.8 |  3.961 % |
c |    608560 |    4706    16962 |    4066    3498   131542    37.6 |  3.961 % |
c |    614326 |    4706    16962 |    4473    2821    97832    34.7 |  3.961 % |
c |    622975 |    4706    16962 |    4921    4479   151557    33.8 |  3.961 % |
c |    635949 |    4706    16962 |    5413    4685   165824    35.4 |  3.961 % |
c |    655410 |    4706    16962 |    5954    4395   194132    44.2 |  3.961 % |
c |    684602 |    4706    16962 |    6549    5928   263851    44.5 |  3.961 % |
c |    728392 |    4706    16962 |    7204    6165   260863    42.3 |  3.961 % |
c |    794076 |    4706    16962 |    7925    5599   201866    36.1 |  3.961 % |
c ==============================================================================
c [1mFound solution: 1790[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3909   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    860400 |    4713    17011 |    1571    7179   305934    42.6 |  3.961 % |
c |    860500 |    4713    17011 |    1728     998     8921     8.9 |  4.316 % |
c |    860650 |    4713    17011 |    1900    1148    12196    10.6 |  4.316 % |
c |    860875 |    4713    17011 |    2091    1373    16649    12.1 |  4.316 % |
c |    861212 |    4713    17011 |    2300    1710    24105    14.1 |  4.316 % |
c |    861718 |    4713    17011 |    2530    2216    46578    21.0 |  4.316 % |
c |    862477 |    4713    17011 |    2783    1618    35872    22.2 |  4.316 % |
c |    863617 |    4713    17011 |    3061    2758    87760    31.8 |  4.316 % |
c |    865326 |    4713    17011 |    3367    2819    93233    33.1 |  4.316 % |
c |    867890 |    4713    17011 |    3704    1830    51842    28.3 |  4.316 % |
c |    871734 |    4713    17011 |    4074    3722   147873    39.7 |  4.316 % |
c |    877501 |    4713    17011 |    4482    3066   118865    38.8 |  4.316 % |
c |    886150 |    4713    17011 |    4930    4710   217816    46.2 |  4.316 % |
c |    899126 |    4713    17011 |    5423    4809   213050    44.3 |  4.316 % |
c |    918587 |    4713    17011 |    5965    4559   221153    48.5 |  4.316 % |
c |    947779 |    4713    17011 |    6562    6119   253615    41.4 |  4.316 % |
c |    991569 |    4713    17011 |    7218    6176   261605    42.4 |  4.316 % |
c |   1057253 |    4713    17011 |    7940    5413   245545    45.4 |  4.316 % |
c |   1155780 |    4713    17011 |    8734    6414   330359    51.5 |  4.316 % |
c ==============================================================================
c [1mFound solution: 1789[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3910   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1158998 |    4715    17027 |    1571    5176   196361    37.9 |  4.316 % |
c |   1159099 |    4715    17027 |    1728    1395    30843    22.1 |  4.428 % |
c |   1159249 |    4715    17027 |    1900    1545    34528    22.3 |  4.428 % |
c |   1159474 |    4715    17027 |    2091    1770    39410    22.3 |  4.428 % |
c |   1159812 |    4715    17027 |    2300    2108    52349    24.8 |  4.428 % |
c |   1160319 |    4715    17027 |    2530    1351    24943    18.5 |  4.428 % |
c |   1161078 |    4715    17027 |    2783    2110    60722    28.8 |  4.428 % |
c |   1162217 |    4715    17027 |    3061    1748    49281    28.2 |  4.428 % |
c |   1163925 |    4715    17027 |    3367    1838    49308    26.8 |  4.428 % |
c |   1166489 |    4715    17027 |    3704    2632    88938    33.8 |  4.428 % |
c |   1170334 |    4715    17027 |    4074    2602    97627    37.5 |  4.428 % |
c |   1176101 |    4715    17027 |    4482    4105   183478    44.7 |  4.428 % |
c |   1184750 |    4715    17027 |    4930    3454   109406    31.7 |  4.428 % |
c |   1197728 |    4715    17027 |    5423    3634   130096    35.8 |  4.428 % |
c |   1217191 |    4715    17027 |    5965    3612   115426    32.0 |  4.428 % |
c |   1246383 |    4715    17027 |    6562    5071   214544    42.3 |  4.428 % |
c |   1290172 |    4715    17027 |    7218    5033   195453    38.8 |  4.428 % |
c |   1355856 |    4715    17027 |    7940    4274   152754    35.7 |  4.428 % |
c |   1454382 |    4715    17027 |    8734    5522   236356    42.8 |  4.428 % |
c ==============================================================================
c [1mFound solution: 1782[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3917   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1544657 |    4721    17066 |    1573    6610   277815    42.0 |  4.428 % |
c |   1544757 |    4721    17066 |    1730     927    11595    12.5 |  4.762 % |
c |   1544908 |    4721    17066 |    1903    1078    14248    13.2 |  4.762 % |
c |   1545133 |    4721    17066 |    2093    1303    23737    18.2 |  4.762 % |
c |   1545470 |    4721    17066 |    2303    1640    34066    20.8 |  4.762 % |
c |   1545979 |    4721    17066 |    2533    2149    50026    23.3 |  4.762 % |
c |   1546738 |    4721    17066 |    2786    1531    29040    19.0 |  4.762 % |
c |   1547878 |    4721    17066 |    3065    2671    74397    27.9 |  4.762 % |
c |   1549587 |    4721    17066 |    3371    2755    84874    30.8 |  4.762 % |
c |   1552153 |    4721    17066 |    3709    1792    48226    26.9 |  4.762 % |
c |   1555997 |    4721    17066 |    4079    3704   121799    32.9 |  4.762 % |
c |   1561764 |    4721    17066 |    4487    3090    93914    30.4 |  4.762 % |
c |   1570414 |    4721    17066 |    4936    2389    72105    30.2 |  4.762 % |
c |   1583389 |    4721    17066 |    5430    5126   180664    35.2 |  4.762 % |
c |   1602851 |    4721    17066 |    5973    4762   210395    44.2 |  4.762 % |
c ==============================================================================
c [1mFound solution: 1764[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3935   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1620263 |    4722    17075 |    1574    3584   130220    36.3 |  4.762 % |
c |   1620363 |    4722    17075 |    1731     996    12417    12.5 |  4.878 % |
c |   1620513 |    4722    17075 |    1904    1146    17027    14.9 |  4.878 % |
c |   1620738 |    4722    17075 |    2094    1371    25097    18.3 |  4.878 % |
c |   1621078 |    4722    17075 |    2304    1711    36143    21.1 |  4.878 % |
c |   1621584 |    4722    17075 |    2534    2217    55814    25.2 |  4.878 % |
c |   1622345 |    4722    17075 |    2788    1643    34778    21.2 |  4.878 % |
c |   1623484 |    4722    17075 |    3067    2782    92947    33.4 |  4.878 % |
c |   1625192 |    4722    17075 |    3374    2791    91142    32.7 |  4.878 % |
c |   1627756 |    4722    17075 |    3711    3554   142211    40.0 |  4.878 % |
c |   1631602 |    4722    17075 |    4082    3517   130039    37.0 |  4.878 % |
c |   1637368 |    4722    17075 |    4490    2878    97651    33.9 |  4.878 % |
c |   1646018 |    4722    17075 |    4939    4563   178309    39.1 |  4.878 % |
c |   1658994 |    4722    17075 |    5433    4632   200722    43.3 |  4.878 % |
c |   1678457 |    4722    17075 |    5977    4401   191406    43.5 |  4.878 % |
c |   1707650 |    4722    17075 |    6574    5756   253263    44.0 |  4.878 % |
c |   1751439 |    4722    17075 |    7232    5538   222396    40.2 |  4.878 % |
c |   1817125 |    4722    17075 |    7955    4478   193213    43.1 |  4.878 % |
c |   1915652 |    4722    17075 |    8751    5448   181737    33.4 |  4.878 % |
c ==============================================================================
c [1mFound solution: 1713[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3986   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   2028556 |    4731    17137 |    1577    6708   269820    40.2 |  4.878 % |
c |   2028656 |    4731    17137 |    1734     939     9995    10.6 |  5.333 % |
c |   2028811 |    4731    17137 |    1908    1094    12751    11.7 |  5.333 % |
c |   2029036 |    4731    17137 |    2098    1319    19711    14.9 |  5.333 % |
c |   2029373 |    4731    17137 |    2308    1656    30798    18.6 |  5.333 % |
c |   2029879 |    4731    17137 |    2539    2162    48882    22.6 |  5.333 % |
c |   2030638 |    4731    17137 |    2793    1585    29755    18.8 |  5.333 % |
c |   2031777 |    4731    17137 |    3073    2724    72280    26.5 |  5.334 % |
c |   2033485 |    4731    17137 |    3380    2794    92680    33.2 |  5.333 % |
c |   2036047 |    4731    17137 |    3718    3581   117262    32.7 |  5.333 % |
c |   2039892 |    4731    17137 |    4090    3464   124678    36.0 |  5.333 % |
c |   2045658 |    4731    17137 |    4499    2725    86230    31.6 |  5.333 % |
c |   2054307 |    4731    17137 |    4949    4324   171839    39.7 |  5.333 % |
c |   2067281 |    4731    17137 |    5444    4361   163543    37.5 |  5.333 % |
c |   2086742 |    4731    17137 |    5988    4121   145252    35.2 |  5.333 % |
c |   2115938 |    4731    17137 |    6587    5382   191726    35.6 |  5.333 % |
c |   2159727 |    4731    17137 |    7246    5273   193112    36.6 |  5.333 % |
c |   2225411 |    4731    17137 |    7970    4385   173330    39.5 |  5.333 % |
c |   2323939 |    4731    17137 |    8767    5360   190709    35.6 |  5.333 % |
#### 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.98 0.91 2/54 6252
Raw data (stat): 6252 (runsolver) R 6251 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479558249 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 668 0 0 0 996 1 0 0 25 0 1 0 479558249 4280320 646 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1045 646 603 41 0 1004 0
vsize: 4180
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 772 0 0 0 1995 2 0 0 25 0 1 0 479558249 4685824 750 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1144 750 603 41 0 1103 0
vsize: 4576
[startup+30.002 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 884 0 0 0 2994 3 0 0 25 0 1 0 479558249 5083136 862 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1241 862 603 41 0 1200 0
vsize: 4964
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 884 0 0 0 3993 3 0 0 25 0 1 0 479558249 5083136 862 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1241 862 603 41 0 1200 0
vsize: 4964
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 884 0 0 0 4993 3 0 0 25 0 1 0 479558249 5083136 862 4294967295 134512640 134672761 3221224576 3221223680 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1241 862 603 41 0 1200 0
vsize: 4964
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 896 0 0 0 5993 3 0 0 25 0 1 0 479558249 5218304 874 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1274 874 603 41 0 1233 0
vsize: 5096
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 967 0 0 0 6993 3 0 0 25 0 1 0 479558249 5488640 945 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1340 945 603 41 0 1299 0
vsize: 5360
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 979 0 0 0 7993 3 0 0 25 0 1 0 479558249 5488640 957 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1340 957 603 41 0 1299 0
vsize: 5360
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1035 0 0 0 8993 3 0 0 25 0 1 0 479558249 5758976 1013 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1406 1013 603 41 0 1365 0
vsize: 5624
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1068 0 0 0 9993 3 0 0 25 0 1 0 479558249 5890048 1046 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1438 1046 603 41 0 1397 0
vsize: 5752
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1072 0 0 0 10994 3 0 0 25 0 1 0 479558249 5890048 1050 4294967295 134512640 134672761 3221224576 3221223748 134559060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1438 1050 603 41 0 1397 0
vsize: 5752
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1072 0 0 0 11994 3 0 0 25 0 1 0 479558249 5890048 1050 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1438 1050 603 41 0 1397 0
vsize: 5752
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1142 0 0 0 12993 4 0 0 25 0 1 0 479558249 6172672 1120 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1507 1120 603 41 0 1466 0
vsize: 6028
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1159 0 0 0 13994 4 0 0 25 0 1 0 479558249 6307840 1137 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1540 1137 603 41 0 1499 0
vsize: 6160
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1204 0 0 0 14994 4 0 0 25 0 1 0 479558249 6443008 1182 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1573 1182 603 41 0 1532 0
vsize: 6292
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1204 0 0 0 15994 4 0 0 25 0 1 0 479558249 6443008 1182 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1573 1182 603 41 0 1532 0
vsize: 6292
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1226 0 0 0 16994 4 0 0 25 0 1 0 479558249 6578176 1204 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1606 1204 603 41 0 1565 0
vsize: 6424
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 17994 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 18994 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223680 134555205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 19994 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+210.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 20995 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+220.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 21995 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 22995 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 23995 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+250.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 24995 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+260.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 25996 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+270.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1292 0 0 0 26996 4 0 0 25 0 1 0 479558249 6848512 1270 4294967295 134512640 134672761 3221224576 3221223760 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1672 1270 603 41 0 1631 0
vsize: 6688
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1327 0 0 0 27996 4 0 0 25 0 1 0 479558249 6983680 1305 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1705 1305 603 41 0 1664 0
vsize: 6820
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1348 0 0 0 28996 4 0 0 25 0 1 0 479558249 6983680 1326 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1705 1326 603 41 0 1664 0
vsize: 6820
[startup+300.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1348 0 0 0 29996 4 0 0 25 0 1 0 479558249 6983680 1326 4294967295 134512640 134672761 3221224576 3221223712 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1705 1326 603 41 0 1664 0
vsize: 6820
[startup+310.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1348 0 0 0 30996 4 0 0 25 0 1 0 479558249 6983680 1326 4294967295 134512640 134672761 3221224576 3221223728 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1705 1326 603 41 0 1664 0
vsize: 6820
[startup+320.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1348 0 0 0 31997 4 0 0 25 0 1 0 479558249 6983680 1326 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1705 1326 603 41 0 1664 0
vsize: 6820
[startup+330.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1348 0 0 0 32996 5 0 0 25 0 1 0 479558249 6983680 1326 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1705 1326 603 41 0 1664 0
vsize: 6820
[startup+340.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1348 0 0 0 33996 5 0 0 25 0 1 0 479558249 6983680 1326 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1705 1326 603 41 0 1664 0
vsize: 6820
[startup+350.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1348 0 0 0 34996 5 0 0 25 0 1 0 479558249 6983680 1326 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1705 1326 603 41 0 1664 0
vsize: 6820
[startup+360.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1352 0 0 0 35996 5 0 0 25 0 1 0 479558249 7118848 1330 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1738 1330 603 41 0 1697 0
vsize: 6952
[startup+370.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1361 0 0 0 36996 5 0 0 25 0 1 0 479558249 7118848 1339 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1738 1339 603 41 0 1697 0
vsize: 6952
[startup+380.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1378 0 0 0 37996 5 0 0 25 0 1 0 479558249 7118848 1356 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1738 1356 603 41 0 1697 0
vsize: 6952
[startup+390.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1402 0 0 0 38996 5 0 0 25 0 1 0 479558249 7249920 1380 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1380 603 41 0 1729 0
vsize: 7080
[startup+400.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1402 0 0 0 39996 5 0 0 25 0 1 0 479558249 7249920 1380 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1380 603 41 0 1729 0
vsize: 7080
[startup+410.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1415 0 0 0 40996 5 0 0 25 0 1 0 479558249 7249920 1393 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1393 603 41 0 1729 0
vsize: 7080
[startup+420.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1415 0 0 0 41996 5 0 0 25 0 1 0 479558249 7249920 1393 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1393 603 41 0 1729 0
vsize: 7080
[startup+430.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1415 0 0 0 42997 5 0 0 25 0 1 0 479558249 7249920 1393 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1393 603 41 0 1729 0
vsize: 7080
[startup+440.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1415 0 0 0 43997 5 0 0 25 0 1 0 479558249 7249920 1393 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1393 603 41 0 1729 0
vsize: 7080
[startup+450.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1415 0 0 0 44997 5 0 0 25 0 1 0 479558249 7249920 1393 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1393 603 41 0 1729 0
vsize: 7080
[startup+460.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1415 0 0 0 45997 5 0 0 25 0 1 0 479558249 7249920 1393 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1770 1393 603 41 0 1729 0
vsize: 7080
[startup+470.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1426 0 0 0 46997 5 0 0 25 0 1 0 479558249 7385088 1404 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1803 1404 603 41 0 1762 0
vsize: 7212
[startup+480.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1426 0 0 0 47998 5 0 0 25 0 1 0 479558249 7385088 1404 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1803 1404 603 41 0 1762 0
vsize: 7212
[startup+490.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1454 0 0 0 48998 5 0 0 25 0 1 0 479558249 7516160 1432 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1432 603 41 0 1794 0
vsize: 7340
[startup+500.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1494 0 0 0 49998 5 0 0 25 0 1 0 479558249 7651328 1472 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1868 1472 603 41 0 1827 0
vsize: 7472
[startup+510.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1500 0 0 0 50998 5 0 0 25 0 1 0 479558249 7651328 1478 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1868 1478 603 41 0 1827 0
vsize: 7472
[startup+520.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1541 0 0 0 51998 5 0 0 25 0 1 0 479558249 7782400 1519 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1900 1519 603 41 0 1859 0
vsize: 7600
[startup+530.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1594 0 0 0 52998 6 0 0 25 0 1 0 479558249 8048640 1572 4294967295 134512640 134672761 3221224576 3221223760 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1965 1572 603 41 0 1924 0
vsize: 7860
[startup+540.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1606 0 0 0 53998 6 0 0 25 0 1 0 479558249 8048640 1584 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1965 1584 603 41 0 1924 0
vsize: 7860
[startup+550.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1606 0 0 0 54998 6 0 0 25 0 1 0 479558249 8048640 1584 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1965 1584 603 41 0 1924 0
vsize: 7860
[startup+560.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1606 0 0 0 55999 6 0 0 25 0 1 0 479558249 8048640 1584 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1965 1584 603 41 0 1924 0
vsize: 7860
[startup+570.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1606 0 0 0 56999 6 0 0 25 0 1 0 479558249 8048640 1584 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1965 1584 603 41 0 1924 0
vsize: 7860
[startup+580.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 57999 6 0 0 25 0 1 0 479558249 8183808 1598 4294967295 134512640 134672761 3221224576 3221223680 134555105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1998 1598 603 41 0 1957 0
vsize: 7992
[startup+590.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 58999 6 0 0 25 0 1 0 479558249 8183808 1598 4294967295 134512640 134672761 3221224576 3221223712 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1998 1598 603 41 0 1957 0
vsize: 7992
[startup+600.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 60000 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+610.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 61000 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+620.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 62000 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+630.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 63000 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+640.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 64000 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223680 134559808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+650.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 65001 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+660.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 66001 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+670.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 67001 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+680.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 68002 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+690.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 69002 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+700.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 70002 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+710.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 71002 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+720.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1620 0 0 0 72002 6 0 0 25 0 1 0 479558249 8163328 1598 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1993 1598 603 41 0 1952 0
vsize: 7972
[startup+730.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1692 0 0 0 73002 6 0 0 25 0 1 0 479558249 8425472 1670 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2057 1670 603 41 0 2016 0
vsize: 8228
[startup+740.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1692 0 0 0 74002 6 0 0 25 0 1 0 479558249 8425472 1670 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2057 1670 603 41 0 2016 0
vsize: 8228
[startup+750.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1692 0 0 0 75002 6 0 0 25 0 1 0 479558249 8425472 1670 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2057 1670 603 41 0 2016 0
vsize: 8228
[startup+760.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 76003 6 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+770.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 77003 6 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+780.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 78003 6 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+790.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 79003 6 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+800.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 80003 6 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+810.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 81003 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+820.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 82003 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+830.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 83003 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+840.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 84003 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+850.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 85004 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+860.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 86004 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+870.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 87004 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+880.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 88004 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+890.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 89004 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+900.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1711 0 0 0 90004 7 0 0 25 0 1 0 479558249 8560640 1689 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1689 603 41 0 2049 0
vsize: 8360
[startup+910.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1718 0 0 0 91005 7 0 0 25 0 1 0 479558249 8560640 1696 4294967295 134512640 134672761 3221224576 3221223764 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1696 603 41 0 2049 0
vsize: 8360
[startup+920.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1731 0 0 0 92005 7 0 0 25 0 1 0 479558249 8560640 1709 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1709 603 41 0 2049 0
vsize: 8360
[startup+930.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1734 0 0 0 93005 7 0 0 25 0 1 0 479558249 8560640 1712 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2090 1712 603 41 0 2049 0
vsize: 8360
[startup+940.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1740 0 0 0 94005 7 0 0 25 0 1 0 479558249 8708096 1718 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1718 603 41 0 2085 0
vsize: 8504
[startup+950.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1744 0 0 0 95005 7 0 0 25 0 1 0 479558249 8708096 1722 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1722 603 41 0 2085 0
vsize: 8504
[startup+960.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1744 0 0 0 96005 7 0 0 25 0 1 0 479558249 8708096 1722 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1722 603 41 0 2085 0
vsize: 8504
[startup+970.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1750 0 0 0 97006 7 0 0 25 0 1 0 479558249 8708096 1728 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1728 603 41 0 2085 0
vsize: 8504
[startup+980.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1750 0 0 0 98006 7 0 0 25 0 1 0 479558249 8708096 1728 4294967295 134512640 134672761 3221224576 3221223776 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1728 603 41 0 2085 0
vsize: 8504
[startup+990.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1753 0 0 0 99006 7 0 0 25 0 1 0 479558249 8708096 1731 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1731 603 41 0 2085 0
vsize: 8504
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1763 0 0 0 100006 7 0 0 25 0 1 0 479558249 8708096 1741 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2126 1741 603 41 0 2085 0
vsize: 8504
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1789 0 0 0 101006 7 0 0 25 0 1 0 479558249 8851456 1767 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2161 1767 603 41 0 2120 0
vsize: 8644
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1792 0 0 0 102006 7 0 0 25 0 1 0 479558249 8851456 1770 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2161 1770 603 41 0 2120 0
vsize: 8644
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 103006 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 104006 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223680 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 105007 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 106007 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 107007 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 108007 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 109007 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223728 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1100.02 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 110007 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1110.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 111008 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1120.02 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 112008 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1130.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 113008 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1140.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 114008 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1150.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 115008 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1160.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1796 0 0 0 116008 7 0 0 25 0 1 0 479558249 8986624 1774 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1774 603 41 0 2153 0
vsize: 8776
[startup+1170.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1808 0 0 0 117009 7 0 0 25 0 1 0 479558249 8986624 1786 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1786 603 41 0 2153 0
vsize: 8776
[startup+1180.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1816 0 0 0 118009 7 0 0 25 0 1 0 479558249 8986624 1794 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2194 1794 603 41 0 2153 0
vsize: 8776
[startup+1190.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1860 0 0 0 119009 8 0 0 25 0 1 0 479558249 9256960 1838 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2260 1838 603 41 0 2219 0
vsize: 9040
[startup+1200.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 6252
Raw data (stat): 6252 (minisat+) R 6251 3260 3259 0 -1 0 1861 0 0 0 120009 8 0 0 25 0 1 0 479558249 9256960 1839 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2260 1839 603 41 0 2219 0
vsize: 9040
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.01 1.00 0.92 1/54 6252
Raw data (stat): 6252 (minisat+) Z 6251 3260 3259 0 -1 12 1864 0 0 0 120009 8 0 0 25 0 1 0 479558249 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.03
CPU time (s): 1200.18
CPU user time (s): 1200.1
CPU system time (s): 0.085986
CPU usage (%): 100.013
Max. virtual memory (Kb): 9040
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####