PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-misc07.opb
MD5SUM	b8ad25b48a93aa2545086c9eaeaee0ef
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1076879360
Optimality of the best value was proved	NO
Number of terms in the objective function	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	1073741824
Number of bits of the biggest number in a constraint	31
Biggest sum of numbers in a constraint	3287948287
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1227.3
Number of variables	290
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	263
Trace number 30761

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-25 19:18:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22161 boxname=wulflinc19 idbench=977 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  b8ad25b48a93aa2545086c9eaeaee0ef  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-misc07.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-misc07.opb
IDLAUNCH: 22161
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        414344 kB
Buffers:         35820 kB
Cached:         557880 kB
SwapCached:        416 kB
Active:          62308 kB
Inactive:       533620 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        414092 kB
SwapTotal:     2097892 kB
SwapFree:      2096804 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            18752 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 19:38:46 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 22161 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1708   maxlim: 1073742847   bits: 32/31
c ---[ 244]---> BDD-cost:  239
c ---[ 233]---> BDD-cost:  239
c ---[ 200]---> Sorter-cost:  127     Base:
c ---[ 197]---> Sorter-cost:  127     Base:
c ---[ 195]---> Sorter-cost:  127     Base:
c ---[ 193]---> Sorter-cost:  127     Base:
c ---[ 191]---> Sorter-cost:  127     Base:
c ---[ 189]---> Sorter-cost:  127     Base:
c ---[ 187]---> Sorter-cost:  127     Base:
c ---[ 185]---> Sorter-cost:  127     Base:
c ---[ 183]---> Sorter-cost:  127     Base:
c ---[ 181]---> Sorter-cost:  127     Base:
c ---[ 179]---> Sorter-cost:  127     Base:
c ---[ 176]---> Sorter-cost:  127     Base:
c ---[ 174]---> Sorter-cost:  127     Base:
c ---[ 172]---> Sorter-cost:  127     Base:
c ---[ 170]---> Sorter-cost:  127     Base:
c ---[ 168]---> Sorter-cost:  127     Base:
c ---[ 166]---> Sorter-cost:  127     Base:
c ---[ 164]---> Sorter-cost:  127     Base:
c ---[ 162]---> Sorter-cost:  127     Base:
c ---[ 160]---> Sorter-cost:  127     Base:
c ---[ 158]---> Sorter-cost:  127     Base:
c ---[ 155]---> Sorter-cost:  127     Base:
c ---[ 153]---> Sorter-cost:  127     Base:
c ---[ 151]---> Sorter-cost:  127     Base:
c ---[ 149]---> Sorter-cost:  127     Base:
c ---[ 147]---> Sorter-cost:  127     Base:
c ---[ 145]---> Sorter-cost:  127     Base:
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   50
c ---[ 131]---> BDD-cost:   50
c ---[ 130]---> BDD-cost:   50
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   48
c ---[ 124]---> BDD-cost:   48
c ---[ 123]---> BDD-cost:   48
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   50
c ---[ 117]---> BDD-cost:   50
c ---[ 116]---> BDD-cost:   50
c ---[ 115]---> BDD-cost:   27
c ---[ 114]---> BDD-cost:   27
c ---[ 113]---> BDD-cost:   27
c ---[ 112]---> BDD-cost:   48
c ---[ 111]---> BDD-cost:   48
c ---[ 110]---> BDD-cost:   48
c ---[ 109]---> BDD-cost:   27
c ---[ 108]---> BDD-cost:   27
c ---[ 106]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:   27
c ---[ 103]---> BDD-cost:   50
c ---[ 102]---> BDD-cost:   50
c ---[ 101]---> BDD-cost:   50
c ---[ 100]---> BDD-cost:   27
c ---[  99]---> BDD-cost:   27
c ---[  98]---> BDD-cost:   27
c ---[  97]---> BDD-cost:   48
c ---[  96]---> BDD-cost:   48
c ---[  95]---> BDD-cost:   48
c ---[  93]---> BDD-cost:   27
c ---[  92]---> BDD-cost:   27
c ---[  91]---> BDD-cost:   27
c ---[  81]---> BDD-cost:   51
c ---[  69]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   51
c ---[  45]---> BDD-cost:   51
c ---[  33]---> BDD-cost:   51
c ---[  21]---> BDD-cost:   51
c ---[  10]---> BDD-cost:  216
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25851    84536 |    8617       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1079342080[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        11 |   25847    84530 |    8615       4       91    22.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: 1078517760[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        64 |   25866    84573 |    8622      57     1765    31.0 |  0.000 % |
c |       164 |   25866    84573 |    9484     157    10915    69.5 |  3.029 % |
c |       318 |   25866    84573 |   10432     311    16922    54.4 |  3.029 % |
c ==============================================================================
c [1mFound solution: 1078481920[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       339 |   25889    84624 |    8629     332    17661    53.2 |  3.029 % |
c |       439 |   25889    84624 |    9491     432    21117    48.9 |  3.039 % |
c ==============================================================================
c [1mFound solution: 1078420480[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       520 |   25856    84552 |    8618     509    24798    48.7 |  3.039 % |
c |       620 |   25814    84402 |    9479     604    26766    44.3 |  3.279 % |
c ==============================================================================
c [1mFound solution: 1078205440[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       647 |   25825    84427 |    8608     630    27468    43.6 |  3.279 % |
c |       747 |   25825    84427 |    9468     730    37287    51.1 |  3.333 % |
c |       897 |   25825    84427 |   10415     880    44135    50.2 |  3.333 % |
c ==============================================================================
c [1mFound solution: 1078133760[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       961 |   25838    84456 |    8612     942    47501    50.4 |  3.333 % |
c |      1067 |   25838    84456 |    9473    1048    48813    46.6 |  3.373 % |
c ==============================================================================
c [1mFound solution: 1078128640[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1115 |   25857    84500 |    8619    1096    54832    50.0 |  3.373 % |
c |      1215 |   25857    84500 |    9480    1196    55960    46.8 |  3.384 % |
c |      1366 |   25857    84500 |   10428    1347    67021    49.8 |  3.384 % |
c |      1591 |   25785    84246 |   11471    1565    74693    47.7 |  3.456 % |
c ==============================================================================
c [1mFound solution: 1078056960[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1704 |   25805    84292 |    8601    1678    81511    48.6 |  3.456 % |
c ==============================================================================
c [1mFound solution: 1077985280[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1752 |   25812    84307 |    8604    1725    85915    49.8 |  3.456 % |
c |      1853 |   25812    84307 |    9464    1826    86621    47.4 |  3.521 % |
c ==============================================================================
c [1mFound solution: 1077949440[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1938 |   25791    84259 |    8597    1905    89268    46.9 |  3.521 % |
c |      2042 |   25791    84259 |    9456    2009    97273    48.4 |  3.704 % |
c |      2192 |   25731    84043 |   10402    2153   101486    47.1 |  3.732 % |
c ==============================================================================
c [1mFound solution: 1077944320[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2274 |   25750    84083 |    8583    2235   106881    47.8 |  3.732 % |
c |      2376 |   25750    84083 |    9441    2337   110992    47.5 |  3.744 % |
c ==============================================================================
c [1mFound solution: 1077898240[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2455 |   25767    84127 |    8589    2416   117335    48.6 |  3.744 % |
c |      2556 |   25746    84052 |    9447    2514   119722    47.6 |  3.769 % |
c |      2708 |   25731    83999 |   10392    2664   127317    47.8 |  3.783 % |
c |      2934 |   25718    83969 |   11431    2888   162522    56.3 |  3.826 % |
c ==============================================================================
c [1mFound solution: 1077724160[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3124 |   25720    83957 |    8573    3073   171984    56.0 |  3.826 % |
c |      3226 |   25720    83957 |    9430    3175   176631    55.6 |  3.851 % |
c |      3378 |   25720    83957 |   10373    3327   198826    59.8 |  3.851 % |
c |      3604 |   25720    83957 |   11410    3553   206694    58.2 |  3.851 % |
c |      3941 |   25720    83957 |   12551    3890   257360    66.2 |  3.851 % |
c ==============================================================================
c [1mFound solution: 1077611520[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4345 |   25705    83882 |    8568    4292   298875    69.6 |  3.851 % |
c |      4445 |   25609    83544 |    9424    4381   301713    68.9 |  3.990 % |
c |      4595 |   25609    83544 |   10367    4531   311528    68.8 |  3.990 % |
c |      4820 |   25609    83544 |   11404    4756   331547    69.7 |  3.990 % |
c |      5157 |   25591    83505 |   12544    5089   376075    73.9 |  4.061 % |
c ==============================================================================
c [1mFound solution: 1077565440[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5223 |   25609    83547 |    8536    5155   380655    73.8 |  4.061 % |
c |      5323 |   25609    83547 |    9389    5255   386864    73.6 |  4.071 % |
c |      5474 |   25609    83547 |   10328    5406   407086    75.3 |  4.071 % |
c |      5702 |   25541    83359 |   11361    5605   421575    75.2 |  4.255 % |
c |      6039 |   25541    83359 |   12497    5942   453221    76.3 |  4.255 % |
c ==============================================================================
c [1mFound solution: 1077478400[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6099 |   25556    83394 |    8518    6002   460270    76.7 |  4.255 % |
c |      6199 |   25556    83394 |    9369    6102   465232    76.2 |  4.266 % |
c |      6350 |   25556    83394 |   10306    6253   486947    77.9 |  4.266 % |
c |      6575 |   25493    83175 |   11337    6471   490780    75.8 |  4.352 % |
c |      6913 |   25482    83151 |   12471    6807   508713    74.7 |  4.394 % |
c |      7420 |   25482    83151 |   13718    7314   553071    75.6 |  4.394 % |
c |      8179 |   25482    83151 |   15090    8073   641561    79.5 |  4.394 % |
c ==============================================================================
c [1mFound solution: 1077457920[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8472 |   25500    83192 |    8500    8366   660683    79.0 |  4.394 % |
c |      8573 |   25500    83192 |    9350    8467   668523    79.0 |  4.404 % |
c |      8723 |   25500    83192 |   10285    8617   692126    80.3 |  4.404 % |
c |      8949 |   25472    83110 |   11313    8840   704972    79.7 |  4.475 % |
c |      9289 |   25472    83110 |   12444    9180   740265    80.6 |  4.475 % |
c |      9795 |   25472    83110 |   13689    9686   793671    81.9 |  4.475 % |
c ==============================================================================
c [1mFound solution: 1077345280[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9842 |   25489    83152 |    8496    9733   795140    81.7 |  4.475 % |
c |      9942 |   25489    83152 |    9345    4967   337006    67.8 |  4.485 % |
c |     10094 |   25489    83152 |   10280    5119   341325    66.7 |  4.485 % |
c |     10323 |   25478    83128 |   11308    5347   364771    68.2 |  4.527 % |
c |     10664 |   25478    83128 |   12438    5688   383232    67.4 |  4.527 % |
c ==============================================================================
c [1mFound solution: 1076710400[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10744 |   25500    83178 |    8500    5768   393632    68.2 |  4.527 % |
c |     10844 |   25500    83178 |    9350    5868   395656    67.4 |  4.535 % |
c |     10998 |   25418    82996 |   10285    6006   411279    68.5 |  4.874 % |
c |     11225 |   25418    82996 |   11313    6233   426973    68.5 |  4.874 % |
c |     11563 |   25418    82996 |   12444    6571   466696    71.0 |  4.874 % |
c |     12071 |   25418    82996 |   13689    7079   493302    69.7 |  4.874 % |
c |     12830 |   25418    82996 |   15058    7838   591857    75.5 |  4.874 % |
c |     13970 |   25401    82958 |   16564    8977   714946    79.6 |  4.945 % |
c |     15678 |   25390    82934 |   18220   10684   897257    84.0 |  4.987 % |
c |     18244 |   25352    82816 |   20042   13246  1116382    84.3 |  5.086 % |
c |     22088 |   25309    82665 |   22046   17087  1618618    94.7 |  5.171 % |
c |     27858 |   25259    82519 |   24251   22843  1989220    87.1 |  5.284 % |
c |     36507 |   25128    82090 |   26676   18784  1656576    88.2 |  5.538 % |
c |     49481 |   25077    81913 |   29344   17628  1387747    78.7 |  5.609 % |
c |     68945 |   25045    81842 |   32278   21913  2178315    99.4 |  5.736 % |
c |     98137 |   24726    80932 |   35506   33927  3079942    90.8 |  6.654 % |
c ==============================================================================
c [1mFound solution: 1076705280[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127765 |   24673    80815 |    8224   23020  2111284    91.7 |  6.654 % |
c |    127866 |   24673    80815 |    9046    5856   311589    53.2 |  6.985 % |
c |    128016 |   24673    80815 |    9951    6006   314957    52.4 |  6.985 % |
c |    128241 |   24673    80815 |   10946    6231   333603    53.5 |  6.985 % |
c |    128578 |   24666    80800 |   12040    6567   366560    55.8 |  7.013 % |
c |    129084 |   24666    80800 |   13244    7073   399224    56.4 |  7.013 % |
c |    129843 |   24666    80800 |   14569    7832   460274    58.8 |  7.013 % |
c |    130982 |   24666    80800 |   16026    8971   574639    64.1 |  7.013 % |
c |    132690 |   24629    80718 |   17628   10673   736057    69.0 |  7.168 % |
c |    135252 |   24622    80703 |   19391   13233  1087697    82.2 |  7.196 % |
c ==============================================================================
c [1mFound solution: 1076674560[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    138836 |   24639    80741 |    8213   16817  1536401    91.4 |  7.196 % |
c |    138937 |   24639    80741 |    9034    8510   711192    83.6 |  7.204 % |
c |    139088 |   24639    80741 |    9937    8661   724525    83.7 |  7.204 % |
c |    139313 |   24639    80741 |   10931    8886   743774    83.7 |  7.204 % |
c |    139652 |   24639    80741 |   12024    9225   781501    84.7 |  7.204 % |
c |    140158 |   24639    80741 |   13227    9731   854334    87.8 |  7.204 % |
c |    140917 |   24527    80364 |   14549   10482   920049    87.8 |  7.430 % |
c |    142057 |   24527    80364 |   16004   11622  1096546    94.4 |  7.430 % |
c |    143765 |   24510    80326 |   17605   13329  1275622    95.7 |  7.500 % |
c |    146328 |   24477    80254 |   19365   15885  1484207    93.4 |  7.627 % |
c |    150176 |   24463    80221 |   21302   19731  1818948    92.2 |  7.670 % |
c |    155942 |   24463    80221 |   23432   13932   973168    69.9 |  7.670 % |
c |    164593 |   24392    79987 |   25775   22563  1808661    80.2 |  7.782 % |
c ==============================================================================
c [1mFound solution: 1076618240[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    171481 |   24409    80027 |    8136   15404  1317756    85.5 |  7.782 % |
c |    171583 |   24409    80027 |    8949    7804   576344    73.9 |  7.789 % |
c |    171733 |   24409    80027 |    9844    7954   588964    74.0 |  7.789 % |
c |    171958 |   24409    80027 |   10829    8179   607574    74.3 |  7.789 % |
c |    172296 |   24409    80027 |   11911    8517   636233    74.7 |  7.789 % |
c |    172803 |   24409    80027 |   13103    9024   692041    76.7 |  7.789 % |
c |    173562 |   24409    80027 |   14413    9783   788676    80.6 |  7.789 % |
c |    174702 |   24400    80007 |   15854   10922   851407    78.0 |  7.831 % |
c |    176413 |   24400    80007 |   17440   12633  1095521    86.7 |  7.831 % |
c |    178977 |   24363    79914 |   19184   15189  1334750    87.9 |  7.958 % |
c |    182825 |   24356    79899 |   21102   19035  1658896    87.1 |  7.986 % |
c |    188591 |   24356    79899 |   23212   13144   933338    71.0 |  7.986 % |
c |    197240 |   24356    79899 |   25534   21793  1707844    78.4 |  7.986 % |
c |    210214 |   24320    79788 |   28087   21107  1426821    67.6 |  8.070 % |
c |    229675 |   24311    79768 |   30896   25479  1931526    75.8 |  8.113 % |
c |    258870 |   24252    79596 |   33986   21829  1523178    69.8 |  8.254 % |
c |    302660 |   24206    79495 |   37384   26569  2716830   102.3 |  8.437 % |
c |    368346 |   24189    79457 |   41123   26723  2058177    77.0 |  8.507 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 26278 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.98 2/54 26274
Raw data (stat): 26274 (runsolver) R 26273 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841332448 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0005 s]
Raw data (loadavg): 0.96 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0011 s]
Raw data (loadavg): 0.97 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0022 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0015 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.001 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.008 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.008 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.009 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.009 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.011 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.023 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.035 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.039 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.039 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.041 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.041 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.042 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.042 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.042 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.043 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.042 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.044 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.044 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.044 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.044 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.046 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.046 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.046 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.047 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.047 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.047 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.048 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.048 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.049 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.049 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.049 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.06 s]
Raw data (loadavg): 1.07 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.06 s]
Raw data (loadavg): 1.06 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.07 s]
Raw data (loadavg): 1.05 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.06 s]
Raw data (loadavg): 1.04 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.06 s]
Raw data (loadavg): 1.04 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.06 s]
Raw data (loadavg): 1.03 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.07 s]
Raw data (loadavg): 1.03 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.07 s]
Raw data (loadavg): 1.02 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.06 s]
Raw data (loadavg): 1.02 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.07 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.07 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.07 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.07 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.07 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.74 s]
Raw data (loadavg): 1.00 1.00 0.99 1/53 26278
Raw data (stat): 26274 (minisat+_script) S 26273 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841332448 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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