PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare2.opb
MD5SUM	c00b2eef1eabd5880b83093b756a5dd4
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	429056
Optimality of the best value was proved	NO
Number of terms in the objective function	210
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	7516192761
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	7516192761
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	1201.34
Number of variables	270
Total number of constraints	67
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	7
Minimum length of a constraint	1
Maximum length of a constraint	90
Trace number 31943

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-05-27 07:02:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23330 boxname=wulflinc3 idbench=974 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c00b2eef1eabd5880b83093b756a5dd4  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare2.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare2.opb
IDLAUNCH: 23330
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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		: 451.190
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:        808156 kB
Buffers:         33224 kB
Cached:         173620 kB
SwapCached:         12 kB
Active:          65480 kB
Inactive:       144052 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        807876 kB
SwapTotal:     2097136 kB
SwapFree:      2096788 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6580 kB
Slab:            11264 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 07:23:28 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23330 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> BDD-cost:33300
c ---[  10]---> BDD-cost:39181
c ---[   8]---> BDD-cost:34989
c ---[   6]---> BDD-cost:41590
c ---[   4]---> BDD-cost:41670
c ---[   2]---> BDD-cost:41238
c ---[   0]---> BDD-cost:35327
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  774421  2270408 |  258140       0        0     nan |  0.000 % |
c |       100 |  774421  2270408 |  283954     100    10529   105.3 |  0.026 % |
c ==============================================================================
c [1mFound solution: 8321024[0m
c ---[   0]---> Sorter-cost: 2158     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 |  779941  2283300 |  259980     101    10563   104.6 |  0.026 % |
c ==============================================================================
c [1mFound solution: 8070144[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 |       103 |  779972  2283416 |  259990     103    10593   102.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7919616[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 |       103 |  779984  2283446 |  259994     103    10593   102.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7883776[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 |       103 |  779998  2283478 |  259999     103    10593   102.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7766016[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 |       195 |  780011  2283508 |  260003     195    17056    87.5 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7600128[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 |       195 |  780017  2283523 |  260005     195    17056    87.5 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7581696[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 |       210 |  780028  2283551 |  260009     210    17898    85.2 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7541760[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 |       289 |  780041  2283581 |  260013     289    22921    79.3 |  0.026 % |
c |       389 |  780041  2283581 |  286014     389    28159    72.4 |  0.029 % |
c |       542 |  780041  2283581 |  314615     542    36432    67.2 |  0.029 % |
c ==============================================================================
c [1mFound solution: 7353344[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 |       611 |  780051  2283603 |  260017     611    40926    67.0 |  0.029 % |
c |       711 |  780051  2283603 |  286018     711    45549    64.1 |  0.029 % |
c |       861 |  780051  2283603 |  314620     861    53044    61.6 |  0.029 % |
c |      1088 |  780051  2283603 |  346082    1088    68036    62.5 |  0.029 % |
c |      1425 |  780051  2283603 |  380690    1425    89057    62.5 |  0.029 % |
c ==============================================================================
c [1mFound solution: 7134208[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 |      1552 |  780074  2283662 |  260024    1552    96231    62.0 |  0.029 % |
c ==============================================================================
c [1mFound solution: 7091200[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 |      1588 |  780084  2283688 |  260028    1588    98169    61.8 |  0.029 % |
c ==============================================================================
c [1mFound solution: 6865920[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 |      1629 |  780095  2283714 |  260031    1629   100375    61.6 |  0.029 % |
c |      1730 |  780095  2283714 |  286034    1730   105382    60.9 |  0.030 % |
c ==============================================================================
c [1mFound solution: 6863872[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 |      1870 |  780107  2283742 |  260035    1870   113202    60.5 |  0.030 % |
c |      1970 |  780107  2283742 |  286038    1970   117506    59.6 |  0.031 % |
c |      2120 |  780107  2283742 |  314642    2120   124851    58.9 |  0.031 % |
c ==============================================================================
c [1mFound solution: 6833152[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 |      2280 |  780117  2283765 |  260039    2280   133876    58.7 |  0.031 % |
c |      2380 |  780117  2283765 |  286042    2380   138500    58.2 |  0.031 % |
c |      2530 |  780117  2283765 |  314647    2530   147991    58.5 |  0.031 % |
c |      2755 |  780117  2283765 |  346111    2755   162068    58.8 |  0.031 % |
c ==============================================================================
c [1mFound solution: 6819840[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 |      3070 |  780129  2283792 |  260043    3070   178746    58.2 |  0.031 % |
c ==============================================================================
c [1mFound solution: 6724608[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 |      3123 |  780139  2283816 |  260046    3123   181367    58.1 |  0.031 % |
c |      3223 |  780139  2283816 |  286050    3223   188180    58.4 |  0.032 % |
c |      3374 |  780139  2283816 |  314655    3374   196412    58.2 |  0.032 % |
c ==============================================================================
c [1mFound solution: 6516736[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 |      3454 |  780148  2283838 |  260049    3454   201541    58.4 |  0.032 % |
c ==============================================================================
c [1mFound solution: 6364160[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 |      3517 |  780157  2283858 |  260052    3517   205162    58.3 |  0.032 % |
c |      3618 |  780157  2283858 |  286057    3618   211177    58.4 |  0.033 % |
c |      3769 |  780157  2283858 |  314662    3769   217893    57.8 |  0.033 % |
c |      3994 |  780157  2283858 |  346129    3994   227695    57.0 |  0.033 % |
c ==============================================================================
c [1mFound solution: 6243328[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 |      4031 |  780166  2283883 |  260055    4031   229780    57.0 |  0.033 % |
c |      4131 |  780166  2283883 |  286060    4131   234574    56.8 |  0.033 % |
c |      4285 |  780166  2283883 |  314666    4285   242550    56.6 |  0.033 % |
c ==============================================================================
c [1mFound solution: 5986304[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 |      4421 |  780176  2283908 |  260058    4421   249628    56.5 |  0.033 % |
c |      4521 |  780176  2283908 |  286063    4521   255299    56.5 |  0.033 % |
c |      4672 |  780176  2283908 |  314670    4672   264929    56.7 |  0.033 % |
c ==============================================================================
c [1mFound solution: 5938176[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 |      4877 |  780183  2283925 |  260061    4877   273374    56.1 |  0.033 % |
c |      4980 |  780183  2283925 |  286067    4980   278523    55.9 |  0.034 % |
c ==============================================================================
c [1mFound solution: 5903360[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 |      5049 |  780192  2283946 |  260064    5049   282254    55.9 |  0.034 % |
c |      5149 |  780192  2283946 |  286070    5149   287079    55.8 |  0.034 % |
c |      5299 |  780192  2283946 |  314677    5299   295239    55.7 |  0.034 % |
c ==============================================================================
c [1mFound solution: 5857280[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 |      5385 |  780205  2283977 |  260068    5385   300440    55.8 |  0.034 % |
c |      5486 |  780205  2283977 |  286074    5486   305598    55.7 |  0.035 % |
c |      5636 |  780205  2283977 |  314682    5636   313066    55.5 |  0.035 % |
c |      5863 |  780205  2283977 |  346150    5863   324692    55.4 |  0.035 % |
c |      6200 |  780205  2283977 |  380765    6200   347453    56.0 |  0.035 % |
c ==============================================================================
c [1mFound solution: 5834752[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 |      6661 |  780219  2284009 |  260073    6661   378987    56.9 |  0.035 % |
c |      6761 |  780219  2284009 |  286080    6761   384193    56.8 |  0.035 % |
c |      6911 |  780219  2284009 |  314688    6911   393158    56.9 |  0.035 % |
c ==============================================================================
c [1mFound solution: 5734400[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 |      7077 |  780224  2284023 |  260074    7077   402215    56.8 |  0.035 % |
c |      7177 |  780224  2284023 |  286081    7177   407628    56.8 |  0.035 % |
c |      7328 |  780224  2284023 |  314689    7328   415420    56.7 |  0.035 % |
c |      7554 |  780224  2284023 |  346158    7554   427298    56.6 |  0.035 % |
c ==============================================================================
c [1mFound solution: 5697536[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 |      7670 |  780232  2284043 |  260077    7670   433847    56.6 |  0.035 % |
c |      7770 |  780232  2284043 |  286084    7770   439094    56.5 |  0.036 % |
c |      7920 |  780232  2284043 |  314693    7920   447260    56.5 |  0.036 % |
c |      8146 |  780232  2284043 |  346162    8146   459809    56.4 |  0.036 % |
c ==============================================================================
c [1mFound solution: 5468160[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 |      8426 |  780238  2284056 |  260079    8426   473802    56.2 |  0.036 % |
c |      8527 |  780238  2284056 |  286086    8527   477769    56.0 |  0.036 % |
c |      8677 |  780238  2284056 |  314695    8677   487858    56.2 |  0.036 % |
c |      8902 |  780238  2284056 |  346165    8902   499073    56.1 |  0.036 % |
c |      9240 |  780238  2284056 |  380781    9240   518923    56.2 |  0.036 % |
c |      9746 |  780238  2284056 |  418859    9746   545702    56.0 |  0.036 % |
c |     10505 |  780238  2284056 |  460745   10505   592588    56.4 |  0.036 % |
c |     11645 |  780238  2284056 |  506820   11645   666340    57.2 |  0.036 % |
c ==============================================================================
c [1mFound solution: 5413888[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 |     11919 |  780242  2284065 |  260080   11919   681943    57.2 |  0.036 % |
c |     12019 |  780242  2284065 |  286088   12019   686729    57.1 |  0.036 % |
c |     12169 |  780242  2284065 |  314696   12169   695133    57.1 |  0.036 % |
c |     12394 |  780242  2284065 |  346166   12394   708680    57.2 |  0.036 % |
c |     12731 |  780242  2284065 |  380783   12731   730101    57.3 |  0.036 % |
c |     13238 |  780242  2284065 |  418861   13238   763643    57.7 |  0.036 % |
c ==============================================================================
c [1mFound solution: 5405696[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 |     13777 |  780252  2284088 |  260084   13777   795945    57.8 |  0.036 % |
c |     13878 |  780252  2284088 |  286092   13878   802651    57.8 |  0.037 % |
c ==============================================================================
c [1mFound solution: 5364736[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 |     14021 |  780259  2284104 |  260086   14021   812373    57.9 |  0.037 % |
c |     14121 |  780259  2284104 |  286094   14121   817922    57.9 |  0.037 % |
c |     14273 |  780259  2284104 |  314704   14273   826360    57.9 |  0.037 % |
c |     14498 |  780259  2284104 |  346174   14498   838932    57.9 |  0.037 % |
c |     14835 |  780259  2284104 |  380791   14835   857354    57.8 |  0.037 % |
c ==============================================================================
c [1mFound solution: 5243904[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 |     15330 |  780268  2284123 |  260089   15330   887315    57.9 |  0.037 % |
c ==============================================================================
c [1mFound solution: 5239808[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 |     15423 |  780279  2284155 |  260093   15423   893070    57.9 |  0.037 % |
c |     15523 |  780279  2284155 |  286102   15523   899973    58.0 |  0.038 % |
c |     15673 |  780279  2284155 |  314712   15673   908713    58.0 |  0.038 % |
c ==============================================================================
c [1mFound solution: 5169152[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 |     15833 |  780287  2284178 |  260095   15833   916731    57.9 |  0.038 % |
c |     15935 |  780287  2284178 |  286104   15935   920864    57.8 |  0.038 % |
c |     16086 |  780287  2284178 |  314714   16086   931652    57.9 |  0.038 % |
c ==============================================================================
c [1mFound solution: 5128192[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 |     16122 |  780297  2284203 |  260099   16122   933881    57.9 |  0.038 % |
c |     16222 |  780297  2284203 |  286108   16222   939703    57.9 |  0.039 % |
c |     16372 |  780297  2284203 |  314719   16372   946289    57.8 |  0.039 % |
c |     16597 |  780297  2284203 |  346191   16597   961057    57.9 |  0.039 % |
c ==============================================================================
c [1mFound solution: 4799488[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 |     16734 |  780307  2284226 |  260102   16734   967493    57.8 |  0.039 % |
c |     16837 |  780307  2284226 |  286112   16837   971971    57.7 |  0.039 % |
c |     16990 |  780307  2284226 |  314723   16990   978660    57.6 |  0.039 % |
c |     17215 |  780307  2284226 |  346195   17215   989567    57.5 |  0.039 % |
c ==============================================================================
c [1mFound solution: 4767744[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 |     17378 |  780316  2284247 |  260105   17378   996586    57.3 |  0.039 % |
c |     17478 |  780316  2284247 |  286115   17478  1001832    57.3 |  0.039 % |
c |     17629 |  780316  2284247 |  314727   17629  1007314    57.1 |  0.039 % |
c |     17856 |  780316  2284247 |  346199   17856  1021289    57.2 |  0.039 % |
c |     18193 |  780316  2284247 |  380819   18193  1034294    56.9 |  0.039 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 12247 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.97 0.91 2/54 12243
Raw data (stat): 12243 (runsolver) R 12242 20224 20223 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795980854 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.0003 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.0011 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.0015 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.0018 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.0026 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.0032 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.0042 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.0036 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12247
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.84 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 12249
Raw data (stat): 12243 (minisat+_script) S 12242 20224 20223 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795980854 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.84
CPU time (s): 1229.88
CPU user time (s): 1229.04
CPU system time (s): 0.847871
CPU usage (%): 100.004
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####