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/miplib2003/normalized-mps-v2-13-7-misc07.opb
MD5SUM	a3dd3cd7dd293e24bffaff8bb73da54c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1408128
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11486079
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	280
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	253
Trace number 31144

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-25 22:27:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22545 boxname=wulflinc7 idbench=1361 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  a3dd3cd7dd293e24bffaff8bb73da54c  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 22545
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        916184 kB
Buffers:         31228 kB
Cached:          67580 kB
SwapCached:        676 kB
Active:          17872 kB
Inactive:        82992 kB
HighTotal:      131008 kB
HighFree:       102480 kB
LowTotal:       903652 kB
LowFree:        813704 kB
SwapTotal:     2097136 kB
SwapFree:      2095524 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5068 kB
Slab:            11980 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 22:48:00 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 22545 7 1229.84 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 244]---> BDD-cost:  239
c ---[ 233]---> BDD-cost:  239
c ---[ 200]---> Sorter-cost:  127     Base:
c ---[ 197]---> Sorter-cost:  127     Base:
c ---[ 195]---> Sorter-cost:  127     Base:
c ---[ 193]---> Sorter-cost:  127     Base:
c ---[ 191]---> Sorter-cost:  127     Base:
c ---[ 189]---> Sorter-cost:  127     Base:
c ---[ 187]---> Sorter-cost:  127     Base:
c ---[ 185]---> Sorter-cost:  127     Base:
c ---[ 183]---> Sorter-cost:  127     Base:
c ---[ 181]---> Sorter-cost:  127     Base:
c ---[ 179]---> Sorter-cost:  127     Base:
c ---[ 176]---> Sorter-cost:  127     Base:
c ---[ 174]---> Sorter-cost:  127     Base:
c ---[ 172]---> Sorter-cost:  127     Base:
c ---[ 170]---> Sorter-cost:  127     Base:
c ---[ 168]---> Sorter-cost:  127     Base:
c ---[ 166]---> Sorter-cost:  127     Base:
c ---[ 164]---> Sorter-cost:  127     Base:
c ---[ 162]---> Sorter-cost:  127     Base:
c ---[ 160]---> Sorter-cost:  127     Base:
c ---[ 158]---> Sorter-cost:  127     Base:
c ---[ 155]---> Sorter-cost:  127     Base:
c ---[ 153]---> Sorter-cost:  127     Base:
c ---[ 151]---> Sorter-cost:  127     Base:
c ---[ 149]---> Sorter-cost:  127     Base:
c ---[ 147]---> Sorter-cost:  127     Base:
c ---[ 145]---> Sorter-cost:  127     Base:
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   50
c ---[ 131]---> BDD-cost:   50
c ---[ 130]---> BDD-cost:   50
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   48
c ---[ 124]---> BDD-cost:   48
c ---[ 123]---> BDD-cost:   48
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   50
c ---[ 117]---> BDD-cost:   50
c ---[ 116]---> BDD-cost:   50
c ---[ 115]---> BDD-cost:   27
c ---[ 114]---> BDD-cost:   27
c ---[ 113]---> BDD-cost:   27
c ---[ 112]---> BDD-cost:   48
c ---[ 111]---> BDD-cost:   48
c ---[ 110]---> BDD-cost:   48
c ---[ 109]---> BDD-cost:   27
c ---[ 108]---> BDD-cost:   27
c ---[ 106]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:   27
c ---[ 103]---> BDD-cost:   50
c ---[ 102]---> BDD-cost:   50
c ---[ 101]---> BDD-cost:   50
c ---[ 100]---> BDD-cost:   27
c ---[  99]---> BDD-cost:   27
c ---[  98]---> BDD-cost:   27
c ---[  97]---> BDD-cost:   48
c ---[  96]---> BDD-cost:   48
c ---[  95]---> BDD-cost:   48
c ---[  93]---> BDD-cost:   27
c ---[  92]---> BDD-cost:   27
c ---[  91]---> BDD-cost:   27
c ---[  81]---> BDD-cost:   51
c ---[  69]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   51
c ---[  45]---> BDD-cost:   51
c ---[  33]---> BDD-cost:   51
c ---[  21]---> BDD-cost:   51
c ---[  10]---> BDD-cost:  216
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25782    84321 |    8594       0        0     nan |  0.000 % |
c |       100 |   25752    84253 |    9453      98     6192    63.2 |  2.792 % |
c ==============================================================================
c [1mFound solution: 1583488[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       220 |   25767    84288 |    8589     218    12443    57.1 |  2.792 % |
c ==============================================================================
c [1mFound solution: 1580928[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       268 |   25776    84312 |    8592     266    20437    76.8 |  2.792 % |
c |       368 |   25776    84312 |    9451     366    22162    60.6 |  2.817 % |
c |       518 |   25776    84312 |   10396     516    29655    57.5 |  2.817 % |
c |       744 |   25776    84312 |   11435     742    42680    57.5 |  2.817 % |
c ==============================================================================
c [1mFound solution: 1508608[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       870 |   25789    84343 |    8596     868    48024    55.3 |  2.817 % |
c |       970 |   25789    84343 |    9455     968    60363    62.4 |  2.829 % |
c |      1120 |   25778    84319 |   10401    1117    68505    61.3 |  2.872 % |
c |      1347 |   25778    84319 |   11441    1344    77932    58.0 |  2.872 % |
c |      1684 |   25778    84319 |   12585    1681   103593    61.6 |  2.872 % |
c |      2190 |   25778    84319 |   13843    2187   126927    58.0 |  2.872 % |
c |      2950 |   25767    84295 |   15228    2946   212260    72.1 |  2.916 % |
c |      4090 |   25767    84295 |   16751    4086   295763    72.4 |  2.916 % |
c |      5798 |   25731    84167 |   18426    5787   492222    85.1 |  2.945 % |
c ==============================================================================
c [1mFound solution: 1477248[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7454 |   25683    83993 |    8561    7434   643106    86.5 |  2.945 % |
c |      7556 |   25683    83993 |    9417    7536   659060    87.5 |  3.056 % |
c |      7706 |   25683    83993 |   10358    7686   665481    86.6 |  3.056 % |
c |      7931 |   25683    83993 |   11394    7911   690952    87.3 |  3.056 % |
c |      8270 |   25672    83969 |   12534    8249   707791    85.8 |  3.099 % |
c |      8776 |   25672    83969 |   13787    8755   792296    90.5 |  3.099 % |
c |      9537 |   25618    83822 |   15166    9509   863713    90.8 |  3.243 % |
c |     10678 |   25536    83532 |   16682   10641   946280    88.9 |  3.358 % |
c |     12386 |   25503    83415 |   18351   12346  1087746    88.1 |  3.387 % |
c |     14949 |   25449    83245 |   20186   14900  1399535    93.9 |  3.488 % |
c |     18793 |   25395    83098 |   22205   18736  1754727    93.7 |  3.632 % |
c ==============================================================================
c [1mFound solution: 1475328[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20218 |   25398    83107 |    8466   20160  1881199    93.3 |  3.632 % |
c |     20322 |   25398    83107 |    9312    5144   289617    56.3 |  3.686 % |
c |     20472 |   25398    83107 |   10243    5294   299464    56.6 |  3.686 % |
c |     20697 |   25398    83107 |   11268    5519   320431    58.1 |  3.686 % |
c |     21034 |   25387    83083 |   12395    5854   334549    57.1 |  3.729 % |
c |     21540 |   25387    83083 |   13634    6360   407264    64.0 |  3.729 % |
c |     22300 |   25354    82966 |   14998    7118   497542    69.9 |  3.758 % |
c |     23439 |   25343    82942 |   16497    8256   599062    72.6 |  3.801 % |
c |     25148 |   25316    82847 |   18147    9957   832837    83.6 |  3.830 % |
c |     27712 |   25316    82847 |   19962   12521  1060640    84.7 |  3.830 % |
c |     31557 |   25316    82847 |   21958   16366  1691483   103.4 |  3.830 % |
c ==============================================================================
c [1mFound solution: 1460608[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34542 |   25294    82772 |    8431   19345  1961844   101.4 |  3.830 % |
c |     34643 |   25294    82772 |    9274    4938   275109    55.7 |  3.899 % |
c |     34793 |   25294    82772 |   10201    5088   277980    54.6 |  3.899 % |
c |     35019 |   25294    82772 |   11221    5314   292878    55.1 |  3.899 % |
c |     35357 |   25294    82772 |   12343    5652   319785    56.6 |  3.899 % |
c |     35863 |   25294    82772 |   13578    6158   364356    59.2 |  3.899 % |
c |     36623 |   25294    82772 |   14936    6918   441267    63.8 |  3.899 % |
c |     37763 |   25294    82772 |   16429    8058   574366    71.3 |  3.899 % |
c ==============================================================================
c [1mFound solution: 1458688[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38579 |   25307    82802 |    8435    8874   681730    76.8 |  3.899 % |
c |     38679 |   25307    82802 |    9278    4537   324758    71.6 |  3.910 % |
c |     38830 |   25296    82778 |   10206    4686   329928    70.4 |  3.953 % |
c |     39055 |   25280    82743 |   11226    4907   340655    69.4 |  4.025 % |
c |     39392 |   25204    82492 |   12349    5238   355692    67.9 |  4.168 % |
c ==============================================================================
c [1mFound solution: 1438848[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39556 |   25216    82524 |    8405    5402   383073    70.9 |  4.168 % |
c |     39656 |   25173    82401 |    9245    5496   384861    70.0 |  4.279 % |
c |     39806 |   25173    82401 |   10170    5646   400312    70.9 |  4.279 % |
c |     40032 |   25151    82353 |   11187    5868   408033    69.5 |  4.365 % |
c |     40369 |   25106    82252 |   12305    6197   430376    69.4 |  4.566 % |
c |     40875 |   25106    82252 |   13536    6703   493435    73.6 |  4.566 % |
c |     41634 |   25106    82252 |   14889    7462   569328    76.3 |  4.566 % |
c |     42773 |   25106    82252 |   16378    8601   707090    82.2 |  4.566 % |
c |     44481 |   25032    82007 |   18016   10298   853239    82.9 |  4.709 % |
c |     47043 |   25021    81983 |   19818   12858  1115212    86.7 |  4.752 % |
c |     50892 |   24980    81840 |   21800   16699  1507898    90.3 |  4.824 % |
c ==============================================================================
c [1mFound solution: 1431808[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53691 |   24988    81862 |    8329   19495  1771927    90.9 |  4.824 % |
c |     53791 |   24988    81862 |    9161    4974   265913    53.5 |  4.847 % |
c |     53941 |   24988    81862 |   10078    5124   269820    52.7 |  4.847 % |
c |     54167 |   24988    81862 |   11085    5350   286961    53.6 |  4.847 % |
c |     54504 |   24958    81794 |   12194    5679   304170    53.6 |  4.962 % |
c |     55010 |   24958    81794 |   13413    6185   351539    56.8 |  4.962 % |
c |     55769 |   24958    81794 |   14755    6944   416677    60.0 |  4.962 % |
c |     56909 |   24958    81794 |   16230    8084   562839    69.6 |  4.962 % |
c |     58619 |   24947    81770 |   17853    9793   735565    75.1 |  5.005 % |
c |     61182 |   24920    81700 |   19639   12351   959102    77.7 |  5.091 % |
c |     65026 |   24907    81671 |   21603   16193  1315910    81.3 |  5.148 % |
c |     70795 |   24907    81671 |   23763   21962  1922551    87.5 |  5.148 % |
c |     79447 |   24865    81540 |   26139   18016  1482239    82.3 |  5.234 % |
c |     92423 |   24801    81385 |   28753   16615  1259492    75.8 |  5.464 % |
c ==============================================================================
c [1mFound solution: 1427968[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107128 |   24723    81184 |    8241   16283  1157306    71.1 |  5.464 % |
c |    107230 |   24723    81184 |    9065    8244   476372    57.8 |  5.758 % |
c |    107382 |   24723    81184 |    9971    8396   489220    58.3 |  5.759 % |
c |    107608 |   24723    81184 |   10968    8622   522291    60.6 |  5.759 % |
c |    107945 |   24723    81184 |   12065    8959   555312    62.0 |  5.758 % |
c |    108452 |   24723    81184 |   13272    9466   618197    65.3 |  5.759 % |
c |    109212 |   24678    81023 |   14599   10221   672039    65.8 |  5.787 % |
c |    110351 |   24678    81023 |   16059   11360   765864    67.4 |  5.787 % |
c |    112060 |   24678    81023 |   17665   13069  1024443    78.4 |  5.787 % |
c |    114622 |   24620    80894 |   19431   15623  1365937    87.4 |  6.031 % |
c |    118467 |   24590    80816 |   21375   19460  1763317    90.6 |  6.131 % |
c |    124235 |   24590    80816 |   23512   14161  1019179    72.0 |  6.131 % |
c |    132891 |   24551    80683 |   25863   22813  1779717    78.0 |  6.203 % |
c |    145865 |   24551    80683 |   28450   22536  2054772    91.2 |  6.203 % |
c ==============================================================================
c [1mFound solution: 1423488[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    146568 |   24563    80714 |    8187   23239  2124527    91.4 |  6.203 % |
c |    146668 |   24563    80714 |    9005    5910   256320    43.4 |  6.210 % |
c |    146819 |   24563    80714 |    9906    6061   262458    43.3 |  6.210 % |
c |    147044 |   24463    80383 |   10896    6275   285602    45.5 |  6.410 % |
c |    147381 |   24423    80256 |   11986    6604   292865    44.3 |  6.496 % |
c |    147887 |   24423    80256 |   13185    7110   338836    47.7 |  6.496 % |
c |    148646 |   24423    80256 |   14503    7869   435930    55.4 |  6.496 % |
c |    149788 |   24423    80256 |   15954    9011   542343    60.2 |  6.496 % |
c |    151497 |   24406    80218 |   17549   10719   752216    70.2 |  6.567 % |
c |    154060 |   24386    80171 |   19304   13280   990365    74.6 |  6.639 % |
c |    157906 |   24386    80171 |   21234   17126  1287121    75.2 |  6.639 % |
c |    163672 |   24340    80044 |   23358   11559   700256    60.6 |  6.796 % |
c |    172321 |   24340    80044 |   25694   20208  1333788    66.0 |  6.796 % |
c |    185296 |   24314    79967 |   28263   19623  1161767    59.2 |  6.854 % |
c |    204758 |   24314    79967 |   31090   23903  1595766    66.8 |  6.854 % |
c |    233951 |   24224    79722 |   34199   21100  1491804    70.7 |  7.154 % |
c ==============================================================================
c [1mFound solution: 1420288[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    269048 |   24088    79244 |    8029   16815  1491486    88.7 |  7.154 % |
c |    269148 |   24088    79244 |    8831    8508   640879    75.3 |  7.459 % |
c |    269298 |   24088    79244 |    9715    8658   661275    76.4 |  7.459 % |
c |    269523 |   24088    79244 |   10686    8883   678039    76.3 |  7.459 % |
c |    269860 |   24088    79244 |   11755    9220   719171    78.0 |  7.460 % |
c |    270367 |   24088    79244 |   12930    9727   729922    75.0 |  7.459 % |
c |    271127 |   24088    79244 |   14223   10487   840546    80.2 |  7.459 % |
c |    272266 |   24073    79211 |   15646   11624   968142    83.3 |  7.516 % |
c |    273975 |   24073    79211 |   17210   13333  1152071    86.4 |  7.516 % |
c |    276537 |   24045    79149 |   18931   15889  1433911    90.2 |  7.631 % |
c |    280383 |   23865    78603 |   20825   19704  1796107    91.2 |  8.117 % |
c |    286151 |   23865    78603 |   22907   14391  1054594    73.3 |  8.117 % |
c |    294801 |   23865    78603 |   25198   23041  1954414    84.8 |  8.117 % |
c |    307776 |   23854    78579 |   27718   22285  2001861    89.8 |  8.159 % |
c |    327237 |   23847    78564 |   30490   27154  2268727    83.6 |  8.188 % |
c |    356429 |   23803    78464 |   33539   24241  1688878    69.7 |  8.402 % |
c ==============================================================================
c [1mFound solution: 1416448[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    384550 |   23765    78382 |    7921   32917  2863259    87.0 |  8.402 % |
c |    384650 |   23754    78358 |    8713    7690   702581    91.4 |  8.665 % |
c |    384801 |   23754    78358 |    9584    7841   714078    91.1 |  8.665 % |
c |    385027 |   23754    78358 |   10542    8067   743664    92.2 |  8.665 % |
c |    385364 |   23754    78358 |   11597    8404   790915    94.1 |  8.665 % |
c |    385870 |   23678    78088 |   12756    8901   805477    90.5 |  8.822 % |
c |    386631 |   23678    78088 |   14032    9662   860772    89.1 |  8.822 % |
c |    387773 |   23678    78088 |   15435   10804  1046707    96.9 |  8.822 % |
c |    389481 |   23678    78088 |   16979   12512  1164690    93.1 |  8.822 % |
c |    392043 |   23678    78088 |   18677   15074  1561117   103.6 |  8.822 % |
c |    395887 |   23678    78088 |   20545   18918  1996674   105.5 |  8.822 % |
c |    401654 |   23678    78088 |   22599   13746  1222434    88.9 |  8.822 % |
c |    410306 |   23665    78059 |   24859   22395  2137343    95.4 |  8.879 % |
c |    423280 |   23647    77997 |   27345   21922  2153316    98.2 |  8.908 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 14980 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.91 2/54 14976
Raw data (stat): 14976 (runsolver) R 14975 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784262234 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.0005 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.0012 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.0021 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.0023 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.0032 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.0043 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.0049 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.73 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 14980
Raw data (stat): 14976 (minisat+_script) S 14975 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784262234 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.73
CPU time (s): 1229.84
CPU user time (s): 1229.5
CPU system time (s): 0.347947
CPU usage (%): 100.009
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####