PB'05 competition: run trace

Some explanations

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

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        903096 kB
Buffers:         26748 kB
Cached:          84976 kB
SwapCached:          0 kB
Active:          34256 kB
Inactive:        80332 kB
HighTotal:      131008 kB
HighFree:        42420 kB
LowTotal:       903652 kB
LowFree:        860676 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11308 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:04:37 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 3819 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 843 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     833    29551 |     249       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  369/369          
c |         0 |     754    28838 |      --       0       --      -- |     --   | -79/-713
c |         0 |     754    28838 |     301       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.39094 s)
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:17506     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   19279    71994 |    5783       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12534          
c   -- var.elim.:  2000/12534          
c   -- var.elim.:  3000/12534          
c   -- var.elim.:  4000/12534          
c   -- var.elim.:  5000/12534          
c   -- var.elim.:  6000/12534          
c   -- var.elim.:  7000/12534          
c   -- var.elim.:  8000/12534          
c   -- var.elim.:  9000/12534          
c   -- var.elim.:  10000/12534          
c   -- var.elim.:  11000/12534          
c   -- var.elim.:  12000/12534          
c   -- var.elim.:  12534/12534          
c   -- var.elim.:  1000/6214          
c   -- var.elim.:  2000/6214          
c   -- var.elim.:  3000/6214          
c   -- var.elim.:  4000/6214          
c   -- var.elim.:  5000/6214          
c   -- var.elim.:  6000/6214          
c   -- var.elim.:  6214/6214          
c   -- subsuming                       
c   -- var.elim.:  1000/4474          
c   -- var.elim.:  2000/4474          
c   -- var.elim.:  3000/4474          
c   -- var.elim.:  4000/4474          
c   -- var.elim.:  4474/4474          
c   -- var.elim.:  84/84          
c |         0 |   13203   102706 |      --       0       --      -- |     --   | -6076/30713
c |         0 |   13203   102706 |    5281       0        0     nan |  0.000 % |
c |       100 |   13203   102706 |    5809     100    10869   108.7 |  0.032 % |
c |       252 |   13203   102706 |    6390     252    29406   116.7 |  0.032 % |
c ==============================================================================
c (current CPU-time: 6.81796 s)
c ==============================================================================
c [1mFound solution: 17[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       384 |   13416   103293 |    4024     384    39068   101.7 |  0.032 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4619          
c   -- var.elim.:  2000/4619          
c   -- var.elim.:  3000/4619          
c   -- var.elim.:  4000/4619          
c   -- var.elim.:  4619/4619          
c   -- var.elim.:  1000/3658          
c   -- var.elim.:  2000/3658          
c   -- var.elim.:  3000/3658          
c   -- var.elim.:  3658/3658          
c   -- var.elim.:  1000/1882          
c   -- var.elim.:  1882/1882          
c   -- var.elim.:  1000/1381          
c   -- var.elim.:  1381/1381          
c   -- var.elim.:  798/798          
c   -- var.elim.:  96/96          
c   -- subsuming                       
c   -- var.elim.:  769/769          
c   -- var.elim.:  92/92          
c |       384 |    8477    61819 |      --     384       --      -- |     --   | -2575/-6141
c |       384 |    8477    61819 |    3390     219    18284    83.5 |  0.032 % |
c |       484 |    8477    61819 |    3729     319    30394    95.3 | 14.496 % |
c |       634 |    8467    61779 |    4098     467    49582   106.2 | 14.562 % |
c |       864 |    8467    61779 |    4507     697    78555   112.7 | 14.562 % |
c ==============================================================================
c (current CPU-time: 8.48871 s)
c ==============================================================================
c [1mFound solution: 16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1050 |   16917    83692 |    5075     883   108804   123.2 | 14.562 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10045          
c   -- var.elim.:  2000/10045          
c   -- var.elim.:  3000/10045          
c   -- var.elim.:  4000/10045          
c   -- var.elim.:  5000/10045          
c   -- var.elim.:  6000/10045          
c   -- var.elim.:  7000/10045          
c   -- var.elim.:  8000/10045          
c   -- var.elim.:  9000/10045          
c   -- var.elim.:  10000/10045          
c   -- var.elim.:  10045/10045          
c   -- var.elim.:  1000/5474          
c   -- var.elim.:  2000/5474          
c   -- var.elim.:  3000/5474          
c   -- var.elim.:  4000/5474          
c   -- var.elim.:  5000/5474          
c   -- var.elim.:  5474/5474          
c   -- var.elim.:  1000/3730          
c   -- var.elim.:  2000/3730          
c   -- var.elim.:  3000/3730          
c   -- var.elim.:  3730/3730          
c   -- var.elim.:  1000/1336          
c   -- var.elim.:  1336/1336          
c   -- var.elim.:  518/518          
c   -- var.elim.:  203/203          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  613/613          
c   -- var.elim.:  30/30          
c   -- var.elim.:  28/28          
c   -- var.elim.:  33/33          
c |      1050 |    8507    61861 |      --     883       --      -- |     --   | -8410/-21830
c |      1050 |    8507    61861 |    3402     807    95022   117.7 | 14.562 % |
c |      1150 |    8507    61861 |    3743     907   106567   117.5 | 13.832 % |
c |      1301 |    8494    61789 |    4111    1056   123979   117.4 | 13.853 % |
c |      1526 |    8494    61789 |    4522    1281   146408   114.3 | 13.853 % |
c |      1864 |    8494    61789 |    4974    1619   186529   115.2 | 13.853 % |
c |      2370 |    8494    61789 |    5471    2125   250931   118.1 | 13.853 % |
c ==============================================================================
c (current CPU-time: 12.3441 s)
c ==============================================================================
c [1mFound solution: 15[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2891 |    8500    61797 |    2549    2643   300045   113.5 | 13.853 % |
c   -- subsuming                       
c   -- var.elim.:  86/86          
c   -- var.elim.:  140/140          
c |      2891 |    8483    61753 |      --    2643       --      -- |     --   | -6/14
c |      2891 |    8483    61753 |    3393    2263   250406   110.7 | 13.853 % |
c |      2992 |    8483    61753 |    3732    2364   257133   108.8 | 13.964 % |
c |      3144 |    8483    61753 |    4105    2516   272281   108.2 | 13.964 % |
c |      3371 |    8480    61740 |    4514    2737   304456   111.2 | 13.985 % |
c |      3709 |    8480    61740 |    4966    3075   354822   115.4 | 13.985 % |
c |      4215 |    8480    61740 |    5462    3581   419102   117.0 | 13.985 % |
c |      4974 |    8480    61740 |    6009    4340   513434   118.3 | 13.985 % |
c |      6121 |    8480    61740 |    6610    5487   672574   122.6 | 13.985 % |
c |      7830 |    8480    61740 |    7271    7196   927129   128.8 | 13.985 % |
c |     10399 |    8480    61740 |    7998    6811  1019072   149.6 | 13.985 % |
c |     14244 |    8480    61740 |    8797    7695  1329529   172.8 | 13.985 % |
c |     20013 |    8480    61740 |    9677    6758  1129323   167.1 | 13.985 % |
c |     28662 |    8480    61740 |   10645    8158  1521003   186.4 | 13.985 % |
c |     41638 |    8480    61740 |   11710   12515  2272351   181.6 | 13.985 % |
c |     61099 |    8480    61740 |   12881    9934  1557555   156.8 | 13.985 % |
c |     90292 |    8480    61740 |   14169    9958  1621197   162.8 | 13.985 % |
c |    134082 |    8480    61740 |   15586   15198  2400616   158.0 | 13.985 % |
c ==============================================================================
c (current CPU-time: 329.621 s)
c ==============================================================================
c [1mFound solution: 14[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    159157 |   17332    84561 |    5199   12058  2036407   168.9 | 13.985 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10367          
c   -- var.elim.:  2000/10367          
c   -- var.elim.:  3000/10367          
c   -- var.elim.:  4000/10367          
c   -- var.elim.:  5000/10367          
c   -- var.elim.:  6000/10367          
c   -- var.elim.:  7000/10367          
c   -- var.elim.:  8000/10367          
c   -- var.elim.:  9000/10367          
c   -- var.elim.:  10000/10367          
c   -- var.elim.:  10367/10367          
c   -- var.elim.:  1000/5558          
c   -- var.elim.:  2000/5558          
c   -- var.elim.:  3000/5558          
c   -- var.elim.:  4000/5558          
c   -- var.elim.:  5000/5558          
c   -- var.elim.:  5558/5558          
c   -- var.elim.:  1000/3775          
c   -- var.elim.:  2000/3775          
c   -- var.elim.:  3000/3775          
c   -- var.elim.:  3775/3775          
c   -- var.elim.:  1000/1362          
c   -- var.elim.:  1362/1362          
c   -- var.elim.:  840/840          
c   -- subsuming                       
c   -- var.elim.:  21/21          
c |    159157 |    8502    61879 |      --   12058       --      -- |     --   | -8824/-22669
c |    159157 |    8502    61879 |    3400   12058  2036407   168.9 | 13.985 % |
c |    159257 |    8502    61879 |    3740    3674   531578   144.7 | 13.967 % |
c |    159408 |    8502    61879 |    4114    3825   543289   142.0 | 13.967 % |
c |    159636 |    8502    61879 |    4526    4053   570312   140.7 | 13.967 % |
c |    159973 |    8502    61879 |    4979    4390   603714   137.5 | 13.967 % |
c |    160480 |    8502    61879 |    5477    4897   677654   138.4 | 13.967 % |
c |    161239 |    8502    61879 |    6024    5656   782557   138.4 | 13.967 % |
c |    162378 |    8502    61879 |    6627    6795   958148   141.0 | 13.967 % |
c |    164086 |    8502    61879 |    7289    8503  1232527   145.0 | 13.967 % |
c |    166650 |    8502    61879 |    8018    8233  1063515   129.2 | 13.967 % |
c |    170494 |    8502    61879 |    8820    9045   972350   107.5 | 13.967 % |
c |    176263 |    8502    61879 |    9702    8210   910055   110.8 | 13.967 % |
c |    184913 |    8502    61879 |   10673    9581  1356153   141.5 | 13.967 % |
c |    197887 |    8502    61879 |   11740   10252  1387767   135.4 | 13.967 % |
c |    217348 |    8502    61879 |   12914   12380  1812788   146.4 | 13.967 % |
c |    246540 |    8502    61879 |   14205   13495  1718231   127.3 | 13.967 % |
c |    290330 |    8500    61867 |   15622   11940  1247618   104.5 | 13.988 % |
c |    356014 |    8500    61867 |   17185   16270  1962707   120.6 | 13.988 % |
c ==============================================================================
c (current CPU-time: 777.864 s)
c ==============================================================================
c [1mFound solution: 13[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 |    356891 |    8511    61893 |    2553   17147  2077261   121.1 | 13.988 % |
c   -- subsuming                       
c   -- var.elim.:  103/103          
c   -- var.elim.:  115/115          
c |    356891 |    8448    61537 |      --   17147       --      -- |     --   | -8/35
c |    356891 |    8448    61537 |    3379    5350   469915    87.8 | 13.988 % |
c |    356991 |    8448    61537 |    3717    3667   281091    76.7 | 14.322 % |
c |    357141 |    8448    61537 |    4088    3817   297607    78.0 | 14.322 % |
c |    357368 |    8448    61537 |    4497    4044   318608    78.8 | 14.322 % |
c |    357705 |    8448    61537 |    4947    4381   368925    84.2 | 14.322 % |
c |    358213 |    8448    61537 |    5442    4889   412743    84.4 | 14.322 % |
c |    358972 |    8448    61537 |    5986    5648   483670    85.6 | 14.322 % |
c |    360111 |    8448    61537 |    6585    6787   622178    91.7 | 14.322 % |
c |    361819 |    8448    61537 |    7243    8495   812039    95.6 | 14.322 % |
c |    364381 |    8448    61537 |    7967    5495   483911    88.1 | 14.322 % |
c |    368227 |    8448    61537 |    8764    9341  1016170   108.8 | 14.322 % |
c |    373994 |    8448    61537 |    9641    8244  1241709   150.6 | 14.322 % |
c |    382644 |    8448    61537 |   10605    9844  1237814   125.7 | 14.322 % |
c |    395618 |    8448    61537 |   11665   11234  1476031   131.4 | 14.322 % |
c |    415079 |    8448    61537 |   12832    8791  1172503   133.4 | 14.322 % |
c |    444274 |    8448    61537 |   14115   14312  2145399   149#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.97 0.91 1/55 2553
Raw data (stat): 2553 (runsolver) R 2552 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 357272311 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99991 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 3060 0 0 0 986 13 0 0 25 0 1 0 357272311 13246464 2515 4294967295 134512640 134672761 3221224576 3221223024 134643499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3234 2515 603 41 0 3193 0
vsize: 12936
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 4810 0 0 0 1979 20 0 0 25 0 1 0 357272311 17862656 3652 4294967295 134512640 134672761 3221224576 3221223760 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4361 3652 603 41 0 4320 0
vsize: 17444
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 5220 0 0 0 2978 21 0 0 25 0 1 0 357272311 19558400 4062 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4775 4062 603 41 0 4734 0
vsize: 19100
[startup+40.001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 5497 0 0 0 3976 23 0 0 25 0 1 0 357272311 20705280 4339 4294967295 134512640 134672761 3221224576 3221223616 134603517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5055 4339 603 41 0 5014 0
vsize: 20220
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 5786 0 0 0 4976 23 0 0 25 0 1 0 357272311 21884928 4628 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5343 4628 603 41 0 5302 0
vsize: 21372
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 5845 0 0 0 5975 24 0 0 25 0 1 0 357272311 22114304 4687 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5399 4687 603 41 0 5358 0
vsize: 21596
[startup+70.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6258 0 0 0 6974 25 0 0 25 0 1 0 357272311 23801856 5100 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5811 5100 603 41 0 5770 0
vsize: 23244
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6279 0 0 0 7974 25 0 0 25 0 1 0 357272311 23945216 5121 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5846 5121 603 41 0 5805 0
vsize: 23384
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6292 0 0 0 8974 26 0 0 25 0 1 0 357272311 23945216 5134 4294967295 134512640 134672761 3221224576 3221223616 134612835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5846 5134 603 41 0 5805 0
vsize: 23384
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6293 0 0 0 9974 26 0 0 25 0 1 0 357272311 23945216 5135 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5846 5135 603 41 0 5805 0
vsize: 23384
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6293 0 0 0 10974 26 0 0 25 0 1 0 357272311 23945216 5135 4294967295 134512640 134672761 3221224576 3221223760 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5846 5135 603 41 0 5805 0
vsize: 23384
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6293 0 0 0 11974 26 0 0 25 0 1 0 357272311 23945216 5135 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5846 5135 603 41 0 5805 0
vsize: 23384
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6351 0 0 0 12974 27 0 0 25 0 1 0 357272311 24186880 5193 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5905 5193 603 41 0 5864 0
vsize: 23620
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6402 0 0 0 13974 27 0 0 25 0 1 0 357272311 24322048 5244 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5938 5244 603 41 0 5897 0
vsize: 23752
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6480 0 0 0 14973 28 0 0 25 0 1 0 357272311 24707072 5322 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6032 5322 603 41 0 5991 0
vsize: 24128
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6480 0 0 0 15973 28 0 0 25 0 1 0 357272311 24702976 5322 4294967295 134512640 134672761 3221224576 3221223760 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5322 603 41 0 5990 0
vsize: 24124
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6480 0 0 0 16973 28 0 0 25 0 1 0 357272311 24702976 5322 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6031 5322 603 41 0 5990 0
vsize: 24124
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6480 0 0 0 17973 28 0 0 25 0 1 0 357272311 24698880 5322 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6030 5322 603 41 0 5989 0
vsize: 24120
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6601 0 0 0 18973 29 0 0 25 0 1 0 357272311 25210880 5443 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6155 5443 603 41 0 6114 0
vsize: 24620
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6925 0 0 0 19972 30 0 0 25 0 1 0 357272311 26591232 5767 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6492 5767 603 41 0 6451 0
vsize: 25968
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6942 0 0 0 20972 30 0 0 25 0 1 0 357272311 26656768 5783 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6508 5783 603 41 0 6467 0
vsize: 26032
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6942 0 0 0 21972 30 0 0 25 0 1 0 357272311 26656768 5783 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6508 5783 603 41 0 6467 0
vsize: 26032
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6942 0 0 0 22972 30 0 0 25 0 1 0 357272311 26656768 5783 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6508 5783 603 41 0 6467 0
vsize: 26032
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6943 0 0 0 23972 30 0 0 25 0 1 0 357272311 26656768 5784 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6508 5784 603 41 0 6467 0
vsize: 26032
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6943 0 0 0 24972 30 0 0 25 0 1 0 357272311 26656768 5784 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6508 5784 603 41 0 6467 0
vsize: 26032
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6943 0 0 0 25973 30 0 0 25 0 1 0 357272311 26656768 5784 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6508 5784 603 41 0 6467 0
vsize: 26032
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 6999 0 0 0 26973 30 0 0 25 0 1 0 357272311 26877952 5840 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6562 5840 603 41 0 6521 0
vsize: 26248
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 7192 0 0 0 27972 31 0 0 25 0 1 0 357272311 27701248 6032 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6763 6032 603 41 0 6722 0
vsize: 27052
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 7330 0 0 0 28972 31 0 0 25 0 1 0 357272311 28262400 6169 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6900 6169 603 41 0 6859 0
vsize: 27600
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 7330 0 0 0 29972 31 0 0 25 0 1 0 357272311 28262400 6169 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6900 6169 603 41 0 6859 0
vsize: 27600
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 7462 0 0 0 30972 31 0 0 25 0 1 0 357272311 28807168 6300 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7033 6300 603 41 0 6992 0
vsize: 28132
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 7462 0 0 0 31972 31 0 0 25 0 1 0 357272311 28807168 6300 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7033 6300 603 41 0 6992 0
vsize: 28132
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8144 0 0 0 32970 33 0 0 25 0 1 0 357272311 32702464 6981 4294967295 134512640 134672761 3221224576 3221222900 134605328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 6981 603 41 0 7943 0
vsize: 31936
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 33966 37 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 34966 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 35967 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223752 134615850 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 36966 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223728 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 37967 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 38967 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 39967 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 40967 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 41967 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 42967 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 43968 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 44968 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 45968 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 46968 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 47968 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 48968 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 49969 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 50969 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 51969 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 52969 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 53969 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 54969 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 55969 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223756 134615849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 56970 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615848 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 57970 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+590.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 58970 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223616 134613122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+600.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 59970 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 60970 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+620 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 61970 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+630 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 62971 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+640 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 63971 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+650 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 64971 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+660 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 65971 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+670 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 66971 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+680 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 67971 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223604 134612938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+689.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 68972 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+699.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 69972 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223632 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+709.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 70972 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 71972 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+729.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 72972 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+739.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 73972 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+749.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 74973 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+759.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 75973 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223632 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+770.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 8333 0 0 0 76973 38 0 0 25 0 1 0 357272311 30703616 6838 4294967295 134512640 134672761 3221224576 3221223712 134614683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6838 603 41 0 7455 0
vsize: 29984
[startup+780.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 77970 41 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+790.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 78970 41 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 79970 41 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 80970 42 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+820.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 81970 42 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223616 134612634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+830.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 82970 42 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 83971 42 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 84971 42 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 85971 42 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223672 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+870.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 86970 43 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 87970 43 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223184 134645372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 88970 43 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 89970 43 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 90970 43 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2553
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 91970 43 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 2594
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 92970 44 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+940.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2606
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 93974 44 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+950.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2606
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 94974 44 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+960.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2606
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 95974 44 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+970.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2606
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 96974 44 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+980.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2606
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9200 0 0 0 97974 44 0 0 25 0 1 0 357272311 31387648 7018 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7018 603 41 0 7622 0
vsize: 30652
[startup+990.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2608
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 98973 45 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223388 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2608
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 99973 45 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 100973 46 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 101972 46 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 102972 46 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 103972 46 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 104973 46 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 105973 46 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 106973 46 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223616 134612668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 107973 46 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223616 134612606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 108973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 109973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 110973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 111973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 112973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 113973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223500 1075346673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 114973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 115973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 116973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 117973 47 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 118973 48 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2610
Raw data (stat): 2553 (minisat+) R 2552 30927 30926 0 -1 0 9201 0 0 0 119973 48 0 0 25 0 1 0 357272311 31387648 7019 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7019 603 41 0 7622 0
vsize: 30652
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 2610
Raw data (stat): 2553 (minisat+) Z 2552 30927 30926 0 -1 12 9202 0 0 0 119974 49 0 0 25 0 1 0 357272311 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.07
CPU time (s): 1200.24
CPU user time (s): 1199.74
CPU system time (s): 0.498924
CPU usage (%): 100.014
Max. virtual memory (Kb): 31936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####