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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.02884
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 19445

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 19:02:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16612 boxname=wulflinc20 idbench=1278 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air01.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air01.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air01.opb
IDLAUNCH: 16612
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        661916 kB
Buffers:         25392 kB
Cached:         324292 kB
SwapCached:        516 kB
Active:          27936 kB
Inactive:       323704 kB
HighTotal:      131008 kB
HighFree:        79576 kB
LowTotal:       903652 kB
LowFree:        582340 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            15500 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:22:56 (client local time) WITH STATUS 10 IN 1200.42 SECONDS
stats: 16612 7 1200.42 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.515921 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.16452 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.66229 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.17706 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: 11.0633 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.6168 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: 16.1975 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.2789 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: 41.1157 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_b#### 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.92 0.97 0.93 2/54 11078
Raw data (stat): 11078 (runsolver) R 11077 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547447420 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 9070 0 0 0 974 24 0 0 25 0 1 0 547447420 31862784 6255 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7779 6255 603 41 0 7738 0
vsize: 31116
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 11196 0 0 0 1968 30 0 0 25 0 1 0 547447420 34385920 6848 4294967295 134512640 134672761 3221224544 3221223712 134564746 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.002 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 12633 0 0 0 2964 34 0 0 25 0 1 0 547447420 36847616 7446 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8996 7446 603 41 0 8955 0
vsize: 35984
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 14417 0 0 0 3960 38 0 0 25 0 1 0 547447420 44232704 9230 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9230 603 41 0 10758 0
vsize: 43196
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 16324 0 0 0 4956 42 0 0 25 0 1 0 547447420 48730112 10540 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11897 10540 603 41 0 11856 0
vsize: 47588
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 17249 0 0 0 5954 44 0 0 25 0 1 0 547447420 52555776 11465 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12831 11465 603 41 0 12790 0
vsize: 51324
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 18026 0 0 0 6953 46 0 0 25 0 1 0 547447420 55713792 12242 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13602 12242 603 41 0 13561 0
vsize: 54408
[startup+80.0033 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 19601 0 0 0 7949 50 0 0 25 0 1 0 547447420 62152704 13817 4294967295 134512640 134672761 3221224544 3221223648 134603706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 13817 603 41 0 15133 0
vsize: 60696
[startup+90.0034 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 20646 0 0 0 8947 52 0 0 25 0 1 0 547447420 66473984 14862 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16229 14862 603 41 0 16188 0
vsize: 64916
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 21387 0 0 0 9945 54 0 0 25 0 1 0 547447420 69488640 15603 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16965 15603 603 41 0 16924 0
vsize: 67860
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 22083 0 0 0 10944 56 0 0 25 0 1 0 547447420 72245248 16299 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17638 16299 603 41 0 17597 0
vsize: 70552
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 23002 0 0 0 11942 58 0 0 25 0 1 0 547447420 76148736 17218 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18591 17218 603 41 0 18550 0
vsize: 74364
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 23845 0 0 0 12940 60 0 0 25 0 1 0 547447420 79536128 18061 4294967295 134512640 134672761 3221224544 3221223728 134615835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19418 18061 603 41 0 19377 0
vsize: 77672
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 24912 0 0 0 13937 63 0 0 25 0 1 0 547447420 83959808 19128 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20498 19128 603 41 0 20457 0
vsize: 81992
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11078
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 25999 0 0 0 14934 67 0 0 25 0 1 0 547447420 88371200 20215 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21575 20215 603 41 0 21534 0
vsize: 86300
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 27026 0 0 0 15932 68 0 0 25 0 1 0 547447420 92602368 21242 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22608 21242 603 41 0 22567 0
vsize: 90432
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 27929 0 0 0 16930 71 0 0 25 0 1 0 547447420 96272384 22145 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23504 22145 603 41 0 23463 0
vsize: 94016
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 28697 0 0 0 17928 73 0 0 25 0 1 0 547447420 99405824 22913 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24269 22913 603 41 0 24228 0
vsize: 97076
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 29424 0 0 0 18926 75 0 0 25 0 1 0 547447420 102391808 23640 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24998 23640 603 41 0 24957 0
vsize: 99992
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 30408 0 0 0 19924 78 0 0 25 0 1 0 547447420 106381312 24624 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25972 24624 603 41 0 25931 0
vsize: 103888
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 31813 0 0 0 20921 81 0 0 25 0 1 0 547447420 112226304 26029 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27399 26029 603 41 0 27358 0
vsize: 109596
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 32869 0 0 0 21919 83 0 0 25 0 1 0 547447420 116527104 27085 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28449 27085 603 41 0 28408 0
vsize: 113796
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 34018 0 0 0 22917 85 0 0 25 0 1 0 547447420 121257984 28234 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29604 28234 603 41 0 29563 0
vsize: 118416
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 35278 0 0 0 23915 88 0 0 25 0 1 0 547447420 126316544 29494 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30839 29494 603 41 0 30798 0
vsize: 123356
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 36600 0 0 0 24913 90 0 0 25 0 1 0 547447420 131780608 30816 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32173 30816 603 41 0 32132 0
vsize: 128692
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 37948 0 0 0 25910 93 0 0 25 0 1 0 547447420 137297920 32164 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33520 32164 603 41 0 33479 0
vsize: 134080
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 38964 0 0 0 26908 95 0 0 25 0 1 0 547447420 141467648 33180 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34538 33180 603 41 0 34497 0
vsize: 138152
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 40041 0 0 0 27906 97 0 0 25 0 1 0 547447420 145915904 34257 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35624 34257 603 41 0 35583 0
vsize: 142496
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 41271 0 0 0 28904 100 0 0 25 0 1 0 547447420 150843392 35487 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36827 35487 603 41 0 36786 0
vsize: 147308
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 42517 0 0 0 29901 103 0 0 25 0 1 0 547447420 156053504 36733 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38099 36733 603 41 0 38058 0
vsize: 152396
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 42951 0 0 0 30900 104 0 0 25 0 1 0 547447420 157728768 37167 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38508 37167 603 41 0 38467 0
vsize: 154032
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 43805 0 0 0 31899 105 0 0 25 0 1 0 547447420 161333248 38021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39388 38021 603 41 0 39347 0
vsize: 157552
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 44383 0 0 0 32898 106 0 0 25 0 1 0 547447420 163799040 38599 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39990 38599 603 41 0 39949 0
vsize: 159960
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 45179 0 0 0 33897 108 0 0 25 0 1 0 547447420 166973440 39395 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40765 39395 603 41 0 40724 0
vsize: 163060
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 45940 0 0 0 34895 110 0 0 25 0 1 0 547447420 170168320 40156 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41545 40156 603 41 0 41504 0
vsize: 166180
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 46656 0 0 0 35893 112 0 0 25 0 1 0 547447420 173051904 40872 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42249 40872 603 41 0 42208 0
vsize: 168996
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 47349 0 0 0 36891 114 0 0 25 0 1 0 547447420 175853568 41565 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42933 41565 603 41 0 42892 0
vsize: 171732
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 48090 0 0 0 37889 116 0 0 25 0 1 0 547447420 178913280 42306 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43680 42306 603 41 0 43639 0
vsize: 174720
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 48792 0 0 0 38887 119 0 0 25 0 1 0 547447420 181772288 43008 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44378 43008 603 41 0 44337 0
vsize: 177512
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 49520 0 0 0 39885 121 0 0 25 0 1 0 547447420 184745984 43736 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45104 43736 603 41 0 45063 0
vsize: 180416
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 50217 0 0 0 40884 122 0 0 25 0 1 0 547447420 187596800 44433 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45800 44433 603 41 0 45759 0
vsize: 183200
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 51018 0 0 0 41883 123 0 0 25 0 1 0 547447420 190951424 45234 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46619 45234 603 41 0 46578 0
vsize: 186476
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 51908 0 0 0 42881 125 0 0 25 0 1 0 547447420 194543616 46124 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47496 46124 603 41 0 47455 0
vsize: 189984
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 52680 0 0 0 43879 127 0 0 25 0 1 0 547447420 197685248 46896 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48263 46896 603 41 0 48222 0
vsize: 193052
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 53830 0 0 0 44877 129 0 0 25 0 1 0 547447420 202477568 48046 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49433 48046 603 41 0 49392 0
vsize: 197732
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 54797 0 0 0 45876 130 0 0 25 0 1 0 547447420 206471168 49013 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50408 49013 603 41 0 50367 0
vsize: 201632
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 55990 0 0 0 46874 132 0 0 25 0 1 0 547447420 211283968 50206 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51583 50206 603 41 0 51542 0
vsize: 206332
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 56813 0 0 0 47872 134 0 0 25 0 1 0 547447420 214671360 51029 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52410 51029 603 41 0 52369 0
vsize: 209640
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 57681 0 0 0 48871 136 0 0 25 0 1 0 547447420 218251264 51897 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53284 51897 603 41 0 53243 0
vsize: 213136
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 58578 0 0 0 49870 137 0 0 25 0 1 0 547447420 221925376 52794 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54181 52794 603 41 0 54140 0
vsize: 216724
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 59446 0 0 0 50868 140 0 0 25 0 1 0 547447420 225439744 53662 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55039 53662 603 41 0 54998 0
vsize: 220156
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 60306 0 0 0 51866 141 0 0 25 0 1 0 547447420 229003264 54522 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55909 54522 603 41 0 55868 0
vsize: 223636
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 61508 0 0 0 52864 143 0 0 25 0 1 0 547447420 233906176 55724 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57106 55724 603 41 0 57065 0
vsize: 228424
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 62504 0 0 0 53863 145 0 0 25 0 1 0 547447420 237973504 56720 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58099 56720 603 41 0 58058 0
vsize: 232396
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 63289 0 0 0 54862 146 0 0 25 0 1 0 547447420 241242112 57505 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58897 57505 603 41 0 58856 0
vsize: 235588
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 63895 0 0 0 55860 148 0 0 25 0 1 0 547447420 243728384 58111 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59504 58111 603 41 0 59463 0
vsize: 238016
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 64806 0 0 0 56858 150 0 0 25 0 1 0 547447420 247422976 59022 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60406 59022 603 41 0 60365 0
vsize: 241624
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 65767 0 0 0 57857 152 0 0 25 0 1 0 547447420 251305984 59983 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61354 59983 603 41 0 61313 0
vsize: 245416
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 66835 0 0 0 58855 154 0 0 25 0 1 0 547447420 255672320 61051 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62420 61051 603 41 0 62379 0
vsize: 249680
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 67752 0 0 0 59853 156 0 0 25 0 1 0 547447420 259493888 61968 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63353 61968 603 41 0 63312 0
vsize: 253412
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 68577 0 0 0 60851 158 0 0 25 0 1 0 547447420 262844416 62793 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64171 62793 603 41 0 64130 0
vsize: 256684
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 69329 0 0 0 61851 158 0 0 25 0 1 0 547447420 265895936 63545 4294967295 134512640 134672761 3221224544 3221223728 134615538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64916 63545 603 41 0 64875 0
vsize: 259664
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 70341 0 0 0 62849 160 0 0 25 0 1 0 547447420 270086144 64557 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65939 64557 603 41 0 65898 0
vsize: 263756
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 71313 0 0 0 63847 163 0 0 25 0 1 0 547447420 274014208 65529 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66898 65529 603 41 0 66857 0
vsize: 267592
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 72603 0 0 0 64845 165 0 0 25 0 1 0 547447420 279400448 66819 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68213 66819 603 41 0 68172 0
vsize: 272852
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 73694 0 0 0 65842 168 0 0 25 0 1 0 547447420 283865088 67910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69303 67910 603 41 0 69262 0
vsize: 277212
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 74615 0 0 0 66840 170 0 0 25 0 1 0 547447420 287559680 68831 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70205 68831 603 41 0 70164 0
vsize: 280820
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 75887 0 0 0 67838 173 0 0 25 0 1 0 547447420 292786176 70103 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71481 70103 603 41 0 71440 0
vsize: 285924
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 76802 0 0 0 68836 175 0 0 25 0 1 0 547447420 296517632 71018 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72392 71018 603 41 0 72351 0
vsize: 289568
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 77808 0 0 0 69835 176 0 0 25 0 1 0 547447420 300666880 72024 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73405 72024 603 41 0 73364 0
vsize: 293620
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 78757 0 0 0 70832 179 0 0 25 0 1 0 547447420 304578560 72973 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74360 72973 603 41 0 74319 0
vsize: 297440
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 79531 0 0 0 71830 181 0 0 25 0 1 0 547447420 307695616 73747 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75121 73747 603 41 0 75080 0
vsize: 300484
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 80265 0 0 0 72828 184 0 0 25 0 1 0 547447420 310730752 74481 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75862 74481 603 41 0 75821 0
vsize: 303448
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 81279 0 0 0 73825 186 0 0 25 0 1 0 547447420 314843136 75495 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76866 75495 603 41 0 76825 0
vsize: 307464
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 82369 0 0 0 74824 188 0 0 25 0 1 0 547447420 319328256 76585 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77961 76585 603 41 0 77920 0
vsize: 311844
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 83474 0 0 0 75822 190 0 0 25 0 1 0 547447420 323866624 77690 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79069 77690 603 41 0 79028 0
vsize: 316276
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 84802 0 0 0 76820 192 0 0 25 0 1 0 547447420 329347072 79018 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80407 79018 603 41 0 80366 0
vsize: 321628
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 85917 0 0 0 77817 195 0 0 25 0 1 0 547447420 333844480 80133 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81505 80133 603 41 0 81464 0
vsize: 326020
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 86827 0 0 0 78816 196 0 0 25 0 1 0 547447420 337645568 81043 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82433 81043 603 41 0 82392 0
vsize: 329732
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 87732 0 0 0 79814 198 0 0 25 0 1 0 547447420 341258240 81948 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83315 81948 603 41 0 83274 0
vsize: 333260
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 88381 0 0 0 80813 200 0 0 25 0 1 0 547447420 343916544 82597 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83964 82597 603 41 0 83923 0
vsize: 335856
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 89140 0 0 0 81813 201 0 0 25 0 1 0 547447420 347049984 83356 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84729 83356 603 41 0 84688 0
vsize: 338916
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 90212 0 0 0 82812 203 0 0 25 0 1 0 547447420 351526912 84428 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85822 84428 603 41 0 85781 0
vsize: 343288
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 91114 0 0 0 83809 206 0 0 25 0 1 0 547447420 355143680 85330 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86705 85330 603 41 0 86664 0
vsize: 346820
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 91707 0 0 0 84808 207 0 0 25 0 1 0 547447420 357617664 85923 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87309 85923 603 41 0 87268 0
vsize: 349236
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 92043 0 0 0 85808 207 0 0 25 0 1 0 547447420 359014400 86259 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87650 86259 603 41 0 87609 0
vsize: 350600
[startup+870.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 92169 0 0 0 86808 208 0 0 25 0 1 0 547447420 359796736 86385 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87841 86385 603 41 0 87800 0
vsize: 351364
[startup+880.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 92529 0 0 0 87807 209 0 0 25 0 1 0 547447420 361238528 86745 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88193 86745 603 41 0 88152 0
vsize: 352772
[startup+890.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 92961 0 0 0 88807 209 0 0 25 0 1 0 547447420 363098112 87177 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88647 87177 603 41 0 88606 0
vsize: 354588
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 93678 0 0 0 89806 210 0 0 25 0 1 0 547447420 366018560 87894 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 89360 87894 603 41 0 89319 0
vsize: 357440
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 94449 0 0 0 90804 212 0 0 25 0 1 0 547447420 369192960 88665 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90135 88665 603 41 0 90094 0
vsize: 360540
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 94510 0 0 0 91805 212 0 0 25 0 1 0 547447420 369459200 88726 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90200 88726 603 41 0 90159 0
vsize: 360800
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 95358 0 0 0 92803 214 0 0 25 0 1 0 547447420 372813824 89574 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 91019 89574 603 41 0 90978 0
vsize: 364076
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 96177 0 0 0 93802 215 0 0 25 0 1 0 547447420 376188928 90393 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 91843 90393 603 41 0 91802 0
vsize: 367372
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 96666 0 0 0 94801 216 0 0 25 0 1 0 547447420 378265600 90882 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 92350 90882 603 41 0 92309 0
vsize: 369400
[startup+960.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 97371 0 0 0 95801 217 0 0 25 0 1 0 547447420 381128704 91587 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 93049 91587 603 41 0 93008 0
vsize: 372196
[startup+970.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 97835 0 0 0 96800 218 0 0 25 0 1 0 547447420 383062016 92051 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 93521 92051 603 41 0 93480 0
vsize: 374084
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 98462 0 0 0 97798 219 0 0 25 0 1 0 547447420 385540096 92678 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 94126 92678 603 41 0 94085 0
vsize: 376504
[startup+990.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 99228 0 0 0 98797 221 0 0 25 0 1 0 547447420 388665344 93444 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 94889 93444 603 41 0 94848 0
vsize: 379556
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 99671 0 0 0 99796 222 0 0 25 0 1 0 547447420 390496256 93887 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 95336 93887 603 41 0 95295 0
vsize: 381344
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 100178 0 0 0 100795 223 0 0 25 0 1 0 547447420 392568832 94394 4294967295 134512640 134672761 3221224544 3221223584 134612827 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 95842 94394 603 41 0 95801 0
vsize: 383368
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 100663 0 0 0 101795 224 0 0 25 0 1 0 547447420 394641408 94879 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 96348 94879 603 41 0 96307 0
vsize: 385392
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 101316 0 0 0 102793 226 0 0 25 0 1 0 547447420 397230080 95532 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 96980 95532 603 41 0 96939 0
vsize: 387920
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 101916 0 0 0 103791 228 0 0 25 0 1 0 547447420 399695872 96132 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 97582 96132 603 41 0 97541 0
vsize: 390328
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 102535 0 0 0 104790 229 0 0 25 0 1 0 547447420 402276352 96751 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 98212 96751 603 41 0 98171 0
vsize: 392848
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 103033 0 0 0 105789 230 0 0 25 0 1 0 547447420 404238336 97249 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 98691 97249 603 41 0 98650 0
vsize: 394764
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 103492 0 0 0 106788 232 0 0 25 0 1 0 547447420 406192128 97708 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99168 97708 603 41 0 99127 0
vsize: 396672
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 104287 0 0 0 107786 233 0 0 25 0 1 0 547447420 409423872 98503 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99957 98503 603 41 0 99916 0
vsize: 399828
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 104896 0 0 0 108785 235 0 0 25 0 1 0 547447420 411926528 99112 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100568 99112 603 41 0 100527 0
vsize: 402272
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 105315 0 0 0 109785 235 0 0 25 0 1 0 547447420 413638656 99531 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100986 99531 603 41 0 100945 0
vsize: 403944
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 105711 0 0 0 110784 236 0 0 25 0 1 0 547447420 415240192 99927 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101377 99927 603 41 0 101336 0
vsize: 405508
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 106108 0 0 0 111783 237 0 0 25 0 1 0 547447420 416952320 100324 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101795 100324 603 41 0 101754 0
vsize: 407180
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 106418 0 0 0 112783 238 0 0 25 0 1 0 547447420 418127872 100634 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 102082 100634 603 41 0 102041 0
vsize: 408328
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 106610 0 0 0 113782 238 0 0 25 0 1 0 547447420 418918400 100826 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 102275 100826 603 41 0 102234 0
vsize: 409100
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 107038 0 0 0 114781 239 0 0 25 0 1 0 547447420 420745216 101254 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 102721 101254 603 41 0 102680 0
vsize: 410884
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 107454 0 0 0 115780 241 0 0 25 0 1 0 547447420 422449152 101670 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 103137 101670 603 41 0 103096 0
vsize: 412548
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 108155 0 0 0 116779 242 0 0 25 0 1 0 547447420 425271296 102371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 103826 102371 603 41 0 103785 0
vsize: 415304
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 108675 0 0 0 117778 244 0 0 25 0 1 0 547447420 427360256 102891 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 104336 102891 603 41 0 104295 0
vsize: 417344
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 109179 0 0 0 118777 245 0 0 25 0 1 0 547447420 429436928 103395 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 104843 103395 603 41 0 104802 0
vsize: 419372
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 11080
Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 109869 0 0 0 119775 246 0 0 25 0 1 0 547447420 432250880 104085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 105530 104085 603 41 0 105489 0
vsize: 422120
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 11080
Raw data (stat): 11078 (minisat+) Z 11077 27565 27564 0 -1 12 109870 0 0 0 119775 266 0 0 25 0 1 0 547447420 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.24
CPU time (s): 1200.42
CPU user time (s): 1197.76
CPU system time (s): 2.66259
CPU usage (%): 100.015
Max. virtual memory (Kb): 422120
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####