PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10b.opb
MD5SUM	c76102ddcf7f5ab3b2677033d320eaa3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	756736
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	502612132
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	502612132
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	422.405
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 32442

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-05-27 09:59:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23834 boxname=wulflinc25 idbench=1478 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c76102ddcf7f5ab3b2677033d320eaa3  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-ran10x10b.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-ran10x10b.opb
IDLAUNCH: 23834
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        897724 kB
Buffers:          3664 kB
Cached:         113940 kB
SwapCached:        988 kB
Active:          19008 kB
Inactive:       100656 kB
HighTotal:      131008 kB
HighFree:        14224 kB
LowTotal:       903652 kB
LowFree:        883500 kB
SwapTotal:     2097892 kB
SwapFree:      2095960 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           4980 kB
Slab:            11680 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 10:19:31 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23834 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> BDD-cost: 1135
c ---[ 136]---> BDD-cost:  973
c ---[ 134]---> BDD-cost:  886
c ---[ 132]---> BDD-cost: 1137
c ---[ 130]---> BDD-cost:  918
c ---[ 128]---> BDD-cost: 1080
c ---[ 126]---> BDD-cost: 1031
c ---[ 124]---> BDD-cost:  815
c ---[ 122]---> BDD-cost:  886
c ---[ 120]---> BDD-cost: 1169
c ---[ 118]---> BDD-cost:  817
c ---[ 116]---> BDD-cost: 1118
c ---[ 114]---> BDD-cost:  960
c ---[ 112]---> BDD-cost: 1164
c ---[ 110]---> BDD-cost: 1153
c ---[ 108]---> BDD-cost:  817
c ---[ 106]---> BDD-cost: 1164
c ---[ 104]---> BDD-cost: 1040
c ---[ 102]---> BDD-cost:  607
c ---[ 100]---> BDD-cost: 1040
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   12
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   57945   166633 |   19315       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3554095[0m
c ---[   0]---> Sorter-cost:142488     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        19 |  451839  1086276 |  150613      19      407    21.4 |  0.000 % |
c |       119 |  451839  1086276 |  165674     119     6132    51.5 |  0.719 % |
c |       271 |  450725  1083741 |  182241     262     8372    32.0 |  0.916 % |
c |       498 |  450725  1083741 |  200465     489     9823    20.1 |  0.916 % |
c |       835 |  450725  1083741 |  220512     826    20152    24.4 |  0.916 % |
c ==============================================================================
c [1mFound solution: 2991769[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1025 |  452391  1088540 |  150797    1013    25464    25.1 |  0.916 % |
c |      1125 |  452391  1088540 |  165876    1113    26020    23.4 |  0.916 % |
c |      1277 |  452363  1088477 |  182464    1264    29328    23.2 |  0.921 % |
c |      1505 |  452363  1088477 |  200710    1492    47856    32.1 |  0.921 % |
c |      1842 |  452363  1088477 |  220781    1829   131633    72.0 |  0.921 % |
c |      2348 |  452363  1088477 |  242860    2335   140684    60.3 |  0.921 % |
c |      3109 |  452363  1088477 |  267146    3096   147102    47.5 |  0.921 % |
c |      4248 |  452363  1088477 |  293860    4235   159852    37.7 |  0.921 % |
c |      5956 |  452363  1088477 |  323246    5943   178132    30.0 |  0.921 % |
c |      8518 |  452363  1088477 |  355571    8505   207079    24.3 |  0.921 % |
c |     12362 |  452128  1087947 |  391128   12346   372248    30.2 |  0.960 % |
c |     18129 |  452128  1087947 |  430241   18113   626340    34.6 |  0.960 % |
c ==============================================================================
c [1mFound solution: 2465935[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18481 |  450352  1084070 |  150117   18425   639305    34.7 |  0.960 % |
c |     18581 |  450352  1084070 |  165128   18525   641180    34.6 |  1.384 % |
c |     18731 |  450352  1084070 |  181641   18675   644570    34.5 |  1.384 % |
c |     18956 |  450352  1084070 |  199805   18900   653860    34.6 |  1.384 % |
c |     19293 |  450352  1084070 |  219786   19237   659781    34.3 |  1.384 % |
c |     19800 |  450352  1084070 |  241764   19744   664387    33.7 |  1.384 % |
c |     20559 |  450352  1084070 |  265941   20503   670011    32.7 |  1.384 % |
c |     21700 |  449814  1082847 |  292535   21629   703984    32.5 |  1.481 % |
c |     23409 |  449724  1082642 |  321789   23337   723736    31.0 |  1.498 % |
c |     25971 |  449712  1082615 |  353968   25897   760457    29.4 |  1.499 % |
c |     29816 |  449712  1082615 |  389364   29742  1044732    35.1 |  1.499 % |
c |     35582 |  449712  1082615 |  428301   35508  1153707    32.5 |  1.499 % |
c |     44233 |  449712  1082615 |  471131   44159  1346382    30.5 |  1.499 % |
c |     57207 |  449712  1082615 |  518244   57133  1611565    28.2 |  1.499 % |
c ==============================================================================
c [1mFound solution: 2004246[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74957 |  450532  1084799 |  150177   74878  2230234    29.8 |  1.499 % |
c |     75057 |  450453  1084620 |  165194   74972  2233402    29.8 |  1.585 % |
c |     75209 |  450245  1084143 |  181714   75114  2234609    29.7 |  1.625 % |
c |     75435 |  450245  1084143 |  199885   75340  2236778    29.7 |  1.625 % |
c |     75772 |  450245  1084143 |  219874   75677  2239981    29.6 |  1.625 % |
c |     76278 |  450245  1084143 |  241861   76183  2246982    29.5 |  1.625 % |
c |     77037 |  450245  1084143 |  266047   76942  2252208    29.3 |  1.625 % |
c |     78176 |  450245  1084143 |  292652   78081  2271138    29.1 |  1.625 % |
c |     79884 |  450245  1084143 |  321917   79789  2293573    28.7 |  1.625 % |
c |     82446 |  450245  1084143 |  354109   82351  2545845    30.9 |  1.625 % |
c ==============================================================================
c [1mFound solution: 1634335[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82599 |  450511  1084971 |  150170   82504  2555090    31.0 |  1.625 % |
c |     82699 |  450511  1084971 |  165187   82604  2555944    30.9 |  1.624 % |
c |     82849 |  450511  1084971 |  181705   82754  2556727    30.9 |  1.624 % |
c |     83074 |  450221  1084315 |  199876   82936  2559843    30.9 |  1.675 % |
c |     83412 |  450221  1084315 |  219863   83274  2576658    30.9 |  1.675 % |
c |     83919 |  450221  1084315 |  241850   83781  2651590    31.6 |  1.675 % |
c |     84678 |  450221  1084315 |  266035   84540  2683234    31.7 |  1.675 % |
c |     85822 |  450221  1084315 |  292638   85684  2695210    31.5 |  1.675 % |
c |     87530 |  449807  1083374 |  321902   87367  2797333    32.0 |  1.750 % |
c |     90092 |  449807  1083374 |  354093   89929  3433440    38.2 |  1.750 % |
c |     93940 |  449807  1083374 |  389502   93777  3806073    40.6 |  1.750 % |
c |     99706 |  449807  1083374 |  428452   99543  4030589    40.5 |  1.750 % |
c |    108355 |  449764  1083277 |  471297  108191  4251518    39.3 |  1.758 % |
c |    121330 |  449659  1083036 |  518427  121165  6299349    52.0 |  1.777 % |
c ==============================================================================
c [1mFound solution: 1632925[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    121883 |  450049  1083999 |  150016  121717  6318891    51.9 |  1.777 % |
c |    121983 |  450049  1083999 |  165017  121817  6325444    51.9 |  1.781 % |
c |    122133 |  450049  1083999 |  181519  121967  6326342    51.9 |  1.781 % |
c |    122358 |  450049  1083999 |  199671  122192  6345604    51.9 |  1.781 % |
c |    122695 |  450049  1083999 |  219638  122529  6383044    52.1 |  1.781 % |
c ==============================================================================
c [1mFound solution: 1496403[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122862 |  450159  1084290 |  150053  122696  6391355    52.1 |  1.781 % |
c |    122964 |  450159  1084290 |  165058  122798  6399593    52.1 |  1.781 % |
c |    123114 |  450159  1084290 |  181564  122948  6400603    52.1 |  1.781 % |
c |    123341 |  450159  1084290 |  199720  123175  6408555    52.0 |  1.781 % |
c |    123678 |  450159  1084290 |  219692  123512  6419657    52.0 |  1.781 % |
c |    124185 |  450159  1084290 |  241661  124019  6439491    51.9 |  1.781 % |
c |    124946 |  450159  1084290 |  265828  124780  6541832    52.4 |  1.781 % |
c |    126086 |  450159  1084290 |  292410  125920  6649726    52.8 |  1.781 % |
c |    127794 |  449672  1083169 |  321651  127572  7022762    55.0 |  1.878 % |
c |    130357 |  449672  1083169 |  353817  130135  7676190    59.0 |  1.878 % |
c |    134201 |  449672  1083169 |  389198  133979  7729697    57.7 |  1.878 % |
c |    139968 |  449617  1083045 |  428118  139745  7945961    56.9 |  1.888 % |
c |    148618 |  449517  1082816 |  470930  148393  8179059    55.1 |  1.906 % |
c ==============================================================================
c [1mFound solution: 1464834[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150916 |  448514  1080532 |  149504  150608  8337031    55.4 |  1.906 % |
c |    151016 |  448514  1080532 |  164454  150708  8337632    55.3 |  2.110 % |
c |    151166 |  448493  1080486 |  180899  150856  8338695    55.3 |  2.114 % |
c |    151391 |  448493  1080486 |  198989  151081  8341444    55.2 |  2.114 % |
c |    151728 |  448416  1080310 |  218888  151414  8343716    55.1 |  2.128 % |
c |    152234 |  447905  1079142 |  240777  151888  8352890    55.0 |  2.222 % |
c |    152993 |  447905  1079142 |  264855  152647  8410937    55.1 |  2.222 % |
c |    154133 |  447905  1079142 |  291341  153787  8682887    56.5 |  2.222 % |
c |    155841 |  447905  1079142 |  320475  155495  8717725    56.1 |  2.222 % |
c |    158407 |  447665  1078596 |  352522  158054  9040255    57.2 |  2.264 % |
c ==============================================================================
c [1mFound solution: 1396323[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    158783 |  447734  1078785 |  149244  158430  9059659    57.2 |  2.264 % |
c |    158883 |  447734  1078785 |  164168   34029  1084457    31.9 |  2.264 % |
c |    159035 |  447734  1078785 |  180585   34181  1085391    31.8 |  2.264 % |
c |    159263 |  447734  1078785 |  198643   34409  1087596    31.6 |  2.264 % |
c |    159600 |  447734  1078785 |  218508   34746  1093375    31.5 |  2.264 % |
c |    160106 |  447734  1078785 |  240358   35252  1112539    31.6 |  2.264 % |
c |    160867 |  447734  1078785 |  264394   36013  1236961    34.3 |  2.264 % |
c |    162006 |  447734  1078785 |  290834   37152  1250526    33.7 |  2.264 % |
c |    163714 |  447734  1078785 |  319917   38860  1482573    38.2 |  2.264 % |
c ==============================================================================
c [1mFound solution: 780995[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165968 |  448044  1079523 |  149348   41114  1886613    45.9 |  2.264 % |
c |    166071 |  448044  1079523 |  164282   41217  1898309    46.1 |  2.262 % |
c |    166222 |  448044  1079523 |  180711   41368  1901097    46.0 |  2.262 % |
c |    166447 |  447765  1078880 |  198782   41592  1915132    46.0 |  2.318 % |
c |    166784 |  447662  1078646 |  218660   41924  1922316    45.9 |  2.336 % |
c |    167292 |  447460  1078181 |  240526   42412  1978442    46.6 |  2.375 % |
c |    168051 |  447460  1078181 |  264579   43171  2100330    48.7 |  2.375 % |
c ==============================================================================
c [1mFound solution: 765056[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168184 |  447495  1078277 |  149165   43304  2114380    48.8 |  2.375 % |
c |    168285 |  447495  1078277 |  164081   43405  2120084    48.8 |  2.376 % |
c |    168435 |  447495  1078277 |  180489   43555  2127503    48.8 |  2.376 % |
c |    168660 |  447495  1078277 |  198538   43780  2153537    49.2 |  2.376 % |
c |    168998 |  447495  1078277 |  218392   44118  2160897    49.0 |  2.376 % |
c |    169506 |  447495  1078277 |  240231   44626  2164575    48.5 |  2.376 % |
c |    170265 |  447495  1078277 |  264254   45385  2225715    49.0 |  2.376 % |
c |    171405 |  447484  1078254 |  290680   46524  2290349    49.2 |  2.378 % |
c |    173114 |  447484  1078254 |  319748   48233  2740940    56.8 |  2.378 % |
c |    175676 |  447484  1078254 |  351723   50795  3385891    66.7 |  2.378 % |
c |    179524 |  447484  1078254 |  386895   54643  4667185    85.4 |  2.378 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 29456 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.91 0.95 0.90 2/54 29452
Raw data (stat): 29452 (runsolver) R 29451 1586 1585 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855280927 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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+9.9996 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 29456
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 29456
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29456
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29456
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0007 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29456
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29456
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0015 s]
Raw data (loadavg): 1.05 0.98 0.91 2/55 29509
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0016 s]
Raw data (loadavg): 1.04 0.98 0.91 2/55 29509
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0012 s]
Raw data (loadavg): 1.04 0.98 0.91 2/55 29509
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.001 s]
Raw data (loadavg): 1.03 0.98 0.91 2/55 29509
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.001 s]
Raw data (loadavg): 1.03 0.98 0.91 2/55 29509
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.002 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 29509
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 29509
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 29509
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.003 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.003 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.003 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.003 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.004 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.004 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.004 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.005 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.006 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29511
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.78 s]
Raw data (loadavg): 1.00 0.98 0.91 1/53 29513
Raw data (stat): 29452 (minisat+_script) S 29451 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855280927 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.78
CPU time (s): 1229.88
CPU user time (s): 1228.99
CPU system time (s): 0.886865
CPU usage (%): 100.008
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####