PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-sentoy.opb
MD5SUM	4df3e7eb358d27d446e34b975724a6c1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-7772
Optimality of the best value was proved	NO
Number of terms in the objective function	60
Biggest coefficient in the objective function	974
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	9460
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	6000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	26162
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	60
Total number of constraints	90
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	30
Minimum length of a constraint	1
Maximum length of a constraint	60
Trace number 32306

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-05-27 09:00:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23684 boxname=wulflinc2 idbench=1328 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-sentoy.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-sentoy.opb
IDLAUNCH: 23684
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        830804 kB
Buffers:         28964 kB
Cached:         154896 kB
SwapCached:        556 kB
Active:          24120 kB
Inactive:       162032 kB
HighTotal:      131008 kB
HighFree:         3304 kB
LowTotal:       903652 kB
LowFree:        827500 kB
SwapTotal:     2097136 kB
SwapFree:      2095840 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5592 kB
Slab:            12048 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 09:21:28 (client local time) WITH STATUS 152 IN 1230.14 SECONDS
stats: 23684 7 1230.14 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  29]---> BDD-cost:72336
c ---[  28]---> BDD-cost:37152
c ---[  27]---> BDD-cost:65344
c ---[  26]---> BDD-cost:70690
c ---[  25]---> BDD-cost:61701
c ---[  24]---> BDD-cost:69736
c ---[  23]---> BDD-cost:70681
c ---[  22]---> BDD-cost:60569
c ---[  21]---> BDD-cost:59590
c ---[  20]---> BDD-cost:68898
c ---[  19]---> BDD-cost:51292
c ---[  18]---> BDD-cost:68218
c ---[  17]---> BDD-cost:44969
c ---[  16]---> BDD-cost:66420
c ---[  15]---> BDD-cost:66330
c ---[  14]---> BDD-cost:57913
c ---[  13]---> BDD-cost:62873
c ---[  12]---> BDD-cost:56928
c ---[  11]---> BDD-cost:71330
c ---[  10]---> BDD-cost:72214
c ---[   9]---> BDD-cost:59705
c ---[   8]---> BDD-cost:66833
c ---[   7]---> BDD-cost:69775
c ---[   6]---> BDD-cost:33741
c ---[   5]---> BDD-cost:61412
c ---[   4]---> BDD-cost:55558
c ---[   3]---> BDD-cost:67780
c ---[   2]---> BDD-cost:57716
c ---[   1]---> BDD-cost:60300
c ---[   0]---> BDD-cost:58322
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 5120745 15004487 | 1706915       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -74[0m
c ---[   0]---> Sorter-cost: 4579     Base: 3 5 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 5126230 15017358 | 1708743       0        0     nan |  0.000 % |
c |       101 | 5126230 15017358 | 1879617     101     2767    27.4 |  0.002 % |
c ==============================================================================
c [1mFound solution: -2115[0m
c ---[   0]---> Sorter-cost: 6379     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       109 | 5142900 15056363 | 1714300     109     2842    26.1 |  0.002 % |
c ==============================================================================
c [1mFound solution: -2148[0m
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       110 | 5143019 15056682 | 1714339     110     2994    27.2 |  0.002 % |
c ==============================================================================
c [1mFound solution: -2167[0m
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       115 | 5143186 15057132 | 1714395     115     3310    28.8 |  0.002 % |
c ==============================================================================
c [1mFound solution: -2223[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       116 | 5143272 15057360 | 1714424     116     3332    28.7 |  0.002 % |
c ==============================================================================
c [1mFound solution: -4014[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       164 | 5143329 15057503 | 1714443     164     5234    31.9 |  0.002 % |
c ==============================================================================
c [1mFound solution: -4018[0m
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       245 | 5143340 15057543 | 1714446     245    10867    44.4 |  0.002 % |
c ==============================================================================
c [1mFound solution: -4303[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       246 | 5143370 15057624 | 1714456     246    10881    44.2 |  0.002 % |
c ==============================================================================
c [1mFound solution: -4314[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       248 | 5143377 15057647 | 1714459     248    11251    45.4 |  0.002 % |
c ==============================================================================
c [1mFound solution: -4476[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       249 | 5143454 15057851 | 1714484     249    11297    45.4 |  0.002 % |
c ==============================================================================
c [1mFound solution: -4498[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       251 | 5143464 15057887 | 1714488     251    11645    46.4 |  0.002 % |
c ==============================================================================
c [1mFound solution: -4799[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       255 | 5143484 15057940 | 1714494     255    12355    48.5 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5339[0m
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       261 | 5143509 15058007 | 1714503     261    12475    47.8 |  0.002 % |
c |       361 | 5143509 15058007 | 1885953     361    19045    52.8 |  0.002 % |
c |       511 | 5143509 15058007 | 2074548     511    25704    50.3 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5739[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       711 | 5143535 15058072 | 1714511     711    31763    44.7 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5742[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       720 | 5143544 15058096 | 1714514     720    32506    45.1 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5748[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       721 | 5143553 15058117 | 1714517     721    32518    45.1 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5753[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       724 | 5143562 15058138 | 1714520     724    32925    45.5 |  0.002 % |
c |       824 | 5143562 15058138 | 1885972     824    38956    47.3 |  0.003 % |
c |       976 | 5143562 15058138 | 2074569     976    42516    43.6 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6174[0m
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1150 | 5143570 15058158 | 1714523    1150    46885    40.8 |  0.003 % |
c |      1251 | 5143570 15058158 | 1885975    1251    49317    39.4 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6182[0m
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1278 | 5143580 15058181 | 1714526    1278    50102    39.2 |  0.003 % |
c |      1378 | 5143580 15058181 | 1885978    1378    53005    38.5 |  0.003 % |
c |      1529 | 5143580 15058181 | 2074576    1529    56946    37.2 |  0.003 % |
c |      1756 | 5143580 15058181 | 2282034    1756    65379    37.2 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6198[0m
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1783 | 5143586 15058194 | 1714528    1783    66361    37.2 |  0.003 % |
c |      1889 | 5143586 15058194 | 1885980    1889    69160    36.6 |  0.003 % |
c |      2040 | 5143586 15058194 | 2074578    2040    75368    36.9 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6456[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2175 | 5143613 15058263 | 1714537    2175    82741    38.0 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6468[0m
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2217 | 5143617 15058277 | 1714539    2217    85055    38.4 |  0.003 % |
c |      2318 | 5143617 15058277 | 1885992    2318    88469    38.2 |  0.003 % |
c |      2468 | 5143617 15058277 | 2074592    2468    92790    37.6 |  0.003 % |
c |      2693 | 5143617 15058277 | 2282051    2693   102057    37.9 |  0.003 % |
c |      3030 | 5143617 15058277 | 2510256    3030   117955    38.9 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6540[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3096 | 5143627 15058304 | 1714542    3096   120680    39.0 |  0.003 % |
c |      3196 | 5143627 15058304 | 1885996    3196   126137    39.5 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6569[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3238 | 5143633 15058318 | 1714544    3238   128108    39.6 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6629[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3244 | 5143641 15058337 | 1714547    3244   128712    39.7 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6683[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3337 | 5143649 15058355 | 1714549    3337   133758    40.1 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6803[0m
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3404 | 5143664 15058394 | 1714554    3404   136067    40.0 |  0.003 % |
c |      3507 | 5143664 15058394 | 1886009    3507   140200    40.0 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6989[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3547 | 5143672 15058415 | 1714557    3547   141592    39.9 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6993[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3577 | 5143680 15058434 | 1714560    3577   142953    40.0 |  0.003 % |
c |      3677 | 5143680 15058434 | 1886016    3677   147101    40.0 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7017[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3789 | 5143685 15058445 | 1714561    3789   151268    39.9 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7018[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3794 | 5143690 15058456 | 1714563    3794   151798    40.0 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7024[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3823 | 5143697 15058475 | 1714565    3823   153501    40.2 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7073[0m
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3848 | 5143700 15058482 | 1714566    3848   154397    40.1 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7080[0m
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3854 | 5143703 15058489 | 1714567    3854   154517    40.1 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7083[0m
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3861 | 5143706 15058496 | 1714568    3861   155514    40.3 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7084[0m
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3869 | 5143715 15058518 | 1714571    3869   155912    40.3 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7122[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3873 | 5143721 15058532 | 1714573    3873   156187    40.3 |  0.003 % |
c |      3974 | 5143721 15058532 | 1886030    3974   161884    40.7 |  0.004 % |
c |      4125 | 5143721 15058532 | 2074633    4125   166558    40.4 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7136[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4140 | 5143728 15058549 | 1714576    4140   167891    40.6 |  0.004 % |
c |      4240 | 5143728 15058549 | 1886033    4240   171154    40.4 |  0.004 % |
c |      4390 | 5143728 15058549 | 2074636    4390   176368    40.2 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7289[0m
c ---[   0]---> Sorter-cost:    1     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4553 | 5143742 15058585 | 1714580    4553   184434    40.5 |  0.004 % |
c |      4653 | 5143742 15058585 | 1886038    4653   187269    40.2 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7296[0m
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4759 | 5143747 15058601 | 1714582    4759   190059    39.9 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7345[0m
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4770 | 5143754 15058618 | 1714584    4770   191193    40.1 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7351[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4780 | 5143761 15058636 | 1714587    4780   191588    40.1 |  0.004 % |
c |      4881 | 5143761 15058636 | 1886045    4881   194680    39.9 |  0.004 % |
c |      5032 | 5143761 15058636 | 2074650    5032   200411    39.8 |  0.004 % |
c |      5259 | 5143761 15058636 | 2282115    5259   208312    39.6 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7367[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5376 | 5143767 15058650 | 1714589    5376   214197    39.8 |  0.004 % |
c |      5476 | 5143767 15058650 | 1886047    5476   217837    39.8 |  0.004 % |
c |      5626 | 5143767 15058650 | 2074652    5626   226727    40.3 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7377[0m
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5813 | 5143776 15058671 | 1714592    5813   235166    40.5 |  0.004 % |
c |      5913 | 5143776 15058671 | 1886051    5913   241541    40.8 |  0.004 % |
c |      6063 | 5143776 15058671 | 2074656    6063   247268    40.8 |  0.004 % |
c |      6289 | 5143776 15058671 | 2282121    6289   254345    40.4 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7500[0m
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6310 | 5143782 15058685 | 1714594    6310   254903    40.4 |  0.004 % |
c |      6412 | 5143782 15058685 | 1886053    6412   260396    40.6 |  0.004 % |
c |      6562 | 5143782 15058685 | 2074658    6562   268270    40.9 |  0.004 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 28228 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.94 0.97 0.91 2/54 28224
Raw data (stat): 28224 (runsolver) R 28223 31399 31398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 796699666 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.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 28228
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.95 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.0017 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.0019 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.0025 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.0018 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.0035 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.007 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.007 s]
Raw data (loadavg): 1.14 1.00 0.92 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.008 s]
Raw data (loadavg): 1.11 1.00 0.92 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.007 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.008 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.008 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 28230
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.009 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.009 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.009 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.01 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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): 1.02 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.024 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.024 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.025 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.145 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.153 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.157 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.157 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.158 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.157 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.157 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.157 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.161 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.161 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.161 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.162 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.162 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.162 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.162 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.161 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.167 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.168 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.167 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.167 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.168 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.168 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.168 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.168 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.17 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.18 s]
Raw data (loadavg): 1.00 1.00 0.92 3/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.18 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.18 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.18 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.18 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.18 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.19 s]
Raw data (loadavg): 1.00 1.00 0.92 3/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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.2 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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+1230.03 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 28232
Raw data (stat): 28224 (minisat+_script) S 28223 31399 31398 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796699666 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): 1230.03
CPU time (s): 1230.14
CPU user time (s): 1226.05
CPU system time (s): 4.09138
CPU usage (%): 100.009
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####