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/submitted/een/normalized-lseu.opb
MD5SUM	a578bf261896413ca78de4dc6db2447f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1120
Optimality of the best value was proved	NO
Number of terms in the objective function	85
Biggest coefficient in the objective function	517
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	15494
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1656
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	15494
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02184
Number of variables	89
Total number of constraints	28
Number of constraints which are clauses	2
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	2
Maximum length of a constraint	47
Trace number 31725

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-05-27 06:04:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23141 boxname=wulflinc8 idbench=387 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a578bf261896413ca78de4dc6db2447f  /oldhome/oroussel/tmp/wulflinc8/normalized-lseu.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc8/normalized-lseu.opb
IDLAUNCH: 23141
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        717508 kB
Buffers:         34884 kB
Cached:         255612 kB
SwapCached:          0 kB
Active:          17016 kB
Inactive:       280472 kB
HighTotal:      131008 kB
HighFree:        92680 kB
LowTotal:       903652 kB
LowFree:        624828 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7068 kB
Slab:            13852 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 06:14:27 (client local time) WITH STATUS 30 IN 626.586 SECONDS
stats: 23141 0 626.586 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): .....s
c ---[  26]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   28
c ---[   6]---> BDD-cost:  202
c ---[   4]---> BDD-cost:  469
c ---[   3]---> BDD-cost: 1803
c ---[   1]---> BDD-cost: 5998
c ---[   0]---> BDD-cost:   22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23842    70296 |    7947       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3310[0m
c ---[   0]---> Sorter-cost:12496     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        12 |   53328   139237 |   17776      12       97     8.1 |  0.000 % |
c |       112 |   53312   139205 |   19553     111     4698    42.3 |  0.163 % |
c |       262 |   53204   138963 |   21508     257     5822    22.7 |  0.309 % |
c ==============================================================================
c [1mFound solution: 3298[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       337 |   52611   137720 |   17537     293     5946    20.3 |  0.309 % |
c ==============================================================================
c [1mFound solution: 3255[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       340 |   52790   138131 |   17596     296     5967    20.2 |  0.309 % |
c |       440 |   51339   134810 |   19355     371     6882    18.5 |  3.858 % |
c ==============================================================================
c [1mFound solution: 2963[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       505 |   50435   132753 |   16811     380     6839    18.0 |  3.858 % |
c |       607 |   49708   131081 |   18492     470     8443    18.0 |  6.875 % |
c ==============================================================================
c [1mFound solution: 2922[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       687 |   49635   130940 |   16545     545    12350    22.7 |  6.875 % |
c |       788 |   49635   130940 |   18199     646    14765    22.9 |  7.157 % |
c |       939 |   48823   129062 |   20019     778    16254    20.9 |  8.581 % |
c |      1164 |   48001   127169 |   22021     956    20857    21.8 |  9.777 % |
c |      1502 |   47748   126585 |   24223    1277    27208    21.3 | 10.158 % |
c |      2009 |   47681   126427 |   26645    1782    42929    24.1 | 10.270 % |
c ==============================================================================
c [1mFound solution: 2902[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2245 |   47793   126719 |   15931    2018    52194    25.9 | 10.270 % |
c |      2345 |   47793   126719 |   17524    2118    57251    27.0 | 10.258 % |
c ==============================================================================
c [1mFound solution: 2429[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2373 |   47901   126996 |   15967    2146    58216    27.1 | 10.258 % |
c |      2473 |   47901   126996 |   17563    2246    61107    27.2 | 10.249 % |
c ==============================================================================
c [1mFound solution: 2160[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2507 |   47922   127061 |   15974    2280    63410    27.8 | 10.249 % |
c ==============================================================================
c [1mFound solution: 1880[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2516 |   47943   127129 |   15981    2289    63648    27.8 | 10.249 % |
c ==============================================================================
c [1mFound solution: 1828[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2612 |   47951   127150 |   15983    2385    68018    28.5 | 10.249 % |
c ==============================================================================
c [1mFound solution: 1804[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2650 |   47958   127166 |   15986    2423    70008    28.9 | 10.249 % |
c |      2750 |   47958   127166 |   17584    2523    73306    29.1 | 10.250 % |
c |      2902 |   47958   127166 |   19343    2675    80079    29.9 | 10.250 % |
c |      3127 |   47901   127036 |   21277    2899    91133    31.4 | 10.336 % |
c |      3465 |   47901   127036 |   23405    3237   107745    33.3 | 10.336 % |
c ==============================================================================
c [1mFound solution: 1802[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3926 |   47906   127048 |   15968    3698   135475    36.6 | 10.336 % |
c |      4026 |   47906   127048 |   17564    3798   141406    37.2 | 10.339 % |
c |      4176 |   47906   127048 |   19321    3948   149355    37.8 | 10.339 % |
c |      4402 |   47906   127048 |   21253    4174   163065    39.1 | 10.339 % |
c ==============================================================================
c [1mFound solution: 1787[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4623 |   48005   127304 |   16001    4395   177764    40.4 | 10.339 % |
c |      4724 |   48005   127304 |   17601    4496   180004    40.0 | 10.329 % |
c |      4874 |   48005   127304 |   19361    4646   183991    39.6 | 10.329 % |
c |      5099 |   48005   127304 |   21297    4871   190244    39.1 | 10.329 % |
c |      5436 |   48005   127304 |   23427    5208   198741    38.2 | 10.329 % |
c |      5945 |   48005   127304 |   25769    5717   214518    37.5 | 10.329 % |
c |      6708 |   48005   127304 |   28346    6480   238731    36.8 | 10.329 % |
c |      7852 |   48005   127304 |   31181    7624   266707    35.0 | 10.329 % |
c |      9565 |   48005   127304 |   34299    9337   311384    33.3 | 10.329 % |
c |     12128 |   47946   127169 |   37729   11898   386342    32.5 | 10.414 % |
c ==============================================================================
c [1mFound solution: 1740[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14665 |   47865   127003 |   15955    5802   209399    36.1 | 10.414 % |
c |     14766 |   47865   127003 |   17550    5903   214200    36.3 | 10.552 % |
c |     14916 |   47865   127003 |   19305    6053   220634    36.5 | 10.552 % |
c |     15142 |   47842   126948 |   21236    6276   229395    36.6 | 10.602 % |
c |     15479 |   47842   126948 |   23359    6613   241806    36.6 | 10.602 % |
c ==============================================================================
c [1mFound solution: 1711[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15912 |   47850   126981 |   15950    7046   262257    37.2 | 10.602 % |
c |     16012 |   47850   126981 |   17545    7146   267359    37.4 | 10.604 % |
c |     16162 |   47850   126981 |   19299    7296   275535    37.8 | 10.604 % |
c |     16388 |   47850   126981 |   21229    7522   286341    38.1 | 10.604 % |
c |     16725 |   47850   126981 |   23352    7859   300573    38.2 | 10.604 % |
c |     17233 |   47850   126981 |   25687    8367   320546    38.3 | 10.604 % |
c |     17993 |   47557   126299 |   28256    9121   351146    38.5 | 11.056 % |
c |     19133 |   47453   126063 |   31082   10257   433012    42.2 | 11.196 % |
c ==============================================================================
c [1mFound solution: 1607[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19500 |   47528   126248 |   15842   10624   451563    42.5 | 11.196 % |
c |     19600 |   47528   126248 |   17426   10724   454574    42.4 | 11.200 % |
c |     19750 |   47528   126248 |   19168   10874   459940    42.3 | 11.200 % |
c ==============================================================================
c [1mFound solution: 1588[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19830 |   47535   126268 |   15845   10954   462149    42.2 | 11.200 % |
c |     19930 |   47535   126268 |   17429   11054   465515    42.1 | 11.202 % |
c ==============================================================================
c [1mFound solution: 1587[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20008 |   47539   126279 |   15846   11132   468364    42.1 | 11.202 % |
c |     20108 |   47539   126279 |   17430   11232   473653    42.2 | 11.206 % |
c ==============================================================================
c [1mFound solution: 1563[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20256 |   47543   126290 |   15847   11380   481343    42.3 | 11.206 % |
c |     20356 |   47543   126290 |   17431   11480   485481    42.3 | 11.209 % |
c |     20508 |   47543   126290 |   19174   11632   489972    42.1 | 11.209 % |
c |     20733 |   47543   126290 |   21092   11857   495826    41.8 | 11.209 % |
c |     21070 |   47543   126290 |   23201   12194   507365    41.6 | 11.209 % |
c |     21577 |   47543   126290 |   25521   12701   521923    41.1 | 11.209 % |
c |     22336 |   47543   126290 |   28073   13460   548597    40.8 | 11.209 % |
c |     23476 |   47539   126281 |   30881   14599   593826    40.7 | 11.214 % |
c ==============================================================================
c [1mFound solution: 1526[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23805 |   47449   126085 |   15816   14926   608071    40.7 | 11.214 % |
c ==============================================================================
c [1mFound solution: 1503[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23882 |   47454   126097 |   15818   15003   611506    40.8 | 11.214 % |
c ==============================================================================
c [1mFound solution: 1492[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23948 |   47459   126108 |   15819   15069   614061    40.7 | 11.214 % |
c ==============================================================================
c [1mFound solution: 1489[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23953 |   47466   126124 |   15822   15074   614181    40.7 | 11.214 % |
c |     24054 |   47466   126124 |   17404   15175   617698    40.7 | 11.366 % |
c ==============================================================================
c [1mFound solution: 1474[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24152 |   47473   126140 |   15824   15273   621487    40.7 | 11.366 % |
c |     24252 |   47473   126140 |   17406   15373   625677    40.7 | 11.368 % |
c |     24402 |   47473   126140 |   19147   15523   631688    40.7 | 11.368 % |
c |     24627 |   47473   126140 |   21061   15748   640702    40.7 | 11.368 % |
c |     24966 |   47473   126140 |   23167   16087   652835    40.6 | 11.368 % |
c |     25474 |   47137   125365 |   25484   16588   670699    40.4 | 11.893 % |
c |     26234 |   46646   124227 |   28033   17342   701952    40.5 | 12.678 % |
c ==============================================================================
c [1mFound solution: 1430[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26853 |   46556   124018 |   15518   17954   724254    40.3 | 12.678 % |
c |     26954 |   46556   124018 |   17069   18055   726900    40.3 | 12.849 % |
c |     27104 |   46556   124018 |   18776   18205   734802    40.4 | 12.849 % |
c |     27331 |   46556   124018 |   20654   18432   745297    40.4 | 12.849 % |
c |     27669 |   46191   123170 |   22719   18757   751877    40.1 | 13.434 % |
c |     28176 |   45405   121352 |   24991   19136   763912    39.9 | 14.688 % |
c |     28935 |   45405   121352 |   27491   19895   794574    39.9 | 14.688 % |
c |     30074 |   45359   121246 |   30240   21032   835481    39.7 | 14.758 % |
c ==============================================================================
c [1mFound solution: 1330[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30646 |   45366   121262 |   15122   21604   860437    39.8 | 14.758 % |
c |     30748 |   45366   121262 |   16634   10904   351647    32.2 | 14.760 % |
c |     30898 |   45366   121262 |   18297   11054   356563    32.3 | 14.760 % |
c |     31123 |   45366   121262 |   20127   11279   366016    32.5 | 14.760 % |
c ==============================================================================
c [1mFound solution: 1325[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31161 |   45371   121274 |   15123   11317   367798    32.5 | 14.760 % |
c |     31262 |   45371   121274 |   16635   11418   371578    32.5 | 14.763 % |
c |     31413 |   45371   121274 |   18298   11569   375783    32.5 | 14.763 % |
c |     31639 |   45371   121274 |   20128   11795   382255    32.4 | 14.763 % |
c |     31976 |   45371   121274 |   22141   12132   389944    32.1 | 14.763 % |
c |     32486 |   45371   121274 |   24355   12642   404067    32.0 | 14.763 % |
c |     33247 |   45371   121274 |   26791   13403   439779    32.8 | 14.763 % |
c |     34387 |   45357   121240 |   29470   14538   486647    33.5 | 14.778 % |
c ==============================================================================
c [1mFound solution: 1319[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36052 |   45348   121219 |   15116   16202   557783    34.4 | 14.778 % |
c |     36153 |   45348   121219 |   16627   16303   561701    34.5 | 14.801 % |
c |     36303 |   45348   121219 |   18290   16453   568068    34.5 | 14.801 % |
c ==============================================================================
c [1mFound solution: 1309[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36322 |   45417   121384 |   15139   16472   568834    34.5 | 14.801 % |
c |     36424 |   45417   121384 |   16652   16574   572089    34.5 | 14.799 % |
c |     36575 |   45417   121384 |   18318   16725   578103    34.6 | 14.799 % |
c |     36801 |   45417   121384 |   20150   16951   588872    34.7 | 14.799 % |
c ==============================================================================
c [1mFound solution: 1302[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37044 |   45421   121393 |   15140   17194   600354    34.9 | 14.799 % |
c |     37145 |   45421   121393 |   16654   17295   605273    35.0 | 14.802 % |
c ==============================================================================
c [1mFound solution: 1292[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37229 |   45435   121428 |   15145   17379   608747    35.0 | 14.802 % |
c |     37331 |   45435   121428 |   16659   17481   613311    35.1 | 14.801 % |
c ==============================================================================
c [1mFound solution: 1230[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37339 |   45442   121448 |   15147   17489   613587    35.1 | 14.801 % |
c |     37439 |   45442   121448 |   16661   17589   617654    35.1 | 14.802 % |
c |     37590 |   45442   121448 |   18327   17740   623640    35.2 | 14.802 % |
c |     37815 |   45442   121448 |   20160   17965   632939    35.2 | 14.802 % |
c ==============================================================================
c [1mFound solution: 1221[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37978 |   45445   121455 |   15148   18128   640411    35.3 | 14.802 % |
c |     38079 |   45445   121455 |   16662    9165   293847    32.1 | 14.806 % |
c |     38229 |   45445   121455 |   18329    9315   298243    32.0 | 14.806 % |
c |     38454 |   45445   121455 |   20161    9540   305599    32.0 | 14.806 % |
c ==============================================================================
c [1mFound solution: 1215[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38476 |   45450   121467 |   15150    9562   306372    32.0 | 14.806 % |
c ==============================================================================
c [1mFound solution: 1153[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38567 |   45455   121478 |   15151    9653   309883    32.1 | 14.806 % |
c ==============================================================================
c [1mFound solution: 1136[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38568 |   45461   121493 |   15153    9654   309904    32.1 | 14.806 % |
c |     38668 |   45461   121493 |   16668    9754   312924    32.1 | 14.813 % |
c |     38822 |   45461   121493 |   18335    9908   316872    32.0 | 14.813 % |
c |     39047 |   45461   121493 |   20168   10133   323707    31.9 | 14.813 % |
c |     39384 |   45461   121493 |   22185   10470   333289    31.8 | 14.813 % |
c |     39890 |   45457   121484 |   24404   10975   348814    31.8 | 14.818 % |
c |     40649 |   45457   121484 |   26844   11734   371697    31.7 | 14.818 % |
c |     41788 |   45437   121437 |   29528   12871   401192    31.2 | 14.833 % |
c |     43496 |   45437   121437 |   32481   14579   453702    31.1 | 14.833 % |
c ==============================================================================
c [1mFound solution: 1128[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45439 |   45441   121447 |   15147   16522   527626    31.9 | 14.833 % |
c |     45539 |   45379   121301 |   16661   16621   529249    31.8 | 14.935 % |
c |     45696 |   45379   121301 |   18327   16778   531296    31.7 | 14.935 % |
c |     45921 |   45379   121301 |   20160   17003   539062    31.7 | 14.935 % |
c |     46260 |   45379   121301 |   22176   17342   549123    31.7 | 14.935 % |
c |     46767 |   45379   121301 |   24394   17849   564499    31.6 | 14.935 % |
c |     47528 |   45379   121301 |   26833   18610   583212    31.3 | 14.935 % |
c |     48667 |   45379   121301 |   29517   19749   615658    31.2 | 14.935 % |
c |     50375 |   45379   121301 |   32468   21457   685002    31.9 | 14.935 % |
c |     52940 |   45379   121301 |   35715   24022   786924    32.8 | 14.935 % |
c |     56784 |   45379   121301 |   39287   27866   923230    33.1 | 14.935 % |
c ==============================================================================
c [1mFound solution: 1120[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57940 |   45382   121308 |   15127   29022   962363    33.2 | 14.935 % |
c |     58042 |   45382   121308 |   16639   14613   441762    30.2 | 14.939 % |
c |     58192 |   45382   121308 |   18303   14763   446956    30.3 | 14.939 % |
c |     58418 |   45382   121308 |   20134   14989   454161    30.3 | 14.939 % |
c |     58762 |   45382   121308 |   22147   15333   464669    30.3 | 14.939 % |
c |     59268 |   45382   121308 |   24362   15839   479806    30.3 | 14.939 % |
c |     60028 |   45382   121308 |   26798   16599   501294    30.2 | 14.939 % |
c |     61169 |   45382   121308 |   29478   17740   541348    30.5 | 14.939 % |
c |     62879 |   45382   121308 |   32426   19450   605293    31.1 | 14.939 % |
c |     65441 |   45382   121308 |   35668   22012   702077    31.9 | 14.939 % |
c |     69287 |   45382   121308 |   39235   25858   821529    31.8 | 14.939 % |
c |     75057 |   45382   121308 |   43159   31628  1051655    33.3 | 14.939 % |
c |     83706 |   45382   121308 |   47475   40277  1345729    33.4 | 14.939 % |
c |     96680 |   45334   121197 |   52222   19901   543345    27.3 | 15.008 % |
c ==============================================================================
c [1mOptimal solution: 1120[0m
s OPTIMUM FOUND
v x0 x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 x22 -x23 -x24 -x25 -x26 -x27 -x28 x29 -x30 -x31 -x32 -x33 x34 -x35 -x36 -x37 -x38 x39 -x40 -x41 -x42 -x43 -x44 -x45 x46 -x47 x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 x59 -x60 x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 x81 -x82 -x83 -x84 -x85 x86 -x87 -x88
c _______________________________________________________________________________
c 
c restarts              : 156
c conflicts             : 113246         (181 /sec)
c decisions             : 216557         (346 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 626.377 s
c _______________________________________________________________________________
#### 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.90 0.98 0.92 2/54 30353
Raw data (stat): 30353 (runsolver) R 30352 3132 3131 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782068537 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.91 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.001 s]
Raw data (loadavg): 0.92 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0005 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0005 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0012 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0016 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0014 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0017 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30357
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.004 s]
Raw data (loadavg): 1.07 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.005 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.005 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.006 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.005 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.005 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.006 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.004 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.004 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+626.536 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 30359
Raw data (stat): 30353 (minisat+_script) S 30352 3132 3131 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 782068537 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 626.535
CPU time (s): 626.586
CPU user time (s): 626.399
CPU system time (s): 0.186971
CPU usage (%): 100.008
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####