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/miplib3/normalized-mps-v2-13-7-pk1.opb
MD5SUM	b6007187ad037f56a5e2b97a0b86cea8
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5120
Optimality of the best value was proved	NO
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	2421502
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.03
Number of variables	675
Total number of constraints	100
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	45
Minimum length of a constraint	1
Maximum length of a constraint	95
Trace number 31230

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-05-25 23:16:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22627 boxname=wulflinc27 idbench=1443 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  b6007187ad037f56a5e2b97a0b86cea8  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-pk1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-pk1.opb
IDLAUNCH: 22627
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        887948 kB
Buffers:         20208 kB
Cached:         105728 kB
SwapCached:        612 kB
Active:          15824 kB
Inactive:       112200 kB
HighTotal:      131008 kB
HighFree:        29960 kB
LowTotal:       903652 kB
LowFree:        857988 kB
SwapTotal:     2097892 kB
SwapFree:      2096360 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5072 kB
Slab:            13108 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 23:36:50 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 22627 7 1229.84 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############
c   -- Clauses(.)/Splits(s): (none)
c ---[  58]---> Adder-cost: 358   maxlim: 1151871   bits: 22/21
c ---[  56]---> Adder-cost: 382   maxlim: 1183231   bits: 22/21
c ---[  54]---> Adder-cost: 338   maxlim: 1135231   bits: 22/21
c ---[  52]---> Adder-cost: 362   maxlim: 1185791   bits: 22/21
c ---[  50]---> Adder-cost: 360   maxlim: 1161855   bits: 22/21
c ---[  48]---> Adder-cost: 354   maxlim: 1184383   bits: 22/21
c ---[  46]---> Adder-cost: 362   maxlim: 1156479   bits: 22/21
c ---[  45]---> BDD-cost:   58
c ---[  44]---> BDD-cost:   58
c ---[  43]---> BDD-cost:   58
c ---[  42]---> BDD-cost:   58
c ---[  40]---> Adder-cost: 352   maxlim: 1176959   bits: 22/21
c ---[  39]---> BDD-cost:   58
c ---[  38]---> BDD-cost:   58
c ---[  37]---> BDD-cost:   58
c ---[  36]---> BDD-cost:   58
c ---[  35]---> BDD-cost:   58
c ---[  34]---> BDD-cost:   58
c ---[  33]---> BDD-cost:   58
c ---[  32]---> BDD-cost:   58
c ---[  31]---> BDD-cost:   58
c ---[  30]---> BDD-cost:   58
c ---[  28]---> Adder-cost: 368   maxlim: 1155967   bits: 22/21
c ---[  27]---> BDD-cost:   58
c ---[  26]---> BDD-cost:   58
c ---[  25]---> BDD-cost:   58
c ---[  24]---> BDD-cost:   58
c ---[  23]---> BDD-cost:   58
c ---[  22]---> BDD-cost:   58
c ---[  21]---> BDD-cost:   58
c ---[  20]---> BDD-cost:   58
c ---[  19]---> BDD-cost:   58
c ---[  18]---> BDD-cost:   58
c ---[  16]---> Adder-cost: 362   maxlim: 1178367   bits: 22/21
c ---[  15]---> BDD-cost:   58
c ---[  14]---> BDD-cost:   58
c ---[  13]---> BDD-cost:   58
c ---[  12]---> BDD-cost:   58
c ---[  11]---> BDD-cost:   58
c ---[  10]---> BDD-cost:   58
c ---[   8]---> Adder-cost: 374   maxlim: 1184767   bits: 22/21
c ---[   6]---> Adder-cost: 348   maxlim: 1169791   bits: 22/21
c ---[   4]---> Adder-cost: 352   maxlim: 1145087   bits: 22/21
c ---[   2]---> Adder-cost: 368   maxlim: 1171455   bits: 22/21
c ---[   0]---> Adder-cost: 384   maxlim: 1175295   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   39453   136875 |   13151       0        0     nan |  0.000 % |
c |       100 |   39447   136857 |   14466      99      387     3.9 |  8.290 % |
c |       250 |   39439   136831 |   15912     248     1467     5.9 |  8.303 % |
c |       475 |   39425   136787 |   17503     471     2953     6.3 |  8.327 % |
c |       812 |   39401   136709 |   19254     805     6605     8.2 |  8.364 % |
c |      1318 |   39303   136389 |   21179    1293    11310     8.7 |  8.523 % |
c |      2077 |   39272   136288 |   23297    2048    17663     8.6 |  8.572 % |
c |      3217 |   39045   135547 |   25627    3144    35150    11.2 |  8.953 % |
c |      4925 |   39022   135472 |   28190    4849    68728    14.2 |  8.989 % |
c |      7487 |   38936   135194 |   31009    7394   126289    17.1 |  9.137 % |
c ==============================================================================
c [1mFound solution: 1032188[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11175 |   38567   133997 |   12855   10992   196903    17.9 |  9.137 % |
c |     11275 |   38551   133943 |   14140   11087   198273    17.9 |  9.808 % |
c ==============================================================================
c [1mFound solution: 1031548[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11361 |   38561   133977 |   12853   11173   199002    17.8 |  9.808 % |
c |     11461 |   38561   133977 |   14138   11273   201356    17.9 |  9.811 % |
c |     11612 |   38561   133977 |   15552   11424   205134    18.0 |  9.811 % |
c |     11837 |   38553   133951 |   17107   11648   211611    18.2 |  9.824 % |
c ==============================================================================
c [1mFound solution: 999316[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11949 |   38564   133985 |   12854   11760   212665    18.1 |  9.824 % |
c |     12050 |   38564   133985 |   14139   11861   213681    18.0 |  9.829 % |
c |     12201 |   38514   133821 |   15553   12001   215264    17.9 |  9.914 % |
c ==============================================================================
c [1mFound solution: 900724[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12334 |   38517   133828 |   12839   12133   217327    17.9 |  9.914 % |
c |     12435 |   38517   133828 |   14122   12234   218286    17.8 |  9.930 % |
c |     12586 |   38517   133828 |   15535   12385   220130    17.8 |  9.930 % |
c |     12812 |   38509   133802 |   17088   12610   222918    17.7 |  9.943 % |
c ==============================================================================
c [1mFound solution: 900020[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13064 |   38510   133803 |   12836   12860   227360    17.7 |  9.943 % |
c |     13165 |   38466   133657 |   14119   12949   228997    17.7 | 10.042 % |
c ==============================================================================
c [1mFound solution: 769020[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13229 |   38476   133687 |   12825   13013   230078    17.7 | 10.042 % |
c |     13334 |   38476   133687 |   14107   13118   232125    17.7 | 10.045 % |
c |     13484 |   38476   133687 |   15518   13268   234387    17.7 | 10.045 % |
c |     13709 |   38476   133687 |   17070   13493   236832    17.6 | 10.045 % |
c ==============================================================================
c [1mFound solution: 703676[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13796 |   38493   133732 |   12831   13580   238203    17.5 | 10.045 % |
c |     13896 |   38493   133732 |   14114   13680   240714    17.6 | 10.044 % |
c ==============================================================================
c [1mFound solution: 638428[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14024 |   38507   133772 |   12835   13808   242939    17.6 | 10.044 % |
c |     14124 |   38507   133772 |   14118    7004   104595    14.9 | 10.045 % |
c |     14274 |   38507   133772 |   15530    7154   107672    15.1 | 10.045 % |
c |     14501 |   38507   133772 |   17083    7381   111538    15.1 | 10.045 % |
c |     14838 |   38507   133772 |   18791    7718   116976    15.2 | 10.045 % |
c ==============================================================================
c [1mFound solution: 636344[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15054 |   38524   133816 |   12841    7934   120685    15.2 | 10.045 % |
c |     15155 |   38524   133816 |   14125    8035   123448    15.4 | 10.044 % |
c |     15306 |   38524   133816 |   15537    8186   127081    15.5 | 10.044 % |
c |     15531 |   38524   133816 |   17091    8411   129719    15.4 | 10.044 % |
c ==============================================================================
c [1mFound solution: 602108[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15864 |   38528   133819 |   12842    8743   134226    15.4 | 10.044 % |
c |     15964 |   38528   133819 |   14126    8843   135467    15.3 | 10.060 % |
c ==============================================================================
c [1mFound solution: 597428[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16015 |   38541   133852 |   12847    8894   136196    15.3 | 10.060 % |
c |     16115 |   38541   133852 |   14131    8994   136847    15.2 | 10.063 % |
c |     16265 |   38541   133852 |   15544    9144   139325    15.2 | 10.063 % |
c |     16491 |   38541   133852 |   17099    9370   142064    15.2 | 10.063 % |
c |     16828 |   38541   133852 |   18809    9707   148938    15.3 | 10.063 % |
c ==============================================================================
c [1mFound solution: 597424[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17192 |   38507   133728 |   12835   10058   158021    15.7 | 10.063 % |
c ==============================================================================
c [1mFound solution: 571244[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17251 |   38525   133774 |   12841   10117   158593    15.7 | 10.063 % |
c |     17351 |   38525   133774 |   14125   10216   162923    15.9 | 10.160 % |
c ==============================================================================
c [1mFound solution: 470844[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17378 |   38185   132707 |   12728   10242   163117    15.9 | 10.160 % |
c ==============================================================================
c [1mFound solution: 438116[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17426 |   38200   132747 |   12733   10290   163932    15.9 | 10.160 % |
c ==============================================================================
c [1mFound solution: 437588[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17447 |   38218   132791 |   12739   10311   164180    15.9 | 10.160 % |
c ==============================================================================
c [1mFound solution: 408412[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17505 |   38230   132823 |   12743   10369   165755    16.0 | 10.160 % |
c |     17605 |   38230   132823 |   14017   10469   166737    15.9 | 11.624 % |
c |     17755 |   38222   132797 |   15419   10618   167941    15.8 | 11.636 % |
c ==============================================================================
c [1mFound solution: 342700[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17794 |   38239   132839 |   12746   10657   168345    15.8 | 11.636 % |
c |     17894 |   38239   132839 |   14020   10757   169464    15.8 | 11.633 % |
c |     18045 |   38239   132839 |   15422   10908   172308    15.8 | 11.633 % |
c ==============================================================================
c [1mFound solution: 339528[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18081 |   38257   132882 |   12752   10944   172755    15.8 | 11.633 % |
c ==============================================================================
c [1mFound solution: 338528[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18149 |   38275   132924 |   12758   11012   174024    15.8 | 11.633 % |
c |     18249 |   38275   132924 |   14033   11112   175147    15.8 | 11.628 % |
c ==============================================================================
c [1mFound solution: 269032[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18274 |   38291   132963 |   12763   11137   175440    15.8 | 11.628 % |
c ==============================================================================
c [1mFound solution: 267460[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18294 |   38308   133002 |   12769   11157   175904    15.8 | 11.628 % |
c |     18394 |   38308   133002 |   14045   11257   177555    15.8 | 11.629 % |
c ==============================================================================
c [1mFound solution: 265440[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18450 |   38321   133032 |   12773   11313   179038    15.8 | 11.629 % |
c |     18551 |   38321   133032 |   14050   11414   179872    15.8 | 11.634 % |
c ==============================================================================
c [1mFound solution: 263756[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18564 |   38337   133068 |   12779   11427   179959    15.7 | 11.634 % |
c ==============================================================================
c [1mFound solution: 158920[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18629 |   38000   132024 |   12666   11492   181243    15.8 | 11.634 % |
c |     18729 |   38000   132024 |   13932   11592   182173    15.7 | 13.088 % |
c ==============================================================================
c [1mFound solution: 142412[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18810 |   38011   132050 |   12670   11673   183844    15.7 | 13.088 % |
c |     18912 |   38011   132050 |   13937   11775   184544    15.7 | 13.090 % |
c |     19062 |   38011   132050 |   15330   11925   187341    15.7 | 13.090 % |
c ==============================================================================
c [1mFound solution: 140972[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19147 |   38021   132073 |   12673   12010   189602    15.8 | 13.090 % |
c |     19248 |   38021   132073 |   13940   12111   191119    15.8 | 13.094 % |
c |     19398 |   38021   132073 |   15334   12261   192404    15.7 | 13.094 % |
c ==============================================================================
c [1mFound solution: 140012[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19411 |   38035   132105 |   12678   12274   192575    15.7 | 13.094 % |
c |     19512 |   38035   132105 |   13945   12375   194923    15.8 | 13.095 % |
c ==============================================================================
c [1mFound solution: 139980[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19532 |   38049   132137 |   12683   12395   195223    15.8 | 13.095 % |
c ==============================================================================
c [1mFound solution: 139940[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19541 |   38066   132176 |   12688   12404   195352    15.7 | 13.095 % |
c ==============================================================================
c [1mFound solution: 139820[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19581 |   38080   132207 |   12693   12444   196195    15.8 | 13.095 % |
c ==============================================================================
c [1mFound solution: 139816[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19593 |   38096   132243 |   12698   12456   196315    15.8 | 13.095 % |
c ==============================================================================
c [1mFound solution: 139812[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19661 |   38110   132274 |   12703   12524   198150    15.8 | 13.095 % |
c |     19762 |   38110   132274 |   13973   12625   200106    15.8 | 13.100 % |
c |     19913 |   38110   132274 |   15370   12776   202386    15.8 | 13.100 % |
c ==============================================================================
c [1mFound solution: 134348[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19951 |   38120   132297 |   12706   12814   203025    15.8 | 13.100 % |
c ==============================================================================
c [1mFound solution: 132268[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19982 |   38131   132321 |   12710   12845   203417    15.8 | 13.100 % |
c ==============================================================================
c [1mFound solution: 131148[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20019 |   38140   132340 |   12713   12882   203941    15.8 | 13.100 % |
c ==============================================================================
c [1mFound solution: 131108[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20059 |   38150   132361 |   12716   12922   204966    15.9 | 13.100 % |
c ==============================================================================
c [1mFound solution: 131104[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20088 |   38163   132388 |   12721   12951   205451    15.9 | 13.100 % |
c ==============================================================================
c [1mFound solution: 131076[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20118 |   38176   132415 |   12725   12981   205799    15.9 | 13.100 % |
c |     20220 |   38176   132415 |   13997   13083   210002    16.1 | 13.147 % |
c ==============================================================================
c [1mFound solution: 131072[0m
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20309 |   37814   131312 |   12604   13171   211513    16.1 | 13.147 % |
c |     20409 |   37814   131312 |   13864   13271   213184    16.1 | 14.582 % |
c ==============================================================================
c [1mFound solution: 98532[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20486 |   37824   131335 |   12608   13348   214437    16.1 | 14.582 % |
c |     20586 |   37824   131335 |   13868   13448   215561    16.0 | 14.589 % |
c ==============================================================================
c [1mFound solution: 98380[0m
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20627 |   37831   131351 |   12610   13489   215928    16.0 | 14.589 % |
c |     20727 |   37831   131351 |   13871   13589   218006    16.0 | 14.597 % |
c ==============================================================================
c [1mFound solution: 98372[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20747 |   37842   131376 |   12614   13609   218241    16.0 | 14.597 % |
c ==============================================================================
c [1mFound solution: 98368[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20780 |   37852   131398 |   12617   13642   218780    16.0 | 14.597 % |
c |     20880 |   37852   131398 |   13878   13742   219699    16.0 | 14.612 % |
c ==============================================================================
c [1mFound solution: 65772[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21024 |   37861   131417 |   12620   13886   221900    16.0 | 14.612 % |
c |     21127 |   37861   131417 |   13882    7046    93558    13.3 | 14.621 % |
c |     21277 |   37847   131373 |   15270    7194    94459    13.1 | 14.645 % |
c ==============================================================================
c [1mFound solution: 36008[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21471 |   37490   130280 |   12496    7385    98544    13.3 | 14.645 % |
c |     21572 |   37490   130280 |   13745    7486   100549    13.4 | 16.079 % |
c |     21723 |   37490   130280 |   15120    7637   104959    13.7 | 16.079 % |
c ==============================================================================
c [1mFound solution: 36000[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21897 |   37502   130308 |   12500    7811   107277    13.7 | 16.079 % |
c |     21998 |   37502   130308 |   13750    7912   109182    13.8 | 16.079 % |
c |     22149 |   37502   130308 |   15125    8063   112160    13.9 | 16.079 % |
c |     22376 |   37502   130308 |   16637    8290   115326    13.9 | 16.079 % |
c |     22715 |   37502   130308 |   18301    8629   121340    14.1 | 16.079 % |
c ==============================================================================
c [1mFound solution: 23588[0m
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23197 |   37143   129228 |   12381    9109   130456    14.3 | 16.079 % |
c |     23297 |   37143   129228 |   13619    9209   131580    14.3 | 17.514 % |
c ==============================================================================
c [1mFound solution: 22572[0m
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23394 |   37150   129245 |   12383    9306   133607    14.4 | 17.514 % |
c |     23495 |   37150   129245 |   13621    9407   135033    14.4 | 17.518 % |
c |     23646 |   37150   129245 |   14983    9558   137670    14.4 | 17.518 % |
c |     23871 |   37150   129245 |   16481    9783   141845    14.5 | 17.518 % |
c ==============================================================================
c [1mFound solution: 22568[0m
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24053 |   37157   129262 |   12385    9965   145314    14.6 | 17.518 % |
c |     24154 |   37157   129262 |   13623   10066   146158    14.5 | 17.521 % |
c |     24304 |   37149   129236 |   14985   10215   147556    14.4 | 17.533 % |
c |     24530 |   37149   129236 |   16484   10441   150377    14.4 | 17.533 % |
c |     24867 |   37149   129236 |   18132   10778   157768    14.6 | 17.533 % |
c |     25373 |   37149   129236 |   19946   11284   173225    15.4 | 17.533 % |
c ==============================================================================
c [1mFound solution: 22564[0m
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25675 |   37155   129251 |   12385   11586   180952    15.6 | 17.533 % |
c |     25775 |   37155   129251 |   13623   11686   182432    15.6 | 17.537 % |
c |     25925 |   37155   129251 |   14985   11836   187672    15.9 | 17.537 % |
c |     26152 |   37155   129251 |   16484   12063   191383    15.9 | 17.537 % |
c |     26491 |   37155   129251 |   18132   12402   198077    16.0 | 17.537 % |
c ==============================================================================
c [1mFound solution: 21668[0m
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26746 |   37164   129272 |   12388   12657   201035    15.9 | 17.537 % |
c |     26846 |   37164   129272 |   13626   12757   203685    16.0 | 17.536 % |
c |     26996 |   37164   129272 |   14989   12907   208447    16.1 | 17.536 % |
c |     27221 |   37164   129272 |   16488   13132   214257    16.3 | 17.536 % |
c |     27558 |   37164   129272 |   18137   13469   217763    16.2 | 17.536 % |
c ==============================================================================
c [1mFound solution: 16544[0m
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27707 |   37170   129285 |   12390   13618   219822    16.1 | 17.536 % |
c |     27808 |   37170   129285 |   13629   13719   221409    16.1 | 17.544 % |
c |     27958 |   37170   129285 |   14991   13869   226366    16.3 | 17.544 % |
c |     28184 |   37170   129285 |   16491   14095   228647    16.2 | 17.544 % |
c |     28521 |   37170   129285 |   18140   14432   239750    16.6 | 17.544 % |
c |     29027 |   37170   129285 |   19954   14938   253849    17.0 | 17.544 % |
c ==============================================================================
c [1mFound solution: 16524[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29673 |   37181   129309 |   12393   15584   272030    17.5 | 17.544 % |
c |     29774 |   37181   129309 |   13632    7893   137617    17.4 | 17.547 % |
c |     29924 |   37181   129309 |   14995    8043   139888    17.4 | 17.547 % |
c |     30149 |   37181   129309 |   16495    8268   145904    17.6 | 17.547 % |
c |     30488 |   37181   129309 |   18144    8607   153568    17.8 | 17.547 % |
c |     30994 |   37181   129309 |   19959    9113   166116    18.2 | 17.547 % |
c |     31754 |   37181   129309 |   21954    9873   193403    19.6 | 17.547 % |
c |     32893 |   37181   129309 |   24150   11012   216824    19.7 | 17.547 % |
c |     34602 |   37181   129309 |   26565   12721   262463    20.6 | 17.547 % |
c ==============================================================================
c [1mFound solution: 16520[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35592 |   37192   129333 |   12397   13711   293702    21.4 | 17.547 % |
c |     35692 |   37192   129333 |   13636   13811   294721    21.3 | 17.551 % |
c |     35842 |   37192   129333 |   15000   13961   297442    21.3 | 17.551 % |
c |     36069 |   37192   129333 |   16500   14188   300629    21.2 | 17.551 % |
c |     36407 |   37192   129333 |   18150   14526   309396    21.3 | 17.551 % |
c |     36914 |   37192   129333 |   19965   15033   324455    21.6 | 17.551 % |
c ==============================================================================
c [1mFound solution: 15496[0m
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37582 |   36812   128207 |   12270   15624   334459    21.4 | 17.551 % |
c |     37683 |   36812   128207 |   13497    7913   167346    21.1 | 18.984 % |
c |     37833 |   36812   128207 |   14846    8063   168686    20.9 | 18.984 % |
c |     38060 |   36812   128207 |   16331    8290   171955    20.7 | 18.984 % |
c |     38397 |   36812   128207 |   17964    8627   186378    21.6 | 18.984 % |
c |     38905 |   36812   128207 |   19760    9135   199250    21.8 | 18.984 % |
c |     39665 |   36812   128207 |   21737    9895   223851    22.6 | 18.984 % |
c |     40806 |   36812   128207 |   23910   11036   267122    24.2 | 18.984 % |
c |     42514 |   36812   128207 |   26301   12744   328129    25.7 | 18.984 % |
c |     45076 |   36812   128207 |   28932   15306   412358    26.9 | 18.984 % |
c ==============================================================================
c [1mFound solution: 15492[0m
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46273 |   36819   128226 |   12273   16503   446142    27.0 | 18.984 % |
c |     46375 |   36819   128226 |   13500    8354   218481    26.2 | 18.987 % |
c |     46525 |   36819   128226 |   14850    8504   219448    25.8 | 18.987 % |
c |     46750 |   36819   128226 |   16335    8729   223297    25.6 | 18.987 % |
c |     47087 |   36819   128226 |   17968    9066   231276    25.5 | 18.987 % |
c |     47593 |   36819   128226 |   19765    9572   242126    25.3 | 18.987 % |
c |     48352 |   36819   128226 |   21742   10331   266491    25.8 | 18.987 % |
c |     49491 |   36819   128226 |   23916   11470   301953    26.3 | 18.987 % |
c |     51199 |   36819   128226 |   26308   13178   372554    28.3 | 18.987 % |
c |     53761 |   36819   128226 |   28939   15740   465301    29.6 | 18.987 % |
c ==============================================================================
c [1mFound solution: 14516[0m
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56057 |   36825   128242 |   12275   18036   539152    29.9 | 18.987 % |
c |     56157 |   36825   128242 |   13502    9118   270230    29.6 | 18.992 % |
c |     56309 |   36825   128242 |   14852    9270   273833    29.5 | 18.992 % |
c |     56534 |   36825   128242 |   16338    9495   275433    29.0 | 18.992 % |
c |     56871 |   36825   128242 |   17971    9832   280944    28.6 | 18.992 % |
c |     57377 |   36825   128242 |   19769   10338   292852    28.3 | 18.992 % |
c |     58136 |   36825   128242 |   21745   11097   321161    28.9 | 18.992 % |
c |     59276 |   36825   128242 |   23920   12237   362408    29.6 | 18.992 % |
c |     60985 |   36825   128242 |   26312   13946   413995    29.7 | 18.992 % |
c |     63548 |   36825   128242 |   28943   16509   509356    30.9 | 18.992 % |
c |     67394 |   36825   128242 |   31838   20355   665859    32.7 | 18.992 % |
c |     73160 |   36825   128242 |   35022   26121   926100    35.5 | 18.992 % |
c ==============================================================================
c [1mFound solution: 14452[0m
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74281 |   36829   128253 |   12276   27242   956014    35.1 | 18.992 % |
c |     74381 |   36829   128253 |   13503   12868   470218    36.5 | 18.999 % |
c |     74531 |   36829   128253 |   14853   13018   471153    36.2 | 18.999 % |
c |     74756 |   36829   128253 |   16339   13243   474383    35.8 | 18.999 % |
c |     75095 |   36829   128253 |   17973   13582   482641    35.5 | 18.999 % |
c |     75602 |   36829   128253 |   19770   14089   494660    35.1 | 18.999 % |
c |     76361 |   36829   128253 |   21747   14848   510233    34.4 | 18.999 % |
c |     77501 |   36829   128253 |   23922   15988   537418    33.6 | 18.999 % |
c |     79209 |   36829   128253 |   26314   17696   580456    32.8 | 18.999 % |
c |     81772 |   36829   128253 |   28946   20259   667461    32.9 | 18.999 % |
c |     85618 |   36829   128253 |   31840   24105   781852    32.4 | 18.999 % |
c |     91385 |   36829   128253 |   35024   29872   993586    33.3 | 18.999 % |
c ==============================================================================
c [1mFound solution: 14428[0m
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95801 |   36834   128266 |   12278   34288  1184646    34.5 | 18.999 % |
c |     95903 |   36834   128266 |   13505    7065   213373    30.2 | 19.007 % |
c |     96055 |   36834   128266 |   14856    7217   216410    30.0 | 19.007 % |
c |     96280 |   36834   128266 |   16342    7442   218148    29.3 | 19.007 % |
c |     96618 |   36834   128266 |   17976    7780   224906    28.9 | 19.007 % |
c |     97124 |   36834   128266 |   19773    8286   238918    28.8 | 19.007 % |
c |     97885 |   36834   128266 |   21751    9047   260057    28.7 | 19.007 % |
c ==============================================================================
c [1mFound solution: 13724[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98124 |   36843   128289 |   12281    9286   264979    28.5 | 19.007 % |
c |     98224 |   36843   128289 |   13509    9386   265508    28.3 | 19.005 % |
c |     98374 |   36843   128289 |   14860    9536   267139    28.0 | 19.005 % |
c |     98601 |   36843   128289 |   16346    9763   270535    27.7 | 19.005 % |
c |     98939 |   36843   128289 |   17980   10101   275717    27.3 | 19.005 % |
c |     99447 |   36843   128289 |   19778   10609   293159    27.6 | 19.005 % |
c |    100207 |   36843   128289 |   21756   11369   304277    26.8 | 19.005 % |
c |    101348 |   36843   128289 |   23932   12510   334789    26.8 | 19.005 % |
c ==============================================================================
c [1mFound solution: 13644[0m
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    101688 |   36852   128311 |   12284   12850   342245    26.6 | 19.005 % |
c |    101789 |   36852   128311 |   13512   12951   342884    26.5 | 19.003 % |
c |    101940 |   36852   128311 |   14863   13102   343846    26.2 | 19.003 % |
c |    102166 |   36845   128288 |   16350   13327   347272    26.1 | 19.015 % |
c |    102503 |   36845   128288 |   17985   13664   353135    25.8 | 19.015 % |
c |    103010 |   36845   128288 |   19783   14171   365913    25.8 | 19.015 % |
c |    103769 |   36845   128288 |   21761   14930   388571    26.0 | 19.015 % |
c |    104909 |   36845   128288 |   23938   16070   421710    26.2 | 19.015 % |
c |    106617 |   36845   128288 |   26331   17778   484189    27.2 | 19.015 % |
c |    109179 |   36845   128288 |   28965   20340   575241    28.3 | 19.015 % |
c ==============================================================================
c [1mFound solution: 12572[0m
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111904 |   36853   128307 |   12284   23065   672026    29.1 | 19.015 % |
c |    112006 |   36853   128307 |   13512   11635   320975    27.6 | 19.018 % |
c |    112156 |   36853   128307 |   14863   11785   324077    27.5 | 19.018 % |
c |    112381 |   36853   128307 |   16350   12010   328289    27.3 | 19.018 % |
c |    112719 |   36853   128307 |   17985   12348   336145    27.2 | 19.018 % |
c |    113226 |   36853   128307 |   19783   12855   345644    26.9 | 19.018 % |
c |    113986 |   36853   128307 |   21761   13615   371037    27.3 | 19.018 % |
c |    115127 |   36853   128307 |   23938   14756   404373    27.4 | 19.018 % |
c |    116835 |   36853   128307 |   26331   16464   461239    28.0 | 19.018 % |
c |    119398 |   36853   128307 |   28965   19027   545495    28.7 | 19.018 % |
c |    123242 |   36853   128307 |   31861   22871   639038    27.9 | 19.018 % |
c |    129010 |   36853   128307 |   35047   28639   882207    30.8 | 19.018 % |
c |    137660 |   36853   128307 |   38552   13830   485312    35.1 | 19.018 % |
c |    150634 |   36853   128307 |   42407   26804  1127282    42.1 | 19.018 % |
c |    170096 |   36853   128307 |   46648   15068   588063    39.0 | 19.018 % |
c ==============================================================================
c [1mFound solution: 12564[0m
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    171077 |   36861   128326 |   12287   16049   612333    38.2 | 19.018 % |
c |    171178 |   36861   128326 |   13515    8126   296422    36.5 | 19.021 % |
c |    171328 |   36861   128326 |   14867    8276   297256    35.9 | 19.021 % |
c |    171553 |   36861   128326 |   16353    8501   302353    35.6 | 19.021 % |
c |    171890 |   36861   128326 |   17989    8838   306531    34.7 | 19.021 % |
c |    172397 |   36861   128326 |   19788    9345   318405    34.1 | 19.021 % |
c |    173157 |   36861   128326 |   21767   10105   329823    32.6 | 19.021 % |
c |    174296 |   36861   128326 |   23943   11244   367773    32.7 | 19.021 % |
c |    176005 |   36861   128326 |   26338   12953   419145    32.4 | 19.021 % |
c ==============================================================================
c [1mFound solution: 12380[0m
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    176994 |   36864   128334 |   12288   13942   439645    31.5 | 19.021 % |
c |    177094 |   36864   128334 |   13516    7071   152283    21.5 | 19.028 % |
c |    177244 |   36864   128334 |   14868    7221   153279    21.2 | 19.028 % |
c |    177469 |   36864   128334 |   16355    7446   155909    20.9 | 19.028 % |
c |    177808 |   36864   128334 |   17990    7785   163986    21.1 | 19.028 % |
c |    178314 |   36864   128334 |   19789    8291   180208    21.7 | 19.028 % |
c |    179074 |   36864   128334 |   21768    9051   199445    22.0 | 19.028 % |
c |    180213 |   36864   128334 |   23945   10190   243214    23.9 | 19.028 % |
c |    181922 |   36864   128334 |   26340   11899   290182    24.4 | 19.028 % |
c |    184484 |   36864   128334 |   28974   14461   377967    26.1 | 19.028 % |
c |    188329 |   36864   128334 |   31871   18306   538763    29.4 | 19.028 % |
c |    194096 |   36864   128334 |   35059   24073   731057    30.4 | 19.028 % |
c |    202745 |   36864   128334 |   38565   32722  1000173    30.6 | 19.028 % |
c |    215719 |   36864   128334 |   42421   18645   716290    38.4 | 19.028 % |
c |    235182 |   36864   128334 |   46663   38108  1426096    37.4 | 19.028 % |
c |    264375 |   36864   128334 |   51330   32704  1699302    52.0 | 19.028 % |
c ==============================================================================
c [1mFound solution: 12376[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    287208 |   36875   128360 |   12291   16661   884812    53.1 | 19.028 % |
c |    287310 |   36875   128360 |   13520    8433   371193    44.0 | 19.029 % |
c |    287460 |   36875   128360 |   14872    8583   373817    43.6 | 19.029 % |
c |    287685 |   36875   128360 |   16359    8808   377028    42.8 | 19.029 % |
c |    288022 |   36875   128360 |   17995    9145   379856    41.5 | 19.029 % |
c |    288529 |   36875   128360 |   19794    9652   386997    40.1 | 19.029 % |
c |    289288 |   36875   128360 |   21774   10411   417070    40.1 | 19.029 % |
c |    290427 |   36875   128360 |   23951   11550   453289    39.2 | 19.029 % |
c |    292136 |   36875   128360 |   26346   13259   501736    37.8 | 19.029 % |
c |    294699 |   36875   128360 |   28981   15822   607437    38.4 | 19.029 % |
c |    298543 |   36875   128360 |   31879   19666   754415    38.4 | 19.029 % |
c |    304309 |   36875   128360 |   35067   25432   976585    38.4 | 19.029 % |
c |    312958 |   36875   128360 |   38574   34081  1371811    40.3 | 19.029 % |
c ==============================================================================
c [1mFound solution: 12352[0m
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    319353 |   36882   128376 |   12294   40476  1598657    39.5 | 19.029 % |
c |    319453 |   36882   128376 |   13523    7082   205798    29.1 | 19.036 % |
c |    319604 |   36882   128376 |   14875    7233   206704    28.6 | 19.036 % |
c |    319829 |   36882   128376 |   16363    7458   209007    28.0 | 19.036 % |
c |    320166 |   36882   128376 |   17999    7795   215612    27.7 | 19.036 % |
c |    320674 |   36882   128376 |   19799    8303   223348    26.9 | 19.036 % |
c |    321433 |   36882   128376 |   21779    9062   250219    27.6 | 19.036 % |
c |    322572 |   36882   128376 |   23957   10201   282129    27.7 | 19.036 % |
c |    324282 |   36882   128376 |   26353   11911   358349    30.1 | 19.036 % |
c |    326844 |   36882   128376 |   28988   14473   441330    30.5 | 19.036 % |
c |    330689 |   36882   128376 |   31887   18318   589478    32.2 | 19.036 % |
c |    336455 |   36882   128376 |   35076   24084   823104    34.2 | 19.036 % |
c |    345104 |   36882   128376 |   38583   32733  1226373    37.5 | 19.036 % |
c |    358078 |   36882   128376 |   42442   19067   786517    41.3 | 19.036 % |
c |    377539 |   36882   128376 |   46686   38528  1589767    41.3 | 19.036 % |
c ==============================================================================
c [1mFound solution: 12308[0m
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    404877 |   36888   128390 |   12296   31387  1372032    43.7 | 19.036 % |
c |    404977 |   36888   128390 |   13525   13898   517090    37.2 | 19.043 % |
c |    405128 |   36888   128390 |   14878   14049   518096    36.9 | 19.043 % |
c |    405354 |   36888   128390 |   16365   14275   522256    36.6 | 19.043 % |
c |    405691 |   36888   128390 |   18002   14612   528261    36.2 | 19.043 % |
c |    406200 |   36888   128390 |   19802   15121   540334    35.7 | 19.043 % |
c |    406959 |   36888   128390 |   21783   15880   563197    35.5 | 19.043 % |
c |    408100 |   36888   128390 |   23961   17021   592453    34.8 | 19.043 % |
c |    409808 |   36888   128390 |   26357   18729   659724    35.2 | 19.043 % |
c |    412372 |   36888   128390 |   28993   21293   746976    35.1 | 19.043 % |
c |    416216 |   36888   128390 |   31892   25137   891860    35.5 | 19.043 % |
c |    421982 |   36888   128390 |   35081   30903  1112849    36.0 | 19.043 % |
c |    430632 |   36888   128390 |   38590   15691   553318    35.3 | 19.043 % |
c ==============================================================================
c [1mFound solution: 12304[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    435245 |   36897   128410 |   12299   20304   714432    35.2 | 19.043 % |
c |    435345 |   36897   128410 |   13528   10252   334706    32.6 | 19.050 % |
c |    435497 |   36897   128410 |   14881   10404   335682    32.3 | 19.050 % |
c |    435722 |   36897   128410 |   16369   10629   340217    32.0 | 19.050 % |
c |    436060 |   36897   128410 |   18006   10967   344797    31.4 | 19.050 % |
c |    436566 |   36897   128410 |   19807   11473   352241    30.7 | 19.050 % |
c |    437325 |   36897   128410 |   21788   12232   372264    30.4 | 19.050 % |
c |    438466 |   36897   128410 |   23967   13373   405058    30.3 | 19.050 % |
c |    440174 |   36897   128410 |   26363   15081   464949    30.8 | 19.050 % |
c |    442738 |   36897   128410 |   29000   17645   587210    33.3 | 19.050 % |
c |    446583 |   36897   128410 |   31900   21490   740992    34.5 | 19.050 % |
c |    452351 |   36897   128410 |   35090   27258   975686    35.8 | 19.050 % |
c ==============================================================================
c [1mFound solution: 12300[0m
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    459893 |   36904   128426 |   12301   34800  1269525    36.5 | 19.050 % |
c |    459994 |   36904   128426 |   13531   12782   465076    36.4 | 19.058 % |
c |    460144 |   36904   128426 |   14884   12932   466107    36.0 | 19.058 % |
c |    460370 |   36904   128426 |   16372   13158   470093    35.7 | 19.058 % |
c |    460707 |   36904   128426 |   18009   13495   478617    35.5 | 19.058 % |
c |    461215 |   36904   128426 |   19810   14003   491629    35.1 | 19.058 % |
c |    461974 |   36904   128426 |   21791   14762   524771    35.5 | 19.058 % |
c |    463113 |   36904   128426 |   23971   15901   560101    35.2 | 19.058 % |
c |    464822 |   36904   128426 |   26368   17610   611527    34.7 | 19.058 % |
c |    467385 |   36904   128426 |   29005   20173   701515    34.8 | 19.058 % |
c |    471229 |   36904   128426 |   31905   24017   834838    34.8 | 19.058 % |
c |    476996 |   36904   128426 |   35096   29784  1055919    35.5 | 19.058 % |
c |    485645 |   36904   128426 |   38605   13465   445759    33.1 | 19.058 % |
c |    498619 |   36904   128426 |   42466   26439   986258    37.3 | 19.058 % |
c ==============================================================================
c [1mFound solution: 12296[0m
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    500304 |   36911   128442 |   12303   28124  1044146    37.1 | 19.058 % |
c |    500405 |   36911   128442 |   13533   12951   474327    36.6 | 19.065 % |
c |    500556 |   36911   128442 |   14886   13102   475139    36.3 | 19.065 % |
c |    500782 |   36911   128442 |   16375   13328   479053    35.9 | 19.065 % |
c |    501119 |   36911   128442 |   18012   13665   492568    36.0 | 19.065 % |
c |    501625 |   36911   128442 |   19814   14171   498742    35.2 | 19.065 % |
c |    502385 |   36911   128442 |   21795   14931   522892    35.0 | 19.065 % |
c |    503524 |   36911   128442 |   23975   16070   560981    34.9 | 19.065 % |
c |    505232 |   36911   128442 |   26372   17778   621666    35.0 | 19.065 % |
c |    507795 |   36911   128442 |   29009   20341   724349    35.6 | 19.065 % |
c |    511639 |   36911   128442 |   31910   24185   892062    36.9 | 19.065 % |
c |    517405 |   36911   128442 |   35101   29951  1120245    37.4 | 19.065 % |
c |    526054 |   36911   128442 |   38612   14957   555573    37.1 | 19.065 % |
c ==============================================================================
c [1mFound solution: 12292[0m
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    538824 |   36918   128458 |   12306   27727  1041990    37.6 | 19.065 % |
c |    538925 |   36918   128458 |   13536   13300   445778    33.5 | 19.072 % |
c |    539075 |   36918   128458 |   14890   13450   447494    33.3 | 19.072 % |
c |    539300 |   36918   128458 |   16379   13675   451225    33.0 | 19.072 % |
c |    539638 |   36918   128458 |   18017   14013   454258    32.4 | 19.072 % |
c |    540144 |   36918   128458 |   19818   14519   466428    32.1 | 19.072 % |
c |    540903 |   36918   128458 |   21800   15278   485291    31.8 | 19.072 % |
c |    542042 |   36918   128458 |   23980   16417   509433    31.0 | 19.072 % |
c |    543752 |   36918   128458 |   26379   18127   568529    31.4 | 19.072 % |
c |    546316 |   36918   128458 |   29016   20691   665788    32.2 | 19.072 % |
c |    550164 |   36918   128458 |   31918   24539   807746    32.9 | 19.072 % |
c ==============================================================================
c [1mFound solution: 12288[0m
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    553313 |   36919   128461 |   12306   27688   901704    32.6 | 19.072 % |
c |    553413 |   36919   128461 |   13536   13355   399236    29.9 | 19.082 % |
c |    553564 |   36919   128461 |   14890   13506   402397    29.8 | 19.082 % |
c |    553790 |   36919   128461 |   16379   13732   408434    29.7 | 19.082 % |
c |    554127 |   36919   128461 |   18017   14069   413835    29.4 | 19.082 % |
c |    554634 |   36919   128461 |   19818   14576   428619    29.4 | 19.082 % |
c |    555394 |   36919   128461 |   21800   15336   453713    29.6 | 19.082 % |
c |    556533 |   36919   128461 |   23980   16475   501139    30.4 | 19.082 % |
c ==============================================================================
c [1mFound solution: 11308[0m
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    557161 |   36925   128476 |   12308   17103   519226    30.4 | 19.082 % |
c |    557261 |   36925   128476 |   13538    8652   216099    25.0 | 19.084 % |
c |    557412 |   36925   128476 |   14892    8803   217982    24.8 | 19.084 % |
c |    557637 |   36925   128476 |   16381    9028   220294    24.4 | 19.084 % |
c |    557975 |   36925   128476 |   18020    9366   227457    24.3 | 19.084 % |
c |    558481 |   36925   128476 |   19822    9872   233513    23.7 | 19.084 % |
c |    559242 |   36925   128476 |   21804   10633   258958    24.4 | 19.084 % |
c |    560381 |   36925   128476 |   23984   11772   289947    24.6 | 19.084 % |
c |    562090 |   36925   128476 |   26383   13481   368252    27.3 | 19.084 % |
c |    564652 |   36925   128476 |   29021   16043   452259    28.2 | 19.084 % |
c |    568496 |   36925   128476 |   31923   19887   583420    29.3 | 19.084 % |
c ==============================================================================
c [1mFound solution: 10840[0m
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    571855 |   36935   128499 |   12311   23246   708088    30.5 | 19.084 % |
c |    571956 |   36935   128499 |   13542   11724   342079    29.2 | 19.083 % |
c |    572107 |   36935   128499 |   14896   11875   343548    28.9 | 19.083 % |
c |    572332 |   36935   128499 |   16385   12100   346793    28.7 | 19.083 % |
c |    572669 |   36935   128499 |   18024   12437   352077    28.3 | 19.083 % |
c |    573176 |   36935   128499 |   19826   12944   363266    28.1 | 19.083 % |
c |    573936 |   36935   128499 |   21809   13704   382290    27.9 | 19.083 % |
c |    575075 |   36935   128499 |   23990   14843   428729    28.9 | 19.083 % |
c |    576784 |   36935   128499 |   26389   16552   488127    29.5 | 19.083 % |
c |    579347 |   36935   128499 |   29028   19115   583719    30.5 | 19.083 % |
c |    583191 |   36935   128499 |   31931   22959   720947    31.4 | 19.083 % |
c |    588957 |   36935   128499 |   35124   28725   949541    33.1 | 19.083 % |
c |    597606 |   36935   128499 |   38637   13848   527370    38.1 | 19.083 % |
c |    610581 |   36935   128499 |   42500   26823  1067082    39.8 | 19.083 % |
c ==============================================================================
c [1mFound solution: 10524[0m
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    617925 |   36942   128515 |   12314   34167  1322141    38.7 | 19.083 % |
c |    618026 |   36942   128515 |   13545   13741   477183    34.7 | 19.085 % |
c |    618176 |   36942   128515 |   14899   13891   478333    34.4 | 19.085 % |
c |    618401 |   36942   128515 |   16389   14116   481586    34.1 | 19.085 % |
c |    618739 |   36942   128515 |   18028   14454   484344    33.5 | 19.085 % |
c |    619245 |   36942   128515 |   19831   14960   497601    33.3 | 19.085 % |
c |    620005 |   36942   128515 |   21815   15720   515760    32.8 | 19.085 % |
c |    621145 |   36942   128515 |   23996   16860   554466    32.9 | 19.085 % |
c |    622853 |   36942   128515 |   26396   18568   602863    32.5 | 19.085 % |
c |    625417 |   36942   128515 |   29035   21132   711495    33.7 | 19.085 % |
c |    629261 |   36942   128515 |   31939   24976   882134    35.3 | 19.085 % |
c ==============================================================================
c [1mFound solution: 10520[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    633363 |   36953   128540 |   12317   29078  1040042    35.8 | 19.085 % |
c |    633463 |   36953   128540 |   13548   12992   465138    35.8 | 19.084 % |
c |    633614 |   36953   128540 |   14903   13143   466619    35.5 | 19.084 % |
c |    633839 |   36953   128540 |   16393   13368   471791    35.3 | 19.084 % |
c |    634177 |   36953   128540 |   18033   13706   476213    34.7 | 19.084 % |
c |    634683 |   36953   128540 |   19836   14212   487566    34.3 | 19.084 % |
c |    635442 |   36953   128540 |   21820   14971   508943    34.0 | 19.084 % |
c |    636581 |   36953   128540 |   24002   16110   552250    34.3 | 19.084 % |
c |    638289 |   36953   128540 |   26402   17818   607599    34.1 | 19.084 % |
c |    640851 |   36953   128540 |   29042   20380   686359    33.7 | 19.084 % |
c |    644695 |   36953   128540 |   31947   24224   830966    34.3 | 19.084 % |
c |    650461 |   36953   128540 |   35141   29990  1086221    36.2 | 19.084 % |
c |    659111 |   36953   128540 |   38656   14286   613779    43.0 | 19.084 % |
c |    672085 |   36953   128540 |   42521   27260  1168557    42.9 | 19.084 % |
c |    691548 |   36953   128540 |   46773   16332   665480    40.7 | 19.084 % |
c |    720740 |   36953   128540 |   51451   45524  1969401    43.3 | 19.084 % |
c |    764529 |   36953   128540 |   56596   49182  2478158    50.4 | 19.084 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 22834 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.93 0.98 0.99 2/54 22830
Raw data (stat): 22830 (runsolver) R 22829 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842762891 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.94 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0017 s]
Raw data (loadavg): 0.95 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0032 s]
Raw data (loadavg): 0.95 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0036 s]
Raw data (loadavg): 0.96 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0032 s]
Raw data (loadavg): 0.97 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0036 s]
Raw data (loadavg): 0.97 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0036 s]
Raw data (loadavg): 0.98 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/55 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 0.99 0.98 0.99 1/53 22834
Raw data (stat): 22830 (minisat+_script) S 22829 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842762891 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.69
CPU time (s): 1229.84
CPU user time (s): 1229.56
CPU system time (s): 0.277957
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####