PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	c8b965306fec2c21edee64824d12f378
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63488
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	230
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 32019

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-27 07:32:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23396 boxname=wulflinc15 idbench=1040 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c8b965306fec2c21edee64824d12f378  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 23396
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        834416 kB
Buffers:         34936 kB
Cached:         143568 kB
SwapCached:        608 kB
Active:          51084 kB
Inactive:       129456 kB
HighTotal:      131008 kB
HighFree:         4844 kB
LowTotal:       903652 kB
LowFree:        829572 kB
SwapTotal:     2097136 kB
SwapFree:      2095624 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            14116 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 07:52:31 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 23396 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> BDD-cost:23440
c ---[   8]---> BDD-cost:28410
c ---[   6]---> BDD-cost:25975
c ---[   4]---> BDD-cost:24801
c ---[   2]---> BDD-cost:25034
c ---[   0]---> BDD-cost:24120
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  436767  1274769 |  145589       0        0     nan |  0.000 % |
c |       101 |  436767  1274769 |  160147     101     7599    75.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 6404096[0m
c ---[   0]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       101 |  441175  1285058 |  147058     101     7599    75.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5898240[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       102 |  441198  1285135 |  147066     102     7622    74.7 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5855232[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       125 |  441212  1285169 |  147070     125     9078    72.6 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5680128[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       139 |  441234  1285220 |  147078     139     9626    69.3 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5663744[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       186 |  441243  1285242 |  147081     186    11744    63.1 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5647360[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       268 |  441251  1285261 |  147083     268    15602    58.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5596160[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       307 |  441266  1285297 |  147088     307    17285    56.3 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5487616[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       382 |  441275  1285321 |  147091     382    20883    54.7 |  0.040 % |
c |       482 |  441275  1285321 |  161800     482    24693    51.2 |  0.044 % |
c |       632 |  441275  1285321 |  177980     632    30326    48.0 |  0.044 % |
c ==============================================================================
c [1mFound solution: 5464064[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       730 |  441287  1285350 |  147095     730    35225    48.3 |  0.044 % |
c |       830 |  441287  1285350 |  161804     830    39533    47.6 |  0.045 % |
c ==============================================================================
c [1mFound solution: 5440512[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       904 |  441297  1285373 |  147099     904    43500    48.1 |  0.045 % |
c ==============================================================================
c [1mFound solution: 5271552[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       978 |  441308  1285399 |  147102     978    46652    47.7 |  0.045 % |
c |      1078 |  441308  1285399 |  161812    1078    50655    47.0 |  0.046 % |
c |      1229 |  441308  1285399 |  177993    1229    57259    46.6 |  0.046 % |
c |      1457 |  441308  1285399 |  195792    1457    68298    46.9 |  0.046 % |
c |      1796 |  441308  1285399 |  215372    1796    83053    46.2 |  0.046 % |
c |      2303 |  441308  1285399 |  236909    2303   106417    46.2 |  0.046 % |
c ==============================================================================
c [1mFound solution: 5121024[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2367 |  441325  1285442 |  147108    2367   109675    46.3 |  0.046 % |
c |      2468 |  441325  1285442 |  161818    2468   113846    46.1 |  0.047 % |
c ==============================================================================
c [1mFound solution: 5060608[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2522 |  441335  1285468 |  147111    2522   116155    46.1 |  0.047 % |
c |      2623 |  441335  1285468 |  161822    2623   119822    45.7 |  0.048 % |
c |      2776 |  441335  1285468 |  178004    2776   131258    47.3 |  0.048 % |
c ==============================================================================
c [1mFound solution: 5022720[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2826 |  441345  1285492 |  147115    2826   133538    47.3 |  0.048 % |
c |      2926 |  441345  1285492 |  161826    2926   137038    46.8 |  0.048 % |
c ==============================================================================
c [1mFound solution: 4892672[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2993 |  441361  1285530 |  147120    2993   140517    46.9 |  0.048 % |
c |      3093 |  441361  1285530 |  161832    3093   144868    46.8 |  0.049 % |
c |      3243 |  441361  1285530 |  178015    3243   151155    46.6 |  0.049 % |
c |      3468 |  441361  1285530 |  195816    3468   162183    46.8 |  0.049 % |
c |      3805 |  441361  1285530 |  215398    3805   177916    46.8 |  0.049 % |
c |      4313 |  441361  1285530 |  236938    4313   203493    47.2 |  0.049 % |
c |      5073 |  441361  1285530 |  260632    5073   238215    47.0 |  0.049 % |
c |      6212 |  441361  1285530 |  286695    6212   290626    46.8 |  0.049 % |
c |      7925 |  441361  1285530 |  315364    7925   373140    47.1 |  0.049 % |
c |     10487 |  441361  1285530 |  346901   10487   502342    47.9 |  0.049 % |
c ==============================================================================
c [1mFound solution: 3130368[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11357 |  441373  1285563 |  147124   11357   548645    48.3 |  0.049 % |
c ==============================================================================
c [1mFound solution: 3030016[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11368 |  441383  1285588 |  147127   11368   548955    48.3 |  0.049 % |
c |     11468 |  441383  1285588 |  161839   11468   553078    48.2 |  0.050 % |
c ==============================================================================
c [1mFound solution: 2987008[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11526 |  441396  1285620 |  147132   11526   555621    48.2 |  0.050 % |
c |     11627 |  441396  1285620 |  161845   11627   559847    48.2 |  0.051 % |
c ==============================================================================
c [1mFound solution: 2855936[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11752 |  441403  1285637 |  147134   11752   565521    48.1 |  0.051 % |
c |     11855 |  441403  1285637 |  161847   11855   569209    48.0 |  0.052 % |
c |     12005 |  441403  1285637 |  178032   12005   578630    48.2 |  0.052 % |
c |     12230 |  441403  1285637 |  195835   12230   588352    48.1 |  0.052 % |
c ==============================================================================
c [1mFound solution: 2851840[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12386 |  441412  1285660 |  147137   12386   595871    48.1 |  0.052 % |
c ==============================================================================
c [1mFound solution: 2816000[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12476 |  441422  1285685 |  147140   12476   599897    48.1 |  0.052 % |
c |     12576 |  441415  1285670 |  161854   12571   604076    48.1 |  0.054 % |
c ==============================================================================
c [1mFound solution: 2775040[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12595 |  441424  1285691 |  147141   12590   604749    48.0 |  0.054 % |
c |     12695 |  441424  1285691 |  161855   12690   608940    48.0 |  0.055 % |
c |     12846 |  441424  1285691 |  178040   12841   616100    48.0 |  0.055 % |
c ==============================================================================
c [1mFound solution: 2662400[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12972 |  441436  1285719 |  147145   12967   622239    48.0 |  0.055 % |
c |     13072 |  441436  1285719 |  161859   13067   626166    47.9 |  0.056 % |
c |     13222 |  441436  1285719 |  178045   13217   633053    47.9 |  0.056 % |
c |     13448 |  441436  1285719 |  195849   13443   643739    47.9 |  0.056 % |
c |     13785 |  441436  1285719 |  215434   13780   659014    47.8 |  0.056 % |
c |     14291 |  441436  1285719 |  236978   14286   680978    47.7 |  0.056 % |
c |     15050 |  441436  1285719 |  260676   15045   715068    47.5 |  0.056 % |
c ==============================================================================
c [1mFound solution: 2650112[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15554 |  441445  1285739 |  147148   15549   738967    47.5 |  0.056 % |
c |     15654 |  441440  1285729 |  161862   15644   742466    47.5 |  0.057 % |
c |     15805 |  441440  1285729 |  178049   15795   748653    47.4 |  0.057 % |
c |     16031 |  441440  1285729 |  195853   16021   759741    47.4 |  0.057 % |
c |     16369 |  441440  1285729 |  215439   16359   777405    47.5 |  0.057 % |
c ==============================================================================
c [1mFound solution: 2510848[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16562 |  441452  1285758 |  147150   16552   785530    47.5 |  0.057 % |
c ==============================================================================
c [1mFound solution: 2456576[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16639 |  441463  1285784 |  147154   16629   788726    47.4 |  0.057 % |
c |     16739 |  441463  1285784 |  161869   16729   792734    47.4 |  0.059 % |
c |     16889 |  441463  1285784 |  178056   16879   799286    47.4 |  0.059 % |
c |     17114 |  441463  1285784 |  195861   17104   809644    47.3 |  0.059 % |
c |     17451 |  441463  1285784 |  215448   17441   825471    47.3 |  0.059 % |
c |     17957 |  441463  1285784 |  236992   17947   850339    47.4 |  0.059 % |
c ==============================================================================
c [1mFound solution: 2454528[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18184 |  441474  1285811 |  147158   18174   861848    47.4 |  0.059 % |
c ==============================================================================
c [1mFound solution: 2437120[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18214 |  441486  1285839 |  147162   18204   863992    47.5 |  0.059 % |
c |     18315 |  441486  1285839 |  161878   18305   867683    47.4 |  0.060 % |
c ==============================================================================
c [1mFound solution: 2432000[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18354 |  441499  1285869 |  147166   18344   869636    47.4 |  0.060 % |
c |     18455 |  441499  1285869 |  161882   18445   873073    47.3 |  0.061 % |
c |     18607 |  441499  1285869 |  178070   18597   884539    47.6 |  0.061 % |
c |     18832 |  441499  1285869 |  195877   18822   898770    47.8 |  0.061 % |
c ==============================================================================
c [1mFound solution: 2405376[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18988 |  441511  1285897 |  147170   18978   904556    47.7 |  0.061 % |
c ==============================================================================
c [1mFound solution: 2371584[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19036 |  441519  1285915 |  147173   19026   906591    47.7 |  0.061 % |
c |     19136 |  441519  1285915 |  161890   19126   910640    47.6 |  0.062 % |
c |     19286 |  441519  1285915 |  178079   19276   917023    47.6 |  0.062 % |
c |     19511 |  441519  1285915 |  195887   19501   926601    47.5 |  0.062 % |
c ==============================================================================
c [1mFound solution: 2337792[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19570 |  441525  1285930 |  147175   19560   929041    47.5 |  0.062 % |
c ==============================================================================
c [1mFound solution: 2190336[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19602 |  441534  1285950 |  147178   19592   930390    47.5 |  0.062 % |
c |     19704 |  441534  1285950 |  161895   19694   934818    47.5 |  0.063 % |
c |     19857 |  441534  1285950 |  178085   19847   941270    47.4 |  0.063 % |
c |     20085 |  441516  1285910 |  195893   20046   949831    47.4 |  0.067 % |
c ==============================================================================
c [1mFound solution: 2168832[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20272 |  441526  1285932 |  147175   20233   956629    47.3 |  0.067 % |
c |     20374 |  441526  1285932 |  161892   20335   960960    47.3 |  0.067 % |
c ==============================================================================
c [1mFound solution: 2154496[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20514 |  441534  1285950 |  147178   20475   967662    47.3 |  0.067 % |
c |     20614 |  441534  1285950 |  161895   20575   972104    47.2 |  0.068 % |
c |     20769 |  441534  1285950 |  178085   20730   978293    47.2 |  0.068 % |
c ==============================================================================
c [1mFound solution: 2117632[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20947 |  441540  1285963 |  147180   20908   986503    47.2 |  0.068 % |
c |     21047 |  441540  1285963 |  161898   21008   990370    47.1 |  0.069 % |
c |     21197 |  441540  1285963 |  178087   21158   997355    47.1 |  0.069 % |
c |     21422 |  441540  1285963 |  195896   21383  1007184    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 2114560[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21696 |  441549  1285983 |  147183   21657  1019168    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 1947648[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21730 |  441557  1286002 |  147185   21691  1020931    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 1937408[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21744 |  441566  1286025 |  147188   21705  1021695    47.1 |  0.069 % |
c |     21844 |  441566  1286025 |  161906   21805  1026027    47.1 |  0.070 % |
c ==============================================================================
c [1mFound solution: 1893376[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21949 |  441574  1286045 |  147191   21910  1029023    47.0 |  0.070 % |
c |     22049 |  441574  1286045 |  161910   22010  1033110    46.9 |  0.071 % |
c |     22199 |  441574  1286045 |  178101   22160  1038508    46.9 |  0.071 % |
c ==============================================================================
c [1mFound solution: 1881088[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22225 |  441578  1286055 |  147192   22186  1039839    46.9 |  0.071 % |
c ==============================================================================
c [1mFound solution: 1748992[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22319 |  441590  1286083 |  147196   22280  1043648    46.8 |  0.071 % |
c |     22419 |  441590  1286083 |  161915   22380  1047923    46.8 |  0.072 % |
c ==============================================================================
c [1mFound solution: 1742848[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22427 |  441602  1286111 |  147200   22388  1048258    46.8 |  0.072 % |
c ==============================================================================
c [1mFound solution: 1703936[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22453 |  441605  1286118 |  147201   22414  1049690    46.8 |  0.072 % |
c |     22555 |  441605  1286118 |  161921   22516  1054292    46.8 |  0.074 % |
c |     22705 |  441605  1286118 |  178113   22666  1061590    46.8 |  0.074 % |
c |     22931 |  441605  1286118 |  195924   22892  1071090    46.8 |  0.074 % |
c |     23268 |  441605  1286118 |  215516   23229  1088121    46.8 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1601536[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23453 |  441608  1286125 |  147202   23414  1096341    46.8 |  0.074 % |
c |     23555 |  441608  1286125 |  161922   23516  1098789    46.7 |  0.074 % |
c |     23705 |  441608  1286125 |  178114   23666  1105702    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1558528[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23717 |  441615  1286145 |  147205   23678  1106109    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1415168[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23734 |  441623  1286164 |  147207   23695  1106742    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1394688[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23797 |  441634  1286190 |  147211   23758  1109356    46.7 |  0.074 % |
c |     23897 |  441627  1286175 |  161932   23853  1112691    46.6 |  0.078 % |
c |     24047 |  441627  1286175 |  178125   24003  1119318    46.6 |  0.078 % |
c |     24272 |  441627  1286175 |  195937   24228  1131072    46.7 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1338368[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24446 |  441634  1286191 |  147211   24402  1138915    46.7 |  0.078 % |
c |     24547 |  441634  1286191 |  161932   24503  1145546    46.8 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1326080[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24682 |  441641  1286207 |  147213   24638  1150434    46.7 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1316864[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24715 |  441649  1286225 |  147216   24671  1151706    46.7 |  0.078 % |
c |     24815 |  441649  1286225 |  161937   24771  1155628    46.7 |  0.080 % |
c ==============================================================================
c [1mFound solution: 1281024[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24842 |  441658  1286247 |  147219   24798  1156594    46.6 |  0.080 % |
c ==============================================================================
c [1mFound solution: 1177600[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24907 |  441665  1286263 |  147221   24863  1159311    46.6 |  0.080 % |
c |     25008 |  441665  1286263 |  161943   24964  1164044    46.6 |  0.081 % |
c |     25158 |  441665  1286263 |  178137   25114  1172031    46.7 |  0.081 % |
c |     25384 |  441665  1286263 |  195951   25340  1181976    46.6 |  0.081 % |
c ==============================================================================
c [1mFound solution: 1070080[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25476 |  441676  1286287 |  147225   25432  1185106    46.6 |  0.081 % |
c ==============================================================================
c [1mFound solution: 1029120[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25551 |  441653  1286224 |  147217   24181  1129685    46.7 |  0.081 % |
c |     25651 |  441632  1286176 |  161938   22327  1030708    46.2 |  0.094 % |
c ==============================================================================
c [1mFound solution: 959488[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25753 |  441638  1286191 |  147212   22429  1033691    46.1 |  0.094 % |
c ==============================================================================
c [1mFound solution: 914432[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25851 |  441645  1286209 |  147215   22527  1037806    46.1 |  0.094 % |
c |     25951 |  441645  1286209 |  161936   22627  1041265    46.0 |  0.095 % |
c |     26102 |  441645  1286209 |  178130   22778  1047328    46.0 |  0.095 % |
c ==============================================================================
c [1mFound solution: 880640[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26239 |  441654  1286230 |  147218   22915  1053422    46.0 |  0.095 % |
c |     26339 |  441573  1286043 |  161939   20824   956529    45.9 |  0.113 % |
c |     26490 |  441573  1286043 |  178133   20975   963244    45.9 |  0.113 % |
c |     26715 |  441573  1286043 |  195947   21200   972484    45.9 |  0.113 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 20215 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.91 2/54 20211
Raw data (stat): 20211 (runsolver) R 20210 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 796156469 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0039 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0037 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0041 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0054 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0062 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.007 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.007 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 0.99 0.98 0.91 1/53 20215
Raw data (stat): 20211 (minisat+_script) S 20210 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796156469 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.7
CPU time (s): 1229.86
CPU user time (s): 1229.38
CPU system time (s): 0.479927
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####