PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-egout.opb
MD5SUM	46c4db5f8baf54496e00a723c85beb20
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	58880896
Optimality of the best value was proved	NO
Number of terms in the objective function	1095
Biggest coefficient in the objective function	533200896
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	14929722305
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	533200896
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	14929722305
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	1155
Total number of constraints	153
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	98
Minimum length of a constraint	1
Maximum length of a constraint	280
Trace number 31089

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-05-25 21:53:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22476 boxname=wulflinc21 idbench=1292 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  46c4db5f8baf54496e00a723c85beb20  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-egout.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-egout.opb
IDLAUNCH: 22476
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        844492 kB
Buffers:         13368 kB
Cached:         156140 kB
SwapCached:        968 kB
Active:          18836 kB
Inactive:       152784 kB
HighTotal:      131008 kB
HighFree:        55832 kB
LowTotal:       903652 kB
LowFree:        788660 kB
SwapTotal:     2097892 kB
SwapFree:      2096008 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            12964 kB
Committed_AS:    63916 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 22:13:38 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22476 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 115 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 113]---> Adder-cost: 273   maxlim: 13440   bits: 15/14
c ---[ 111]---> BDD-cost:   40
c ---[ 109]---> BDD-cost:   25
c ---[ 107]---> BDD-cost:   45
c ---[ 105]---> BDD-cost:   83
c ---[ 101]---> BDD-cost:   39
c ---[  99]---> BDD-cost:  100
c ---[  97]---> BDD-cost:   34
c ---[  91]---> BDD-cost:   55
c ---[  89]---> BDD-cost:   40
c ---[  85]---> BDD-cost:  128
c ---[  83]---> BDD-cost:   40
c ---[  81]---> BDD-cost:  112
c ---[  79]---> BDD-cost:   49
c ---[  75]---> BDD-cost:   45
c ---[  73]---> BDD-cost:   28
c ---[  71]---> Sorter-cost:  514     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> BDD-cost:   55
c ---[  67]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> BDD-cost:  118
c ---[  59]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   40
c ---[  55]---> BDD-cost:   40
c ---[  53]---> BDD-cost:   51
c ---[  49]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   49
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:   10
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   11
c ---[  37]---> BDD-cost:   12
c ---[  36]---> BDD-cost:   12
c ---[  35]---> BDD-cost:   12
c ---[  34]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   12
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   10
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   26
c ---[  17]---> BDD-cost:   26
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   26
c ---[  13]---> BDD-cost:   26
c ---[  12]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   26
c ---[   8]---> BDD-cost:   26
c ---[   7]---> BDD-cost:   26
c ---[   6]---> BDD-cost:   26
c ---[   4]---> BDD-cost:   26
c ---[   3]---> BDD-cost:   26
c ---[   2]---> BDD-cost:   26
c ---[   1]---> BDD-cost:   26
c ---[   0]---> BDD-cost:   26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8871    23614 |    2957       0        0     nan |  0.000 % |
c |       100 |    8706    23213 |    3252      62      334     5.4 | 23.506 % |
c |       250 |    8614    23023 |    3577     176      817     4.6 | 24.498 % |
c |       477 |    8528    22841 |    3935     375     2437     6.5 | 25.341 % |
c ==============================================================================
c [1mFound solution: 98251161[0m
c ---[   0]---> Sorter-cost:93899     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       730 |  274243   643179 |   91414     601     3802     6.3 | 25.341 % |
c |       830 |  273012   640414 |  100555     689     4783     6.9 |  1.488 % |
c |       980 |  272757   639831 |  110610     835     6097     7.3 |  1.557 % |
c |      1209 |  272173   638509 |  121672    1057     7316     6.9 |  1.728 % |
c |      1546 |  271248   636409 |  133839    1388    10219     7.4 |  2.008 % |
c |      2053 |  270967   635780 |  147223    1885    16941     9.0 |  2.090 % |
c ==============================================================================
c [1mFound solution: 90380944[0m
c ---[   0]---> Sorter-cost:56645     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2528 |  421107   986844 |  140369    2270    26867    11.8 |  2.090 % |
c |      2628 |  420986   986571 |  154405    2368    27410    11.6 |  2.870 % |
c |      2778 |  418881   981794 |  169846    2509    29164    11.6 |  3.270 % |
c ==============================================================================
c [1mFound solution: 83601220[0m
c ---[   0]---> Sorter-cost:51266     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2859 |  560988  1313562 |  186996    2590    37268    14.4 |  3.270 % |
c |      2959 |  560234  1311863 |  205695    2684    37786    14.1 |  2.647 % |
c |      3109 |  560085  1311520 |  226265    2833    52989    18.7 |  2.671 % |
c |      3334 |  559906  1311131 |  248891    3057    54077    17.7 |  2.703 % |
c |      3672 |  559906  1311131 |  273780    3395    57914    17.1 |  2.703 % |
c ==============================================================================
c [1mFound solution: 75080280[0m
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3889 |  560311  1312659 |  186770    3605    66861    18.5 |  2.703 % |
c |      3989 |  560053  1312084 |  205447    3701    67324    18.2 |  2.799 % |
c |      4139 |  559865  1311660 |  225991    3849    71131    18.5 |  2.827 % |
c |      4364 |  559744  1311385 |  248590    4073    72701    17.8 |  2.846 % |
c |      4701 |  559733  1311361 |  273449    4409    75036    17.0 |  2.848 % |
c |      5207 |  559649  1311172 |  300794    4914    78073    15.9 |  2.858 % |
c ==============================================================================
c [1mFound solution: 72902771[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5394 |  559424  1310762 |  186474    5083    83077    16.3 |  2.858 % |
c |      5494 |  559424  1310762 |  205121    5183    84108    16.2 |  2.900 % |
c |      5644 |  559424  1310762 |  225633    5333    94640    17.7 |  2.899 % |
c |      5869 |  559350  1310597 |  248196    5557   103255    18.6 |  2.910 % |
c |      6207 |  559293  1310471 |  273016    5888   119017    20.2 |  2.918 % |
c |      6715 |  558850  1309460 |  300318    6394   140155    21.9 |  2.985 % |
c ==============================================================================
c [1mFound solution: 70799895[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7150 |  557562  1306544 |  185854    6823   185362    27.2 |  2.985 % |
c |      7250 |  557562  1306544 |  204439    6923   191283    27.6 |  3.180 % |
c |      7400 |  557562  1306544 |  224883    7073   196159    27.7 |  3.180 % |
c ==============================================================================
c [1mFound solution: 68823191[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7433 |  557596  1306628 |  185865    7106   197145    27.7 |  3.180 % |
c |      7535 |  557596  1306628 |  204451    7208   207757    28.8 |  3.181 % |
c |      7689 |  557596  1306628 |  224896    7362   210303    28.6 |  3.181 % |
c ==============================================================================
c [1mFound solution: 66801712[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7739 |  557622  1306690 |  185874    7412   211372    28.5 |  3.181 % |
c |      7839 |  557622  1306690 |  204461    7512   214674    28.6 |  3.181 % |
c |      7990 |  557622  1306690 |  224907    7663   221258    28.9 |  3.181 % |
c |      8215 |  557575  1306584 |  247398    7887   224224    28.4 |  3.187 % |
c |      8553 |  556893  1305042 |  272138    8018   226835    28.3 |  3.287 % |
c |      9059 |  556893  1305042 |  299351    8524   351418    41.2 |  3.287 % |
c |      9818 |  556828  1304894 |  329287    9282   372202    40.1 |  3.297 % |
c |     10957 |  555966  1302938 |  362215   10397   418014    40.2 |  3.424 % |
c ==============================================================================
c [1mFound solution: 65961920[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12376 |  555644  1302223 |  185214   11760   470077    40.0 |  3.424 % |
c |     12477 |  555644  1302223 |  203735   11861   473070    39.9 |  3.486 % |
c |     12628 |  555140  1301079 |  224108   12008   479077    39.9 |  3.560 % |
c |     12853 |  555140  1301079 |  246519   12233   483370    39.5 |  3.560 % |
c |     13193 |  555140  1301079 |  271171   12572   490526    39.0 |  3.573 % |
c ==============================================================================
c [1mFound solution: 65957568[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13361 |  554865  1300533 |  184955   12724   500141    39.3 |  3.573 % |
c |     13464 |  554865  1300533 |  203450   12827   503589    39.3 |  3.603 % |
c |     13618 |  554865  1300533 |  223795   12981   514623    39.6 |  3.603 % |
c |     13843 |  554865  1300533 |  246175   13206   519440    39.3 |  3.603 % |
c |     14180 |  554865  1300533 |  270792   13543   529329    39.1 |  3.603 % |
c ==============================================================================
c [1mFound solution: 64888022[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14535 |  554886  1300584 |  184962   13898   594958    42.8 |  3.603 % |
c |     14636 |  554872  1300551 |  203458   13996   595705    42.6 |  3.606 % |
c |     14788 |  554843  1300486 |  223804   14134   596715    42.2 |  3.610 % |
c ==============================================================================
c [1mFound solution: 64714286[0m
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14980 |  554864  1300536 |  184954   14326   613466    42.8 |  3.610 % |
c |     15081 |  554864  1300536 |  203449   14427   616582    42.7 |  3.611 % |
c |     15231 |  554864  1300536 |  223794   14577   625465    42.9 |  3.611 % |
c |     15456 |  554864  1300536 |  246173   14802   646941    43.7 |  3.611 % |
c |     15795 |  554864  1300536 |  270791   15141   669297    44.2 |  3.611 % |
c |     16301 |  554864  1300536 |  297870   15647   708282    45.3 |  3.611 % |
c |     17060 |  554730  1300230 |  327657   16373   715663    43.7 |  3.633 % |
c |     18200 |  554730  1300230 |  360423   17513   730350    41.7 |  3.633 % |
c ==============================================================================
c [1mFound solution: 64484352[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19484 |  554438  1299569 |  184812   18777   796102    42.4 |  3.633 % |
c |     19584 |  554438  1299569 |  203293   18877   799033    42.3 |  3.678 % |
c |     19735 |  554438  1299569 |  223622   19028   800696    42.1 |  3.678 % |
c |     19961 |  554438  1299569 |  245984   19254   807646    41.9 |  3.678 % |
c |     20299 |  554346  1299358 |  270583   19587   822303    42.0 |  3.696 % |
c |     20808 |  554342  1299350 |  297641   20093   845460    42.1 |  3.698 % |
c ==============================================================================
c [1mFound solution: 64437712[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21505 |  554360  1299393 |  184786   20790   904089    43.5 |  3.698 % |
c |     21606 |  554360  1299393 |  203264   20891   909522    43.5 |  3.698 % |
c |     21757 |  554360  1299393 |  223591   21042   912661    43.4 |  3.698 % |
c ==============================================================================
c [1mFound solution: 64396544[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21945 |  554376  1299432 |  184792   21230   918944    43.3 |  3.698 % |
c |     22046 |  554376  1299432 |  203271   21331   922113    43.2 |  3.698 % |
c |     22196 |  554376  1299432 |  223598   21481   931036    43.3 |  3.698 % |
c |     22421 |  554376  1299432 |  245958   21706   950010    43.8 |  3.698 % |
c |     22759 |  554376  1299432 |  270553   22044   962059    43.6 |  3.698 % |
c |     23266 |  554376  1299432 |  297609   22551   985413    43.7 |  3.698 % |
c |     24025 |  554376  1299432 |  327370   23310  1062588    45.6 |  3.698 % |
c ==============================================================================
c [1mFound solution: 62242606[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24056 |  554406  1299510 |  184802   23341  1064546    45.6 |  3.698 % |
c ==============================================================================
c [1mFound solution: 62227456[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24064 |  554420  1299552 |  184806   23349  1065485    45.6 |  3.698 % |
c ==============================================================================
c [1mFound solution: 61803904[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24109 |  554437  1299595 |  184812   23394  1073902    45.9 |  3.698 % |
c |     24209 |  554437  1299595 |  203293   23494  1080333    46.0 |  3.699 % |
c |     24359 |  554437  1299595 |  223622   23644  1085303    45.9 |  3.699 % |
c |     24585 |  554437  1299595 |  245984   23870  1090840    45.7 |  3.699 % |
c |     24922 |  554437  1299595 |  270583   24207  1126010    46.5 |  3.699 % |
c |     25429 |  554437  1299595 |  297641   24714  1143562    46.3 |  3.699 % |
c |     26188 |  554437  1299595 |  327405   25473  1189554    46.7 |  3.699 % |
c ==============================================================================
c [1mFound solution: 61163008[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26618 |  554456  1299640 |  184818   25903  1208767    46.7 |  3.699 % |
c |     26718 |  554456  1299640 |  203299   26003  1211182    46.6 |  3.699 % |
c |     26868 |  554456  1299640 |  223629   26153  1216316    46.5 |  3.699 % |
c |     27097 |  554456  1299640 |  245992   26382  1226946    46.5 |  3.699 % |
c |     27434 |  554456  1299640 |  270592   26719  1256775    47.0 |  3.699 % |
c ==============================================================================
c [1mFound solution: 61074176[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27834 |  554469  1299675 |  184823   27119  1270285    46.8 |  3.699 % |
c |     27937 |  554469  1299675 |  203305   27222  1273811    46.8 |  3.700 % |
c |     28088 |  554469  1299675 |  223635   27373  1277562    46.7 |  3.700 % |
c |     28313 |  554469  1299675 |  245999   27598  1281403    46.4 |  3.700 % |
c |     28650 |  554368  1299448 |  270599   27338  1282042    46.9 |  3.716 % |
c |     29157 |  554368  1299448 |  297659   27845  1311748    47.1 |  3.716 % |
c |     29916 |  554368  1299448 |  327425   28604  1384699    48.4 |  3.716 % |
c |     31056 |  554270  1299227 |  360167   28464  1403177    49.3 |  3.736 % |
c ==============================================================================
c [1mFound solution: 60755072[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31220 |  554285  1299261 |  184761   28628  1411761    49.3 |  3.736 % |
c |     31322 |  554285  1299261 |  203237   28730  1418292    49.4 |  3.737 % |
c |     31473 |  554285  1299261 |  223560   28881  1422836    49.3 |  3.737 % |
c |     31698 |  554285  1299261 |  245916   29106  1431324    49.2 |  3.737 % |
c |     32035 |  554278  1299246 |  270508   29441  1440465    48.9 |  3.738 % |
c |     32541 |  554278  1299246 |  297559   29947  1458101    48.7 |  3.738 % |
c |     33300 |  554278  1299246 |  327315   30706  1493978    48.7 |  3.738 % |
c |     34440 |  554078  1298787 |  360046   31691  1539085    48.6 |  3.771 % |
c ==============================================================================
c [1mFound solution: 60662144[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35760 |  554090  1298817 |  184696   33011  1588723    48.1 |  3.771 % |
c |     35862 |  554090  1298817 |  203165   33113  1591007    48.0 |  3.771 % |
c |     36012 |  554090  1298817 |  223482   33263  1597886    48.0 |  3.771 % |
c |     36238 |  554090  1298817 |  245830   33489  1605823    48.0 |  3.771 % |
c |     36575 |  554090  1298817 |  270413   33826  1614991    47.7 |  3.771 % |
c |     37081 |  554080  1298795 |  297454   34330  1637375    47.7 |  3.772 % |
c |     37840 |  554080  1298795 |  327200   35089  1664108    47.4 |  3.772 % |
c |     38980 |  554080  1298795 |  359920   36229  1727605    47.7 |  3.773 % |
c |     40688 |  554080  1298795 |  395912   37937  1878610    49.5 |  3.772 % |
c |     43254 |  554032  1298686 |  435503   40502  2026738    50.0 |  3.784 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 18503 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.91 0.97 0.96 2/55 18499
Raw data (stat): 18499 (runsolver) R 18498 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 719534422 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0009 s]
Raw data (loadavg): 0.95 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0016 s]
Raw data (loadavg): 0.95 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0021 s]
Raw data (loadavg): 0.96 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0028 s]
Raw data (loadavg): 0.97 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0038 s]
Raw data (loadavg): 0.97 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0038 s]
Raw data (loadavg): 0.98 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18503
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18556
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18556
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18556
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18556
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18556
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18556
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18558
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18560
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.07 0.99 0.96 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.14 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.11 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 1.10 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.08 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.07 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.005 s]
Raw data (loadavg): 1.06 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.05 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.04 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.03 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.03 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.02 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.02 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.006 s]
Raw data (loadavg): 1.02 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.007 s]
Raw data (loadavg): 1.01 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.01 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.01 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.01 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 1.00 0.97 2/56 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.69 s]
Raw data (loadavg): 1.00 1.00 0.97 1/54 18562
Raw data (stat): 18499 (minisat+_script) S 18498 32363 32362 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 719534422 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.69
CPU time (s): 1229.87
CPU user time (s): 1229.34
CPU system time (s): 0.530919
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####