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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-1.opb
MD5SUM	16a8eb66aae2bcfd534a482dd0a3948e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	27856
Number of constraints which are clauses	27856
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5235

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-13 22:46:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3703 boxname=wulflinc17 idbench=319 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  16a8eb66aae2bcfd534a482dd0a3948e  /oldhome/oroussel/tmp/wulflinc17/normalized-frb35-17-1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc17/normalized-frb35-17-1.opb /oldhome/oroussel/tmp/wulflinc17/normalized-frb35-17-1.opb
IDLAUNCH: 3703
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        828736 kB
Buffers:         34404 kB
Cached:         136960 kB
SwapCached:       2376 kB
Active:          54836 kB
Inactive:       121860 kB
HighTotal:      131008 kB
HighFree:         1260 kB
LowTotal:       903652 kB
LowFree:        827476 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23732 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:06:50 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3703 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27856 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27856    55712 |    9285       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1165   maxlim: 25   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   35814    84166 |   11938       0        0     nan |  0.000 % |
c |       100 |   35814    84166 |   13131     100      705     7.0 |  0.176 % |
c |       250 |   35805    84135 |   14444     248     2177     8.8 |  0.235 % |
c |       475 |   35787    84073 |   15889     468     5551    11.9 |  0.348 % |
c |       812 |   35715    83825 |   17478     783     9564    12.2 |  0.807 % |
c |      1318 |   35631    83537 |   19226    1269    15670    12.3 |  1.375 % |
c |      2077 |   35595    83413 |   21148    2017    28314    14.0 |  1.661 % |
c |      3216 |   35310    82434 |   23263    3071    47592    15.5 |  3.728 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 26   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4435 |   34806    80710 |   11602    4158    69333    16.7 |  3.728 % |
c |      4535 |   34748    80510 |   12762    4244    70627    16.6 |  8.467 % |
c |      4685 |   34720    80412 |   14038    4386    73407    16.7 |  8.759 % |
c |      4910 |   34597    79989 |   15442    4575    77363    16.9 |  9.783 % |
c |      5247 |   34547    79821 |   16986    4901    99226    20.2 | 10.240 % |
c |      5753 |   34076    78198 |   18685    5278   110091    20.9 | 14.989 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 27   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6143 |   33979    77865 |   11326    5613   122167    21.8 | 14.989 % |
c |      6243 |   33935    77711 |   12458    5705   124250    21.8 | 16.467 % |
c |      6393 |   33935    77711 |   13704    5855   130201    22.2 | 16.471 % |
c |      6618 |   33926    77680 |   15074    6072   141150    23.2 | 16.529 % |
c |      6955 |   33871    77491 |   16582    6391   150985    23.6 | 17.038 % |
c |      7461 |   33735    77019 |   18240    6856   170093    24.8 | 18.417 % |
c |      8220 |   33703    76905 |   20064    7598   197504    26.0 | 18.817 % |
c |      9359 |   33697    76885 |   22071    8734   279186    32.0 | 18.868 % |
c |     11067 |   33652    76730 |   24278   10378   390937    37.7 | 19.268 % |
c |     13629 |   33652    76730 |   26706   12940   596660    46.1 | 19.273 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 28   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16251 |   33655    76743 |   11218   15562   782263    50.3 | 19.273 % |
c |     16351 |   33655    76743 |   12339    7881   454462    57.7 | 19.320 % |
c |     16501 |   33655    76743 |   13573    8031   463913    57.8 | 19.314 % |
c |     16726 |   33526    76292 |   14931    8237   470241    57.1 | 20.686 % |
c |     17063 |   33514    76252 |   16424    8565   480466    56.1 | 20.804 % |
c |     17569 |   33478    76126 |   18066    9060   506939    56.0 | 21.205 % |
c |     18328 |   33478    76126 |   19873    9819   542283    55.2 | 21.200 % |
c |     19467 |   33440    75994 |   21860   10952   616285    56.3 | 21.600 % |
c |     21175 |   33416    75912 |   24046   12639   712901    56.4 | 21.776 % |
c |     23737 |   33416    75912 |   26451   15201   896371    59.0 | 21.771 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24838 |   33417    75918 |   11139   16302   965146    59.2 | 21.771 % |
c |     24939 |   33408    75887 |   12252    8248   392106    47.5 | 21.880 % |
c |     25090 |   33408    75887 |   13478    8399   396822    47.2 | 21.873 % |
c |     25316 |   33381    75794 |   14826    8609   405014    47.0 | 22.045 % |
c |     25657 |   33372    75763 |   16308    8933   420738    47.1 | 22.107 % |
c |     26166 |   33363    75732 |   17939    9431   448398    47.5 | 22.159 % |
c |     26925 |   33363    75732 |   19733   10190   499152    49.0 | 22.164 % |
c |     28064 |   33352    75693 |   21706   11325   565451    49.9 | 22.279 % |
c |     29772 |   33308    75543 |   23877   13009   650914    50.0 | 22.673 % |
c |     32336 |   33287    75468 |   26265   15570   847499    54.4 | 22.958 % |
c |     36184 |   33278    75437 |   28891   19403  1128932    58.2 | 23.015 % |
c |     41950 |   33251    75344 |   31780   25163  1583526    62.9 | 23.301 % |
c |     50600 |   33239    75304 |   34958   16090  1102856    68.5 | 23.415 % |
c |     63575 |   33214    75217 |   38454   29061  2182085    75.1 | 23.701 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69859 |   33215    75224 |   11071   35345  2522726    71.4 | 23.701 % |
c |     69959 |   33215    75224 |   12178    7598   304915    40.1 | 23.750 % |
c |     70109 |   33196    75157 |   13395    7744   307642    39.7 | 23.976 % |
c |     70336 |   33196    75157 |   14735    7971   320278    40.2 | 23.979 % |
c |     70674 |   33196    75157 |   16209    8309   336995    40.6 | 23.973 % |
c |     71182 |   33196    75157 |   17829    8817   363903    41.3 | 23.973 % |
c |     71941 |   33196    75157 |   19612    9576   399833    41.8 | 23.973 % |
c |     73081 |   33196    75157 |   21574   10716   469650    43.8 | 23.976 % |
c |     74789 |   33181    75106 |   23731   12416   574778    46.3 | 24.087 % |
c |     77351 |   33181    75106 |   26104   14978   758785    50.7 | 24.087 % |
c |     81196 |   33132    74937 |   28715   18805   985279    52.4 | 24.548 % |
c |     86962 |   33132    74937 |   31586   24571  1474463    60.0 | 24.543 % |
c |     95611 |   33132    74937 |   34745   15141   905025    59.8 | 24.543 % |
c |    108585 |   33132    74937 |   38220   28115  1969322    70.0 | 24.548 % |
c |    128046 |   33121    74898 |   42042   22627  1840477    81.3 | 24.658 % |
c |    157238 |   33113    74870 |   46246   22440  2762184   123.1 | 24.772 % |
c |    201028 |   33095    74808 |   50870   32649  5803781   177.8 | 24.886 % |
c |    266712 |   33067    74710 |   55958   24444  3234796   132.3 | 25.171 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    281935 |   33013    74509 |   11004   39558  4597370   116.2 | 25.171 % |
c |    282035 |   33013    74509 |   12104    7007   551970    78.8 | 25.685 % |
c |    282186 |   33013    74509 |   13314    7158   554251    77.4 | 25.685 % |
c |    282411 |   33013    74509 |   14646    7383   558970    75.7 | 25.685 % |
c |    282748 |   33013    74509 |   16110    7720   568266    73.6 | 25.685 % |
c |    283254 |   33013    74509 |   17722    8226   586705    71.3 | 25.685 % |
c |    284013 |   33013    74509 |   19494    8985   616773    68.6 | 25.690 % |
c |    285153 |   33013    74509 |   21443   10125   726500    71.8 | 25.690 % |
c |    286861 |   33013    74509 |   23588   11833   888226    75.1 | 25.685 % |
c |    289423 |   33013    74509 |   25946   14395  1040824    72.3 | 25.685 % |
c |    293267 |   33013    74509 |   28541   18239  1251436    68.6 | 25.685 % |
c |    299033 |   33004    74478 |   31395   23999  1854285    77.3 | 25.742 % |
c |    307682 |   33004    74478 |   34535   14235  1117370    78.5 | 25.742 % |
c |    320657 |   32964    74342 |   37988   27187  1979445    72.8 | 26.142 % |
c |    340119 |   32932    74230 |   41787   22233  1262914    56.8 | 26.484 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    349994 |   33001    74453 |   11000   32104  2088720    65.1 | 26.484 % |
c |    350095 |   33001    74453 |   12100    7499   455067    60.7 | 26.626 % |
c |    350245 |   33001    74453 |   13310    7649   460545    60.2 | 26.624 % |
c |    350473 |   33001    74453 |   14641    7877   467354    59.3 | 26.622 % |
c |    350811 |   33001    74453 |   16105    8215   481472    58.6 | 26.622 % |
c |    351317 |   33001    74453 |   17715    8721   505832    58.0 | 26.622 % |
c |    352076 |   33001    74453 |   19487    9480   538637    56.8 | 26.622 % |
c |    353217 |   32978    74374 |   21435   10619   587355    55.3 | 26.847 % |
c |    354927 |   32978    74374 |   23579   12329   704072    57.1 | 26.852 % |
c |    357489 |   32978    74374 |   25937   14891   883014    59.3 | 26.847 % |
c |    361335 |   32978    74374 |   28531   18737  1334548    71.2 | 26.851 % |
c |    367101 |   32935    74225 |   31384   24464  1843134    75.3 | 27.242 % |
c |    375750 |   32922    74178 |   34522   15385   858927    55.8 | 27.411 % |
c |    388724 |   32922    74178 |   37974   28359  1631402    57.5 | 27.411 % |
c |    408185 |   32922    74178 |   41772   23120  1253731    54.2 | 27.417 % |
c |    437377 |   32883    74045 |   45949   23795  1419448    59.7 | 27.811 % |
c |    481167 |   32883    74045 |   50544   34790  2591719    74.5 | 27.806 % |
c |    546851 |   32883    74045 |   55599   28209  2258913    80.1 | 27.810 % |
c |    645379 |   32883    74045 |   61159   46095  2871475    62.3 | 27.810 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/55 26044
Raw data (stat): 26044 (runsolver) R 26043 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479669664 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0002 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 1675 0 0 0 994 4 0 0 25 0 1 0 479669664 8359936 1653 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2041 1653 603 41 0 2000 0
vsize: 8164
[startup+20 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 1991 0 0 0 1993 5 0 0 25 0 1 0 479669664 9691136 1969 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2366 1969 603 41 0 2325 0
vsize: 9464
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 2698 0 0 0 2991 7 0 0 25 0 1 0 479669664 12648448 2676 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3088 2676 603 41 0 3047 0
vsize: 12352
[startup+40.001 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 3429 0 0 0 3987 9 0 0 25 0 1 0 479669664 15593472 3407 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3807 3407 603 41 0 3766 0
vsize: 15228
[startup+50.0011 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 3447 0 0 0 4987 9 0 0 25 0 1 0 479669664 15593472 3425 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3807 3425 603 41 0 3766 0
vsize: 15228
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 3646 0 0 0 5987 10 0 0 25 0 1 0 479669664 16523264 3624 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4034 3624 603 41 0 3993 0
vsize: 16136
[startup+70.0008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 3787 0 0 0 6986 11 0 0 25 0 1 0 479669664 17162240 3765 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4190 3765 603 41 0 4149 0
vsize: 16760
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 3787 0 0 0 7986 11 0 0 25 0 1 0 479669664 17162240 3765 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4190 3765 603 41 0 4149 0
vsize: 16760
[startup+90.0013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 3787 0 0 0 8986 11 0 0 25 0 1 0 479669664 17162240 3765 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4190 3765 603 41 0 4149 0
vsize: 16760
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 3787 0 0 0 9987 11 0 0 25 0 1 0 479669664 17162240 3765 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4190 3765 603 41 0 4149 0
vsize: 16760
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 3787 0 0 0 10987 11 0 0 25 0 1 0 479669664 17162240 3765 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4190 3765 603 41 0 4149 0
vsize: 16760
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 4328 0 0 0 11985 12 0 0 25 0 1 0 479669664 19296256 4306 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4711 4306 603 41 0 4670 0
vsize: 18844
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 4349 0 0 0 12986 12 0 0 25 0 1 0 479669664 19427328 4327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4743 4327 603 41 0 4702 0
vsize: 18972
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 4349 0 0 0 13986 12 0 0 25 0 1 0 479669664 19427328 4327 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4743 4327 603 41 0 4702 0
vsize: 18972
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 4537 0 0 0 14985 13 0 0 25 0 1 0 479669664 20221952 4515 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4937 4515 603 41 0 4896 0
vsize: 19748
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 5237 0 0 0 15984 14 0 0 25 0 1 0 479669664 23007232 5215 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5617 5215 603 41 0 5576 0
vsize: 22468
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 5766 0 0 0 16983 16 0 0 25 0 1 0 479669664 25272320 5744 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6170 5744 603 41 0 6129 0
vsize: 24680
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 5774 0 0 0 17983 16 0 0 25 0 1 0 479669664 25272320 5752 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6170 5752 603 41 0 6129 0
vsize: 24680
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 5774 0 0 0 18983 16 0 0 25 0 1 0 479669664 25272320 5752 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6170 5752 603 41 0 6129 0
vsize: 24680
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 5774 0 0 0 19983 16 0 0 25 0 1 0 479669664 25272320 5752 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6170 5752 603 41 0 6129 0
vsize: 24680
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 5949 0 0 0 20983 17 0 0 25 0 1 0 479669664 25948160 5927 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6335 5927 603 41 0 6294 0
vsize: 25340
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26044
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 6622 0 0 0 21981 19 0 0 25 0 1 0 479669664 28798976 6600 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7031 6600 603 41 0 6990 0
vsize: 28124
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 7275 0 0 0 22980 20 0 0 25 0 1 0 479669664 31354880 7253 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7655 7254 603 41 0 7614 0
vsize: 30620
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 7437 0 0 0 23980 20 0 0 25 0 1 0 479669664 32030720 7415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7820 7415 603 41 0 7779 0
vsize: 31280
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 7437 0 0 0 24980 20 0 0 25 0 1 0 479669664 32030720 7415 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7820 7415 603 41 0 7779 0
vsize: 31280
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 7437 0 0 0 25980 20 0 0 25 0 1 0 479669664 32030720 7415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7820 7415 603 41 0 7779 0
vsize: 31280
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 7438 0 0 0 26980 20 0 0 25 0 1 0 479669664 32030720 7416 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7820 7416 603 41 0 7779 0
vsize: 31280
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 7766 0 0 0 27980 21 0 0 25 0 1 0 479669664 33386496 7744 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8151 7744 603 41 0 8110 0
vsize: 32604
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 8298 0 0 0 28979 22 0 0 25 0 1 0 479669664 35540992 8276 4294967295 134512640 134672761 3221224560 3221223744 134559575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8677 8276 603 41 0 8636 0
vsize: 34708
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 8811 0 0 0 29977 24 0 0 25 0 1 0 479669664 37695488 8789 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9203 8789 603 41 0 9162 0
vsize: 36812
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9297 0 0 0 30976 25 0 0 25 0 1 0 479669664 39718912 9275 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9697 9275 603 41 0 9656 0
vsize: 38788
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9658 0 0 0 31975 27 0 0 25 0 1 0 479669664 41189376 9636 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10056 9636 603 41 0 10015 0
vsize: 40224
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 32974 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 33975 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 34975 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 35975 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 36975 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 37975 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223744 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 38976 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 39976 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 40976 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 41976 27 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 42975 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 43975 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223724 134559748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 44975 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 45976 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223696 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 46976 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 47976 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 48976 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223696 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 49976 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 50976 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+520.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26046
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 51976 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 52977 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 53977 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 54977 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 55977 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+570.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 56977 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+580.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 57978 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 58978 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 59978 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 60978 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 61978 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 62979 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 63979 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+650.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 64979 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 65979 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 66980 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 67980 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 68980 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 69980 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9775 0 0 0 70980 28 0 0 25 0 1 0 479669664 41590784 9753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9753 603 41 0 10113 0
vsize: 40616
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 71980 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 72981 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 73981 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 74981 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 75981 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+770.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 76981 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+780.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 77982 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26048
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 78982 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+800.031 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 26089
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 79984 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+810.032 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 26101
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 80985 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+820.031 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 26101
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 81985 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+830.032 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 26103
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 82985 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+840.033 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 26103
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 83985 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+850.032 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 26103
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 84986 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+860.032 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 26103
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 85986 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+870.031 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26103
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 86986 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+880.032 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 87986 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+890.032 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 88986 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223664 134554877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+900.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 89986 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+910.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9776 0 0 0 90986 28 0 0 25 0 1 0 479669664 41590784 9754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9754 603 41 0 10113 0
vsize: 40616
[startup+920.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9777 0 0 0 91986 28 0 0 25 0 1 0 479669664 41590784 9755 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9755 603 41 0 10113 0
vsize: 40616
[startup+930.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 92986 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223716 134565154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+940.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 93987 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+950.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 94987 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+960.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 95987 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+970.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 96987 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+980.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 97987 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+990.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 98987 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 99988 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 100988 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 101988 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 102988 28 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 103988 29 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9780 0 0 0 104987 29 0 0 25 0 1 0 479669664 41590784 9758 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10154 9758 603 41 0 10113 0
vsize: 40616
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9781 0 0 0 105987 29 0 0 25 0 1 0 479669664 41590784 9759 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9759 603 41 0 10113 0
vsize: 40616
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9784 0 0 0 106987 29 0 0 25 0 1 0 479669664 41590784 9762 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9762 603 41 0 10113 0
vsize: 40616
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 107987 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 108987 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 109987 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 110987 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1120.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 26105
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 111988 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1130.03 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 26107
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 112988 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223744 134558836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1140.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 26109
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 113988 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1150.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 26109
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 114988 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1160.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 26109
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 115988 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1170.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 26109
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 116988 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223664 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1180.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 26109
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9786 0 0 0 117989 29 0 0 25 0 1 0 479669664 41590784 9764 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 9764 603 41 0 10113 0
vsize: 40616
[startup+1190.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 26109
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 9943 0 0 0 118989 30 0 0 25 0 1 0 479669664 42328064 9921 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10334 9921 603 41 0 10293 0
vsize: 41336
[startup+1200.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 26109
Raw data (stat): 26044 (minisat+) R 26043 20838 20837 0 -1 0 10342 0 0 0 119988 30 0 0 25 0 1 0 479669664 43937792 10320 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10727 10320 603 41 0 10686 0
vsize: 42908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.02 1.00 0.92 1/55 26109
Raw data (stat): 26044 (minisat+) Z 26043 20838 20837 0 -1 12 10346 0 0 0 119988 32 0 0 25 0 1 0 479669664 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.88
CPU system time (s): 0.328949
CPU usage (%): 100.014
Max. virtual memory (Kb): 42908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####