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/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-air01.opb
MD5SUM	90db1995bd949fc5ac74143a523f3bcf
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3398
Optimality of the best value was proved	NO
Number of terms in the objective function	771
Biggest coefficient in the objective function	3698
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	1192753
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	3698
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	1192753
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03384
Number of variables	771
Total number of constraints	794
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	794
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	438
Trace number 22531

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-22 03:18:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11620 boxname=wulflinc19 idbench=894 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-air01.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-air01.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-air01.opb
IDLAUNCH: 11620
/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:        425424 kB
Buffers:         21280 kB
Cached:         564388 kB
SwapCached:        560 kB
Active:          38068 kB
Inactive:       549656 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        425172 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5172 kB
Slab:            15732 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 03:38:15 (client local time) WITH STATUS 10 IN 1200.52 SECONDS
stats: 11620 7 1200.52 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 46 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################
c   -- Clauses(.)/Splits(s): (none)
c ---[  44]---> BDD-cost:   49
c ---[  42]---> BDD-cost:   39
c ---[  40]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   53
c ---[  36]---> BDD-cost:   63
c ---[  34]---> BDD-cost:   61
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  139
c ---[  26]---> BDD-cost:  197
c ---[  24]---> BDD-cost:  233
c ---[  22]---> BDD-cost:  273
c ---[  20]---> BDD-cost:  353
c ---[  18]---> BDD-cost:  331
c ---[  16]---> BDD-cost:  527
c ---[  14]---> BDD-cost:  589
c ---[  12]---> BDD-cost:  607
c ---[  10]---> BDD-cost:  559
c ---[   8]---> BDD-cost:  755
c ---[   6]---> BDD-cost:  769
c ---[   4]---> BDD-cost:  741
c ---[   2]---> BDD-cost:  781
c ---[   0]---> BDD-cost:  873
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   20564    53488 |    6169       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8975          
c   -- var.elim.:  2000/8975          
c   -- var.elim.:  3000/8975          
c   -- var.elim.:  4000/8975          
c   -- var.elim.:  5000/8975          
c   -- var.elim.:  6000/8975          
c   -- var.elim.:  7000/8975          
c   -- var.elim.:  8000/8975          
c   -- var.elim.:  8975/8975          
c   -- var.elim.:  139/139          
c   -- subsuming                       
c   -- var.elim.:  89/89          
c   -- var.elim.:  86/86          
c |         0 |   20490    53248 |      --       0       --      -- |     --   | -74/-171
c |         0 |   20490    53248 |    8196       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.507922 s)
c ==============================================================================
c [1mFound solution: 9485[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7920   maxlim: 1183268   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        24 |   75815   250842 |   22744      24     2670   111.2 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8525          
c   -- var.elim.:  2000/8525          
c   -- var.elim.:  3000/8525          
c   -- var.elim.:  4000/8525          
c   -- var.elim.:  5000/8525          
c   -- var.elim.:  6000/8525          
c   -- var.elim.:  7000/8525          
c   -- var.elim.:  8000/8525          
c   -- var.elim.:  8525/8525          
c   -- var.elim.:  22/22          
c |        24 |   74329   244892 |      --      24       --      -- |     --   | -1459/-5819
c |        24 |   74329   244892 |   29731      24     2670   111.2 |  0.000 % |
c ==============================================================================
c (current CPU-time: 3.11253 s)
c ==============================================================================
c [1mFound solution: 7373[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185380   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        32 |   74372   245079 |   22311      32     3822   119.4 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  35/35          
c   -- var.elim.:  21/21          
c |        32 |   74337   244905 |      --      32       --      -- |     --   | -19/-61
c |        32 |   74337   244905 |   29734      32     3822   119.4 |  0.000 % |
c ==============================================================================
c (current CPU-time: 4.6123 s)
c ==============================================================================
c [1mFound solution: 7303[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185450   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        40 |   74362   245032 |   22308      40     4020   100.5 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  30/30          
c   -- var.elim.:  18/18          
c |        40 |   74357   245070 |      --      40       --      -- |     --   | -5/43
c |        40 |   74357   245070 |   29742      40     4020   100.5 |  0.000 % |
c ==============================================================================
c (current CPU-time: 6.10007 s)
c ==============================================================================
c [1mFound solution: 6939[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185814   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        60 |   74386   245211 |   22315      60     5555    92.6 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  31/31          
c   -- var.elim.:  13/13          
c |        60 |   74368   245070 |      --      60       --      -- |     --   | -6/-10
c |        60 |   74368   245070 |   29747      60     5555    92.6 |  0.000 % |
c |       160 |   74368   245070 |   32721     160    13685    85.5 |  1.535 % |
c |       310 |   74368   245070 |   35994     310    72941   235.3 |  1.535 % |
c |       535 |   74368   245070 |   39593     535   174006   325.2 |  1.535 % |
c ==============================================================================
c (current CPU-time: 10.9013 s)
c ==============================================================================
c [1mFound solution: 6605[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186148   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       787 |   74394   245190 |   22318     787   195076   247.9 |  1.535 % |
c   -- subsuming                       
c   -- var.elim.:  31/31          
c   -- var.elim.:  14/14          
c |       787 |   74388   245180 |      --     787       --      -- |     --   | -6/-5
c |       787 |   74388   245180 |   29755     787   195076   247.9 |  1.535 % |
c |       889 |   74388   245180 |   32730     889   217869   245.1 |  1.565 % |
c |      1041 |   74388   245180 |   36003    1041   289623   278.2 |  1.565 % |
c |      1267 |   74388   245180 |   39604    1267   421021   332.3 |  1.565 % |
c ==============================================================================
c (current CPU-time: 14.4178 s)
c ==============================================================================
c [1mFound solution: 6051[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186702   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1304 |   74400   245269 |   22319    1304   423466   324.7 |  1.565 % |
c   -- subsuming                       
c   -- var.elim.:  17/17          
c   -- var.elim.:  12/12          
c |      1304 |   74387   245175 |      --    1304       --      -- |     --   | -7/-27
c |      1304 |   74387   245175 |   29754    1304   423466   324.7 |  1.565 % |
c ==============================================================================
c (current CPU-time: 15.9836 s)
c ==============================================================================
c [1mFound solution: 5111[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1187642   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1322 |   74405   245281 |   22321    1322   424561   321.2 |  1.565 % |
c   -- subsuming                       
c   -- var.elim.:  22/22          
c   -- var.elim.:  13/13          
c |      1322 |   74392   245203 |      --    1322       --      -- |     --   | -4/-3
c |      1322 |   74392   245203 |   29756    1322   424561   321.2 |  1.565 % |
c |      1422 |   74392   245203 |   32732    1422   513647   361.2 |  1.652 % |
c |      1573 |   74392   245203 |   36005    1573   533037   338.9 |  1.652 % |
c |      1799 |   74392   245203 |   39606    1799   677054   376.4 |  1.652 % |
c ==============================================================================
c (current CPU-time: 20.011 s)
c ==============================================================================
c [1mFound solution: 4588[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1188165   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1872 |   74413   245300 |   22323    1872   715296   382.1 |  1.652 % |
c   -- subsuming                       
c   -- var.elim.:  487/487          
c   -- var.elim.:  35/35          
c |      1872 |   72796   238753 |      --    1872       --      -- |     --   | -10/-865
c |      1872 |   72796   238753 |   29118    1834   713716   389.2 |  1.652 % |
c |      1979 |   72796   238753 |   32030    1941   725118   373.6 |  2.972 % |
c |      2130 |   72796   238753 |   35233    2092   753016   360.0 |  2.972 % |
c |      2355 |   72796   238753 |   38756    2317   824527   355.9 |  2.972 % |
c |      2692 |   72796   238753 |   42632    2654   876997   330.4 |  2.972 % |
c |      3198 |   72796   238753 |   46895    3160   987776   312.6 |  2.972 % |
c |      3957 |   72796   238753 |   51585    3919  1303486   332.6 |  2.972 % |
c |      5098 |   72796   238753 |   56743    5060  2082990   411.7 |  2.972 % |
c |      6807 |   72796   238753 |   62417    6769  3138315   463.6 |  2.972 % |
c ==============================================================================
c (current CPU-time: 40.6518 s)
c ==============================================================================
c [1mFound solution: 3579[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5026   maxlim: 1185476   bits: 21/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7025 |  107755   363557 |   32326    6987  3169525   453.6 |  2.972 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6998          
c   -- var.elim.:  2000/6998          
c   -- var.elim.:  3000/6998          
c   -- var.elim.:  4000/6998          
c   -- var.elim.:  5000/6998          
c   -- var.elim.:  6000/6998          
c   -- var.elim.:  6998/6998          
c   -- var.elim.:  79/79          
c |      7025 |  106409   358285 |      --    6987       --      -- |     --   | -1265/-4914
c |      7025 |  106409   358285 |   42563    6825  3037532   445.1 |  2.972 % |
c |      7125 |  106409   358285 |   46819    6925  3047198   440.0 |  3.237 % |
c |      7278 |  106409   358285 |   51501    7078  3114086   440.0 |  3.237 % |
c |      7504 |  106409   358285 |   56652    7304  3253460   445.4 |  3.237 % |
c |      7842 |  106409   358285 |   62317    7642  3366629   440.5 |  3.237 % |
c |      8351 |  106409   358285 |   68549    8151  3751806   460.3 |  3.237 % |
c |      9111 |  106409   358285 |   75404    8911  4322060   485.0 |  3.237 % |
c |     10252 |  106345   358040 |   82894   10048  4911057   488.8 |  3.260 % |
c |     11960 |  106345   358040 |   91183   11756  6588634   560.4 |  3.260 % |
c |     14522 |  106345   358040 |  100302   14318  8165270   570.3 |  3.260 % |
c |     18371 |  106204   357526 |  110186   18158 10845871   597.3 |  3.324 % |
c |     24139 |  106204   357526 |  121204   23926 16243260   678.9 |  3.324 % |
c |     32788 |  105431   354871 |  132355   32574 30915058   949.1 |  3.804 % |
c |     45763 |  105431   354871 |  145590   45549 50244390  1103.1 |  3.804 % |
c |     65231 |  105431   354871 |  160149   65017 78862660  1213.0 |  3.804 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -CL000001_bit0 -CL000002_bit0 -CL000003_bit0 -CL000004_bit0 -CL000005_bit0 -CL000006_bit0 -CL000007_bit0 -CL000008_bit0 -CL000009_bit0 -CL000010_bit0 -CL000011_bit0 -CL000012_bit0 -CL000013_bit0 -CL000014_bit0 CL000015_bit0 -CL000016_bit0 -CL000017_bit0 -CL000018_bit0 -CL000019_bit0 -CL000020_bit0 -CL000021_bit0 -CL000022_bit0 -CL000023_bit0 -CL000024_bit0 -CL000025_bit0 -CL000026_bit0 -CL000027_bit0 -CL000028_bit0 -CL000029_bit0 -CL000030_bit0 -CL000031_bit0 -CL000032_bit0 -CL000033_bit0 -CL000034_bit0 -CL000035_bit0 -CL000036_bit0 -CL000037_bit0 -CL000038_bit0 CL000039_bit0 -CL000040_bit0 -CL000041_bit0 -CL000042_bit0 -CL000043_bit0 -CL000044_bit0 -CL000045_bit0 -CL000046_bit0 -CL000047_bit0 -CL000048_bit0 -CL000049_bit0 -CL000050_bit0 -CL000051_bit0 -CL000052_bit0 -CL000053_bit0 -CL000054_bit0 -CL000055_bit0 -CL000056_bit0 -CL000057_bit0 -CL000058_bit0 -CL000059_bit0 -CL000060_bit0 -CL000061_bit0 -CL000062_bit0 -CL000063_bit0 -CL000064_bit0 -CL000065_bit0 -CL000066_bit0 -CL000067_bit0 -CL000068_bit0 -CL000069_bit0 -CL000070_bit0 -CL000071_bit0 -CL000072_bit0 -CL000073_bit0 -CL000074_bit0 -CL000075_bit0 -CL000076_bit0 -CL000077_bit0 -CL000078_bit0 -CL000079_bit0 -CL000080_bit0 -CL000081_bit0 -CL000082_bit0 -CL000083_bit0 -CL000084_bit0 -CL000085_bit0 -CL000086_bit0 -CL000087_bit0 -CL000088_bit0 -CL000089_bit0 -CL000090_bit0 -CL000091_bit0 -CL000092_bit0 -CL000093_bit0 -CL000094_bit0 -CL000095_bit0 -CL000096_bit0 -CL000097_bit0 -CL000098_bit0 -CL000099_bit0 -CL000100_bit0 -CL000101_bit0 -CL000102_bit0 -CL000103_bit0 -CL000104_bit0 -CL000105_bit0 -CL000106_bit0 -CL000107_bit0 -CL000108_bit0 -CL000109_bit0 -CL000110_bit0 -CL000111_bit0 -CL000112_bit0 -CL000113_bit0 -CL000114_bit0 -CL000115_bit0 -CL000116_bit0 -CL000117_bit0 -CL000118_bit0 -CL000119_bit0 -CL000120_bit0 -CL000121_bit0 -CL000122_bit0 -CL000123_bit0 -CL000124_bit0 -CL000125_bit0 -CL000126_bit0 -CL000127_bit0 -CL000128_bit0 -CL000129_bit0 -CL000130_bit0 CL000131_bit0 -CL000132_bit0 -CL000133_bit0 -CL000134_bit0 -CL000135_bit0 -CL000136_bit0 -CL000137_bit0 -CL000138_bit0 -CL000139_bit0 -CL000140_bit0 -CL000141_bit0 -CL000142_bit0 -CL000143_bit0 -CL000144_bit0 -CL000145_bit0 -CL000146_bit0 -CL000147_bit0 -CL000148_bit0 -CL000149_bit0 -CL000150_bit0 -CL000151_bit0 -CL000152_bit0 -CL000153_bit0 -CL000154_bit0 -CL000155_bit0 -CL000156_bit0 -CL000157_bit0 -CL000158_bit0 -CL000159_bit0 -CL000160_bit0 -CL000161_bit0 -CL000162_bit0 -CL000163_bit0 -CL000164_bit0 -CL000165_bit0 -CL000166_bit0 -CL000167_bit0 -CL000168_bit0 -CL000169_bit0 -CL000170_bit0 -CL000171_bit0 -CL000172_bit0 -CL000173_bit0 -CL000174_bit0 -CL000175_bit0 -CL000176_bit0 -CL000177_bit0 -CL000178_bit0 -CL000179_bit0 -CL000180_bit0 -CL000181_bit0 -CL000182_bit0 -CL000183_bit0 -CL000184_bit0 -CL000185_bit0 -CL000186_bit0 -CL000187_bit0 -CL000188_bit0 -CL000189_bit0 -CL000190_bit0 -CL000191_bit0 -CL000192_bit0 -CL000193_bit0 -CL000194_bit0 -CL000195_bit0 -CL000196_bit0 -CL000197_bit0 -CL000198_bit0 -CL000199_bit0 -CL000200_bit0 -CL000201_bit0 -CL000202_bit0 -CL000203_bit0 -CL000204_bit0 -CL000205_bit0 -CL000206_bit0 -CL000207_bit0 -CL000208_bit0 -CL000209_bit0 -CL000210_bit0 -CL000211_bit0 -CL000212_bit0 -CL000213_bit0 -CL000214_bit0 -CL000215_bit0 -CL000216_bit0 -CL000217_bit0 -CL000218_bit0 -CL000219_bit0 -CL000220_bit0 -CL000221_bit0 -CL000222_bit0 -CL000223_bit0 -CL000224_bit0 -CL000225_bit0 -CL000226_bit0 -CL000227_bit0 -CL000228_bit0 -CL000229_bit0 -CL000230_bit0 -CL000231_bit0 -CL000232_bit0 -CL000233_bit0 -CL000234_bit0 -CL000235_bit0 -CL000236_bit0 -CL000237_bit0 -CL000238_bit0 -CL000239_bit0 -CL000240_bit0 -CL000241_bit0 -CL000242_bit0 -CL000243_bit0 -CL000244_bit0 -CL000245_bit0 -CL000246_bit0 -CL000247_bit0 -CL000248_bit0 -CL000249_bit0 -CL000250_bit0 -CL000251_bit0 -CL000252_bit0 -CL000253_bit0 -CL000254_bit0 -CL000255_bit0 -CL000256_bit0 -CL000257_bit0 -CL000258_bit0 -CL000259_bit0 -CL000260_bit0 -CL000261_bit0 -CL000262_bit0 -CL000263_bit0 -CL000264_bit0 -CL000265_bit0 -CL000266_bit0 -CL000267_bit0 -CL000268_bit0 -CL000269_bit0 -CL000270_bit0 -CL000271_bit0 -CL000272_bit0 -CL000273_bit0 -CL000274_bit0 -CL000275_bit0 -CL000276_bit0 -CL000277_bit0 -CL000278_bit0 -CL000279_bit0 -CL000280_bit0 -CL000281_bit0 -CL000282_bit0 -CL000283_bit0 -CL000284_bit0 -CL000285_bit0 -CL000286_bit0 CL000287_bit0 -CL000288_bit0 -CL000289_bit0 -CL000290_bit0 -CL000291_bit0 -CL000292_bit0 -CL000293_bit0 -CL000294_bit0 -CL000295_bit0 -CL000296_bit0 -CL000297_bit0 -CL000298_bit0 -CL000299_bit0 -CL000300_bit0 -CL000301_bit0 -CL000302_bit0 -CL000303_bit0 -CL000304_bit0 -CL000305_bit0 -CL000306_bit0 -CL000307_bit0 -CL000308_bit0 -CL000309_bit0 -CL000310_bit0 -CL000311_bit0 -CL000312_bit0 -CL000313_bit0 -CL000314_bit0 -CL000315_bit0 -CL000316_bit0 -CL000317_bit0 -CL000318_bit0 -CL000319_bit0 -CL000320_bit0 -CL000321_bit0 -CL000322_bit0 -CL000323_bit0 -CL000324_bit0 -CL000325_bit0 -CL000326_bit0 -CL000327_bit0 -CL000328_bit0 -CL000329_bit0 -CL000330_bit0 -CL000331_bit0 -CL000332_bit0 -CL000333_bit0 -CL000334_bit0 -CL000335_bit0 -CL000336_bit0 -CL000337_bit0 -CL000338_bit0 -CL000339_bit0 -CL000340_bit0 -CL000341_bit0 -CL000342_bit0 -CL000343_bit0 -CL000344_bit0 -CL000345_bit0 -CL000346_bit0 -CL000347_bit0 -CL000348_bit0 -CL000349_bit0 -CL000350_bit0 -CL000351_bit0 -CL000352_bit0 -CL000353_bit0 -CL000354_bit0 -CL000355_bit0 -CL000356_bit0 -CL000357_bit0 -CL000358_bit0 -CL000359_bit0 -CL000360_bit0 -CL000361_bit0 -CL000362_bit0 -CL000363_bit0 -CL000364_bit0 -CL000365_bit0 -CL000366_bit0 -CL000367_bit0 -CL000368_bit0 -CL000369_bit0 -CL000370_bit0 -CL000371_bit0 -CL000372_bit0 -CL000373_bit0 -CL000374_bit0 -CL000375_bit0 -CL000376_bit0 -CL000377_bit0 -CL000378_bit0 -CL000379_bit0 -CL000380_bit0 -CL000381_bit0 -CL000382_bit0 -CL000383_bit0 -CL000384_bit0 -CL000385_bit0 -CL000386_bit0 -CL000387_bit0 -CL000388_bit0 -CL000389_bit0 -CL000390_bit0 -CL000391_bit0 -CL000392_bit0 -CL000393_bit0 -CL000394_bit0 -CL000395_bit0 -CL000396_bit0 -CL000397_bit0 -CL000398_bit0 -CL000399_bit0 -CL000400_bit0 -CL000401_bit0 -CL000402_bit0 -CL000403_bit0 -CL000404_bit0 -CL000405_bit0 -CL000406_bit0 -CL000407_bit0 -CL000408_bit0 -CL000409_bit0 -CL000410_bit0 -CL000411_bit0 -CL000412_bit0 -CL000413_bit0 -CL000414_bit0 -CL000415_bit0 -CL000416_bit0 -CL000417_bit0 -CL000418_bit0 -CL000419_bit0 -CL000420_bit0 -CL000421_bit0 -CL000422_bit0 -CL000423_bit0 -CL000424_bit0 -CL000425_bit0 -CL000426_bit0 -CL000427_bit0 -CL000428_bit0 -CL000429_bit0 -CL000430_bit0 -CL000431_bit0 -CL000432_bit0 -CL000433_bit0 -CL000434_bit0 -CL000435_bit0 -CL000436_bit0 -CL000437_bit0 -CL000438_bit0 -CL000439_bit0 -CL000440_bit0 -CL000441_bit0 -CL000442_bit0 -CL000443_bit0 -CL000444_bit0 -CL000445_bit0 -CL000446_bit0 -CL000447_bit0 -CL000448_bit0 -CL000449_bit0 -CL000450_bit0 -CL000451_bit0 -CL000452_bit0 -CL000453_bit0 -CL000454_bit0 -CL000455_bit0 -CL000456_bit0 -CL000457_bit0 -CL000458_bit0 -CL000459_bit0 -CL000460_bit0 -CL000461_bit0 -CL000462_bit0 -CL000463_bit0 -CL000464_bit0 -CL000465_bit0 -CL000466_bit0 -CL000467_bit0 -CL000468_bit0 -CL000469_bit0 -CL000470_bit0 -CL000471_bit0 -CL000472_bit0 -CL000473_bit0 -CL000474_bit0 -CL000475_bit0 -CL000476_bit0 -CL000477_bit0 -CL000478_bit0 -CL000479_bit0 -CL000480_bit0 -CL000481_bit0 -CL000482_bit0 -CL000483_bit0 -CL000484_bit0 -CL000485_bit0 -CL000486_bit0 -CL000487_bit0 -CL000488_bit0 -CL000489_bit0 -CL000490_bit0 -CL000491_bit0 -CL000492_bit0 -CL000493_bit0 -CL000494_bit0 -CL000495_bit0 -CL000496_bit0 -CL000497_bit0 -CL000498_bit0 -CL000499_bit0 -CL000500_bit0 -CL000501_bit0 -CL000502_bit0 -CL000503_bit0 -CL000504_bit0 -CL000505_bit0 -CL000506_bit0 -CL000507_bit0 -CL000508_bit0 -CL000509_bit0 -CL000510_bit0 -CL000511_bit0 -CL000512_bit0 -CL000513_bit0 CL000514_bit0 -CL000515_bit0 -CL000516_bit0 -CL000517_bit0 -CL000518_bit0 -CL000519_bit0 -CL000520_bit0 -CL000521_bit0 CL000522_bit0 -CL000523_bit0 -CL000524_bit0 -CL000525_bit0 -CL000526_bit0 -CL000527_bit0 -CL000528_bit0 -CL000529_bit0 -CL000530_bit0 -CL000531_bit0 -CL000532_bit0 -CL000533_bit0 -CL000534_bit0 -CL000535_bit0 -CL000536_bit0 -CL000537_bit0 -CL000538_bit0 -CL000539_bit0 -CL000540_bit0 -CL000541_bit0 -CL000542_bit0 -CL000543_bit0 -CL000544_bit0 -CL000545_bit0 -CL000546_bit0 -CL000547_bit0 -CL000548_bit0 -CL000549_bit0 -CL000550_bit0 -CL000551_bit0 -CL000552_bit0 -CL000553_bit0 -CL000554_bit0 -CL000555_bit0 -CL000556_bit0 -CL000557_bit0 -CL000558_bit0 -CL000559_bit0 -CL000560_bit0 -CL000561_bit0 -CL000562_bit0 -CL000563_bit0 -CL000564_bit0 -CL000565_bit0 -CL000566_bit0 -CL000567_bit0 -CL000568_bit0 -CL000569_bit0 -CL000570_bit0 -CL000571_bit0 -CL000572_bit0 -CL000573_bit0 -CL000574_bit0 -CL000575_bit0 -CL000576_bit0 -CL000577_bit0 -CL000578_bit0 -CL000579_bit0 -CL000580_bit0 -CL000581_bit0 -CL000582_bit0 -CL000583_bit0 -CL000584_bit0 -CL000585_bit0 -CL000586_bit0 -CL000587_bit0 -CL000588_bit0 -CL000589_bit0 -CL000590_bit0 -CL000591_bit0 -CL000592_bit0 -CL000593_bit0 -CL000594_bit0 -CL000595_bit0 -CL000596_bit0 -CL000597_bit0 -CL000598_bit0 -CL000599_bit0 -CL000600_bit0 -CL000601_bit0 -CL000602_bit0 -CL000603_bit0 -CL000604_bit0 -CL000605_bit0 -CL000606_bit0 -CL000607_bit0 -CL000608_bit0 -CL000609_bit0 -CL000610_bit0 -CL000611_bit0 -CL000612_bit0 -CL000613_bit0 -CL000614_bit0 -CL000615_bit0 -CL000616_bit0 -CL000617_bit0 -CL000618_bit0 -CL000619_bit0 -CL000620_bit0 -CL000621_bit0 -CL000622_bit0 -CL000623_bit0 -CL000624_bit0 -CL000625_bit0 -CL000626_bit0 -CL000627_bit0 -CL000628_bit0 -CL000629_bit0 -CL000630_bit0 -CL000631_bit0 -CL000632_bit0 -CL000633_bit0 -CL000634_bit0 -CL000635_bit0 -CL000636_bit0 -CL000637_bit0 -CL000638_bit0 -CL000639_bit0 -CL000640_bit0 -CL000641_bit0 -CL000642_bit0 -CL000643_bit0 -CL000644_bit0 -CL000645_bit0 -CL000646_bit0 -CL000647_bit0 -CL000648_bit0 -CL000649_bit0 -CL000650_bit0 -CL000651_bit0 -CL000652_bit0 -CL000653_bit0 -CL000654_bit#### 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.98 2/55 15172
Raw data (stat): 15172 (runsolver) R 15171 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550415228 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 9087 0 0 0 977 21 0 0 25 0 1 0 550415228 31993856 6272 4294967295 134512640 134672761 3221224544 3221223552 134522555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7811 6272 603 41 0 7770 0
vsize: 31244
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 11196 0 0 0 1971 26 0 0 25 0 1 0 550415228 34385920 6848 4294967295 134512640 134672761 3221224544 3221223584 134612516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8395 6848 603 41 0 8354 0
vsize: 33580
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 12646 0 0 0 2967 30 0 0 25 0 1 0 550415228 36978688 7459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9028 7459 603 41 0 8987 0
vsize: 36112
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 14479 0 0 0 3962 34 0 0 25 0 1 0 550415228 44490752 9292 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10862 9292 603 41 0 10821 0
vsize: 43448
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 16373 0 0 0 4958 39 0 0 25 0 1 0 550415228 48861184 10589 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11929 10589 603 41 0 11888 0
vsize: 47716
[startup+60.0015 s]
Raw data (loadavg): 0.94 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 17313 0 0 0 5955 42 0 0 25 0 1 0 550415228 52822016 11529 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12896 11529 603 41 0 12855 0
vsize: 51584
[startup+70.0011 s]
Raw data (loadavg): 0.95 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 18111 0 0 0 6953 43 0 0 25 0 1 0 550415228 56098816 12327 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13696 12327 603 41 0 13655 0
vsize: 54784
[startup+80.0042 s]
Raw data (loadavg): 0.96 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 19663 0 0 0 7950 47 0 0 25 0 1 0 550415228 62431232 13879 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15242 13879 603 41 0 15201 0
vsize: 60968
[startup+90.0115 s]
Raw data (loadavg): 0.96 0.97 0.98 2/55 15172
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 20709 0 0 0 8948 49 0 0 25 0 1 0 550415228 66736128 14925 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16293 14925 603 41 0 16252 0
vsize: 65172
[startup+100.012 s]
Raw data (loadavg): 0.97 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 21411 0 0 0 9946 51 0 0 25 0 1 0 550415228 69488640 15627 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16965 15627 603 41 0 16924 0
vsize: 67860
[startup+110.013 s]
Raw data (loadavg): 0.97 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 22159 0 0 0 10944 53 0 0 25 0 1 0 550415228 72638464 16375 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17734 16375 603 41 0 17693 0
vsize: 70936
[startup+120.012 s]
Raw data (loadavg): 0.98 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 23055 0 0 0 11943 55 0 0 25 0 1 0 550415228 76279808 17271 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18623 17271 603 41 0 18582 0
vsize: 74492
[startup+130.032 s]
Raw data (loadavg): 0.98 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 23932 0 0 0 12942 58 0 0 25 0 1 0 550415228 79929344 18148 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19514 18148 603 41 0 19473 0
vsize: 78056
[startup+140.056 s]
Raw data (loadavg): 0.98 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 25001 0 0 0 13942 61 0 0 25 0 1 0 550415228 84348928 19217 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20593 19217 603 41 0 20552 0
vsize: 82372
[startup+150.065 s]
Raw data (loadavg): 0.98 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 26146 0 0 0 14941 63 0 0 25 0 1 0 550415228 89018368 20362 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21733 20362 603 41 0 21692 0
vsize: 86932
[startup+160.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 27108 0 0 0 15939 65 0 0 25 0 1 0 550415228 92856320 21324 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22670 21324 603 41 0 22629 0
vsize: 90680
[startup+170.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 28044 0 0 0 16937 67 0 0 25 0 1 0 550415228 96788480 22260 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23630 22260 603 41 0 23589 0
vsize: 94520
[startup+180.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 28787 0 0 0 17935 69 0 0 25 0 1 0 550415228 99790848 23003 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24363 23003 603 41 0 24322 0
vsize: 97452
[startup+190.083 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 29489 0 0 0 18935 71 0 0 25 0 1 0 550415228 102658048 23705 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25063 23705 603 41 0 25022 0
vsize: 100252
[startup+200.087 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 30586 0 0 0 19933 74 0 0 25 0 1 0 550415228 107163648 24802 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26163 24802 603 41 0 26122 0
vsize: 104652
[startup+210.093 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 31989 0 0 0 20931 77 0 0 25 0 1 0 550415228 112848896 26205 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27551 26205 603 41 0 27510 0
vsize: 110204
[startup+220.105 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 32986 0 0 0 21929 80 0 0 25 0 1 0 550415228 116932608 27202 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28548 27202 603 41 0 28507 0
vsize: 114192
[startup+230.105 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 34143 0 0 0 22927 82 0 0 25 0 1 0 550415228 121647104 28359 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29699 28359 603 41 0 29658 0
vsize: 118796
[startup+240.108 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 35427 0 0 0 23924 86 0 0 25 0 1 0 550415228 126922752 29643 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30987 29643 603 41 0 30946 0
vsize: 123948
[startup+250.112 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 36801 0 0 0 24921 89 0 0 25 0 1 0 550415228 132603904 31017 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32374 31017 603 41 0 32333 0
vsize: 129496
[startup+260.112 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 38066 0 0 0 25918 92 0 0 25 0 1 0 550415228 137781248 32282 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33638 32282 603 41 0 33597 0
vsize: 134552
[startup+270.112 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 39074 0 0 0 26916 94 0 0 25 0 1 0 550415228 141918208 33290 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34648 33290 603 41 0 34607 0
vsize: 138592
[startup+280.127 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 40169 0 0 0 27915 97 0 0 25 0 1 0 550415228 146432000 34385 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35750 34385 603 41 0 35709 0
vsize: 143000
[startup+290.136 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 41394 0 0 0 28914 99 0 0 25 0 1 0 550415228 151359488 35610 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36953 35610 603 41 0 36912 0
vsize: 147812
[startup+300.136 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 42624 0 0 0 29912 102 0 0 25 0 1 0 550415228 156426240 36840 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38190 36840 603 41 0 38149 0
vsize: 152760
[startup+310.136 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 43035 0 0 0 30911 102 0 0 25 0 1 0 550415228 158113792 37251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38602 37251 603 41 0 38561 0
vsize: 154408
[startup+320.136 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 43859 0 0 0 31909 105 0 0 25 0 1 0 550415228 161464320 38075 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39420 38075 603 41 0 39379 0
vsize: 157680
[startup+330.136 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 44430 0 0 0 32907 106 0 0 25 0 1 0 550415228 163930112 38646 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40022 38646 603 41 0 39981 0
vsize: 160088
[startup+340.136 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 45253 0 0 0 33905 109 0 0 25 0 1 0 550415228 167370752 39469 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40862 39469 603 41 0 40821 0
vsize: 163448
[startup+350.137 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 46003 0 0 0 34904 110 0 0 25 0 1 0 550415228 170430464 40219 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41609 40219 603 41 0 41568 0
vsize: 166436
[startup+360.138 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 46730 0 0 0 35902 112 0 0 25 0 1 0 550415228 173436928 40946 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42343 40946 603 41 0 42302 0
vsize: 169372
[startup+370.137 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 47405 0 0 0 36900 114 0 0 25 0 1 0 550415228 176115712 41621 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42997 41621 603 41 0 42956 0
vsize: 171988
[startup+380.137 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 48147 0 0 0 37898 116 0 0 25 0 1 0 550415228 179171328 42363 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43743 42363 603 41 0 43702 0
vsize: 174972
[startup+390.138 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15174
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 48863 0 0 0 38896 118 0 0 25 0 1 0 550415228 182067200 43079 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44450 43079 603 41 0 44409 0
vsize: 177800
[startup+400.139 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 49569 0 0 0 39895 120 0 0 25 0 1 0 550415228 185008128 43785 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45168 43785 603 41 0 45127 0
vsize: 180672
[startup+410.139 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 50259 0 0 0 40894 121 0 0 25 0 1 0 550415228 187863040 44475 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45865 44475 603 41 0 45824 0
vsize: 183460
[startup+420.139 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 51090 0 0 0 41892 124 0 0 25 0 1 0 550415228 191217664 45306 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46684 45306 603 41 0 46643 0
vsize: 186736
[startup+430.139 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 51954 0 0 0 42889 127 0 0 25 0 1 0 550415228 194797568 46170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47558 46170 603 41 0 47517 0
vsize: 190232
[startup+440.139 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 52721 0 0 0 43887 129 0 0 25 0 1 0 550415228 197922816 46937 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48321 46937 603 41 0 48280 0
vsize: 193284
[startup+450.14 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 53868 0 0 0 44885 131 0 0 25 0 1 0 550415228 202600448 48084 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49463 48084 603 41 0 49422 0
vsize: 197852
[startup+460.141 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 54839 0 0 0 45883 133 0 0 25 0 1 0 550415228 206589952 49055 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50437 49055 603 41 0 50396 0
vsize: 201748
[startup+470.141 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 56031 0 0 0 46881 136 0 0 25 0 1 0 550415228 211415040 50247 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51615 50247 603 41 0 51574 0
vsize: 206460
[startup+480.142 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 56838 0 0 0 47880 137 0 0 25 0 1 0 550415228 214806528 51054 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52443 51054 603 41 0 52402 0
vsize: 209772
[startup+490.141 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 57726 0 0 0 48877 140 0 0 25 0 1 0 550415228 218370048 51942 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53313 51942 603 41 0 53272 0
vsize: 213252
[startup+500.142 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 58599 0 0 0 49875 142 0 0 25 0 1 0 550415228 221925376 52815 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54181 52815 603 41 0 54140 0
vsize: 216724
[startup+510.142 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 59449 0 0 0 50873 144 0 0 25 0 1 0 550415228 225439744 53665 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55039 53665 603 41 0 54998 0
vsize: 220156
[startup+520.142 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 60309 0 0 0 51871 146 0 0 25 0 1 0 550415228 229003264 54525 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55909 54525 603 41 0 55868 0
vsize: 223636
[startup+530.143 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 61511 0 0 0 52869 149 0 0 25 0 1 0 550415228 233906176 55727 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57106 55727 603 41 0 57065 0
vsize: 228424
[startup+540.142 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 62500 0 0 0 53867 151 0 0 25 0 1 0 550415228 237973504 56716 4294967295 134512640 134672761 3221224544 3221223584 134612663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58099 56716 603 41 0 58058 0
vsize: 232396
[startup+550.143 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 63285 0 0 0 54865 153 0 0 25 0 1 0 550415228 241115136 57501 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58866 57501 603 41 0 58825 0
vsize: 235464
[startup+560.143 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 63876 0 0 0 55864 154 0 0 25 0 1 0 550415228 243597312 58092 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59472 58092 603 41 0 59431 0
vsize: 237888
[startup+570.143 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 64799 0 0 0 56862 157 0 0 25 0 1 0 550415228 247422976 59015 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60406 59015 603 41 0 60365 0
vsize: 241624
[startup+580.144 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 65735 0 0 0 57860 159 0 0 25 0 1 0 550415228 251203584 59951 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61329 59951 603 41 0 61288 0
vsize: 245316
[startup+590.144 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 66794 0 0 0 58858 161 0 0 25 0 1 0 550415228 255545344 61010 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62389 61010 603 41 0 62348 0
vsize: 249556
[startup+600.144 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 67712 0 0 0 59856 163 0 0 25 0 1 0 550415228 259362816 61928 4294967295 134512640 134672761 3221224544 3221223584 134612665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63321 61928 603 41 0 63280 0
vsize: 253284
[startup+610.145 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 68548 0 0 0 60854 165 0 0 25 0 1 0 550415228 262713344 62764 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64139 62764 603 41 0 64098 0
vsize: 256556
[startup+620.145 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 69285 0 0 0 61853 166 0 0 25 0 1 0 550415228 265764864 63501 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64884 63501 603 41 0 64843 0
vsize: 259536
[startup+630.146 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 70302 0 0 0 62851 169 0 0 25 0 1 0 550415228 269955072 64518 4294967295 134512640 134672761 3221224544 3221223728 134615994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65907 64518 603 41 0 65866 0
vsize: 263628
[startup+640.147 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 71233 0 0 0 63850 170 0 0 25 0 1 0 550415228 273764352 65449 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66837 65449 603 41 0 66796 0
vsize: 267348
[startup+650.147 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 72514 0 0 0 64847 173 0 0 25 0 1 0 550415228 278929408 66730 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68098 66730 603 41 0 68057 0
vsize: 272392
[startup+660.147 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 73604 0 0 0 65845 175 0 0 25 0 1 0 550415228 283480064 67820 4294967295 134512640 134672761 3221224544 3221223584 134613804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69209 67820 603 41 0 69168 0
vsize: 276836
[startup+670.147 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 74556 0 0 0 66843 178 0 0 25 0 1 0 550415228 287305728 68772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70143 68772 603 41 0 70102 0
vsize: 280572
[startup+680.148 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 75782 0 0 0 67841 180 0 0 25 0 1 0 550415228 292306944 69998 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71364 69998 603 41 0 71323 0
vsize: 285456
[startup+690.148 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15176
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 76695 0 0 0 68840 181 0 0 25 0 1 0 550415228 296026112 70911 4294967295 134512640 134672761 3221224544 3221223584 134612883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72272 70911 603 41 0 72231 0
vsize: 289088
[startup+700.149 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 77770 0 0 0 69838 184 0 0 25 0 1 0 550415228 300535808 71986 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73373 71986 603 41 0 73332 0
vsize: 293492
[startup+710.149 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 78668 0 0 0 70837 185 0 0 25 0 1 0 550415228 304197632 72884 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74267 72884 603 41 0 74226 0
vsize: 297068
[startup+720.149 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 79456 0 0 0 71835 186 0 0 25 0 1 0 550415228 307429376 73672 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75056 73672 603 41 0 75015 0
vsize: 300224
[startup+730.15 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 80163 0 0 0 72834 188 0 0 25 0 1 0 550415228 310235136 74379 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75741 74379 603 41 0 75700 0
vsize: 302964
[startup+740.151 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 81126 0 0 0 73832 190 0 0 25 0 1 0 550415228 314183680 75342 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76705 75342 603 41 0 76664 0
vsize: 306820
[startup+750.152 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 82178 0 0 0 74830 192 0 0 25 0 1 0 550415228 318558208 76394 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77773 76394 603 41 0 77732 0
vsize: 311092
[startup+760.152 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 83357 0 0 0 75827 195 0 0 25 0 1 0 550415228 323354624 77573 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78944 77573 603 41 0 78903 0
vsize: 315776
[startup+770.151 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 84718 0 0 0 76824 198 0 0 25 0 1 0 550415228 328970240 78934 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80315 78934 603 41 0 80274 0
vsize: 321260
[startup+780.152 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 85688 0 0 0 77823 200 0 0 25 0 1 0 550415228 332972032 79904 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81292 79904 603 41 0 81251 0
vsize: 325168
[startup+790.151 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 86694 0 0 0 78821 202 0 0 25 0 1 0 550415228 336986112 80910 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82272 80910 603 41 0 82231 0
vsize: 329088
[startup+800.153 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 87560 0 0 0 79819 204 0 0 25 0 1 0 550415228 340615168 81776 4294967295 134512640 134672761 3221224544 3221223744 134610683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83158 81776 603 41 0 83117 0
vsize: 332632
[startup+810.153 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 88334 0 0 0 80818 206 0 0 25 0 1 0 550415228 343789568 82550 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83933 82550 603 41 0 83892 0
vsize: 335732
[startup+820.153 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 89001 0 0 0 81816 208 0 0 25 0 1 0 550415228 346529792 83217 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84602 83217 603 41 0 84561 0
vsize: 338408
[startup+830.154 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 90069 0 0 0 82813 211 0 0 25 0 1 0 550415228 350867456 84285 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85661 84285 603 41 0 85620 0
vsize: 342644
[startup+840.154 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 90998 0 0 0 83811 213 0 0 25 0 1 0 550415228 354758656 85214 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86611 85214 603 41 0 86570 0
vsize: 346444
[startup+850.154 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 91623 0 0 0 84809 215 0 0 25 0 1 0 550415228 357236736 85839 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87216 85839 603 41 0 87175 0
vsize: 348864
[startup+860.154 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 92024 0 0 0 85808 216 0 0 25 0 1 0 550415228 359014400 86240 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87650 86240 603 41 0 87609 0
vsize: 350600
[startup+870.154 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 92083 0 0 0 86808 216 0 0 25 0 1 0 550415228 359145472 86299 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87682 86299 603 41 0 87641 0
vsize: 350728
[startup+880.155 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 92470 0 0 0 87807 218 0 0 25 0 1 0 550415228 361107456 86686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88161 86686 603 41 0 88120 0
vsize: 352644
[startup+890.155 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 92901 0 0 0 88806 219 0 0 25 0 1 0 550415228 362840064 87117 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88584 87117 603 41 0 88543 0
vsize: 354336
[startup+900.156 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 93473 0 0 0 89805 220 0 0 25 0 1 0 550415228 365133824 87689 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89144 87689 603 41 0 89103 0
vsize: 356576
[startup+910.155 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 94323 0 0 0 90804 221 0 0 25 0 1 0 550415228 368676864 88539 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90009 88539 603 41 0 89968 0
vsize: 360036
[startup+920.155 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 94510 0 0 0 91804 222 0 0 25 0 1 0 550415228 369459200 88726 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90200 88726 603 41 0 90159 0
vsize: 360800
[startup+930.156 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 95058 0 0 0 92803 223 0 0 25 0 1 0 550415228 371679232 89274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90742 89274 603 41 0 90701 0
vsize: 362968
[startup+940.156 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 96020 0 0 0 93802 224 0 0 25 0 1 0 550415228 375558144 90236 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91689 90236 603 41 0 91648 0
vsize: 366756
[startup+950.157 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 96526 0 0 0 94801 225 0 0 25 0 1 0 550415228 377610240 90742 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92190 90742 603 41 0 92149 0
vsize: 368760
[startup+960.157 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 97180 0 0 0 95799 227 0 0 25 0 1 0 550415228 380342272 91396 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92857 91396 603 41 0 92816 0
vsize: 371428
[startup+970.156 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 97699 0 0 0 96798 229 0 0 25 0 1 0 550415228 382435328 91915 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93368 91915 603 41 0 93327 0
vsize: 373472
[startup+980.156 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 98287 0 0 0 97797 230 0 0 25 0 1 0 550415228 384876544 92503 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93964 92503 603 41 0 93923 0
vsize: 375856
[startup+990.157 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15178
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 99063 0 0 0 98795 232 0 0 25 0 1 0 550415228 388022272 93279 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94732 93279 603 41 0 94691 0
vsize: 378928
[startup+1000.16 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 99526 0 0 0 99794 233 0 0 25 0 1 0 550415228 389971968 93742 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95208 93742 603 41 0 95167 0
vsize: 380832
[startup+1010.16 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 100048 0 0 0 100793 234 0 0 25 0 1 0 550415228 392048640 94264 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95715 94264 603 41 0 95674 0
vsize: 382860
[startup+1020.16 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 100489 0 0 0 101792 236 0 0 25 0 1 0 550415228 393871360 94705 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96160 94705 603 41 0 96119 0
vsize: 384640
[startup+1030.16 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 101161 0 0 0 102790 238 0 0 25 0 1 0 550415228 396578816 95377 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96821 95377 603 41 0 96780 0
vsize: 387284
[startup+1040.16 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 101756 0 0 0 103788 239 0 0 25 0 1 0 550415228 399048704 95972 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97424 95972 603 41 0 97383 0
vsize: 389696
[startup+1050.16 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 102335 0 0 0 104787 242 0 0 25 0 1 0 550415228 401367040 96551 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97990 96551 603 41 0 97949 0
vsize: 391960
[startup+1060.16 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 102907 0 0 0 105786 243 0 0 25 0 1 0 550415228 403828736 97123 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98591 97123 603 41 0 98550 0
vsize: 394364
[startup+1070.16 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 103345 0 0 0 106785 244 0 0 25 0 1 0 550415228 405549056 97561 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99011 97561 603 41 0 98970 0
vsize: 396044
[startup+1080.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 104005 0 0 0 107784 245 0 0 25 0 1 0 550415228 408268800 98221 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99675 98221 603 41 0 99634 0
vsize: 398700
[startup+1090.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 104836 0 0 0 108783 247 0 0 25 0 1 0 550415228 411672576 99052 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100506 99052 603 41 0 100465 0
vsize: 402024
[startup+1100.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 105187 0 0 0 109782 248 0 0 25 0 1 0 550415228 413118464 99403 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100859 99403 603 41 0 100818 0
vsize: 403436
[startup+1110.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 105600 0 0 0 110782 248 0 0 25 0 1 0 550415228 414851072 99816 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101282 99816 603 41 0 101241 0
vsize: 405128
[startup+1120.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 106032 0 0 0 111781 250 0 0 25 0 1 0 550415228 416555008 100248 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101698 100248 603 41 0 101657 0
vsize: 406792
[startup+1130.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 106268 0 0 0 112781 250 0 0 25 0 1 0 550415228 417607680 100484 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101955 100484 603 41 0 101914 0
vsize: 407820
[startup+1140.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 106473 0 0 0 113780 250 0 0 25 0 1 0 550415228 418390016 100689 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 102146 100689 603 41 0 102105 0
vsize: 408584
[startup+1150.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 106907 0 0 0 114780 251 0 0 25 0 1 0 550415228 420225024 101123 4294967295 134512640 134672761 3221224544 3221223680 134614664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 102594 101123 603 41 0 102553 0
vsize: 410376
[startup+1160.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 107334 0 0 0 115779 252 0 0 25 0 1 0 550415228 421924864 101550 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 103009 101550 603 41 0 102968 0
vsize: 412036
[startup+1170.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 107866 0 0 0 116778 253 0 0 25 0 1 0 550415228 424112128 102082 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 103543 102082 603 41 0 103502 0
vsize: 414172
[startup+1180.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 108505 0 0 0 117777 255 0 0 25 0 1 0 550415228 426704896 102721 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 104176 102721 603 41 0 104135 0
vsize: 416704
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 109014 0 0 0 118776 256 0 0 25 0 1 0 550415228 428781568 103230 4294967295 134512640 134672761 3221224544 3221223744 134610712 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 104683 103230 603 41 0 104642 0
vsize: 418732
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 15180
Raw data (stat): 15172 (minisat+) R 15171 22929 22928 0 -1 0 109656 0 0 0 119775 257 0 0 25 0 1 0 550415228 431484928 103872 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 105343 103872 603 41 0 105302 0
vsize: 421372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.37 s]
Raw data (loadavg): 0.99 0.97 0.98 1/55 15180
Raw data (stat): 15172 (minisat+) Z 15171 22929 22928 0 -1 12 109657 0 0 0 119775 277 0 0 25 0 1 0 550415228 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.37
CPU time (s): 1200.52
CPU user time (s): 1197.75
CPU system time (s): 2.77058
CPU usage (%): 100.013
Max. virtual memory (Kb): 421372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####