PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a4.opb
MD5SUM	8a77190c2eeefb9e88447a9087adfd6f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	283
Optimality of the best value was proved	NO
Number of terms in the objective function	792
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	792
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	792
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02084
Number of variables	792
Total number of constraints	3194
Number of constraints which are clauses	3194
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 6257

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 04:01:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4678 boxname=wulflinc30 idbench=166 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8a77190c2eeefb9e88447a9087adfd6f  /oldhome/oroussel/tmp/wulflinc30/normalized-ii8a4.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-ii8a4.opb /oldhome/oroussel/tmp/wulflinc30/normalized-ii8a4.opb
IDLAUNCH: 4678
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        720288 kB
Buffers:         38276 kB
Cached:         235628 kB
SwapCached:          0 kB
Active:          84664 kB
Inactive:       192056 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        720036 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32060 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:21:30 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4678 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3194 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3194     8388 |    1064       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36470     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   91926   215917 |   30642       4       26     6.5 |  0.000 % |
c |       106 |   91891   215839 |   33706     105     1070    10.2 |  0.063 % |
c |       256 |   89946   211410 |   37076     217     3482    16.0 |  1.927 % |
c |       485 |   89946   211410 |   40784     446     9160    20.5 |  1.927 % |
c |       822 |   89946   211410 |   44862     783    18950    24.2 |  1.927 % |
c |      1328 |   80691   190157 |   49349    1070    24918    23.3 | 11.455 % |
c |      2087 |   71468   168944 |   54284    1660    33964    20.5 | 20.783 % |
c |      3226 |   57203   136026 |   59712    2479    41662    16.8 | 35.723 % |
c |      4936 |   47999   114737 |   65683    3922    70518    18.0 | 45.390 % |
c ==============================================================================
c [1mFound solution: 353[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5524 |   46534   111358 |   15511    4471    82448    18.4 | 45.390 % |
c |      5624 |   46407   111062 |   17062    4567    83818    18.4 | 47.139 % |
c ==============================================================================
c [1mFound solution: 352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5741 |   45784   109612 |   15261    4646    84283    18.1 | 47.139 % |
c ==============================================================================
c [1mFound solution: 351[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5770 |   45847   109776 |   15282    4675    84791    18.1 | 47.139 % |
c |      5870 |   45170   108199 |   16810    4745    85558    18.0 | 48.497 % |
c |      6021 |   44480   106603 |   18491    4869    87250    17.9 | 49.215 % |
c |      6246 |   44403   106427 |   20340    5092    88828    17.4 | 49.292 % |
c ==============================================================================
c [1mFound solution: 350[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6280 |   44082   105675 |   14694    5101    88726    17.4 | 49.292 % |
c |      6380 |   44082   105675 |   16163    5201    90246    17.4 | 49.609 % |
c |      6530 |   43234   103712 |   17779    5284    93038    17.6 | 50.503 % |
c |      6757 |   42963   103083 |   19557    5501    95615    17.4 | 50.788 % |
c |      7094 |   42443   101884 |   21513    5808    99655    17.2 | 51.311 % |
c ==============================================================================
c [1mFound solution: 349[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7266 |   42512   102062 |   14170    5980   111695    18.7 | 51.311 % |
c |      7369 |   42512   102062 |   15587    6083   115409    19.0 | 51.298 % |
c |      7520 |   41566    99856 |   17145    6216   119385    19.2 | 52.333 % |
c ==============================================================================
c [1mFound solution: 346[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7728 |   41269    99166 |   13756    6404   120486    18.8 | 52.333 % |
c ==============================================================================
c [1mFound solution: 342[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7754 |   41328    99322 |   13776    6425   120413    18.7 | 52.333 % |
c |      7854 |   41199    99020 |   15153    6508   121590    18.7 | 52.848 % |
c |      8004 |   41096    98781 |   16668    6657   124748    18.7 | 52.957 % |
c |      8229 |   40913    98354 |   18335    6873   128151    18.6 | 53.158 % |
c |      8567 |   40561    97538 |   20169    7201   135486    18.8 | 53.538 % |
c |      9073 |   40466    97315 |   22186    7706   146207    19.0 | 53.650 % |
c |      9834 |   39939    96086 |   24405    8457   159306    18.8 | 54.221 % |
c ==============================================================================
c [1mFound solution: 341[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10141 |   39711    95576 |   13237    8559   163875    19.1 | 54.221 % |
c |     10241 |   39553    95214 |   14560    8638   164699    19.1 | 54.682 % |
c |     10391 |   39553    95214 |   16016    8788   167344    19.0 | 54.682 % |
c |     10616 |   39468    95016 |   17618    9011   170305    18.9 | 54.777 % |
c |     10954 |   39468    95016 |   19380    9349   173733    18.6 | 54.777 % |
c |     11460 |   38888    93673 |   21318    9582   187707    19.6 | 55.401 % |
c ==============================================================================
c [1mFound solution: 340[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11908 |   38698    93221 |   12899    9976   193890    19.4 | 55.401 % |
c |     12010 |   38625    93049 |   14188   10073   194640    19.3 | 55.664 % |
c |     12160 |   38423    92580 |   15607   10212   197628    19.4 | 55.885 % |
c |     12385 |   38423    92580 |   17168   10437   204485    19.6 | 55.885 % |
c ==============================================================================
c [1mFound solution: 339[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12574 |   38485    92741 |   12828   10626   208201    19.6 | 55.885 % |
c |     12674 |   38485    92741 |   14110   10726   209182    19.5 | 55.860 % |
c |     12824 |   38485    92741 |   15521   10876   212763    19.6 | 55.860 % |
c |     13050 |   37872    91310 |   17074   11062   223260    20.2 | 56.542 % |
c ==============================================================================
c [1mFound solution: 338[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13095 |   37824    91182 |   12608   11102   223733    20.2 | 56.542 % |
c |     13195 |   37824    91182 |   13868   11202   226764    20.2 | 56.581 % |
c ==============================================================================
c [1mFound solution: 332[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13234 |   37936    91462 |   12645   11224   226124    20.1 | 56.581 % |
c |     13336 |   37936    91462 |   13909   11326   227888    20.1 | 56.568 % |
c |     13486 |   37936    91462 |   15300   11476   230870    20.1 | 56.568 % |
c |     13711 |   37936    91462 |   16830   11701   233590    20.0 | 56.568 % |
c |     14048 |   37681    90868 |   18513   11858   240510    20.3 | 56.854 % |
c |     14555 |   36708    88594 |   20364   12273   246556    20.1 | 57.893 % |
c ==============================================================================
c [1mFound solution: 331[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15084 |   36769    88752 |   12256   12802   267707    20.9 | 57.893 % |
c |     15184 |   36769    88752 |   13481   12902   270257    20.9 | 57.867 % |
c |     15334 |   36769    88752 |   14829   13052   272933    20.9 | 57.867 % |
c |     15560 |   36769    88752 |   16312   13278   277166    20.9 | 57.867 % |
c |     15897 |   36769    88752 |   17944   13615   281975    20.7 | 57.867 % |
c ==============================================================================
c [1mFound solution: 330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16183 |   36617    88390 |   12205   13858   285375    20.6 | 57.867 % |
c |     16285 |   36617    88390 |   13425   13960   288756    20.7 | 58.017 % |
c |     16436 |   36617    88390 |   14768   14111   293493    20.8 | 58.017 % |
c |     16662 |   36489    88097 |   16244   14333   296391    20.7 | 58.145 % |
c ==============================================================================
c [1mFound solution: 322[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16836 |   36640    88468 |   12213   14498   298337    20.6 | 58.145 % |
c |     16937 |   36640    88468 |   13434   14599   300076    20.6 | 58.106 % |
c |     17087 |   36640    88468 |   14777   14749   302731    20.5 | 58.106 % |
c |     17313 |   36640    88468 |   16255   14975   307774    20.6 | 58.106 % |
c |     17652 |   36423    87970 |   17881   15216   316263    20.8 | 58.326 % |
c ==============================================================================
c [1mFound solution: 321[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18143 |   36490    88142 |   12163   15707   325581    20.7 | 58.326 % |
c |     18243 |   36490    88142 |   13379   15807   327005    20.7 | 58.306 % |
c |     18393 |   36490    88142 |   14717   15957   331337    20.8 | 58.306 % |
c |     18620 |   36480    88118 |   16188   16172   333796    20.6 | 58.319 % |
c |     18958 |   36480    88118 |   17807   16510   346781    21.0 | 58.319 % |
c |     19465 |   36460    88073 |   19588   16991   362871    21.4 | 58.336 % |
c ==============================================================================
c [1mFound solution: 320[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19948 |   36382    87865 |   12127   17419   365723    21.0 | 58.336 % |
c |     20048 |   36382    87865 |   13339   17519   371363    21.2 | 58.388 % |
c |     20199 |   36382    87865 |   14673   17670   375335    21.2 | 58.388 % |
c |     20426 |   36382    87865 |   16141   17897   380055    21.2 | 58.388 % |
c |     20763 |   36382    87865 |   17755   18234   387345    21.2 | 58.388 % |
c ==============================================================================
c [1mFound solution: 319[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20806 |   36443    88023 |   12147   18277   388111    21.2 | 58.388 % |
c ==============================================================================
c [1mFound solution: 318[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20813 |   36387    87870 |   12129   18265   386202    21.1 | 58.388 % |
c |     20913 |   36387    87870 |   13341   18365   387812    21.1 | 58.406 % |
c |     21063 |   36387    87870 |   14676   18515   390095    21.1 | 58.406 % |
c |     21289 |   36387    87870 |   16143   18741   392945    21.0 | 58.406 % |
c ==============================================================================
c [1mFound solution: 317[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21599 |   36454    88042 |   12151   19051   401324    21.1 | 58.406 % |
c ==============================================================================
c [1mFound solution: 316[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21696 |   36400    87898 |   12133   19073   397523    20.8 | 58.406 % |
c |     21796 |   36400    87898 |   13346   19173   399338    20.8 | 58.429 % |
c |     21946 |   36249    87545 |   14680   19316   402401    20.8 | 58.580 % |
c |     22173 |   36249    87545 |   16149   19543   406993    20.8 | 58.580 % |
c ==============================================================================
c [1mFound solution: 314[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22299 |   36261    87570 |   12087   19659   410005    20.9 | 58.580 % |
c |     22399 |   36261    87570 |   13295   19759   411779    20.8 | 58.592 % |
c |     22549 |   36261    87570 |   14625   19909   420053    21.1 | 58.592 % |
c |     22774 |   36261    87570 |   16087   20134   424998    21.1 | 58.592 % |
c ==============================================================================
c [1mFound solution: 313[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22953 |   36328    87742 |   12109   20313   428053    21.1 | 58.592 % |
c |     23053 |   36328    87742 |   13319   20413   430621    21.1 | 58.573 % |
c |     23204 |   36328    87742 |   14651   20564   458978    22.3 | 58.573 % |
c |     23429 |   36328    87742 |   16117   20789   464534    22.3 | 58.573 % |
c |     23766 |   36328    87742 |   17728   21126   483503    22.9 | 58.573 % |
c |     24272 |   36328    87742 |   19501   21632   497015    23.0 | 58.573 % |
c ==============================================================================
c [1mFound solution: 312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24442 |   36259    87559 |   12086   21744   494260    22.7 | 58.573 % |
c ==============================================================================
c [1mFound solution: 311[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24528 |   36320    87717 |   12106   21830   495232    22.7 | 58.573 % |
c |     24628 |   36320    87717 |   13316   21930   496715    22.7 | 58.598 % |
c |     24778 |   36320    87717 |   14648   22080   498692    22.6 | 58.598 % |
c |     25003 |   36320    87717 |   16113   22305   502689    22.5 | 58.598 % |
c |     25340 |   36302    87675 |   17724   22630   507212    22.4 | 58.618 % |
c |     25846 |   36302    87675 |   19496   23136   522707    22.6 | 58.618 % |
c |     26605 |   35959    86879 |   21446   23771   536960    22.6 | 58.989 % |
c |     27744 |   35959    86879 |   23591   24910   680085    27.3 | 58.989 % |
c ==============================================================================
c [1mFound solution: 306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28203 |   36018    87023 |   12006   25344   701501    27.7 | 58.989 % |
c |     28303 |   35933    86827 |   13206   25442   702123    27.6 | 59.070 % |
c |     28453 |   35919    86795 |   14527   25588   703920    27.5 | 59.083 % |
c |     28678 |   35919    86795 |   15979   25813   721682    28.0 | 59.083 % |
c |     29015 |   35919    86795 |   17577   26150   741852    28.4 | 59.083 % |
c |     29522 |   35919    86795 |   19335   26657   747361    28.0 | 59.083 % |
c |     30281 |   35649    86171 |   21269   26883   780179    29.0 | 59.366 % |
c ==============================================================================
c [1mFound solution: 305[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30672 |   35642    86170 |   11880   27264   798006    29.3 | 59.366 % |
c |     30773 |   35642    86170 |   13068   27365   799887    29.2 | 59.429 % |
c |     30923 |   35642    86170 |   14374   27515   806564    29.3 | 59.429 % |
c |     31148 |   35642    86170 |   15812   27740   826402    29.8 | 59.429 % |
c |     31486 |   35642    86170 |   17393   28078   838161    29.9 | 59.429 % |
c |     31993 |   35642    86170 |   19132   28585   875003    30.6 | 59.429 % |
c |     32752 |   35642    86170 |   21046   29344   928258    31.6 | 59.429 % |
c |     33892 |   35557    85973 |   23150   30483   978792    32.1 | 59.521 % |
c |     35600 |   35557    85973 |   25465   32191  1084264    33.7 | 59.520 % |
c |     38162 |   35484    85802 |   28012   34734  1285002    37.0 | 59.605 % |
c |     42007 |   35484    85802 |   30813   38579  1424543    36.9 | 59.605 % |
c ==============================================================================
c [1mFound solution: 304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43993 |   35330    85422 |   11776   40307  1534198    38.1 | 59.605 % |
c ==============================================================================
c [1mFound solution: 303[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44045 |   35391    85580 |   11797   18159   689024    37.9 | 59.605 % |
c |     44146 |   35112    84933 |   12976   18243   691501    37.9 | 60.029 % |
c |     44296 |   35112    84933 |   14274   18393   693488    37.7 | 60.029 % |
c |     44521 |   35112    84933 |   15701   18618   705417    37.9 | 60.029 % |
c |     44859 |   35112    84933 |   17271   18956   723863    38.2 | 60.029 % |
c |     45366 |   35112    84933 |   18999   19463   764442    39.3 | 60.029 % |
c |     46126 |   35112    84933 |   20899   20223   794490    39.3 | 60.029 % |
c |     47265 |   35112    84933 |   22989   21362   955070    44.7 | 60.029 % |
c |     48973 |   34294    83035 |   25287   23023  1158839    50.3 | 60.933 % |
c ==============================================================================
c [1mFound solution: 298[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49307 |   34342    83150 |   11447   23112  1135376    49.1 | 60.933 % |
c |     49409 |   34342    83150 |   12591   23214  1137267    49.0 | 60.932 % |
c |     49562 |   34342    83150 |   13850   23367  1141044    48.8 | 60.932 % |
c |     49788 |   34342    83150 |   15235   23593  1153172    48.9 | 60.932 % |
c |     50125 |   34342    83150 |   16759   23930  1173248    49.0 | 60.932 % |
c |     50631 |   34342    83150 |   18435   24436  1192336    48.8 | 60.932 % |
c |     51390 |   34342    83150 |   20279   25195  1267095    50.3 | 60.932 % |
c |     52530 |   34263    82967 |   22306   26306  1309095    49.8 | 61.016 % |
c ==============================================================================
c [1mFound solution: 297[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52999 |   34323    83121 |   11441   26775  1335406    49.9 | 61.016 % |
c |     53099 |   34323    83121 |   12585   26875  1337660    49.8 | 60.998 % |
c |     53249 |   34319    83112 |   13843   27024  1342299    49.7 | 61.002 % |
c |     53477 |   34319    83112 |   15227   27252  1357210    49.8 | 61.002 % |
c |     53814 |   34319    83112 |   16750   27589  1382628    50.1 | 61.002 % |
c |     54320 |   34319    83112 |   18425   28095  1399684    49.8 | 61.002 % |
c |     55079 |   34319    83112 |   20268   28854  1440076    49.9 | 61.002 % |
c |     56218 |   34319    83112 |   22295   29993  1493677    49.8 | 61.002 % |
c |     57926 |   34070    82533 |   24524   31664  1563053    49.4 | 61.274 % |
c ==============================================================================
c [1mFound solution: 296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60482 |   34011    82371 |   11337   33372  1484818    44.5 | 61.274 % |
c |     60584 |   34011    82371 |   12470   16788   487137    29.0 | 61.322 % |
c |     60734 |   34011    82371 |   13717   16938   496147    29.3 | 61.322 % |
c |     60961 |   34011    82371 |   15089   17165   504493    29.4 | 61.322 % |
c |     61298 |   34011    82371 |   16598   17502   514743    29.4 | 61.322 % |
c |     61805 |   34011    82371 |   18258   18009   556780    30.9 | 61.322 % |
c |     62565 |   34011    82371 |   20084   18769   597580    31.8 | 61.322 % |
c ==============================================================================
c [1mFound solution: 295[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63003 |   34066    82512 |   11355   19207   619137    32.2 | 61.322 % |
c |     63105 |   34066    82512 |   12490   19309   622377    32.2 | 61.297 % |
c |     63255 |   34066    82512 |   13739   19459   626998    32.2 | 61.297 % |
c |     63480 |   34066    82512 |   15113   19684   632609    32.1 | 61.297 % |
c |     63817 |   34066    82512 |   16624   20021   654929    32.7 | 61.297 % |
c |     64323 |   34066    82512 |   18287   20527   704015    34.3 | 61.297 % |
c ==============================================================================
c [1mFound solution: 294[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64572 |   34000    82334 |   11333   20717   712462    34.4 | 61.297 % |
c |     64672 |   34000    82334 |   12466   20817   720666    34.6 | 61.348 % |
c |     64822 |   34000    82334 |   13712   20967   726712    34.7 | 61.348 % |
c |     65048 |   34000    82334 |   15084   21193   730686    34.5 | 61.348 % |
c ==============================================================================
c [1mFound solution: 293[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65199 |   34058    82482 |   11352   21344   736761    34.5 | 61.348 % |
c ==============================================================================
c [1mFound solution: 292[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65282 |   33992    82304 |   11330   21326   731456    34.3 | 61.348 % |
c |     65382 |   33992    82304 |   12463   21426   737064    34.4 | 61.378 % |
c |     65532 |   33992    82304 |   13709   21576   740869    34.3 | 61.378 % |
c |     65757 |   33992    82304 |   15080   21801   754932    34.6 | 61.378 % |
c ==============================================================================
c [1mFound solution: 291[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66074 |   34047    82445 |   11349   22118   764795    34.6 | 61.378 % |
c |     66174 |   34047    82445 |   12483   22218   770640    34.7 | 61.353 % |
c |     66324 |   33968    82260 |   13732   22363   771951    34.5 | 61.444 % |
c |     66549 |   33835    81954 |   15105   22375   783518    35.0 | 61.580 % |
c |     66886 |   33835    81954 |   16616   22712   810749    35.7 | 61.580 % |
c |     67393 |   33835    81954 |   18277   23219   844290    36.4 | 61.580 % |
c |     68153 |   33835    81954 |   20105   23979   893725    37.3 | 61.580 % |
c |     69292 |   33835    81954 |   22115   25118   943827    37.6 | 61.580 % |
c |     71000 |   33829    81940 |   24327   26817  1095240    40.8 | 61.586 % |
c |     73562 |   33829    81940 |   26760   29379  1278823    43.5 | 61.586 % |
c |     77408 |   33829    81940 |   29436   33225  1594401    48.0 | 61.586 % |
c |     83175 |   33485    81151 |   32380   38954  2025540    52.0 | 61.939 % |
c ==============================================================================
c [1mFound solution: 290[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83501 |   33439    81029 |   11146   39085  2009954    51.4 | 61.939 % |
c |     83603 |   33439    81029 |   12260   19645   905618    46.1 | 61.980 % |
c |     83753 |   33439    81029 |   13486   19795   908154    45.9 | 61.980 % |
c |     83982 |   33439    81029 |   14835   20024   910366    45.5 | 61.980 % |
c |     84319 |   33439    81029 |   16318   20361   914366    44.9 | 61.980 % |
c |     84825 |   33439    81029 |   17950   20867   919586    44.1 | 61.980 % |
c |     85584 |   33213    80502 |   19745   20375   959902    47.1 | 62.229 % |
c |     86723 |   33122    80289 |   21720   21495  1031724    48.0 | 62.333 % |
c |     88432 |   33122    80289 |   23892   23204  1138840    49.1 | 62.333 % |
c |     90995 |   33122    80289 |   26281   25767  1294318    50.2 | 62.333 % |
c |     94839 |   33122    80289 |   28909   29611  1528893    51.6 | 62.333 % |
c |    100605 |   33122    80289 |   31800   35377  1870537    52.9 | 62.333 % |
c |    109255 |   33035    80085 |   34980   44005  2379282    54.1 | 62.433 % |
c |    122229 |   33035    80085 |   38479   56979  3191673    56.0 | 62.433 % |
c |    141690 |   32964    79916 |   42326   35627  1397701    39.2 | 62.524 % |
c |    170883 |   32964    79916 |   46559   21610  1193107    55.2 | 62.524 % |
c |    214672 |   32964    79916 |   51215   65399  4716623    72.1 | 62.524 % |
c |    280357 |   32964    79916 |   56337   25589  1344616    52.5 | 62.524 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 -x23 x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 -x45 x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 -x59 x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 -x77 x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 -x91 x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 -x107 x108 -x109 x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 -x141 x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 -x155 x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 -x171 x172 -x173 x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 -x193 x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 x203 -x204 -x205 x206 -x207 -x208 -x209 -x210 -x211 x212 x213 -x214 -x215 x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 x225 -x226 -x227 -x228 x229 -x230 -x231 x232 -x233 x234 -x235 x236 -x237 x238 -x239 x240 -x241 x242 -x243 -x244 -x245 -x246 -x247 -x248 x249 -x250 -x251 -x252 -x253 x254 -x255 x256 -x257 x258 -x259 -x260 -x261 x262 x263 -x264 -x265 x266 -x267 -x268 -x269 -x270 -x271 -x272 x273 -x274 -x275 -x276 -x277 x278 -x279 -x280 x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 x290 x291 -x292 -x293 -x294 -x295 x296 -x297 -x298 -x299 x300 -x301 x302 -x303 x304 x305 -x306 -x307 x308 -x309 -x310 -x311 x312 -x313 x314 -x315 x316 -x317 x318 -x319 -x320 -x321 x322 x323 -x324 -x325 x326 -x327 -x328 x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 x337 -x338 -x339 x340 -x341 x342 -x343 x344 -x345 x346 -x347 x348 -x349 x350 -x351 -x352 x353 -x354 -x355 x356 -x357 -x358 -x359 x360 -x361 x362 -x363 -x364 -x365 -x366 -x367 -x368 x369 -x370 -x371 -x372 -x373 x374 -x375 -x376 x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 x386 -x387 x388 -x389 x390 x391 -x392 -x393 x394 -x395 -x396 -x397 x398 -x399 -x400 -x401 -x402 -x403 -x404 x405 -x406 -x407 -x408 -x409 x410 -x411 -x412 -x413 -x414 -x415 -x416 x417 -x418 -x419 -x420 -x421 x422 x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 x434 -x435 x436 -x437 x438 -x439 -x440 -x441 x442 x443 -x444 -x445 x446 -x447 -x448 x449 -x450 -x451 x452 -x453 -x454 -x455 x456 -x457 x458 -x459 -x460 -x461 -x462 -x463 x464 x465 -x466 -x467 x468 -x469 x470 -x471 -x472 x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 x482 -x483 -x484 -x485 -x486 -x487 x488 x489 -x490 -x491 x492 x493 -x494 -x495 x496 -x497 x498 -x499 x500 -x501 x502 -x503 x504 -x505 x506 -x507 x508 -x509 x510 x511 -x512 -x513 x514 -x515 -x516 -x517 x518 -x519 x520 -x521 x522 -x523 -x524 -x525 x526 x527 -x528 -x529 x530 -x531 x532 -x533 x534 -x535 -x536 -x537 x538 x539 -x540 -x541 x542 -x543 -x544 -x545 -x546 -x547 x548 x549 -x550 -x551 x552 -x553 x554 x555 -x556 -x557 -x558 -x559 x560 -x561 -x562 -x563 x564 x565 -x566 -x567 x568 -x569 x570 -x571 -x572 -x573 x574 -x575 -x576 -x577 x578 -x579 x580 -x581 x582 x583 -x584 -x585 x586 -x587 -x588 -x589 x590 x591 -x592 -x593 -x594 -x595 x596 -x597 -x598 -x599 x600 -x601 x602 -x603 x604 -x605 x606 x607 -x608 -x609 x610 -x611 -x612 -x613 x614 x615 -x616 -x617 -x618 -x619 x620 -x621 -x622 -x623 x624 x625 -x626 -x627 x628 -x629 x630 -x631 x632 -x633 x634 -x635 x636 -x637 x638 -x639 -x640 x641 -x642 -x643 -x644 x645 -x646 -x647 -x648 -x649 x650 -x651 -x652 -x653 -x654 x655 -x656 -x657 -x658 -x659 -x660 -x661 x662 x663 -x664 -x665 -x666 -x667 x668 -x669 -x670 -x671 x672 -x673 x674 -x675 -x676 -x677 -x678 -x679 x680 x681 -x682 -x683 x684 -x685 x686 -x687 x688 -x689 x690 -x691 -x692 -x693 x694 x695 -x696 -x697 x698 -x699 -x700 -x701 -x702 -x703 x704 x705 -x706 -x707 x708 -x709 x710 -x711 x712 -x713 x714 -x715 -x716 -x717 x718 x719 -x720 -x721 x722 x723 -x724 -x725 -x726 -x727 x728 -x729 -x730 -x731 x732 -x733 x734 x735 -x736 -x737 -x738 -x739 #### 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.94 0.97 0.91 2/54 18993
Raw data (stat): 18993 (runsolver) R 18992 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481547943 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 2877 0 0 0 991 7 0 0 25 0 1 0 481547943 13733888 2801 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3353 2801 603 41 0 3312 0
vsize: 13412
[startup+20.0015 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 2901 0 0 0 1990 7 0 0 25 0 1 0 481547943 13869056 2825 4294967295 134512640 134672761 3221224576 3221223748 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3386 2825 603 41 0 3345 0
vsize: 13544
[startup+30.003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 3031 0 0 0 2990 8 0 0 25 0 1 0 481547943 14565376 2955 4294967295 134512640 134672761 3221224576 3221223700 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3556 2955 603 41 0 3515 0
vsize: 14224
[startup+40.0034 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 3120 0 0 0 3989 8 0 0 25 0 1 0 481547943 14962688 3044 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3653 3044 603 41 0 3612 0
vsize: 14612
[startup+50.0039 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 3256 0 0 0 4989 9 0 0 25 0 1 0 481547943 15482880 3180 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3780 3180 603 41 0 3739 0
vsize: 15120
[startup+60.0043 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 3350 0 0 0 5988 10 0 0 25 0 1 0 481547943 15949824 3274 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3894 3274 603 41 0 3853 0
vsize: 15576
[startup+70.0049 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 3532 0 0 0 6987 10 0 0 25 0 1 0 481547943 16654336 3456 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4066 3456 603 41 0 4025 0
vsize: 16264
[startup+80.0053 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 3761 0 0 0 7987 10 0 0 25 0 1 0 481547943 17592320 3685 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4295 3685 603 41 0 4254 0
vsize: 17180
[startup+90.0055 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 3959 0 0 0 8987 11 0 0 25 0 1 0 481547943 18345984 3883 4294967295 134512640 134672761 3221224576 3221223700 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4479 3883 603 41 0 4438 0
vsize: 17916
[startup+100.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4199 0 0 0 9986 12 0 0 25 0 1 0 481547943 19533824 4123 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4123 603 41 0 4728 0
vsize: 19076
[startup+110.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4438 0 0 0 10986 12 0 0 25 0 1 0 481547943 20471808 4362 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4998 4362 603 41 0 4957 0
vsize: 19992
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4629 0 0 0 11986 13 0 0 25 0 1 0 481547943 21270528 4553 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5193 4553 603 41 0 5152 0
vsize: 20772
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4712 0 0 0 12986 13 0 0 25 0 1 0 481547943 21532672 4636 4294967295 134512640 134672761 3221224576 3221223712 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5257 4636 603 41 0 5216 0
vsize: 21028
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4712 0 0 0 13986 13 0 0 25 0 1 0 481547943 21532672 4636 4294967295 134512640 134672761 3221224576 3221223920 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5257 4636 603 41 0 5216 0
vsize: 21028
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4712 0 0 0 14986 13 0 0 25 0 1 0 481547943 21532672 4636 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5257 4636 603 41 0 5216 0
vsize: 21028
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4712 0 0 0 15986 13 0 0 25 0 1 0 481547943 21532672 4636 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5257 4636 603 41 0 5216 0
vsize: 21028
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4850 0 0 0 16986 14 0 0 25 0 1 0 481547943 22073344 4774 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5389 4774 603 41 0 5348 0
vsize: 21556
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4937 0 0 0 17985 14 0 0 25 0 1 0 481547943 22474752 4861 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 4861 603 41 0 5446 0
vsize: 21948
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4937 0 0 0 18986 14 0 0 25 0 1 0 481547943 22474752 4861 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 4861 603 41 0 5446 0
vsize: 21948
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4938 0 0 0 19985 14 0 0 25 0 1 0 481547943 22474752 4862 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 4862 603 41 0 5446 0
vsize: 21948
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4938 0 0 0 20986 14 0 0 25 0 1 0 481547943 22474752 4862 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 4862 603 41 0 5446 0
vsize: 21948
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4938 0 0 0 21986 14 0 0 25 0 1 0 481547943 22474752 4862 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 4862 603 41 0 5446 0
vsize: 21948
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 4938 0 0 0 22986 15 0 0 25 0 1 0 481547943 22474752 4862 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5487 4862 603 41 0 5446 0
vsize: 21948
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5001 0 0 0 23986 15 0 0 25 0 1 0 481547943 22745088 4925 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5553 4925 603 41 0 5512 0
vsize: 22212
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5245 0 0 0 24985 15 0 0 25 0 1 0 481547943 23683072 5169 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5782 5169 603 41 0 5741 0
vsize: 23128
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18993
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5342 0 0 0 25985 16 0 0 25 0 1 0 481547943 24084480 5266 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5880 5266 603 41 0 5839 0
vsize: 23520
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5342 0 0 0 26985 16 0 0 25 0 1 0 481547943 24084480 5266 4294967295 134512640 134672761 3221224576 3221223724 1074733103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5880 5266 603 41 0 5839 0
vsize: 23520
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5342 0 0 0 27985 16 0 0 25 0 1 0 481547943 24084480 5266 4294967295 134512640 134672761 3221224576 3221223760 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5880 5266 603 41 0 5839 0
vsize: 23520
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5342 0 0 0 28985 16 0 0 25 0 1 0 481547943 24084480 5266 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5880 5266 603 41 0 5839 0
vsize: 23520
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5342 0 0 0 29986 16 0 0 25 0 1 0 481547943 24084480 5266 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5880 5266 603 41 0 5839 0
vsize: 23520
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5342 0 0 0 30986 16 0 0 25 0 1 0 481547943 24084480 5266 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5880 5266 603 41 0 5839 0
vsize: 23520
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5342 0 0 0 31986 16 0 0 25 0 1 0 481547943 24084480 5266 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5880 5266 603 41 0 5839 0
vsize: 23520
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5384 0 0 0 32986 16 0 0 25 0 1 0 481547943 24346624 5308 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5944 5308 603 41 0 5903 0
vsize: 23776
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5550 0 0 0 33986 17 0 0 25 0 1 0 481547943 25014272 5474 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6107 5474 603 41 0 6066 0
vsize: 24428
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5753 0 0 0 34985 17 0 0 25 0 1 0 481547943 25804800 5677 4294967295 134512640 134672761 3221224576 3221223700 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6300 5677 603 41 0 6259 0
vsize: 25200
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 5929 0 0 0 35985 18 0 0 25 0 1 0 481547943 26472448 5853 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6463 5853 603 41 0 6422 0
vsize: 25852
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6084 0 0 0 36985 18 0 0 25 0 1 0 481547943 27140096 6008 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6626 6008 603 41 0 6585 0
vsize: 26504
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6243 0 0 0 37985 18 0 0 25 0 1 0 481547943 27807744 6167 4294967295 134512640 134672761 3221224576 3221223776 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6167 603 41 0 6748 0
vsize: 27156
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6408 0 0 0 38985 19 0 0 25 0 1 0 481547943 28471296 6332 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6951 6332 603 41 0 6910 0
vsize: 27804
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6569 0 0 0 39984 19 0 0 25 0 1 0 481547943 29130752 6493 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7112 6493 603 41 0 7071 0
vsize: 28448
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6707 0 0 0 40984 20 0 0 25 0 1 0 481547943 29663232 6631 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7242 6631 603 41 0 7201 0
vsize: 28968
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6835 0 0 0 41984 20 0 0 25 0 1 0 481547943 30191616 6759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6759 603 41 0 7330 0
vsize: 29484
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6835 0 0 0 42984 20 0 0 25 0 1 0 481547943 30191616 6759 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6759 603 41 0 7330 0
vsize: 29484
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6835 0 0 0 43984 20 0 0 25 0 1 0 481547943 30191616 6759 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6759 603 41 0 7330 0
vsize: 29484
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6835 0 0 0 44984 20 0 0 25 0 1 0 481547943 30191616 6759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6759 603 41 0 7330 0
vsize: 29484
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6835 0 0 0 45985 20 0 0 25 0 1 0 481547943 30191616 6759 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6759 603 41 0 7330 0
vsize: 29484
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6835 0 0 0 46985 20 0 0 25 0 1 0 481547943 30191616 6759 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6759 603 41 0 7330 0
vsize: 29484
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6835 0 0 0 47985 21 0 0 25 0 1 0 481547943 30191616 6759 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6759 603 41 0 7330 0
vsize: 29484
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6839 0 0 0 48985 21 0 0 25 0 1 0 481547943 30191616 6763 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6763 603 41 0 7330 0
vsize: 29484
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6840 0 0 0 49985 21 0 0 25 0 1 0 481547943 30191616 6764 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6764 603 41 0 7330 0
vsize: 29484
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6846 0 0 0 50985 21 0 0 25 0 1 0 481547943 30191616 6770 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6770 603 41 0 7330 0
vsize: 29484
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6847 0 0 0 51985 21 0 0 25 0 1 0 481547943 30191616 6771 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7371 6771 603 41 0 7330 0
vsize: 29484
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6852 0 0 0 52986 21 0 0 25 0 1 0 481547943 30355456 6776 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6776 603 41 0 7370 0
vsize: 29644
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6853 0 0 0 53986 21 0 0 25 0 1 0 481547943 30355456 6777 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6777 603 41 0 7370 0
vsize: 29644
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6853 0 0 0 54986 21 0 0 25 0 1 0 481547943 30355456 6777 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6777 603 41 0 7370 0
vsize: 29644
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 6855 0 0 0 55986 21 0 0 25 0 1 0 481547943 30355456 6779 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6779 603 41 0 7370 0
vsize: 29644
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7011 0 0 0 56986 21 0 0 25 0 1 0 481547943 30879744 6935 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7539 6935 603 41 0 7498 0
vsize: 30156
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7184 0 0 0 57986 21 0 0 25 0 1 0 481547943 31674368 7108 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7733 7108 603 41 0 7692 0
vsize: 30932
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7320 0 0 0 58986 22 0 0 25 0 1 0 481547943 32215040 7244 4294967295 134512640 134672761 3221224576 3221223680 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7244 603 41 0 7824 0
vsize: 31460
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 59985 22 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 60984 22 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 61984 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 62984 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 63984 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 64985 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 65985 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 66985 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 67985 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 68985 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223680 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 69985 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 70985 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7321 0 0 0 71986 23 0 0 25 0 1 0 481547943 32215040 7245 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7865 7245 603 41 0 7824 0
vsize: 31460
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7368 0 0 0 72986 23 0 0 25 0 1 0 481547943 32346112 7292 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7897 7292 603 41 0 7856 0
vsize: 31588
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7507 0 0 0 73986 23 0 0 25 0 1 0 481547943 33005568 7431 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8058 7431 603 41 0 8017 0
vsize: 32232
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7679 0 0 0 74985 24 0 0 25 0 1 0 481547943 33665024 7603 4294967295 134512640 134672761 3221224576 3221223760 134558764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8219 7603 603 41 0 8178 0
vsize: 32876
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 7835 0 0 0 75985 24 0 0 25 0 1 0 481547943 34324480 7759 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8380 7759 603 41 0 8339 0
vsize: 33520
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 8025 0 0 0 76985 25 0 0 25 0 1 0 481547943 35119104 7949 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8574 7949 603 41 0 8533 0
vsize: 34296
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 8196 0 0 0 77985 25 0 0 25 0 1 0 481547943 35782656 8120 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8736 8120 603 41 0 8695 0
vsize: 34944
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 8343 0 0 0 78985 25 0 0 25 0 1 0 481547943 36311040 8267 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8865 8267 603 41 0 8824 0
vsize: 35460
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 8477 0 0 0 79985 26 0 0 25 0 1 0 481547943 36978688 8401 4294967295 134512640 134672761 3221224576 3221223728 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9028 8401 603 41 0 8987 0
vsize: 36112
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 8624 0 0 0 80984 26 0 0 25 0 1 0 481547943 37781504 8548 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8548 603 41 0 9183 0
vsize: 36896
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 8719 0 0 0 81983 27 0 0 25 0 1 0 481547943 38191104 8643 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9324 8643 603 41 0 9283 0
vsize: 37296
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 8838 0 0 0 82983 27 0 0 25 0 1 0 481547943 38715392 8762 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9452 8762 603 41 0 9411 0
vsize: 37808
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 8954 0 0 0 83983 28 0 0 25 0 1 0 481547943 39112704 8878 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9549 8878 603 41 0 9508 0
vsize: 38196
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9061 0 0 0 84982 28 0 0 25 0 1 0 481547943 39510016 8985 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9646 8985 603 41 0 9605 0
vsize: 38584
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9144 0 0 0 85982 29 0 0 25 0 1 0 481547943 39903232 9068 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9068 603 41 0 9701 0
vsize: 38968
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9152 0 0 0 86982 29 0 0 25 0 1 0 481547943 39903232 9076 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9076 603 41 0 9701 0
vsize: 38968
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9152 0 0 0 87983 29 0 0 25 0 1 0 481547943 39903232 9076 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9076 603 41 0 9701 0
vsize: 38968
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9152 0 0 0 88983 29 0 0 25 0 1 0 481547943 39903232 9076 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9076 603 41 0 9701 0
vsize: 38968
[startup+900.029 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9152 0 0 0 89983 29 0 0 25 0 1 0 481547943 39903232 9076 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9076 603 41 0 9701 0
vsize: 38968
[startup+910.029 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9152 0 0 0 90983 29 0 0 25 0 1 0 481547943 39903232 9076 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9076 603 41 0 9701 0
vsize: 38968
[startup+920.029 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9153 0 0 0 91983 29 0 0 25 0 1 0 481547943 39903232 9077 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9077 603 41 0 9701 0
vsize: 38968
[startup+930.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9153 0 0 0 92983 29 0 0 25 0 1 0 481547943 39903232 9077 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9742 9077 603 41 0 9701 0
vsize: 38968
[startup+940.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9163 0 0 0 93984 29 0 0 25 0 1 0 481547943 40071168 9087 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9087 603 41 0 9742 0
vsize: 39132
[startup+950.029 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9164 0 0 0 94984 29 0 0 25 0 1 0 481547943 40071168 9088 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9088 603 41 0 9742 0
vsize: 39132
[startup+960.029 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9165 0 0 0 95984 29 0 0 25 0 1 0 481547943 40071168 9089 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9089 603 41 0 9742 0
vsize: 39132
[startup+970.029 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9165 0 0 0 96984 29 0 0 25 0 1 0 481547943 40071168 9089 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9089 603 41 0 9742 0
vsize: 39132
[startup+980.028 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9166 0 0 0 97984 29 0 0 25 0 1 0 481547943 40071168 9090 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9090 603 41 0 9742 0
vsize: 39132
[startup+990.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9166 0 0 0 98984 29 0 0 25 0 1 0 481547943 40071168 9090 4294967295 134512640 134672761 3221224576 3221223760 134558504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9090 603 41 0 9742 0
vsize: 39132
[startup+1000.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9166 0 0 0 99984 29 0 0 25 0 1 0 481547943 40071168 9090 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9090 603 41 0 9742 0
vsize: 39132
[startup+1010.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9166 0 0 0 100985 29 0 0 25 0 1 0 481547943 40071168 9090 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9090 603 41 0 9742 0
vsize: 39132
[startup+1020.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9166 0 0 0 101985 29 0 0 25 0 1 0 481547943 40071168 9090 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9090 603 41 0 9742 0
vsize: 39132
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9166 0 0 0 102985 29 0 0 25 0 1 0 481547943 40071168 9090 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9090 603 41 0 9742 0
vsize: 39132
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9175 0 0 0 103985 29 0 0 25 0 1 0 481547943 40071168 9099 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9099 603 41 0 9742 0
vsize: 39132
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9176 0 0 0 104985 29 0 0 25 0 1 0 481547943 40071168 9100 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9100 603 41 0 9742 0
vsize: 39132
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9176 0 0 0 105985 29 0 0 25 0 1 0 481547943 40071168 9100 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9100 603 41 0 9742 0
vsize: 39132
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9176 0 0 0 106986 29 0 0 25 0 1 0 481547943 40071168 9100 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9100 603 41 0 9742 0
vsize: 39132
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9177 0 0 0 107986 29 0 0 25 0 1 0 481547943 40071168 9101 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9101 603 41 0 9742 0
vsize: 39132
[startup+1090.03 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9177 0 0 0 108986 29 0 0 25 0 1 0 481547943 40071168 9101 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9101 603 41 0 9742 0
vsize: 39132
[startup+1100.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9177 0 0 0 109986 29 0 0 25 0 1 0 481547943 40071168 9101 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9101 603 41 0 9742 0
vsize: 39132
[startup+1110.03 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9177 0 0 0 110986 29 0 0 25 0 1 0 481547943 40071168 9101 4294967295 134512640 134672761 3221224576 3221223680 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9101 603 41 0 9742 0
vsize: 39132
[startup+1120.03 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9177 0 0 0 111987 29 0 0 25 0 1 0 481547943 40071168 9101 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9101 603 41 0 9742 0
vsize: 39132
[startup+1130.03 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9178 0 0 0 112987 29 0 0 25 0 1 0 481547943 40071168 9102 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9102 603 41 0 9742 0
vsize: 39132
[startup+1140.03 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9178 0 0 0 113987 29 0 0 25 0 1 0 481547943 40071168 9102 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9102 603 41 0 9742 0
vsize: 39132
[startup+1150.03 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9178 0 0 0 114987 29 0 0 25 0 1 0 481547943 40071168 9102 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9102 603 41 0 9742 0
vsize: 39132
[startup+1160.03 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9178 0 0 0 115987 29 0 0 25 0 1 0 481547943 40071168 9102 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9102 603 41 0 9742 0
vsize: 39132
[startup+1170.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9178 0 0 0 116987 29 0 0 25 0 1 0 481547943 40071168 9102 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9102 603 41 0 9742 0
vsize: 39132
[startup+1180.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9178 0 0 0 117987 29 0 0 25 0 1 0 481547943 40071168 9102 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9102 603 41 0 9742 0
vsize: 39132
[startup+1190.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9178 0 0 0 118987 29 0 0 25 0 1 0 481547943 40071168 9102 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9102 603 41 0 9742 0
vsize: 39132
[startup+1200.03 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 18995
Raw data (stat): 18993 (minisat+) R 18992 11931 11930 0 -1 0 9178 0 0 0 119987 30 0 0 25 0 1 0 481547943 40071168 9102 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9783 9102 603 41 0 9742 0
vsize: 39132
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.03 1.01 0.93 1/54 18995
Raw data (stat): 18993 (minisat+) Z 18992 11931 11930 0 -1 12 9181 0 0 0 119988 31 0 0 25 0 1 0 481547943 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.2
CPU user time (s): 1199.88
CPU system time (s): 0.318951
CPU usage (%): 100.012
Max. virtual memory (Kb): 39132
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####