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/miplib3/normalized-mps-v2-13-7-mkc.opb
MD5SUM	b9e9aa470fdb3341d7e10860fcc70cec
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	2946
Biggest coefficient in the objective function	20000
Number of bits for the biggest coefficient in the objective function	15
Sum of the numbers in the objective function	31442101
Number of bits of the sum of numbers in the objective function	25
Biggest number in a constraint	65536000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	629010691
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.11
Number of variables	5363
Total number of constraints	8734
Number of constraints which are clauses	2977
Number of constraints which are cardinality constraints (but not clauses)	5731
Number of constraints which are nor clauses,nor cardinality constraints	26
Minimum length of a constraint	1
Maximum length of a constraint	2942
Trace number 15069

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 02:49:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18616 boxname=wulflinc2 idbench=1432 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b9e9aa470fdb3341d7e10860fcc70cec  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-mkc.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-mkc.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-mkc.opb
IDLAUNCH: 18616
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        813792 kB
Buffers:         28024 kB
Cached:         169788 kB
SwapCached:          0 kB
Active:          35972 kB
Inactive:       164684 kB
HighTotal:      131008 kB
HighFree:        41804 kB
LowTotal:       903652 kB
LowFree:        771988 kB
SwapTotal:     2097136 kB
SwapFree:      2096988 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            14568 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:09:34 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 18616 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3225 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[3223]---> Adder-cost: 26498   maxlim: 479706816   bits: 29/29
c ---[3222]---> BDD-cost: 2265
c ---[3221]---> BDD-cost:   25
c ---[3210]---> BDD-cost:   23
c ---[3199]---> BDD-cost:    9
c ---[3188]---> BDD-cost:   21
c ---[3177]---> BDD-cost:   27
c ---[3138]---> BDD-cost:  461
c ---[3135]---> BDD-cost:    5
c ---[3114]---> Adder-cost: 1804   maxlim: 2264275   bits: 22/22
c ---[3113]---> BDD-cost:   29
c ---[3102]---> BDD-cost:   19
c ---[3091]---> BDD-cost:    7
c ---[3080]---> BDD-cost:    5
c ---[3069]---> BDD-cost:    5
c ---[3058]---> BDD-cost:    5
c ---[3037]---> BDD-cost:   29
c ---[3026]---> BDD-cost:   27
c ---[3015]---> BDD-cost:   27
c ---[3004]---> BDD-cost: 3790
c ---[3003]---> BDD-cost:    5
c ---[2992]---> BDD-cost:    5
c ---[2981]---> BDD-cost:   29
c ---[2970]---> BDD-cost:   27
c ---[2959]---> BDD-cost:   11
c ---[2948]---> BDD-cost:    9
c ---[2930]---> BDD-cost:  485
c ---[2927]---> BDD-cost:   19
c ---[2916]---> BDD-cost:   19
c ---[2905]---> BDD-cost:   27
c ---[2894]---> BDD-cost: 1005
c ---[2893]---> BDD-cost:   19
c ---[2872]---> BDD-cost:   21
c ---[2839]---> BDD-cost:   19
c ---[2828]---> BDD-cost:   19
c ---[2796]---> BDD-cost:   21
c ---[2785]---> Sorter-cost:17311     Base: 5 2 5 2 3 2 2 2 2 2
c ---[2784]---> BDD-cost:    3
c ---[2773]---> BDD-cost:   29
c ---[2752]---> BDD-cost:   29
c ---[2741]---> BDD-cost:   27
c ---[2730]---> BDD-cost:   29
c ---[2711]---> BDD-cost:  461
c ---[2699]---> BDD-cost:    3
c ---[2688]---> BDD-cost:   13
c ---[2677]---> Adder-cost: 1438   maxlim: 1767687   bits: 21/21
c ---[2665]---> BDD-cost:    3
c ---[2654]---> BDD-cost:    3
c ---[2632]---> BDD-cost:    3
c ---[2621]---> BDD-cost:    3
c ---[2610]---> BDD-cost:   21
c ---[2589]---> BDD-cost:   23
c ---[2568]---> Adder-cost: 1090   maxlim: 131883   bits: 18/18
c ---[2567]---> BDD-cost:    3
c ---[2524]---> BDD-cost:    3
c ---[2505]---> BDD-cost:  461
c ---[2503]---> BDD-cost:   23
c ---[2472]---> BDD-cost:   29
c ---[2461]---> Sorter-cost:10972     Base: 2 5 5 3 11 3 2
c ---[2460]---> BDD-cost:   29
c ---[2438]---> BDD-cost:    3
c ---[2367]---> BDD-cost:   27
c ---[2356]---> BDD-cost: 1027
c ---[2355]---> BDD-cost:   29
c ---[2324]---> BDD-cost:    3
c ---[2305]---> BDD-cost:  461
c ---[2283]---> BDD-cost:    3
c ---[2261]---> BDD-cost:    3
c ---[2250]---> BDD-cost:  196
c ---[2239]---> BDD-cost:    5
c ---[2218]---> BDD-cost:   11
c ---[2207]---> BDD-cost:    7
c ---[2196]---> BDD-cost:   15
c ---[2166]---> BDD-cost:   19
c ---[2143]---> Adder-cost: 477   maxlim: 2053920   bits: 22/21
c ---[2142]---> BDD-cost:   81
c ---[2141]---> BDD-cost:   19
c ---[2130]---> BDD-cost:   19
c ---[2119]---> BDD-cost:   17
c ---[2108]---> BDD-cost:   17
c ---[2099]---> BDD-cost:  527
c ---[2097]---> BDD-cost:   19
c ---[2086]---> BDD-cost:   19
c ---[2075]---> BDD-cost:   19
c ---[2033]---> BDD-cost:  171
c ---[2011]---> BDD-cost:   19
c ---[2000]---> BDD-cost:   17
c ---[1989]---> BDD-cost:   19
c ---[1978]---> BDD-cost:   19
c ---[1967]---> BDD-cost:   19
c ---[1946]---> BDD-cost:   21
c ---[1935]---> BDD-cost:   19
c ---[1924]---> BDD-cost:  131
c ---[1923]---> BDD-cost:   17
c ---[1912]---> BDD-cost:   19
c ---[1880]---> BDD-cost:    3
c ---[1869]---> BDD-cost:   15
c ---[1865]---> BDD-cost:  551
c ---[1858]---> BDD-cost:   13
c ---[1848]---> BDD-cost:   19
c ---[1827]---> BDD-cost:   19
c ---[1816]---> BDD-cost:   74
c ---[1815]---> BDD-cost:   19
c ---[1794]---> BDD-cost:   19
c ---[1773]---> BDD-cost:   19
c ---[1752]---> BDD-cost:   19
c ---[1741]---> BDD-cost:   19
c ---[1712]---> BDD-cost:   51
c ---[1711]---> BDD-cost:   15
c ---[1693]---> BDD-cost:   19
c ---[1672]---> BDD-cost:    3
c ---[1661]---> BDD-cost:   15
c ---[1650]---> BDD-cost:   19
c ---[1639]---> BDD-cost:   19
c ---[1628]---> BDD-cost:   19
c ---[1627]---> BDD-cost:  488
c ---[1612]---> BDD-cost:   29
c ---[1611]---> BDD-cost:   17
c ---[1602]---> BDD-cost:   19
c ---[1594]---> BDD-cost:   19
c ---[1577]---> BDD-cost:   19
c ---[1558]---> BDD-cost:   19
c ---[1547]---> BDD-cost:   15
c ---[1526]---> BDD-cost:   17
c ---[1518]---> BDD-cost:    3
c ---[1513]---> BDD-cost:   17
c ---[1482]---> BDD-cost:    7
c ---[1462]---> BDD-cost:  335
c ---[1451]---> BDD-cost:    3
c ---[1430]---> BDD-cost:   17
c ---[1339]---> BDD-cost:   17
c ---[1338]---> BDD-cost:   11
c ---[1327]---> BDD-cost:    7
c ---[1316]---> BDD-cost:  416
c ---[1306]---> BDD-cost:   17
c ---[1295]---> BDD-cost:    5
c ---[1284]---> BDD-cost:    3
c ---[1273]---> BDD-cost:    3
c ---[1262]---> BDD-cost:    7
c ---[1251]---> BDD-cost:    7
c ---[1240]---> BDD-cost:   19
c ---[1229]---> BDD-cost:   19
c ---[1218]---> BDD-cost:   19
c ---[1207]---> BDD-cost:    5
c ---[1196]---> BDD-cost:   17
c ---[1185]---> BDD-cost:   19
c ---[1163]---> BDD-cost:   29
c ---[1152]---> BDD-cost:   29
c ---[1141]---> BDD-cost:   29
c ---[1130]---> BDD-cost:   29
c ---[1128]---> BDD-cost:  260
c ---[1119]---> Adder-cost: 2340   maxlim: 3201964   bits: 22/22
c ---[1118]---> BDD-cost:   21
c ---[1117]---> BDD-cost:   29
c ---[1106]---> BDD-cost:   23
c ---[1095]---> BDD-cost:   17
c ---[1084]---> BDD-cost:   17
c ---[1073]---> BDD-cost:   17
c ---[1062]---> BDD-cost:    7
c ---[1051]---> BDD-cost:    7
c ---[1019]---> BDD-cost:   21
c ---[1008]---> BDD-cost:   29
c ---[1007]---> BDD-cost:    7
c ---[ 996]---> BDD-cost:    5
c ---[ 988]---> BDD-cost:  212
c ---[ 985]---> BDD-cost:    5
c ---[ 974]---> BDD-cost:    5
c ---[ 963]---> BDD-cost:    7
c ---[ 952]---> BDD-cost:    9
c ---[ 931]---> BDD-cost:    5
c ---[ 920]---> BDD-cost:   21
c ---[ 909]---> BDD-cost:   17
c ---[ 891]---> BDD-cost:  161
c ---[ 888]---> BDD-cost:   27
c ---[ 877]---> BDD-cost:   17
c ---[ 866]---> BDD-cost:   17
c ---[ 855]---> BDD-cost:   27
c ---[ 844]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   65
c ---[ 813]---> BDD-cost:   27
c ---[ 802]---> BDD-cost:   19
c ---[ 790]---> BDD-cost:   29
c ---[ 780]---> BDD-cost:   32
c ---[ 779]---> BDD-cost:   23
c ---[ 761]---> BDD-cost:   50
c ---[ 739]---> BDD-cost:   38
c ---[ 738]---> BDD-cost:   21
c ---[ 727]---> BDD-cost:   23
c ---[ 719]---> BDD-cost:   26
c ---[ 704]---> BDD-cost:   17
c ---[ 695]---> BDD-cost:   21
c ---[ 689]---> BDD-cost:   17
c ---[ 684]---> BDD-cost:   11
c ---[ 683]---> BDD-cost:   23
c ---[ 678]---> BDD-cost:   14
c ---[ 672]---> BDD-cost:   11
c ---[ 669]---> BDD-cost:   19
c ---[ 666]---> BDD-cost:   19
c ---[ 664]---> BDD-cost:   29
c ---[ 663]---> BDD-cost:   29
c ---[ 662]---> BDD-cost:   19
c ---[ 661]---> BDD-cost:   29
c ---[ 660]---> BDD-cost:   29
c ---[ 659]---> BDD-cost:   23
c ---[ 658]---> BDD-cost:   25
c ---[ 657]---> BDD-cost:   29
c ---[ 656]---> BDD-cost:   27
c ---[ 655]---> BDD-cost:   19
c ---[ 654]---> BDD-cost:   19
c ---[ 653]---> BDD-cost:   19
c ---[ 652]---> BDD-cost:   19
c ---[ 651]---> BDD-cost:   19
c ---[ 650]---> BDD-cost:   17
c ---[ 649]---> BDD-cost:   19
c ---[ 648]---> BDD-cost:    9
c ---[ 647]---> BDD-cost:   19
c ---[ 644]---> BDD-cost:   23
c ---[ 643]---> BDD-cost:   27
c ---[ 642]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:   19
c ---[ 640]---> BDD-cost:    3
c ---[ 639]---> BDD-cost:   25
c ---[ 637]---> BDD-cost:   23
c ---[ 636]---> BDD-cost:   27
c ---[ 635]---> BDD-cost:   21
c ---[ 634]---> BDD-cost:   15
c ---[ 633]---> BDD-cost:   15
c ---[ 628]---> BDD-cost:    3
c ---[ 627]---> BDD-cost: 1925
c ---[ 626]---> BDD-cost:    5
c ---[ 625]---> BDD-cost:   29
c ---[ 624]---> BDD-cost:   29
c ---[ 623]---> BDD-cost:   29
c ---[ 622]---> BDD-cost:   29
c ---[ 621]---> BDD-cost:   19
c ---[ 620]---> BDD-cost:   21
c ---[ 619]---> BDD-cost:   19
c ---[ 618]---> BDD-cost:   19
c ---[ 616]---> BDD-cost:   19
c ---[ 615]---> BDD-cost:   19
c ---[ 614]---> BDD-cost:   17
c ---[ 613]---> BDD-cost:   19
c ---[ 612]---> BDD-cost:   15
c ---[ 611]---> BDD-cost:   27
c ---[ 610]---> BDD-cost:    3
c ---[ 609]---> BDD-cost:    9
c ---[ 608]---> BDD-cost:    9
c ---[ 607]---> BDD-cost:    7
c ---[ 606]---> BDD-cost:   19
c ---[ 604]---> BDD-cost:   29
c ---[ 603]---> BDD-cost:   23
c ---[ 602]---> BDD-cost:   21
c ---[ 601]---> BDD-cost:   27
c ---[ 600]---> BDD-cost:   23
c ---[ 598]---> BDD-cost:   23
c ---[ 597]---> BDD-cost:   19
c ---[ 596]---> BDD-cost:   29
c ---[ 595]---> BDD-cost:   27
c ---[ 594]---> BDD-cost:   23
c ---[ 593]---> BDD-cost:   25
c ---[ 592]---> BDD-cost:   19
c ---[ 591]---> BDD-cost:   23
c ---[ 590]---> BDD-cost:   27
c ---[ 584]---> BDD-cost:   23
c ---[ 581]---> BDD-cost:   23
c ---[ 580]---> BDD-cost:   19
c ---[ 579]---> BDD-cost:  659
c ---[ 575]---> BDD-cost:   29
c ---[ 554]---> BDD-cost:   19
c ---[ 543]---> Adder-cost: 1584   maxlim: 1898736   bits: 21/21
c ---[ 542]---> BDD-cost:   19
c ---[ 477]---> BDD-cost:   29
c ---[ 466]---> BDD-cost:   23
c ---[ 444]---> BDD-cost:   15
c ---[ 433]---> Adder-cost: 1568   maxlim: 1898736   bits: 21/21
c ---[ 422]---> BDD-cost:   23
c ---[ 400]---> BDD-cost:    5
c ---[ 378]---> BDD-cost:   27
c ---[ 367]---> BDD-cost:   11
c ---[ 356]---> BDD-cost:   29
c ---[ 345]---> BDD-cost:   19
c ---[ 324]---> Adder-cost: 1704   maxlim: 2180627   bits: 22/22
c ---[ 312]---> BDD-cost:   21
c ---[ 279]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:   29
c ---[ 260]---> BDD-cost:  305
c ---[ 246]---> BDD-cost:   29
c ---[ 235]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:   29
c ---[ 213]---> Adder-cost: 1576   maxlim: 1898736   bits: 21/21
c ---[ 212]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   15
c ---[ 190]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   23
c ---[ 158]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:  461
c ---[ 115]---> BDD-cost:    5
c ---[ 105]---> Adder-cost: 1630   maxlim: 1978736   bits: 21/21
c ---[  83]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   27
c ---[  61]---> BDD-cost:    5
c ---[  40]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  461410  1485049 |  153803       0        0     nan |  0.000 % |
c |       100 |  461043  1483794 |  169183      46      131     2.8 |  0.779 % |
c |       250 |  460895  1483378 |  186101     179     1632     9.1 |  0.814 % |
c |       475 |  460881  1483332 |  204711     368     5358    14.6 |  0.816 % |
c |       812 |  460881  1483332 |  225182     705    15475    22.0 |  0.816 % |
c |      1319 |  460881  1483332 |  247701    1212    43424    35.8 |  0.816 % |
c |      2078 |  460881  1483332 |  272471    1971    68179    34.6 |  0.816 % |
c |      3217 |  460584  1482289 |  299718    1725    32091    18.6 |  0.871 % |
c |      4925 |  460364  1481511 |  329690    3355    98483    29.4 |  0.914 % |
c |      7488 |  460268  1481193 |  362659    5904   228276    38.7 |  0.936 % |
c |     11332 |  458920  1477448 |  398925    9128   392619    43.0 |  1.277 % |
c |     17098 |  458259  1475233 |  438817   14574   596570    40.9 |  1.408 % |
c |     25748 |  456823  1471181 |  482699   22288   901893    40.5 |  1.778 % |
c |     38722 |  451079  1454518 |  530969   33212  1356238    40.8 |  3.257 % |
c |     58184 |  447142  1442999 |  584066   49694  1984102    39.9 |  4.187 % |
c |     87376 |  437672  1419569 |  642473   77699  3119799    40.2 |  7.179 % |
c |    131166 |  434055  1409723 |  706720  118805  5264900    44.3 |  8.167 % |
c |    196851 |  432908  1406485 |  777392  184232  7678843    41.7 |  8.461 % |
#### 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.84 0.94 0.95 2/54 17172
Raw data (stat): 17172 (runsolver) R 17171 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483387831 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 3566 0 0 0 989 10 0 0 25 0 1 0 483387831 10706944 2139 4294967295 134512640 134672761 3221224560 3221222256 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2614 2139 603 41 0 2573 0
vsize: 10456
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.94 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 3566 0 0 0 1989 10 0 0 25 0 1 0 483387831 10706944 2139 4294967295 134512640 134672761 3221224560 3221222112 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2614 2139 603 41 0 2573 0
vsize: 10456
[startup+30.0006 s]
Raw data (loadavg): 0.90 0.94 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 9138 0 0 0 2976 23 0 0 25 0 1 0 483387831 27418624 6053 4294967295 134512640 134672761 3221224560 3221222048 134544189 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6694 6053 603 41 0 6653 0
vsize: 26776
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.94 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 16365 0 0 0 3955 43 0 0 25 0 1 0 483387831 59797504 13262 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14599 13262 603 41 0 14558 0
vsize: 58396
[startup+50.0004 s]
Raw data (loadavg): 0.93 0.94 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 16525 0 0 0 4955 43 0 0 25 0 1 0 483387831 60334080 13422 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 13422 603 41 0 14689 0
vsize: 58920
[startup+60.0004 s]
Raw data (loadavg): 0.94 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 16743 0 0 0 5954 44 0 0 25 0 1 0 483387831 61296640 13640 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14965 13640 603 41 0 14924 0
vsize: 59860
[startup+70.0008 s]
Raw data (loadavg): 0.95 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 16874 0 0 0 6953 45 0 0 25 0 1 0 483387831 61698048 13771 4294967295 134512640 134672761 3221224560 3221223684 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15063 13771 603 41 0 15022 0
vsize: 60252
[startup+80.0005 s]
Raw data (loadavg): 0.96 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 16891 0 0 0 7953 45 0 0 25 0 1 0 483387831 61833216 13788 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15096 13788 603 41 0 15055 0
vsize: 60384
[startup+90.0006 s]
Raw data (loadavg): 0.96 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17053 0 0 0 8953 46 0 0 25 0 1 0 483387831 62500864 13950 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 13950 603 41 0 15218 0
vsize: 61036
[startup+99.9999 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17157 0 0 0 9952 46 0 0 25 0 1 0 483387831 62906368 14054 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15358 14054 603 41 0 15317 0
vsize: 61432
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17356 0 0 0 10952 47 0 0 25 0 1 0 483387831 63700992 14253 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15552 14253 603 41 0 15511 0
vsize: 62208
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17441 0 0 0 11951 47 0 0 25 0 1 0 483387831 64098304 14338 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15649 14338 603 41 0 15608 0
vsize: 62596
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17633 0 0 0 12951 48 0 0 25 0 1 0 483387831 64770048 14530 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15813 14530 603 41 0 15772 0
vsize: 63252
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17682 0 0 0 13951 49 0 0 25 0 1 0 483387831 65040384 14579 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15879 14579 603 41 0 15838 0
vsize: 63516
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17807 0 0 0 14950 49 0 0 25 0 1 0 483387831 65581056 14704 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16011 14704 603 41 0 15970 0
vsize: 64044
[startup+160.001 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17915 0 0 0 15950 49 0 0 25 0 1 0 483387831 65986560 14812 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16110 14812 603 41 0 16069 0
vsize: 64440
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 17973 0 0 0 16950 50 0 0 25 0 1 0 483387831 66117632 14870 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16142 14870 603 41 0 16101 0
vsize: 64568
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18084 0 0 0 17950 50 0 0 25 0 1 0 483387831 66654208 14981 4294967295 134512640 134672761 3221224560 3221223756 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16273 14981 603 41 0 16232 0
vsize: 65092
[startup+190.001 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18135 0 0 0 18950 50 0 0 25 0 1 0 483387831 66916352 15032 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16337 15032 603 41 0 16296 0
vsize: 65348
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18177 0 0 0 19949 50 0 0 25 0 1 0 483387831 67186688 15074 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16403 15074 603 41 0 16362 0
vsize: 65612
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18253 0 0 0 20949 51 0 0 25 0 1 0 483387831 67452928 15150 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16468 15150 603 41 0 16427 0
vsize: 65872
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18317 0 0 0 21949 51 0 0 25 0 1 0 483387831 67719168 15214 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16533 15214 603 41 0 16492 0
vsize: 66132
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18479 0 0 0 22949 51 0 0 25 0 1 0 483387831 68386816 15376 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16696 15376 603 41 0 16655 0
vsize: 66784
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18523 0 0 0 23948 51 0 0 25 0 1 0 483387831 68517888 15420 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16728 15420 603 41 0 16687 0
vsize: 66912
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18624 0 0 0 24948 52 0 0 25 0 1 0 483387831 68923392 15521 4294967295 134512640 134672761 3221224560 3221223732 134556669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16827 15521 603 41 0 16786 0
vsize: 67308
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18665 0 0 0 25948 52 0 0 25 0 1 0 483387831 69062656 15562 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16861 15562 603 41 0 16820 0
vsize: 67444
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18700 0 0 0 26948 52 0 0 25 0 1 0 483387831 69197824 15597 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16894 15597 603 41 0 16853 0
vsize: 67576
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18803 0 0 0 27947 53 0 0 25 0 1 0 483387831 69603328 15700 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16993 15700 603 41 0 16952 0
vsize: 67972
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 18944 0 0 0 28946 54 0 0 25 0 1 0 483387831 70275072 15841 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17157 15841 603 41 0 17116 0
vsize: 68628
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 19137 0 0 0 29945 55 0 0 25 0 1 0 483387831 70942720 16034 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17320 16034 603 41 0 17279 0
vsize: 69280
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 19201 0 0 0 30945 55 0 0 25 0 1 0 483387831 71208960 16098 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17385 16098 603 41 0 17344 0
vsize: 69540
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 19255 0 0 0 31945 55 0 0 25 0 1 0 483387831 71475200 16152 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17450 16152 603 41 0 17409 0
vsize: 69800
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 19346 0 0 0 32945 55 0 0 25 0 1 0 483387831 71876608 16243 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17548 16243 603 41 0 17507 0
vsize: 70192
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 19512 0 0 0 33944 56 0 0 25 0 1 0 483387831 72544256 16409 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17711 16409 603 41 0 17670 0
vsize: 70844
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 19717 0 0 0 34944 57 0 0 25 0 1 0 483387831 73605120 16614 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17970 16614 603 41 0 17929 0
vsize: 71880
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 19918 0 0 0 35943 57 0 0 25 0 1 0 483387831 74395648 16815 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 16815 603 41 0 18122 0
vsize: 72652
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 20031 0 0 0 36943 58 0 0 25 0 1 0 483387831 74792960 16928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18260 16928 603 41 0 18219 0
vsize: 73040
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 20091 0 0 0 37943 58 0 0 25 0 1 0 483387831 75059200 16988 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18325 16988 603 41 0 18284 0
vsize: 73300
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 20215 0 0 0 38943 58 0 0 25 0 1 0 483387831 75591680 17112 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18455 17112 603 41 0 18414 0
vsize: 73820
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 20378 0 0 0 39942 59 0 0 25 0 1 0 483387831 76255232 17275 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18617 17275 603 41 0 18576 0
vsize: 74468
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 20583 0 0 0 40942 60 0 0 25 0 1 0 483387831 77058048 17480 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18813 17480 603 41 0 18772 0
vsize: 75252
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 20667 0 0 0 41942 60 0 0 25 0 1 0 483387831 77463552 17564 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18912 17564 603 41 0 18871 0
vsize: 75648
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 20874 0 0 0 42941 61 0 0 25 0 1 0 483387831 78262272 17771 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19107 17771 603 41 0 19066 0
vsize: 76428
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 21019 0 0 0 43941 62 0 0 25 0 1 0 483387831 78798848 17916 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19238 17916 603 41 0 19197 0
vsize: 76952
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 21042 0 0 0 44941 62 0 0 25 0 1 0 483387831 78934016 17939 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19271 17939 603 41 0 19230 0
vsize: 77084
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 21124 0 0 0 45941 62 0 0 25 0 1 0 483387831 79200256 18021 4294967295 134512640 134672761 3221224560 3221223748 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19336 18021 603 41 0 19295 0
vsize: 77344
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 21286 0 0 0 46940 63 0 0 25 0 1 0 483387831 79884288 18183 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19503 18183 603 41 0 19462 0
vsize: 78012
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 21614 0 0 0 47940 63 0 0 25 0 1 0 483387831 81235968 18511 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19833 18511 603 41 0 19792 0
vsize: 79332
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 21724 0 0 0 48939 64 0 0 25 0 1 0 483387831 81637376 18621 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19931 18621 603 41 0 19890 0
vsize: 79724
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 21882 0 0 0 49939 64 0 0 25 0 1 0 483387831 82305024 18779 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20094 18779 603 41 0 20053 0
vsize: 80376
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 22037 0 0 0 50939 65 0 0 25 0 1 0 483387831 82968576 18934 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20256 18934 603 41 0 20215 0
vsize: 81024
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 22116 0 0 0 51939 65 0 0 25 0 1 0 483387831 83238912 19013 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20322 19013 603 41 0 20281 0
vsize: 81288
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 22213 0 0 0 52938 66 0 0 25 0 1 0 483387831 83640320 19110 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20420 19110 603 41 0 20379 0
vsize: 81680
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 22698 0 0 0 53936 68 0 0 25 0 1 0 483387831 85647360 19595 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20910 19595 603 41 0 20869 0
vsize: 83640
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 22911 0 0 0 54935 69 0 0 25 0 1 0 483387831 86450176 19808 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21106 19808 603 41 0 21065 0
vsize: 84424
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23038 0 0 0 55935 69 0 0 25 0 1 0 483387831 86990848 19935 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21238 19935 603 41 0 21197 0
vsize: 84952
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23184 0 0 0 56935 70 0 0 25 0 1 0 483387831 87523328 20081 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21368 20081 603 41 0 21327 0
vsize: 85472
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23315 0 0 0 57934 70 0 0 25 0 1 0 483387831 88055808 20212 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21498 20212 603 41 0 21457 0
vsize: 85992
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23428 0 0 0 58934 70 0 0 25 0 1 0 483387831 88985600 20325 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21725 20325 603 41 0 21684 0
vsize: 86900
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23506 0 0 0 59934 70 0 0 25 0 1 0 483387831 89382912 20403 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21822 20403 603 41 0 21781 0
vsize: 87288
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23623 0 0 0 60934 71 0 0 25 0 1 0 483387831 89784320 20520 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21920 20520 603 41 0 21879 0
vsize: 87680
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23774 0 0 0 61933 72 0 0 25 0 1 0 483387831 90460160 20671 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22085 20671 603 41 0 22044 0
vsize: 88340
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17172
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23844 0 0 0 62933 72 0 0 25 0 1 0 483387831 90730496 20741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22151 20741 603 41 0 22110 0
vsize: 88604
[startup+640.006 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 17225
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 23973 0 0 0 63932 73 0 0 25 0 1 0 483387831 91271168 20870 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22283 20870 603 41 0 22242 0
vsize: 89132
[startup+650.006 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 17225
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 24077 0 0 0 64931 74 0 0 25 0 1 0 483387831 91672576 20974 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22381 20974 603 41 0 22340 0
vsize: 89524
[startup+660.007 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 17225
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 24185 0 0 0 65930 75 0 0 25 0 1 0 483387831 92069888 21082 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22478 21082 603 41 0 22437 0
vsize: 89912
[startup+670.008 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 17225
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 24302 0 0 0 66931 75 0 0 25 0 1 0 483387831 92610560 21199 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22610 21199 603 41 0 22569 0
vsize: 90440
[startup+680.007 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 17225
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 24404 0 0 0 67930 76 0 0 25 0 1 0 483387831 93011968 21301 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22708 21301 603 41 0 22667 0
vsize: 90832
[startup+690.008 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 17225
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 24553 0 0 0 68930 76 0 0 25 0 1 0 483387831 93552640 21450 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22840 21450 603 41 0 22799 0
vsize: 91360
[startup+700.008 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 17225
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 24640 0 0 0 69930 76 0 0 25 0 1 0 483387831 93966336 21537 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22941 21537 603 41 0 22900 0
vsize: 91764
[startup+710.008 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 24721 0 0 0 70930 76 0 0 25 0 1 0 483387831 94232576 21618 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23006 21618 603 41 0 22965 0
vsize: 92024
[startup+720.008 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 24905 0 0 0 71930 77 0 0 25 0 1 0 483387831 94920704 21802 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23174 21802 603 41 0 23133 0
vsize: 92696
[startup+730.008 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25040 0 0 0 72929 78 0 0 25 0 1 0 483387831 95477760 21937 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23310 21937 603 41 0 23269 0
vsize: 93240
[startup+740.007 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25168 0 0 0 73929 78 0 0 25 0 1 0 483387831 96010240 22065 4294967295 134512640 134672761 3221224560 3221223744 134559512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23440 22065 603 41 0 23399 0
vsize: 93760
[startup+750.008 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25275 0 0 0 74928 78 0 0 25 0 1 0 483387831 96550912 22172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23572 22172 603 41 0 23531 0
vsize: 94288
[startup+760.009 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25402 0 0 0 75928 79 0 0 25 0 1 0 483387831 96956416 22299 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23671 22299 603 41 0 23630 0
vsize: 94684
[startup+770.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25477 0 0 0 76928 79 0 0 25 0 1 0 483387831 97234944 22374 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23739 22374 603 41 0 23698 0
vsize: 94956
[startup+780.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25546 0 0 0 77928 79 0 0 25 0 1 0 483387831 97505280 22443 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23805 22443 603 41 0 23764 0
vsize: 95220
[startup+790.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25638 0 0 0 78929 79 0 0 25 0 1 0 483387831 97906688 22535 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23903 22535 603 41 0 23862 0
vsize: 95612
[startup+800.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25751 0 0 0 79928 79 0 0 25 0 1 0 483387831 98455552 22648 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24037 22648 603 41 0 23996 0
vsize: 96148
[startup+810.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25821 0 0 0 80928 80 0 0 25 0 1 0 483387831 98738176 22718 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24106 22718 603 41 0 24065 0
vsize: 96424
[startup+820.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25899 0 0 0 81927 80 0 0 25 0 1 0 483387831 99004416 22796 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24171 22796 603 41 0 24130 0
vsize: 96684
[startup+830.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 25982 0 0 0 82927 81 0 0 25 0 1 0 483387831 99422208 22879 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24273 22879 603 41 0 24232 0
vsize: 97092
[startup+840.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26037 0 0 0 83927 81 0 0 25 0 1 0 483387831 99557376 22934 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24306 22934 603 41 0 24265 0
vsize: 97224
[startup+850.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26099 0 0 0 84927 81 0 0 25 0 1 0 483387831 99840000 22996 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24375 22996 603 41 0 24334 0
vsize: 97500
[startup+860.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26179 0 0 0 85927 81 0 0 25 0 1 0 483387831 100126720 23076 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24445 23076 603 41 0 24404 0
vsize: 97780
[startup+870.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26264 0 0 0 86927 81 0 0 25 0 1 0 483387831 100536320 23161 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24545 23161 603 41 0 24504 0
vsize: 98180
[startup+880.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26311 0 0 0 87927 81 0 0 25 0 1 0 483387831 100667392 23208 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24577 23208 603 41 0 24536 0
vsize: 98308
[startup+890.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26388 0 0 0 88927 82 0 0 25 0 1 0 483387831 100929536 23285 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24641 23285 603 41 0 24600 0
vsize: 98564
[startup+900.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26467 0 0 0 89927 82 0 0 25 0 1 0 483387831 101330944 23364 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24739 23364 603 41 0 24698 0
vsize: 98956
[startup+910.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26582 0 0 0 90927 82 0 0 25 0 1 0 483387831 101732352 23479 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24837 23479 603 41 0 24796 0
vsize: 99348
[startup+920.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26616 0 0 0 91927 82 0 0 25 0 1 0 483387831 101863424 23513 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24869 23513 603 41 0 24828 0
vsize: 99476
[startup+930.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26646 0 0 0 92927 82 0 0 25 0 1 0 483387831 101994496 23543 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24901 23543 603 41 0 24860 0
vsize: 99604
[startup+940.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26702 0 0 0 93927 82 0 0 25 0 1 0 483387831 102264832 23599 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24967 23599 603 41 0 24926 0
vsize: 99868
[startup+950.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26766 0 0 0 94927 83 0 0 25 0 1 0 483387831 102531072 23663 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25032 23663 603 41 0 24991 0
vsize: 100128
[startup+960.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26822 0 0 0 95927 83 0 0 25 0 1 0 483387831 102805504 23719 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25099 23719 603 41 0 25058 0
vsize: 100396
[startup+970.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17227
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 26917 0 0 0 96927 83 0 0 25 0 1 0 483387831 103075840 23814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25165 23814 603 41 0 25124 0
vsize: 100660
[startup+980.014 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27056 0 0 0 97926 84 0 0 25 0 1 0 483387831 103751680 23953 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25330 23953 603 41 0 25289 0
vsize: 101320
[startup+990.015 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27167 0 0 0 98926 85 0 0 25 0 1 0 483387831 104148992 24064 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25427 24064 603 41 0 25386 0
vsize: 101708
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27245 0 0 0 99926 85 0 0 25 0 1 0 483387831 104419328 24142 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25493 24142 603 41 0 25452 0
vsize: 101972
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27299 0 0 0 100926 85 0 0 25 0 1 0 483387831 104689664 24196 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25559 24196 603 41 0 25518 0
vsize: 102236
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27368 0 0 0 101925 86 0 0 25 0 1 0 483387831 104960000 24265 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25625 24265 603 41 0 25584 0
vsize: 102500
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27453 0 0 0 102925 86 0 0 25 0 1 0 483387831 105365504 24350 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25724 24350 603 41 0 25683 0
vsize: 102896
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27530 0 0 0 103925 87 0 0 25 0 1 0 483387831 105631744 24427 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25789 24427 603 41 0 25748 0
vsize: 103156
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27571 0 0 0 104925 87 0 0 25 0 1 0 483387831 105766912 24468 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25822 24468 603 41 0 25781 0
vsize: 103288
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27627 0 0 0 105925 87 0 0 25 0 1 0 483387831 106041344 24524 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25889 24524 603 41 0 25848 0
vsize: 103556
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27682 0 0 0 106924 88 0 0 25 0 1 0 483387831 106176512 24579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25922 24579 603 41 0 25881 0
vsize: 103688
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27754 0 0 0 107923 89 0 0 25 0 1 0 483387831 106573824 24651 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26019 24651 603 41 0 25978 0
vsize: 104076
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27841 0 0 0 108923 89 0 0 25 0 1 0 483387831 106864640 24738 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26090 24738 603 41 0 26049 0
vsize: 104360
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27899 0 0 0 109923 90 0 0 25 0 1 0 483387831 107130880 24796 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26155 24796 603 41 0 26114 0
vsize: 104620
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 27949 0 0 0 110923 90 0 0 25 0 1 0 483387831 107266048 24846 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26188 24846 603 41 0 26147 0
vsize: 104752
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28007 0 0 0 111923 90 0 0 25 0 1 0 483387831 107528192 24904 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26252 24904 603 41 0 26211 0
vsize: 105008
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28066 0 0 0 112923 91 0 0 25 0 1 0 483387831 107794432 24963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26317 24963 603 41 0 26276 0
vsize: 105268
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28152 0 0 0 113922 91 0 0 25 0 1 0 483387831 108199936 25049 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26416 25049 603 41 0 26375 0
vsize: 105664
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28235 0 0 0 114922 91 0 0 25 0 1 0 483387831 108486656 25132 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26486 25132 603 41 0 26445 0
vsize: 105944
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28248 0 0 0 115922 92 0 0 25 0 1 0 483387831 108621824 25145 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26519 25145 603 41 0 26478 0
vsize: 106076
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28295 0 0 0 116922 92 0 0 25 0 1 0 483387831 108756992 25192 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26552 25192 603 41 0 26511 0
vsize: 106208
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28359 0 0 0 117921 93 0 0 25 0 1 0 483387831 109027328 25256 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26618 25256 603 41 0 26577 0
vsize: 106472
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28451 0 0 0 118921 93 0 0 25 0 1 0 483387831 109428736 25348 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26716 25348 603 41 0 26675 0
vsize: 106864
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 17229
Raw data (stat): 17172 (minisat+) R 17171 20937 20936 0 -1 0 28538 0 0 0 119921 93 0 0 25 0 1 0 483387831 109830144 25435 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26814 25435 603 41 0 26773 0
vsize: 107256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 17229
Raw data (stat): 17172 (minisat+) Z 17171 20937 20936 0 -1 12 28540 0 0 0 119921 98 0 0 25 0 1 0 483387831 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: 0
Real time (s): 1200.07
CPU time (s): 1200.2
CPU user time (s): 1199.21
CPU system time (s): 0.986849
CPU usage (%): 100.011
Max. virtual memory (Kb): 107256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####