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-e64.b.opb
MD5SUM	bf7f8537c6faa135d25c67c53576abb5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	49
Optimality of the best value was proved	NO
Number of terms in the objective function	608
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	608
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	608
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	607
Total number of constraints	1053
Number of constraints which are clauses	1022
Number of constraints which are cardinality constraints (but not clauses)	31
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	32
Trace number 5415

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-13 23:48:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3826 boxname=wulflinc6 idbench=66 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bf7f8537c6faa135d25c67c53576abb5  /oldhome/oroussel/tmp/wulflinc6/normalized-e64.b.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-e64.b.opb /oldhome/oroussel/tmp/wulflinc6/normalized-e64.b.opb
IDLAUNCH: 3826
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        909772 kB
Buffers:         35012 kB
Cached:          68016 kB
SwapCached:       2644 kB
Active:          51836 kB
Inactive:        56764 kB
HighTotal:      131008 kB
HighFree:        59052 kB
LowTotal:       903652 kB
LowFree:        850720 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10764 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:08:49 (client local time) WITH STATUS 10 IN 1200.45 SECONDS
stats: 3826 7 1200.45 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1022 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     958     7493 |     287       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  593/593          
c |         0 |     958     7493 |     383       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.065989 s)
c ==============================================================================
c [1mFound solution: 82[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:27428     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         1 |   32835    81920 |    9850       1       16    16.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21530          
c   -- var.elim.:  2000/21530          
c   -- var.elim.:  3000/21530          
c   -- var.elim.:  4000/21530          
c   -- var.elim.:  5000/21530          
c   -- var.elim.:  6000/21530          
c   -- var.elim.:  7000/21530          
c   -- var.elim.:  8000/21530          
c   -- var.elim.:  9000/21530          
c   -- var.elim.:  10000/21530          
c   -- var.elim.:  11000/21530          
c   -- var.elim.:  12000/21530          
c   -- var.elim.:  13000/21530          
c   -- var.elim.:  14000/21530          
c   -- var.elim.:  15000/21530          
c   -- var.elim.:  16000/21530          
c   -- var.elim.:  17000/21530          
c   -- var.elim.:  18000/21530          
c   -- var.elim.:  19000/21530          
c   -- var.elim.:  20000/21530          
c   -- var.elim.:  21000/21530          
c   -- var.elim.:  21530/21530          
c   -- var.elim.:  1000/10725          
c   -- var.elim.:  2000/10725          
c   -- var.elim.:  3000/10725          
c   -- var.elim.:  4000/10725          
c   -- var.elim.:  5000/10725          
c   -- var.elim.:  6000/10725          
c   -- var.elim.:  7000/10725          
c   -- var.elim.:  8000/10725          
c   -- var.elim.:  9000/10725          
c   -- var.elim.:  10000/10725          
c   -- var.elim.:  10725/10725          
c   -- subsuming                       
c   -- var.elim.:  1000/8897          
c   -- var.elim.:  2000/8897          
c   -- var.elim.:  3000/8897          
c   -- var.elim.:  4000/8897          
c   -- var.elim.:  5000/8897          
c   -- var.elim.:  6000/8897          
c   -- var.elim.:  7000/8897          
c   -- var.elim.:  8000/8897          
c   -- var.elim.:  8897/8897          
c   -- var.elim.:  64/64          
c |         1 |   22281   174750 |      --       1       --      -- |     --   | -10543/92863
c |         1 |   22281   174750 |    8912       1       16    16.0 |  0.000 % |
c |       101 |   22178   173763 |    9758      96     2076    21.6 |  0.522 % |
c |       251 |   22168   173693 |   10729     245     6001    24.5 |  0.568 % |
c |       476 |   22146   173528 |   11790     468    16237    34.7 |  0.662 % |
c |       813 |   22146   173528 |   12969     805    22972    28.5 |  0.662 % |
c |      1319 |   22103   173150 |   14238    1308    42097    32.2 |  0.857 % |
c |      2079 |   22085   173060 |   15649    2064    75304    36.5 |  0.932 % |
c |      3218 |   22052   172747 |   17189    3197   113230    35.4 |  1.081 % |
c |      4926 |   22052   172747 |   18908    4905   265773    54.2 |  1.081 % |
c ==============================================================================
c (current CPU-time: 43.8553 s)
c ==============================================================================
c [1mFound solution: 59[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5334 |   22847   174860 |    6854    5311   275361    51.8 |  1.081 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3701          
c   -- var.elim.:  2000/3701          
c   -- var.elim.:  3000/3701          
c   -- var.elim.:  3701/3701          
c   -- var.elim.:  1000/1856          
c   -- var.elim.:  1856/1856          
c   -- subsuming                       
c   -- var.elim.:  1000/1407          
c   -- var.elim.:  1407/1407          
c |      5334 |   22246   174008 |      --    5311       --      -- |     --   | -600/-849
c |      5334 |   22246   174008 |    8898    5179   251990    48.7 |  1.081 % |
c |      5434 |   22246   174008 |    9788    5279   257091    48.7 |  1.299 % |
c |      5585 |   22246   174008 |   10767    5430   261324    48.1 |  1.299 % |
c |      5810 |   22246   174008 |   11843    5655   273430    48.4 |  1.299 % |
c |      6147 |   22246   174008 |   13028    5992   288497    48.1 |  1.299 % |
c |      6654 |   22227   173889 |   14318    6494   317922    49.0 |  1.382 % |
c |      7415 |   22195   173669 |   15727    7251   349029    48.1 |  1.521 % |
c |      8555 |   22174   173553 |   17284    8384   412798    49.2 |  1.614 % |
c |     10263 |   22174   173553 |   19012   10092   549197    54.4 |  1.614 % |
c |     12825 |   22174   173553 |   20914   12654   828113    65.4 |  1.614 % |
c |     16669 |   22174   173553 |   23005   16498  1331378    80.7 |  1.614 % |
c |     22435 |   22174   173553 |   25306   22264  2016904    90.6 |  1.614 % |
c |     31087 |   22174   173553 |   27836   17056  1977863   116.0 |  1.614 % |
c |     44061 |   22174   173553 |   30620   30030  3836207   127.7 |  1.614 % |
c ==============================================================================
c (current CPU-time: 116.235 s)
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     44704 |   22407   174198 |    6722   30673  3869754   126.2 |  1.614 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1135          
c   -- var.elim.:  1135/1135          
c   -- var.elim.:  353/353          
c |     44704 |   22239   174158 |      --   30673       --      -- |     --   | -167/-37
c |     44704 |   22239   174158 |    8895   30673  3869754   126.2 |  1.614 % |
c |     44804 |   22239   174158 |    9785    8737  1167987   133.7 |  1.695 % |
c |     44955 |   22239   174158 |   10763    8888  1170477   131.7 |  1.695 % |
c |     45181 |   22239   174158 |   11840    9114  1179509   129.4 |  1.695 % |
c |     45519 |   22223   174071 |   13014    9451  1201436   127.1 |  1.742 % |
c |     46027 |   22223   174071 |   14316    9959  1219019   122.4 |  1.742 % |
c |     46786 |   22223   174071 |   15747   10718  1258045   117.4 |  1.742 % |
c |     47926 |   22223   174071 |   17322   11858  1351210   113.9 |  1.742 % |
c |     49635 |   22223   174071 |   19054   13567  1501493   110.7 |  1.742 % |
c |     52197 |   22223   174071 |   20960   16129  1730301   107.3 |  1.742 % |
c |     56041 |   22223   174071 |   23056   19973  2086675   104.5 |  1.742 % |
c |     61811 |   22223   174071 |   25361   14108  1339890    95.0 |  1.742 % |
c ==============================================================================
c (current CPU-time: 151.25 s)
c ==============================================================================
c [1mFound solution: 53[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     68589 |   22539   174984 |    6761   20886  2039317    97.6 |  1.742 % |
c   -- subsuming                       
c   -- var.elim.:  697/697          
c   -- var.elim.:  504/504          
c   -- var.elim.:  114/114          
c |     68589 |   22261   174449 |      --   20886       --      -- |     --   | -278/-534
c |     68589 |   22261   174449 |    8904   20886  2039317    97.6 |  1.742 % |
c |     68689 |   22261   174449 |    9794    8688   766246    88.2 |  1.805 % |
c |     68839 |   22261   174449 |   10774    8838   771395    87.3 |  1.805 % |
c |     69064 |   22261   174449 |   11851    9063   781736    86.3 |  1.805 % |
c |     69401 |   22261   174449 |   13036    9400   801116    85.2 |  1.805 % |
c |     69907 |   22261   174449 |   14340    9906   832146    84.0 |  1.805 % |
c |     70666 |   22261   174449 |   15774   10665   875497    82.1 |  1.805 % |
c |     71806 |   22261   174449 |   17352   11805   948396    80.3 |  1.805 % |
c |     73514 |   22261   174449 |   19087   13513  1061183    78.5 |  1.805 % |
c |     76076 |   22261   174449 |   20996   16075  1291690    80.4 |  1.805 % |
c |     79923 |   22261   174449 |   23095   19922  1610392    80.8 |  1.805 % |
c |     85690 |   22261   174449 |   25405   25689  2324440    90.5 |  1.805 % |
c |     94340 |   22261   174449 |   27945   21490  2034354    94.7 |  1.805 % |
c |    107316 |   22261   174449 |   30740   18234  1977588   108.5 |  1.805 % |
c |    126777 |   22261   174449 |   33814   17881  2174153   121.6 |  1.805 % |
c |    155972 |   22261   174449 |   37195   25425  3695256   145.3 |  1.805 % |
c |    199761 |   22261   174449 |   40915   19780  2652503   134.1 |  1.805 % |
c ==============================================================================
c (current CPU-time: 556.207 s)
c ==============================================================================
c [1mFound solution: 52[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    240866 |   22280   174500 |    6683   28722  5376144   187.2 |  1.805 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2704          
c   -- var.elim.:  2000/2704          
c   -- var.elim.:  2704/2704          
c   -- var.elim.:  1000/4354          
c   -- var.elim.:  2000/4354          
c   -- var.elim.:  3000/4354          
c   -- var.elim.:  4000/4354          
c   -- var.elim.:  4354/4354          
c   -- var.elim.:  1000/2529          
c   -- var.elim.:  2000/2529          
c   -- var.elim.:  2529/2529          
c   -- var.elim.:  1000/3392          
c   -- var.elim.:  2000/3392          
c   -- var.elim.:  3000/3392          
c   -- var.elim.:  3392/3392          
c   -- var.elim.:  1000/2237          
c   -- var.elim.:  2000/2237          
c   -- var.elim.:  2237/2237          
c   -- var.elim.:  438/438          
c   -- subsuming                       
c   -- var.elim.:  1000/4011          
c   -- var.elim.:  2000/4011          
c   -- var.elim.:  3000/4011          
c   -- var.elim.:  4000/4011          
c   -- var.elim.:  4011/4011          
c   -- var.elim.:  592/592          
c |    240866 |   21801   169451 |      --   28722       --      -- |     --   | -222/6474
c |    240866 |   21801   169451 |    8720   28722  5376144   187.2 |  1.805 % |
c |    240967 |   21801   169451 |    9592    7225   993316   137.5 |  2.192 % |
c |    241119 |   21801   169451 |   10551    7377   997538   135.2 |  2.192 % |
c |    241344 |   21801   169451 |   11606    7602  1004069   132.1 |  2.192 % |
c |    241683 |   21801   169451 |   12767    7941  1020250   128.5 |  2.192 % |
c |    242190 |   21801   169451 |   14044    8448  1046628   123.9 |  2.192 % |
c |    242950 |   21801   169451 |   15448    9208  1110700   120.6 |  2.192 % |
c |    244089 |   21801   169451 |   16993   10347  1184668   114.5 |  2.192 % |
c |    245797 |   21801   169451 |   18692   12055  1350584   112.0 |  2.192 % |
c |    248360 |   21801   169451 |   20562   14618  1662714   113.7 |  2.192 % |
c |    252205 |   21801   169451 |   22618   18463  1990525   107.8 |  2.192 % |
c |    257971 |   21801   169451 |   24880   24229  2519277   104.0 |  2.192 % |
c |    266620 |   21801   169451 |   27368   19609  1896549    96.7 |  2.192 % |
c |    279596 |   21801   169451 |   30105   16569  1595371    96.3 |  2.192 % |
c |    299058 |   21801   169451 |   33115   17272  2121488   122.8 |  2.192 % |
c |    328252 |   21801   169451 |   36427   23626  3165922   134.0 |  2.192 % |
c |    372041 |   21801   169451 |   40070   15951  2170176   136.1 |  2.192 % |
c |    437725 |   21801   169451 |   44077   29034  3575691   123.2 |  2.192 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 x117 -x118 -x119 x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 x139 -x140 -x141 -x142 -x143 -x144 x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 x192 -x193 -x194 x195#### 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.87 0.94 0.90 2/54 645
Raw data (stat): 645 (runsolver) R 644 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421812415 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.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 3390 0 0 0 985 13 0 0 25 0 1 0 421812415 16363520 3271 4294967295 134512640 134672761 3221224576 3221223024 134643987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3995 3271 603 41 0 3954 0
vsize: 15980
[startup+20.0023 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 3471 0 0 0 1985 14 0 0 25 0 1 0 421812415 16719872 3352 4294967295 134512640 134672761 3221224576 3221223344 134629735 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4082 3352 603 41 0 4041 0
vsize: 16328
[startup+30.0031 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 3471 0 0 0 2985 14 0 0 25 0 1 0 421812415 16719872 3352 4294967295 134512640 134672761 3221224576 3221223120 134621041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4082 3352 603 41 0 4041 0
vsize: 16328
[startup+40.0036 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 3472 0 0 0 3985 14 0 0 25 0 1 0 421812415 16363520 3287 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3995 3287 603 41 0 3954 0
vsize: 15980
[startup+50.0047 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 4612 0 0 0 4982 17 0 0 25 0 1 0 421812415 18477056 3749 4294967295 134512640 134672761 3221224576 3221222032 134566692 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4511 3749 603 41 0 4470 0
vsize: 18044
[startup+60.0045 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 5041 0 0 0 5981 19 0 0 25 0 1 0 421812415 19722240 4112 4294967295 134512640 134672761 3221224576 3221223760 134610652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4848 4112 603 41 0 4807 0
vsize: 19260
[startup+70.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 5832 0 0 0 6978 21 0 0 25 0 1 0 421812415 23130112 4903 4294967295 134512640 134672761 3221224576 3221223776 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5647 4903 603 41 0 5606 0
vsize: 22588
[startup+80.0062 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 6436 0 0 0 7978 23 0 0 25 0 1 0 421812415 25522176 5507 4294967295 134512640 134672761 3221224576 3221223712 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6231 5507 603 41 0 6190 0
vsize: 24924
[startup+90.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 7029 0 0 0 8976 25 0 0 25 0 1 0 421812415 27963392 6100 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6827 6100 603 41 0 6786 0
vsize: 27308
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 7029 0 0 0 9976 25 0 0 25 0 1 0 421812415 27963392 6100 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6827 6100 603 41 0 6786 0
vsize: 27308
[startup+110.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 7861 0 0 0 10974 27 0 0 25 0 1 0 421812415 31379456 6932 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7661 6932 603 41 0 7620 0
vsize: 30644
[startup+120.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9306 0 0 0 11969 32 0 0 25 0 1 0 421812415 34582528 7700 4294967295 134512640 134672761 3221224576 3221223760 134615480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7700 603 41 0 8402 0
vsize: 33772
[startup+130.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9306 0 0 0 12969 32 0 0 25 0 1 0 421812415 34582528 7700 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7700 603 41 0 8402 0
vsize: 33772
[startup+140.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9306 0 0 0 13970 33 0 0 25 0 1 0 421812415 34582528 7700 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7700 603 41 0 8402 0
vsize: 33772
[startup+150.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9306 0 0 0 14970 33 0 0 25 0 1 0 421812415 34582528 7700 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7700 603 41 0 8402 0
vsize: 33772
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9881 0 0 0 15968 35 0 0 25 0 1 0 421812415 34582528 7736 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7736 603 41 0 8402 0
vsize: 33772
[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9881 0 0 0 16969 35 0 0 25 0 1 0 421812415 34582528 7736 4294967295 134512640 134672761 3221224576 3221223776 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7736 603 41 0 8402 0
vsize: 33772
[startup+180.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9881 0 0 0 17969 35 0 0 25 0 1 0 421812415 34582528 7736 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7736 603 41 0 8402 0
vsize: 33772
[startup+190.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9881 0 0 0 18969 35 0 0 25 0 1 0 421812415 34582528 7736 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7736 603 41 0 8402 0
vsize: 33772
[startup+200.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9881 0 0 0 19970 35 0 0 25 0 1 0 421812415 34582528 7736 4294967295 134512640 134672761 3221224576 3221223752 134615850 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7736 603 41 0 8402 0
vsize: 33772
[startup+210.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9881 0 0 0 20970 35 0 0 25 0 1 0 421812415 34582528 7736 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7736 603 41 0 8402 0
vsize: 33772
[startup+220.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9881 0 0 0 21971 35 0 0 25 0 1 0 421812415 34582528 7736 4294967295 134512640 134672761 3221224576 3221223700 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7736 603 41 0 8402 0
vsize: 33772
[startup+230.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 9881 0 0 0 22971 35 0 0 25 0 1 0 421812415 34582528 7736 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8443 7736 603 41 0 8402 0
vsize: 33772
[startup+240.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10002 0 0 0 23971 35 0 0 25 0 1 0 421812415 35065856 7824 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8561 7824 603 41 0 8520 0
vsize: 34244
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10002 0 0 0 24972 35 0 0 25 0 1 0 421812415 35065856 7824 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8561 7824 603 41 0 8520 0
vsize: 34244
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10002 0 0 0 25972 35 0 0 25 0 1 0 421812415 35065856 7824 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8561 7824 603 41 0 8520 0
vsize: 34244
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10002 0 0 0 26972 35 0 0 25 0 1 0 421812415 35065856 7824 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8561 7824 603 41 0 8520 0
vsize: 34244
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10478 0 0 0 27971 36 0 0 25 0 1 0 421812415 37036032 8300 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9042 8300 603 41 0 9001 0
vsize: 36168
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10737 0 0 0 28971 37 0 0 25 0 1 0 421812415 37924864 8524 4294967295 134512640 134672761 3221224576 3221223712 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9259 8524 603 41 0 9218 0
vsize: 37036
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10737 0 0 0 29972 37 0 0 25 0 1 0 421812415 37924864 8524 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9259 8524 603 41 0 9218 0
vsize: 37036
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10737 0 0 0 30972 37 0 0 25 0 1 0 421812415 37924864 8524 4294967295 134512640 134672761 3221224576 3221223584 134522555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9259 8524 603 41 0 9218 0
vsize: 37036
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10737 0 0 0 31972 37 0 0 25 0 1 0 421812415 37924864 8524 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9259 8524 603 41 0 9218 0
vsize: 37036
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 10773 0 0 0 32972 37 0 0 25 0 1 0 421812415 38187008 8560 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9323 8560 603 41 0 9282 0
vsize: 37292
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 11278 0 0 0 33971 39 0 0 25 0 1 0 421812415 40173568 9065 4294967295 134512640 134672761 3221224576 3221223760 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9808 9065 603 41 0 9767 0
vsize: 39232
[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 11853 0 0 0 34969 41 0 0 25 0 1 0 421812415 42536960 9640 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9640 603 41 0 10344 0
vsize: 41540
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12009 0 0 0 35970 41 0 0 25 0 1 0 421812415 43077632 9788 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9788 603 41 0 10476 0
vsize: 42068
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12009 0 0 0 36970 41 0 0 25 0 1 0 421812415 43077632 9788 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9788 603 41 0 10476 0
vsize: 42068
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12009 0 0 0 37970 41 0 0 25 0 1 0 421812415 43077632 9788 4294967295 134512640 134672761 3221224576 3221223712 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9788 603 41 0 10476 0
vsize: 42068
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12009 0 0 0 38971 41 0 0 25 0 1 0 421812415 43077632 9788 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9788 603 41 0 10476 0
vsize: 42068
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12010 0 0 0 39971 41 0 0 25 0 1 0 421812415 43077632 9789 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9789 603 41 0 10476 0
vsize: 42068
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12010 0 0 0 40971 41 0 0 25 0 1 0 421812415 43077632 9789 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9789 603 41 0 10476 0
vsize: 42068
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12010 0 0 0 41972 41 0 0 25 0 1 0 421812415 43077632 9789 4294967295 134512640 134672761 3221224576 3221223700 134566128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9789 603 41 0 10476 0
vsize: 42068
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12010 0 0 0 42972 41 0 0 25 0 1 0 421812415 43077632 9789 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9789 603 41 0 10476 0
vsize: 42068
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12010 0 0 0 43973 41 0 0 25 0 1 0 421812415 43077632 9789 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10517 9789 603 41 0 10476 0
vsize: 42068
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12089 0 0 0 44973 41 0 0 25 0 1 0 421812415 43368448 9860 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10588 9860 603 41 0 10547 0
vsize: 42352
[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12089 0 0 0 45973 41 0 0 25 0 1 0 421812415 43368448 9860 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10588 9860 603 41 0 10547 0
vsize: 42352
[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12089 0 0 0 46974 41 0 0 25 0 1 0 421812415 43368448 9860 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10588 9860 603 41 0 10547 0
vsize: 42352
[startup+480.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12089 0 0 0 47974 41 0 0 25 0 1 0 421812415 43368448 9860 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10588 9860 603 41 0 10547 0
vsize: 42352
[startup+490.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 12142 0 0 0 48974 41 0 0 25 0 1 0 421812415 43630592 9913 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10652 9913 603 41 0 10611 0
vsize: 42608
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 13001 0 0 0 49972 44 0 0 25 0 1 0 421812415 47198208 10772 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10772 603 41 0 11482 0
vsize: 46092
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 13585 0 0 0 50970 46 0 0 25 0 1 0 421812415 49487872 11356 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12082 11356 603 41 0 12041 0
vsize: 48328
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 13857 0 0 0 51970 47 0 0 25 0 1 0 421812415 50401280 11582 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12305 11582 603 41 0 12264 0
vsize: 49220
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 13857 0 0 0 52970 47 0 0 25 0 1 0 421812415 50401280 11582 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12305 11582 603 41 0 12264 0
vsize: 49220
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 13859 0 0 0 53971 47 0 0 25 0 1 0 421812415 50401280 11584 4294967295 134512640 134672761 3221224576 3221223744 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12305 11584 603 41 0 12264 0
vsize: 49220
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 13860 0 0 0 54971 47 0 0 25 0 1 0 421812415 50401280 11585 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12305 11585 603 41 0 12264 0
vsize: 49220
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14510 0 0 0 55968 50 0 0 25 0 1 0 421812415 50401280 11587 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12305 11587 603 41 0 12264 0
vsize: 49220
[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14510 0 0 0 56968 50 0 0 25 0 1 0 421812415 50401280 11587 4294967295 134512640 134672761 3221224576 3221223024 134644032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12305 11587 603 41 0 12264 0
vsize: 49220
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14565 0 0 0 57968 51 0 0 25 0 1 0 421812415 50745344 11642 4294967295 134512640 134672761 3221224576 3221222096 134566667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12389 11642 603 41 0 12348 0
vsize: 49556
[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14565 0 0 0 58968 51 0 0 25 0 1 0 421812415 50401280 11587 4294967295 134512640 134672761 3221224576 3221223024 134643556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12305 11587 603 41 0 12264 0
vsize: 49220
[startup+600.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 59969 51 0 0 25 0 1 0 421812415 50663424 11626 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12369 11626 603 41 0 12328 0
vsize: 49476
[startup+610.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 60969 51 0 0 25 0 1 0 421812415 50663424 11626 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12369 11626 603 41 0 12328 0
vsize: 49476
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 61969 51 0 0 25 0 1 0 421812415 50663424 11626 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12369 11626 603 41 0 12328 0
vsize: 49476
[startup+630.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 62970 51 0 0 25 0 1 0 421812415 50663424 11626 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12369 11626 603 41 0 12328 0
vsize: 49476
[startup+640.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 63970 51 0 0 25 0 1 0 421812415 50663424 11626 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12369 11626 603 41 0 12328 0
vsize: 49476
[startup+650.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 64971 51 0 0 25 0 1 0 421812415 50663424 11626 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12369 11626 603 41 0 12328 0
vsize: 49476
[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 65971 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+670.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 645
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 66971 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+680.038 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 684
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 67972 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223724 134614482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+690.038 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 698
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 68972 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+700.039 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 698
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 69973 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+710.041 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 698
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 70973 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+720.042 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 698
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 71974 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+730.042 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 698
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 72974 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+740.042 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 698
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14604 0 0 0 73974 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+750.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14640 0 0 0 74975 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+760.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14640 0 0 0 75975 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+770.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14640 0 0 0 76975 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+780.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14640 0 0 0 77976 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+790.045 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14640 0 0 0 78976 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+800.046 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14640 0 0 0 79977 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+810.046 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14680 0 0 0 80977 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+820.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14680 0 0 0 81977 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+830.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14680 0 0 0 82978 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+840.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14680 0 0 0 83978 51 0 0 25 0 1 0 421812415 50610176 11613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11613 603 41 0 12315 0
vsize: 49424
[startup+850.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14681 0 0 0 84979 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+860.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14681 0 0 0 85979 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+870.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14681 0 0 0 86979 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+880.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14721 0 0 0 87980 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+890.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14721 0 0 0 88980 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223776 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+900.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14721 0 0 0 89981 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+910.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14721 0 0 0 90981 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+920.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14721 0 0 0 91981 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+930.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14721 0 0 0 92982 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+940.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14721 0 0 0 93982 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+950.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14721 0 0 0 94982 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+960.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14762 0 0 0 95983 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223616 134612587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+970.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14762 0 0 0 96983 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+980.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14762 0 0 0 97983 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+990.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 700
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14762 0 0 0 98984 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223776 134610602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14762 0 0 0 99984 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14762 0 0 0 100984 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14762 0 0 0 101984 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14762 0 0 0 102985 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 103985 51 0 0 25 0 1 0 421812415 50872320 11655 4294967295 134512640 134672761 3221224576 3221223672 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12420 11655 603 41 0 12379 0
vsize: 49680
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 104986 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 105986 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 106986 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223776 134610637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 107987 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 108987 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 109987 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 110988 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14803 0 0 0 111988 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14849 0 0 0 112988 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223616 134603558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14849 0 0 0 113988 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14849 0 0 0 114989 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14849 0 0 0 115989 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14849 0 0 0 116989 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14849 0 0 0 117990 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 14849 0 0 0 118990 51 0 0 25 0 1 0 421812415 50610176 11614 4294967295 134512640 134672761 3221224576 3221223760 134615796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12356 11614 603 41 0 12315 0
vsize: 49424
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 702
Raw data (stat): 645 (minisat+) R 644 29653 29652 0 -1 0 15234 0 0 0 119989 52 0 0 25 0 1 0 421812415 52195328 11999 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12743 11999 603 41 0 12702 0
vsize: 50972
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 702
Raw data (stat): 645 (minisat+) Z 644 29653 29652 0 -1 12 15235 0 0 0 119990 54 0 0 25 0 1 0 421812415 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.08
CPU time (s): 1200.45
CPU user time (s): 1199.9
CPU system time (s): 0.549916
CPU usage (%): 100.031
Max. virtual memory (Kb): 50972
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####