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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-4.opb
MD5SUM	e3892e1941a878802a8ccbbd36201a02
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-27
Optimality of the best value was proved	NO
Number of terms in the objective function	595
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	27842
Number of constraints which are clauses	27842
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5614

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-14 00:55:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4082 boxname=wulflinc6 idbench=322 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e3892e1941a878802a8ccbbd36201a02  /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-4.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-4.opb /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-4.opb
IDLAUNCH: 4082
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        893136 kB
Buffers:         35760 kB
Cached:          83520 kB
SwapCached:       2644 kB
Active:          52868 kB
Inactive:        71920 kB
HighTotal:      131008 kB
HighFree:        43512 kB
LowTotal:       903652 kB
LowFree:        849624 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11140 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:15:44 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 4082 7 1200.37 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27842 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   27842    55684 |    8352       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   27842    55684 |   11136       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.07883 s)
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   56138   122140 |   16841       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19347          
c   -- var.elim.:  2000/19347          
c   -- var.elim.:  3000/19347          
c   -- var.elim.:  4000/19347          
c   -- var.elim.:  5000/19347          
c   -- var.elim.:  6000/19347          
c   -- var.elim.:  7000/19347          
c   -- var.elim.:  8000/19347          
c   -- var.elim.:  9000/19347          
c   -- var.elim.:  10000/19347          
c   -- var.elim.:  11000/19347          
c   -- var.elim.:  12000/19347          
c   -- var.elim.:  13000/19347          
c   -- var.elim.:  14000/19347          
c   -- var.elim.:  15000/19347          
c   -- var.elim.:  16000/19347          
c   -- var.elim.:  17000/19347          
c   -- var.elim.:  18000/19347          
c   -- var.elim.:  19000/19347          
c   -- var.elim.:  19347/19347          
c   -- var.elim.:  1000/9850          
c   -- var.elim.:  2000/9850          
c   -- var.elim.:  3000/9850          
c   -- var.elim.:  4000/9850          
c   -- var.elim.:  5000/9850          
c   -- var.elim.:  6000/9850          
c   -- var.elim.:  7000/9850          
c   -- var.elim.:  8000/9850          
c   -- var.elim.:  9000/9850          
c   -- var.elim.:  9850/9850          
c   -- var.elim.:  85/85          
c   -- var.elim.:  37/37          
c   -- subsuming                       
c   -- var.elim.:  1000/3837          
c   -- var.elim.:  2000/3837          
c   -- var.elim.:  3000/3837          
c   -- var.elim.:  3837/3837          
c   -- var.elim.:  259/259          
c |         0 |   36204   121513 |      --       0       --      -- |     --   | -19929/-612
c |         0 |   36204   121513 |   14481       0        0     nan |  0.000 % |
c |       100 |   36204   121513 |   15929     100    11105   111.0 | 52.803 % |
c |       251 |   36204   121513 |   17522     251    38043   151.6 | 52.802 % |
c |       476 |   36136   120915 |   19238     471    69831   148.3 | 53.118 % |
c |       813 |   36078   120463 |   21128     803   129943   161.8 | 53.414 % |
c |      1319 |   36048   120261 |   23222    1307   197266   150.9 | 53.567 % |
c |      2078 |   36046   120243 |   25543    2062   324725   157.5 | 53.577 % |
c |      3217 |   35981   119681 |   28046    3189   567627   178.0 | 53.903 % |
c ==============================================================================
c (current CPU-time: 43.9683 s)
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4354 |   38859   127504 |   11657    4326   773508   178.8 | 53.903 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6410          
c   -- var.elim.:  2000/6410          
c   -- var.elim.:  3000/6410          
c   -- var.elim.:  4000/6410          
c   -- var.elim.:  5000/6410          
c   -- var.elim.:  6000/6410          
c   -- var.elim.:  6410/6410          
c   -- var.elim.:  1000/2061          
c   -- var.elim.:  2000/2061          
c   -- var.elim.:  2061/2061          
c   -- var.elim.:  4/4          
c |      4354 |   36076   125611 |      --    4326       --      -- |     --   | -2775/-1876
c |      4354 |   36076   125611 |   14430    4326   773508   178.8 | 53.903 % |
c |      4454 |   36014   125079 |   15846    4424   789746   178.5 | 58.140 % |
c |      4604 |   36014   125079 |   17430    4574   812983   177.7 | 58.140 % |
c |      4829 |   36014   125079 |   19173    4799   848071   176.7 | 58.140 % |
c |      5166 |   36014   125079 |   21091    5136   933143   181.7 | 58.140 % |
c |      5672 |   35948   124476 |   23157    5626  1039529   184.8 | 58.436 % |
c |      6432 |   35906   124168 |   25443    6381  1216910   190.7 | 58.602 % |
c |      7571 |   35758   122733 |   27872    7503  1488201   198.3 | 59.212 % |
c |      9280 |   35637   121920 |   30556    9179  1885112   205.4 | 59.684 % |
c |     11843 |   35445   120374 |   33430   11705  2437295   208.2 | 60.516 % |
c ==============================================================================
c (current CPU-time: 66.7599 s)
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11909 |   35551   120702 |   10665   11771  2441797   207.4 | 60.516 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4284          
c   -- var.elim.:  2000/4284          
c   -- var.elim.:  3000/4284          
c   -- var.elim.:  4000/4284          
c   -- var.elim.:  4284/4284          
c   -- var.elim.:  319/319          
c |     11909 |   35429   119901 |      --   11771       --      -- |     --   | -110/-542
c |     11909 |   35429   119901 |   14171    9866  1201036   121.7 | 60.516 % |
c |     12009 |   35429   119901 |   15588    9966  1220359   122.5 | 60.637 % |
c |     12159 |   35429   119901 |   17147   10116  1245107   123.1 | 60.636 % |
c |     12386 |   35399   119646 |   18846   10332  1282260   124.1 | 60.775 % |
c |     12723 |   35399   119646 |   20731   10669  1361660   127.6 | 60.775 % |
c |     13229 |   35368   119424 |   22784   11072  1456322   131.5 | 60.914 % |
c |     13988 |   35219   118186 |   24957   11805  1615127   136.8 | 61.598 % |
c |     15127 |   35181   117818 |   27423   12936  1936030   149.7 | 61.774 % |
c |     16835 |   35003   116244 |   30012   14603  2344044   160.5 | 62.579 % |
c |     19397 |   34703   113556 |   32731   17114  3018479   176.4 | 63.948 % |
c |     23241 |   34621   112788 |   35919   20902  4152111   198.6 | 64.317 % |
c |     29007 |   34203   108993 |   39034   26528  5847459   220.4 | 66.241 % |
c ==============================================================================
c (current CPU-time: 118.698 s)
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     29143 |   34432   109636 |   10329   26664  5888140   220.8 | 66.241 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3370          
c   -- var.elim.:  2000/3370          
c   -- var.elim.:  3000/3370          
c   -- var.elim.:  3370/3370          
c   -- var.elim.:  227/227          
c |     29143 |   34252   109221 |      --   26664       --      -- |     --   | -180/-414
c |     29143 |   34252   109221 |   13700   26183  5728293   218.8 | 66.241 % |
c |     29243 |   34190   108712 |   15043   15306  3227646   210.9 | 66.559 % |
c |     29393 |   34190   108712 |   16547   15456  3252692   210.4 | 66.560 % |
c |     29618 |   34164   108484 |   18188   15670  3301693   210.7 | 66.670 % |
c |     29955 |   34162   108463 |   20006   16003  3380013   211.2 | 66.679 % |
c |     30461 |   34100   107934 |   21967   16496  3467426   210.2 | 66.965 % |
c |     31220 |   34076   107733 |   24147   17248  3669107   212.7 | 67.076 % |
c |     32359 |   34033   107466 |   26528   18382  4018138   218.6 | 67.260 % |
c |     34067 |   33997   107191 |   29150   20085  4449496   221.5 | 67.426 % |
c |     36629 |   33728   104936 |   31811   22534  5151079   228.6 | 68.661 % |
c |     40473 |   33555   103320 |   34813   26333  6207552   235.7 | 69.426 % |
c |     46239 |   33460   102443 |   38186   32063  7898211   246.3 | 69.859 % |
c |     54888 |   33406   101902 |   41936   40700 10382271   255.1 | 70.108 % |
c ==============================================================================
c (current CPU-time: 258.208 s)
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     66552 |   33135    98883 |    9940   20698  4150539   200.5 | 70.108 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3094          
c   -- var.elim.:  2000/3094          
c   -- var.elim.:  3000/3094          
c   -- var.elim.:  3094/3094          
c   -- var.elim.:  230/230          
c   -- var.elim.:  5/5          
c |     66552 |   33022    96561 |      --   20698       --      -- |     --   | -90/-303
c |     66552 |   33022    96561 |   13208   16191  1459480    90.1 | 70.108 % |
c |     66652 |   32990    96265 |   14515   16290  1469036    90.2 | 72.000 % |
c |     66802 |   32990    96265 |   15967   16440  1511440    91.9 | 72.000 % |
c |     67027 |   32990    96265 |   17563   16665  1553519    93.2 | 72.000 % |
c |     67364 |   32990    96265 |   19320   17002  1617358    95.1 | 72.000 % |
c |     67870 |   32990    96265 |   21252   17508  1745478    99.7 | 72.000 % |
c |     68630 |   32990    96265 |   23377   18268  1905302   104.3 | 72.000 % |
c |     69771 |   32990    96265 |   25715   19409  2217793   114.3 | 72.001 % |
c |     71479 |   32931    95761 |   28236   21103  2644011   125.3 | 72.268 % |
c |     74042 |   32931    95761 |   31059   23666  3312257   140.0 | 72.268 % |
c |     77886 |   32931    95761 |   34165   27510  4452456   161.8 | 72.268 % |
c |     83653 |   32931    95761 |   37582   33277  6107331   183.5 | 72.267 % |
c |     92302 |   32775    94439 |   41144   41892  8506948   203.1 | 72.950 % |
c |    105276 |   32669    93588 |   45112   23339  4786051   205.1 | 73.438 % |
c ==============================================================================
c (current CPU-time: 438.748 s)
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    123935 |   34915    98548 |   10474   41958  9975199   237.7 | 73.438 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4553          
c   -- var.elim.:  2000/4553          
c   -- var.elim.:  3000/4553          
c   -- var.elim.:  4000/4553          
c   -- var.elim.:  4553/4553          
c   -- var.elim.:  1000/1533          
c   -- var.elim.:  1533/1533          
c |    123935 |   32587    95618 |      --   41958       --      -- |     --   | -2321/-2915
c |    123935 |   32587    95618 |   13034   41958  9975199   237.7 | 73.438 % |
c |    124035 |   32587    95618 |   14338   18463  3544937   192.0 | 80.308 % |
c |    124185 |   32561    95378 |   15759   18609  3559296   191.3 | 80.398 % |
c |    124411 |   32561    95378 |   17335   18835  3602053   191.2 | 80.398 % |
c |    124749 |   32559    95357 |   19067   19170  3715947   193.8 | 80.405 % |
c |    125255 |   32559    95357 |   20974   19676  3807968   193.5 | 80.405 % |
c |    126014 |   32533    95098 |   23053   20431  3964797   194.1 | 80.496 % |
c |    127153 |   32501    94845 |   25334   21562  4233993   196.4 | 80.593 % |
c |    128862 |   32459    94479 |   27831   23262  4595586   197.6 | 80.739 % |
c |    131425 |   32437    94310 |   30593   25802  5309387   205.8 | 80.816 % |
c |    135269 |   32100    91479 |   33303   29523  6097468   206.5 | 81.937 % |
c |    141035 |   31858    89251 |   36357   35094  7538736   214.8 | 82.723 % |
c |    149684 |   31612    87239 |   39684   43605  9636249   221.0 | 83.489 % |
c |    162658 |   31296    84776 |   43216   23455  4421942   188.5 | 84.443 % |
c |    182119 |   31081    82875 |   47212   42843  9202365   214.8 | 85.166 % |
c |    211311 |   30797    80361 |   51458   29700  6117782   206.0 | 86.134 % |
c |    255100 |   30691    79402 |   56409   27315  5704563   208.8 | 86.503 % |
c |    320784 |   30516    77858 |   61696   40031  9233583   230.7 | 87.095 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 C582 -C581 -C580 -C579 -C578 C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 C375 -C374 -C373 -C372 -C371 -C370 -C369 C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240#### 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.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (runsolver) R 1247 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422214026 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 3648 0 0 0 985 14 0 0 25 0 1 0 422214026 17821696 3626 4294967295 134512640 134672761 3221224560 3221222992 134604645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4351 3626 603 41 0 4310 0
vsize: 17404
[startup+20.0023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 3664 0 0 0 1985 14 0 0 25 0 1 0 422214026 17965056 3642 4294967295 134512640 134672761 3221224560 3221222636 134566531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4386 3642 603 41 0 4345 0
vsize: 17544
[startup+30.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 3694 0 0 0 2985 14 0 0 25 0 1 0 422214026 18161664 3672 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4434 3672 603 41 0 4393 0
vsize: 17736
[startup+40.0031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 3841 0 0 0 3984 14 0 0 25 0 1 0 422214026 18161664 3709 4294967295 134512640 134672761 3221224560 3221223728 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4434 3709 603 41 0 4393 0
vsize: 17736
[startup+50.0047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 5193 0 0 0 4971 28 0 0 25 0 1 0 422214026 22220800 4702 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5425 4702 603 41 0 5384 0
vsize: 21700
[startup+60.0054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 5910 0 0 0 5969 30 0 0 25 0 1 0 422214026 24961024 5419 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6094 5419 603 41 0 6053 0
vsize: 24376
[startup+70.0065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 7330 0 0 0 6963 37 0 0 25 0 1 0 422214026 29233152 6452 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7137 6452 603 41 0 7096 0
vsize: 28548
[startup+80.0082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 7331 0 0 0 7963 37 0 0 25 0 1 0 422214026 29233152 6453 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7137 6453 603 41 0 7096 0
vsize: 28548
[startup+90.0089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 7561 0 0 0 8963 37 0 0 25 0 1 0 422214026 30101504 6683 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7349 6683 603 41 0 7308 0
vsize: 29396
[startup+100.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 8795 0 0 0 9960 41 0 0 25 0 1 0 422214026 35188736 7917 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8591 7917 603 41 0 8550 0
vsize: 34364
[startup+110.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 9548 0 0 0 10958 43 0 0 25 0 1 0 422214026 38178816 8670 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9321 8670 603 41 0 9280 0
vsize: 37284
[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11270 0 0 0 11950 50 0 0 25 0 1 0 422214026 43859968 10003 4294967295 134512640 134672761 3221224560 3221223104 134621164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10708 10003 603 41 0 10667 0
vsize: 42832
[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11270 0 0 0 12950 51 0 0 25 0 1 0 422214026 43859968 10003 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10708 10003 603 41 0 10667 0
vsize: 42832
[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11271 0 0 0 13950 51 0 0 25 0 1 0 422214026 43859968 10004 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10708 10004 603 41 0 10667 0
vsize: 42832
[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11271 0 0 0 14950 51 0 0 25 0 1 0 422214026 43859968 10004 4294967295 134512640 134672761 3221224560 3221223704 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10708 10004 603 41 0 10667 0
vsize: 42832
[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11439 0 0 0 15950 52 0 0 25 0 1 0 422214026 44380160 10172 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10835 10172 603 41 0 10794 0
vsize: 43340
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 12371 0 0 0 16947 55 0 0 25 0 1 0 422214026 48185344 11104 4294967295 134512640 134672761 3221224560 3221223600 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11764 11104 603 41 0 11723 0
vsize: 47056
[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 13233 0 0 0 17944 58 0 0 25 0 1 0 422214026 51826688 11966 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12653 11966 603 41 0 12612 0
vsize: 50612
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 14041 0 0 0 18942 60 0 0 25 0 1 0 422214026 55078912 12774 4294967295 134512640 134672761 3221224560 3221223744 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13447 12774 603 41 0 13406 0
vsize: 53788
[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 15041 0 0 0 19938 64 0 0 25 0 1 0 422214026 59129856 13774 4294967295 134512640 134672761 3221224560 3221223600 134614141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14436 13774 603 41 0 14395 0
vsize: 57744
[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 15848 0 0 0 20936 66 0 0 25 0 1 0 422214026 62521344 14581 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15264 14581 603 41 0 15223 0
vsize: 61056
[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 16409 0 0 0 21935 67 0 0 25 0 1 0 422214026 64704512 15142 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15797 15142 603 41 0 15756 0
vsize: 63188
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 16890 0 0 0 22934 68 0 0 25 0 1 0 422214026 66678784 15623 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16279 15623 603 41 0 16238 0
vsize: 65116
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 17592 0 0 0 23932 71 0 0 25 0 1 0 422214026 69533696 16325 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16976 16325 603 41 0 16935 0
vsize: 67904
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 18289 0 0 0 24929 73 0 0 25 0 1 0 422214026 72413184 17022 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17679 17022 603 41 0 17638 0
vsize: 70716
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1248
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 25924 79 0 0 25 0 1 0 422214026 74280960 17479 4294967295 134512640 134672761 3221224560 3221223104 134621122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18135 17479 603 41 0 18094 0
vsize: 72540
[startup+270.014 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 1304
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 26916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17369 603 41 0 17974 0
vsize: 72060
[startup+280.014 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1304
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 27916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223600 134612827 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17369 603 41 0 17974 0
vsize: 72060
[startup+290.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1304
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 28916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17369 603 41 0 17974 0
vsize: 72060
[startup+300.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1304
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 29916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17369 603 41 0 17974 0
vsize: 72060
[startup+310.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1304
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 30916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17369 603 41 0 17974 0
vsize: 72060
[startup+320.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1304
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 31917 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+330.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1304
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 32917 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+340.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 33917 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+350.013 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 34918 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+360.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 35918 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+370.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 36918 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+380.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 37919 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+390.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 38919 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+400.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 39919 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+410.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 40920 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+420.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 41920 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+430.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 42920 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18015 17370 603 41 0 17974 0
vsize: 72060
[startup+440.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20084 0 0 0 43916 91 0 0 25 0 1 0 422214026 74739712 17608 4294967295 134512640 134672761 3221224560 3221223052 134642759 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18247 17608 603 41 0 18206 0
vsize: 72988
[startup+450.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 44911 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223600 134614261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17498 603 41 0 18006 0
vsize: 72188
[startup+460.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 45911 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223712 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17498 603 41 0 18006 0
vsize: 72188
[startup+470.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 46911 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18047 17498 603 41 0 18006 0
vsize: 72188
[startup+480.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 47911 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17498 603 41 0 18006 0
vsize: 72188
[startup+490.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 48912 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17498 603 41 0 18006 0
vsize: 72188
[startup+500.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 49912 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17499 603 41 0 18006 0
vsize: 72188
[startup+510.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 50912 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17499 603 41 0 18006 0
vsize: 72188
[startup+520.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 51913 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17499 603 41 0 18006 0
vsize: 72188
[startup+530.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 52913 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17499 603 41 0 18006 0
vsize: 72188
[startup+540.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 53913 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17499 603 41 0 18006 0
vsize: 72188
[startup+550.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 54913 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17499 603 41 0 18006 0
vsize: 72188
[startup+560.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 55914 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17499 603 41 0 18006 0
vsize: 72188
[startup+570.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1306
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 56914 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223600 134613748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+580.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 57914 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+590.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 58915 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+600.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 59915 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+610.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 60915 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+620.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 61916 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+630.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 62916 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+640.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 63916 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+650.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 64917 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+660.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 65917 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+670.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 66917 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+680.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 67917 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223408 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17500 603 41 0 18006 0
vsize: 72188
[startup+690.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20180 0 0 0 68918 96 0 0 25 0 1 0 422214026 73920512 17502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17502 603 41 0 18006 0
vsize: 72188
[startup+700.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20182 0 0 0 69918 96 0 0 25 0 1 0 422214026 73920512 17504 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17504 603 41 0 18006 0
vsize: 72188
[startup+710.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20391 0 0 0 70918 97 0 0 25 0 1 0 422214026 74846208 17713 4294967295 134512640 134672761 3221224560 3221223744 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18273 17713 603 41 0 18232 0
vsize: 73092
[startup+720.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21012 0 0 0 71916 99 0 0 25 0 1 0 422214026 77328384 18334 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18879 18334 603 41 0 18838 0
vsize: 75516
[startup+730.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21331 0 0 0 72916 100 0 0 25 0 1 0 422214026 78344192 18593 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18593 603 41 0 19086 0
vsize: 76508
[startup+740.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21331 0 0 0 73916 100 0 0 25 0 1 0 422214026 78344192 18593 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18593 603 41 0 19086 0
vsize: 76508
[startup+750.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21331 0 0 0 74917 100 0 0 25 0 1 0 422214026 78344192 18593 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18593 603 41 0 19086 0
vsize: 76508
[startup+760.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 75917 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+770.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 76917 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+780.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 77917 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+790.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 78918 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+800.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 79918 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+810.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 80918 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+820.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 81919 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+830.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 82919 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+840.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 83920 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+850.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 84920 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+860.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 85920 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+870.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 86921 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 18594 603 41 0 19086 0
vsize: 76508
[startup+880.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21567 0 0 0 87921 100 0 0 25 0 1 0 422214026 79392768 18829 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19383 18829 603 41 0 19342 0
vsize: 77532
[startup+890.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21986 0 0 0 88920 101 0 0 25 0 1 0 422214026 81108992 19248 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19802 19248 603 41 0 19761 0
vsize: 79208
[startup+900.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 89919 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+910.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 90919 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134616042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+920.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 91919 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+930.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 92920 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+940.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 93920 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223708 134614482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+950.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 94920 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+960.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 95921 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+970.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 96921 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+980.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 97921 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+990.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 98922 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19744 603 41 0 20237 0
vsize: 81112
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 99922 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19745 603 41 0 20237 0
vsize: 81112
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 100922 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19745 603 41 0 20237 0
vsize: 81112
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 101923 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19745 603 41 0 20237 0
vsize: 81112
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 102923 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19745 603 41 0 20237 0
vsize: 81112
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 103923 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20278 19745 603 41 0 20237 0
vsize: 81112
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22547 0 0 0 104924 102 0 0 25 0 1 0 422214026 83193856 19746 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20311 19746 603 41 0 20270 0
vsize: 81244
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 23164 0 0 0 105922 104 0 0 25 0 1 0 422214026 85684224 20363 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20919 20363 603 41 0 20878 0
vsize: 83676
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 23727 0 0 0 106921 106 0 0 25 0 1 0 422214026 88178688 20926 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21528 20926 603 41 0 21487 0
vsize: 86112
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24285 0 0 0 107920 107 0 0 25 0 1 0 422214026 90546176 21484 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22106 21484 603 41 0 22065 0
vsize: 88424
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 108919 108 0 0 25 0 1 0 422214026 92917760 22029 4294967295 134512640 134672761 3221224560 3221223656 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22685 22029 603 41 0 22644 0
vsize: 90740
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 109919 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 110920 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 111920 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 112920 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 113921 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 114921 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 115921 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 116922 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 117922 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 118922 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1308
Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 119923 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22557 21960 603 41 0 22516 0
vsize: 90228
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 1308
Raw data (stat): 1248 (minisat+) Z 1247 29653 29652 0 -1 12 24863 0 0 0 119923 113 0 0 25 0 1 0 422214026 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.37
CPU user time (s): 1199.23
CPU system time (s): 1.13783
CPU usage (%): 100.026
Max. virtual memory (Kb): 90740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####