PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a2.opb
MD5SUM	6005a01d3f2ae55b0ca9c19f876c5827
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	139
Optimality of the best value was proved	NO
Number of terms in the objective function	360
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	360
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	360
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	360
Total number of constraints	980
Number of constraints which are clauses	980
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 5501

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-14 00:13:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3924 boxname=wulflinc19 idbench=164 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6005a01d3f2ae55b0ca9c19f876c5827  /oldhome/oroussel/tmp/wulflinc19/normalized-ii8a2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-ii8a2.opb /oldhome/oroussel/tmp/wulflinc19/normalized-ii8a2.opb
IDLAUNCH: 3924
/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:        889280 kB
Buffers:         34344 kB
Cached:          77324 kB
SwapCached:         56 kB
Active:          47792 kB
Inactive:        66896 kB
HighTotal:      131008 kB
HighFree:        49644 kB
LowTotal:       903652 kB
LowFree:        839636 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25060 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:33:47 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 3924 7 1200.15 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 980 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 |     974     2364 |     292       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  360/360          
c |         0 |     974     2364 |     389       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.031995 s)
c ==============================================================================
c [1mFound solution: 155[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13276     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         4 |   16823    39419 |    5046       4       26     6.5 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10620          
c   -- var.elim.:  2000/10620          
c   -- var.elim.:  3000/10620          
c   -- var.elim.:  4000/10620          
c   -- var.elim.:  5000/10620          
c   -- var.elim.:  6000/10620          
c   -- var.elim.:  7000/10620          
c   -- var.elim.:  8000/10620          
c   -- var.elim.:  9000/10620          
c   -- var.elim.:  10000/10620          
c   -- var.elim.:  10620/10620          
c   -- var.elim.:  1000/5202          
c   -- var.elim.:  2000/5202          
c   -- var.elim.:  3000/5202          
c   -- var.elim.:  4000/5202          
c   -- var.elim.:  5000/5202          
c   -- var.elim.:  5202/5202          
c   -- var.elim.:  1000/3136          
c   -- var.elim.:  2000/3136          
c   -- var.elim.:  3000/3136          
c   -- var.elim.:  3136/3136          
c   -- var.elim.:  1000/2140          
c   -- var.elim.:  2000/2140          
c   -- var.elim.:  2140/2140          
c   -- var.elim.:  1000/1777          
c   -- var.elim.:  1777/1777          
c   -- var.elim.:  1000/1178          
c   -- var.elim.:  1178/1178          
c   -- var.elim.:  166/166          
c   -- subsuming                       
c   -- var.elim.:  1000/1513          
c   -- var.elim.:  1513/1513          
c   -- var.elim.:  28/28          
c |         4 |    5485    29536 |      --       4       --      -- |     --   | -11338/-9882
c |         4 |    5485    29536 |    2194       4       26     6.5 |  0.000 % |
c |       104 |    4960    26056 |    2182      76     9115   119.9 |  9.432 % |
c |       254 |    4840    25202 |    2342     216    17524    81.1 | 11.697 % |
c |       480 |    4751    24616 |    2529     438    37566    85.8 | 13.344 % |
c ==============================================================================
c (current CPU-time: 6.37703 s)
c ==============================================================================
c [1mFound solution: 151[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 |       624 |   14813    48960 |    4443     577    52874    91.6 | 13.344 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9169          
c   -- var.elim.:  2000/9169          
c   -- var.elim.:  3000/9169          
c   -- var.elim.:  4000/9169          
c   -- var.elim.:  5000/9169          
c   -- var.elim.:  6000/9169          
c   -- var.elim.:  7000/9169          
c   -- var.elim.:  8000/9169          
c   -- var.elim.:  9000/9169          
c   -- var.elim.:  9169/9169          
c   -- var.elim.:  1000/4240          
c   -- var.elim.:  2000/4240          
c   -- var.elim.:  3000/4240          
c   -- var.elim.:  4000/4240          
c   -- var.elim.:  4240/4240          
c   -- var.elim.:  1000/2548          
c   -- var.elim.:  2000/2548          
c   -- var.elim.:  2548/2548          
c   -- var.elim.:  1000/1665          
c   -- var.elim.:  1665/1665          
c   -- var.elim.:  1000/1210          
c   -- var.elim.:  1210/1210          
c   -- var.elim.:  804/804          
c   -- var.elim.:  22/22          
c   -- var.elim.:  57/57          
c   -- subsuming                       
c   -- var.elim.:  551/551          
c |       624 |    4766    25217 |      --     577       --      -- |     --   | -10011/-23670
c |       624 |    4766    25217 |    1906     379    10568    27.9 | 13.344 % |
c |       724 |    4576    23840 |    2013     466    17079    36.7 | 24.132 % |
c |       874 |    4543    23629 |    2198     612    29407    48.1 | 24.649 % |
c |      1101 |    4497    23295 |    2394     835    58506    70.1 | 25.388 % |
c |      1438 |    4480    23177 |    2623    1171    99171    84.7 | 25.647 % |
c |      1944 |    4357    22264 |    2806    1668   151040    90.6 | 27.605 % |
c |      2706 |    4303    21852 |    3049    2426   220816    91.0 | 28.455 % |
c |      3850 |    4268    21605 |    3326    3562   444771   124.9 | 29.010 % |
c ==============================================================================
c (current CPU-time: 13.126 s)
c ==============================================================================
c [1mFound solution: 145[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 |      5126 |   14274    45615 |    4282    4835   657308   135.9 | 29.010 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8881          
c   -- var.elim.:  2000/8881          
c   -- var.elim.:  3000/8881          
c   -- var.elim.:  4000/8881          
c   -- var.elim.:  5000/8881          
c   -- var.elim.:  6000/8881          
c   -- var.elim.:  7000/8881          
c   -- var.elim.:  8000/8881          
c   -- var.elim.:  8881/8881          
c   -- var.elim.:  1000/4068          
c   -- var.elim.:  2000/4068          
c   -- var.elim.:  3000/4068          
c   -- var.elim.:  4000/4068          
c   -- var.elim.:  4068/4068          
c   -- var.elim.:  1000/2372          
c   -- var.elim.:  2000/2372          
c   -- var.elim.:  2372/2372          
c   -- var.elim.:  1000/1443          
c   -- var.elim.:  1443/1443          
c   -- var.elim.:  1000/1120          
c   -- var.elim.:  1120/1120          
c   -- var.elim.:  840/840          
c   -- var.elim.:  348/348          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  544/544          
c |      5126 |    4291    22166 |      --    4835       --      -- |     --   | -9949/-23380
c |      5126 |    4291    22166 |    1716    3075   175966    57.2 | 29.010 % |
c |      5226 |    4291    22166 |    1888    2150   116941    54.4 | 34.540 % |
c |      5376 |    4291    22166 |    2076    2300   133220    57.9 | 34.540 % |
c |      5601 |    4291    22166 |    2284    2525   149060    59.0 | 34.540 % |
c |      5939 |    4291    22166 |    2512    2863   209842    73.3 | 34.540 % |
c |      6446 |    4259    21917 |    2743    3363   291778    86.8 | 35.022 % |
c |      7206 |    4259    21917 |    3018    4123   356951    86.6 | 35.023 % |
c |      8345 |    4259    21917 |    3319    3888   504573   129.8 | 35.022 % |
c |     10053 |    4182    21342 |    3585    4019   552855   137.6 | 36.263 % |
c |     12616 |    4182    21342 |    3944    4682   969114   207.0 | 36.263 % |
c |     16460 |    4160    21205 |    4315    4792   891714   186.1 | 36.539 % |
c |     22227 |    4160    21205 |    4747    6294  1361627   216.3 | 36.539 % |
c |     30876 |    4147    21112 |    5206    6014   925438   153.9 | 36.746 % |
c |     43852 |    4124    20948 |    5694    4753   978590   205.9 | 37.056 % |
c |     63314 |    4124    20948 |    6264    6267  1649481   263.2 | 37.056 % |
c |     92506 |    4124    20948 |    6890    8117  2008370   247.4 | 37.058 % |
c |    136295 |    4104    20787 |    7543    7313  1907634   260.9 | 37.401 % |
c |    201980 |    4104    20787 |    8297    8496  1986088   233.8 | 37.401 % |
c ==============================================================================
c (current CPU-time: 393.621 s)
c ==============================================================================
c [1mFound solution: 143[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 |    218576 |   13347    43041 |    4004    7948  2284179   287.4 | 37.401 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8226          
c   -- var.elim.:  2000/8226          
c   -- var.elim.:  3000/8226          
c   -- var.elim.:  4000/8226          
c   -- var.elim.:  5000/8226          
c   -- var.elim.:  6000/8226          
c   -- var.elim.:  7000/8226          
c   -- var.elim.:  8000/8226          
c   -- var.elim.:  8226/8226          
c   -- var.elim.:  1000/3688          
c   -- var.elim.:  2000/3688          
c   -- var.elim.:  3000/3688          
c   -- var.elim.:  3688/3688          
c   -- var.elim.:  1000/2147          
c   -- var.elim.:  2000/2147          
c   -- var.elim.:  2147/2147          
c   -- var.elim.:  1000/1339          
c   -- var.elim.:  1339/1339          
c   -- var.elim.:  954/954          
c   -- var.elim.:  482/482          
c   -- var.elim.:  120/120          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  36/36          
c |    218576 |    4127    20979 |      --    7948       --      -- |     --   | -9214/-22049
c |    218576 |    4127    20979 |    1650    5101   881882   172.9 | 37.401 % |
c |    218676 |    4127    20979 |    1815    2368   341893   144.4 | 39.069 % |
c |    218827 |    4127    20979 |    1997    2519   355698   141.2 | 39.069 % |
c#### 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.85 0.97 0.91 2/55 27334
Raw data (stat): 27334 (runsolver) R 27333 22929 22928 0 -1 64 2 0 0 0 0 0 0 0 19 0 1 0 480179315 1052672 97 4294967295 134512640 135381576 3221224464 3221219832 135024953 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.87 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 2441 0 0 0 986 13 0 0 25 0 1 0 480179315 11890688 2282 4294967295 134512640 134672761 3221224576 3221223024 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2903 2282 603 41 0 2862 0
vsize: 11612
[startup+20.0019 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 4293 0 0 0 1975 22 0 0 25 0 1 0 480179315 17661952 3788 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4312 3788 603 41 0 4271 0
vsize: 17248
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 4467 0 0 0 2975 23 0 0 25 0 1 0 480179315 18317312 3962 4294967295 134512640 134672761 3221224576 3221223600 134612939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4472 3962 603 41 0 4431 0
vsize: 17888
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 4650 0 0 0 3974 24 0 0 25 0 1 0 480179315 19091456 4145 4294967295 134512640 134672761 3221224576 3221223616 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4661 4145 603 41 0 4620 0
vsize: 18644
[startup+50.0065 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 4650 0 0 0 4973 24 0 0 25 0 1 0 480179315 19083264 4145 4294967295 134512640 134672761 3221224576 3221223616 134613120 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4659 4145 603 41 0 4618 0
vsize: 18636
[startup+60.0067 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 4759 0 0 0 5973 24 0 0 25 0 1 0 480179315 19476480 4254 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4755 4254 603 41 0 4714 0
vsize: 19020
[startup+70.0068 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5029 0 0 0 6972 25 0 0 25 0 1 0 480179315 20643840 4524 4294967295 134512640 134672761 3221224576 3221223760 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5040 4524 603 41 0 4999 0
vsize: 20160
[startup+80.0065 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5198 0 0 0 7972 25 0 0 25 0 1 0 480179315 21303296 4693 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5201 4693 603 41 0 5160 0
vsize: 20804
[startup+90.0061 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5501 0 0 0 8971 26 0 0 25 0 1 0 480179315 22581248 4996 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5513 4996 603 41 0 5472 0
vsize: 22052
[startup+100.006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5512 0 0 0 9971 26 0 0 25 0 1 0 480179315 22581248 5007 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5513 5007 603 41 0 5472 0
vsize: 22052
[startup+110.007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5512 0 0 0 10972 26 0 0 25 0 1 0 480179315 22581248 5007 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5513 5007 603 41 0 5472 0
vsize: 22052
[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5552 0 0 0 11972 26 0 0 25 0 1 0 480179315 22806528 5047 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5047 603 41 0 5527 0
vsize: 22272
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5620 0 0 0 12972 26 0 0 25 0 1 0 480179315 23068672 5115 4294967295 134512640 134672761 3221224576 3221223760 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5632 5115 603 41 0 5591 0
vsize: 22528
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27334
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5755 0 0 0 13971 27 0 0 25 0 1 0 480179315 23638016 5250 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5771 5250 603 41 0 5730 0
vsize: 23084
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5755 0 0 0 14971 27 0 0 25 0 1 0 480179315 23613440 5250 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5765 5250 603 41 0 5724 0
vsize: 23060
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5802 0 0 0 15971 27 0 0 25 0 1 0 480179315 23826432 5297 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5817 5297 603 41 0 5776 0
vsize: 23268
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5807 0 0 0 16972 27 0 0 25 0 1 0 480179315 23826432 5302 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5817 5302 603 41 0 5776 0
vsize: 23268
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5807 0 0 0 17972 27 0 0 25 0 1 0 480179315 23826432 5302 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5817 5302 603 41 0 5776 0
vsize: 23268
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5883 0 0 0 18972 28 0 0 25 0 1 0 480179315 24158208 5378 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5898 5378 603 41 0 5857 0
vsize: 23592
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5883 0 0 0 19972 28 0 0 25 0 1 0 480179315 24158208 5378 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5898 5378 603 41 0 5857 0
vsize: 23592
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 5962 0 0 0 20972 28 0 0 25 0 1 0 480179315 24481792 5456 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5977 5456 603 41 0 5936 0
vsize: 23908
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6021 0 0 0 21972 28 0 0 25 0 1 0 480179315 24719360 5515 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6035 5515 603 41 0 5994 0
vsize: 24140
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6092 0 0 0 22971 29 0 0 25 0 1 0 480179315 24973312 5586 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6097 5586 603 41 0 6056 0
vsize: 24388
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6092 0 0 0 23971 29 0 0 25 0 1 0 480179315 24973312 5586 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6097 5586 603 41 0 6056 0
vsize: 24388
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6092 0 0 0 24971 29 0 0 25 0 1 0 480179315 24973312 5586 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6097 5586 603 41 0 6056 0
vsize: 24388
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6092 0 0 0 25972 29 0 0 25 0 1 0 480179315 24973312 5586 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6097 5586 603 41 0 6056 0
vsize: 24388
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6174 0 0 0 26972 29 0 0 25 0 1 0 480179315 25366528 5668 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6193 5668 603 41 0 6152 0
vsize: 24772
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6540 0 0 0 27970 30 0 0 25 0 1 0 480179315 26804224 6034 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6544 6034 603 41 0 6503 0
vsize: 26176
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6721 0 0 0 28970 31 0 0 25 0 1 0 480179315 27529216 6215 4294967295 134512640 134672761 3221224576 3221223760 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6721 6215 603 41 0 6680 0
vsize: 26884
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6816 0 0 0 29970 31 0 0 25 0 1 0 480179315 27926528 6310 4294967295 134512640 134672761 3221224576 3221223760 134615776 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6818 6310 603 41 0 6777 0
vsize: 27272
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6816 0 0 0 30970 31 0 0 25 0 1 0 480179315 27922432 6310 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6817 6310 603 41 0 6776 0
vsize: 27268
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6816 0 0 0 31970 31 0 0 25 0 1 0 480179315 27918336 6310 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6816 6310 603 41 0 6775 0
vsize: 27264
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6816 0 0 0 32970 31 0 0 25 0 1 0 480179315 27836416 6298 4294967295 134512640 134672761 3221224576 3221223616 134613756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6796 6298 603 41 0 6755 0
vsize: 27184
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6816 0 0 0 33970 32 0 0 25 0 1 0 480179315 27828224 6296 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6794 6296 603 41 0 6753 0
vsize: 27176
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6816 0 0 0 34970 32 0 0 25 0 1 0 480179315 27828224 6296 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6794 6296 603 41 0 6753 0
vsize: 27176
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6816 0 0 0 35971 32 0 0 25 0 1 0 480179315 27828224 6296 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6794 6296 603 41 0 6753 0
vsize: 27176
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6817 0 0 0 36971 32 0 0 25 0 1 0 480179315 27824128 6296 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6793 6296 603 41 0 6752 0
vsize: 27172
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6817 0 0 0 37971 32 0 0 25 0 1 0 480179315 27820032 6295 4294967295 134512640 134672761 3221224576 3221223616 134612601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6792 6295 603 41 0 6751 0
vsize: 27168
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 6817 0 0 0 38971 32 0 0 25 0 1 0 480179315 27820032 6295 4294967295 134512640 134672761 3221224576 3221223712 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6792 6295 603 41 0 6751 0
vsize: 27168
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 39963 40 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223652 134603930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 40962 40 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 41961 40 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 42961 40 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27336
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 43960 40 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 44960 40 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 45960 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 46960 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 47960 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 48960 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 49961 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 50961 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 51961 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223616 134612701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 52961 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223672 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 53961 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 54961 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 55961 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 56962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 57962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223616 134613120 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 58962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 59962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 60962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 61962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 62962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 63962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 64962 41 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 65963 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 66963 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 67963 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223672 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 68963 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 69963 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 70963 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223616 134614286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 71963 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 72964 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27338
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 73964 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223728 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 74964 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 75964 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223616 134612821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 76964 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223616 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 77964 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 78964 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7770 0 0 0 79965 42 0 0 25 0 1 0 480179315 29622272 6791 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6791 603 41 0 7191 0
vsize: 28928
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7782 0 0 0 80965 42 0 0 25 0 1 0 480179315 29622272 6803 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6803 603 41 0 7191 0
vsize: 28928
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7794 0 0 0 81965 42 0 0 25 0 1 0 480179315 29622272 6815 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6815 603 41 0 7191 0
vsize: 28928
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7794 0 0 0 82965 42 0 0 25 0 1 0 480179315 29622272 6815 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6815 603 41 0 7191 0
vsize: 28928
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7794 0 0 0 83965 42 0 0 25 0 1 0 480179315 29622272 6815 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6815 603 41 0 7191 0
vsize: 28928
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7794 0 0 0 84965 42 0 0 25 0 1 0 480179315 29622272 6815 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6815 603 41 0 7191 0
vsize: 28928
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7794 0 0 0 85966 42 0 0 25 0 1 0 480179315 29622272 6815 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6815 603 41 0 7191 0
vsize: 28928
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7794 0 0 0 86966 42 0 0 25 0 1 0 480179315 29622272 6815 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7232 6815 603 41 0 7191 0
vsize: 28928
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7854 0 0 0 87966 42 0 0 25 0 1 0 480179315 29884416 6875 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7296 6875 603 41 0 7255 0
vsize: 29184
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7854 0 0 0 88966 42 0 0 25 0 1 0 480179315 29884416 6875 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7296 6875 603 41 0 7255 0
vsize: 29184
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7854 0 0 0 89966 42 0 0 25 0 1 0 480179315 29884416 6875 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7296 6875 603 41 0 7255 0
vsize: 29184
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7854 0 0 0 90966 43 0 0 25 0 1 0 480179315 29863936 6874 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7291 6874 603 41 0 7250 0
vsize: 29164
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 7854 0 0 0 91966 43 0 0 25 0 1 0 480179315 29863936 6874 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7291 6874 603 41 0 7250 0
vsize: 29164
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8030 0 0 0 92966 43 0 0 25 0 1 0 480179315 30654464 7050 4294967295 134512640 134672761 3221224576 3221223616 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7484 7050 603 41 0 7443 0
vsize: 29936
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8129 0 0 0 93966 43 0 0 25 0 1 0 480179315 31051776 7149 4294967295 134512640 134672761 3221224576 3221223448 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7581 7149 603 41 0 7540 0
vsize: 30324
[startup+950.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8239 0 0 0 94965 44 0 0 25 0 1 0 480179315 31449088 7259 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7678 7259 603 41 0 7637 0
vsize: 30712
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8239 0 0 0 95965 44 0 0 25 0 1 0 480179315 31449088 7259 4294967295 134512640 134672761 3221224576 3221223672 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7678 7259 603 41 0 7637 0
vsize: 30712
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8239 0 0 0 96965 44 0 0 25 0 1 0 480179315 31449088 7259 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7678 7259 603 41 0 7637 0
vsize: 30712
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8413 0 0 0 97965 45 0 0 25 0 1 0 480179315 32215040 7433 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7433 603 41 0 7824 0
vsize: 31460
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8906 0 0 0 98964 46 0 0 25 0 1 0 480179315 34193408 7926 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8348 7926 603 41 0 8307 0
vsize: 33392
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8970 0 0 0 99964 46 0 0 25 0 1 0 480179315 34455552 7990 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8412 7990 603 41 0 8371 0
vsize: 33648
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8970 0 0 0 100964 47 0 0 25 0 1 0 480179315 34455552 7990 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8412 7990 603 41 0 8371 0
vsize: 33648
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8970 0 0 0 101964 47 0 0 25 0 1 0 480179315 34455552 7990 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8412 7990 603 41 0 8371 0
vsize: 33648
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 8970 0 0 0 102964 47 0 0 25 0 1 0 480179315 34455552 7990 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8412 7990 603 41 0 8371 0
vsize: 33648
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27340
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 103964 47 0 0 25 0 1 0 480179315 34816000 8069 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8500 8069 603 41 0 8459 0
vsize: 34000
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 104964 47 0 0 25 0 1 0 480179315 34816000 8069 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8500 8069 603 41 0 8459 0
vsize: 34000
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 105964 47 0 0 25 0 1 0 480179315 34811904 8069 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 8069 603 41 0 8458 0
vsize: 33996
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 106964 47 0 0 25 0 1 0 480179315 34807808 8069 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8498 8069 603 41 0 8457 0
vsize: 33992
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 107964 47 0 0 25 0 1 0 480179315 34807808 8069 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8498 8069 603 41 0 8457 0
vsize: 33992
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 108964 47 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 109964 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 110965 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 111965 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 112965 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 113964 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 114964 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 115963 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 116963 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 117963 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 118964 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27342
Raw data (stat): 27334 (minisat+) R 27333 22929 22928 0 -1 0 9049 0 0 0 119964 48 0 0 25 0 1 0 480179315 34484224 8006 4294967295 134512640 134672761 3221224576 3221223776 134610630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8419 8006 603 41 0 8378 0
vsize: 33676
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 27342
Raw data (stat): 27334 (minisat+) Z 27333 22929 22928 0 -1 12 9050 0 0 0 119964 50 0 0 25 0 1 0 480179315 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.15
CPU user time (s): 1199.64
CPU system time (s): 0.506922
CPU usage (%): 100.008
Max. virtual memory (Kb): 34000
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####