PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-mkc.opb
MD5SUM	44934b498b6e9897bcf8e950d9d30136
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 18647

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-21 15:55:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17698 boxname=wulflinc17 idbench=1362 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  44934b498b6e9897bcf8e950d9d30136  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-mkc.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-mkc.opb
IDLAUNCH: 17698
/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:        569412 kB
Buffers:          5980 kB
Cached:         433132 kB
SwapCached:        440 kB
Active:          70180 kB
Inactive:       371720 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        569132 kB
SwapTotal:     2097892 kB
SwapFree:      2097208 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6032 kB
Slab:            17712 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:15:49 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 17698 7 1200.22 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 |  412444  1339233 |  137481       0        0     nan |  0.000 % |
c |       101 |  412404  1339099 |  151229      96      298     3.1 |  0.714 % |
c |       251 |  411996  1337793 |  166352     201     8264    41.1 |  0.807 % |
c |       476 |  411996  1337793 |  182987     426    15953    37.4 |  0.807 % |
c |       814 |  411523  1336710 |  201285     589    14598    24.8 |  0.951 % |
c |      1320 |  411523  1336710 |  221414    1095    33853    30.9 |  0.951 % |
c |      2079 |  411523  1336710 |  243555    1854    57475    31.0 |  0.951 % |
c |      3220 |  411515  1336684 |  267911    2994    87576    29.3 |  0.952 % |
c |      4928 |  411515  1336684 |  294702    4702   140804    29.9 |  0.952 % |
c |      7493 |  411515  1336684 |  324173    7267   270478    37.2 |  0.952 % |
c |     11338 |  411515  1336684 |  356590   11112   409874    36.9 |  0.952 % |
c |     17104 |  410719  1334080 |  392249   13076   397285    30.4 |  1.119 % |
c |     25755 |  410426  1333029 |  431474   21587   676127    31.3 |  1.169 % |
c |     38730 |  409921  1331539 |  474621   34454  1130992    32.8 |  1.275 % |
c |     58191 |  409623  1330662 |  522083   53875  1831052    34.0 |  1.343 % |
c |     87383 |  409253  1329565 |  574292   82956  2941040    35.5 |  1.428 % |
c |    131173 |  407943  1325181 |  631721  126260  4482630    35.5 |  1.677 % |
c |    196858 |  403226  1312621 |  694893  191317  6968041    36.4 |  3.041 % |
#### 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.87 0.92 0.92 2/55 797
Raw data (stat): 797 (runsolver) R 796 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546333465 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.89 0.93 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 3566 0 0 0 991 7 0 0 25 0 1 0 546333465 10706944 2139 4294967295 134512640 134672761 3221224624 3221222176 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.91 0.93 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 3566 0 0 0 1991 7 0 0 25 0 1 0 546333465 10706944 2139 4294967295 134512640 134672761 3221224624 3221222320 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.0004 s]
Raw data (loadavg): 0.92 0.93 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 9915 0 0 0 2976 23 0 0 25 0 1 0 546333465 31449088 6827 4294967295 134512640 134672761 3221224624 3221215896 1075350501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7678 6827 603 41 0 7637 0
vsize: 30712
[startup+40.0004 s]
Raw data (loadavg): 0.93 0.93 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 16185 0 0 0 3961 38 0 0 25 0 1 0 546333465 59588608 13097 4294967295 134512640 134672761 3221224624 3221223792 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13097 603 41 0 14507 0
vsize: 58192
[startup+50.001 s]
Raw data (loadavg): 0.94 0.93 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 16557 0 0 0 4960 39 0 0 25 0 1 0 546333465 61194240 13469 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14940 13469 603 41 0 14899 0
vsize: 59760
[startup+60.0012 s]
Raw data (loadavg): 0.95 0.94 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 16726 0 0 0 5959 39 0 0 25 0 1 0 546333465 61730816 13638 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15071 13638 603 41 0 15030 0
vsize: 60284
[startup+70.0012 s]
Raw data (loadavg): 0.96 0.94 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 16885 0 0 0 6958 41 0 0 25 0 1 0 546333465 62484480 13797 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15255 13797 603 41 0 15214 0
vsize: 61020
[startup+80.0021 s]
Raw data (loadavg): 0.96 0.94 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 17049 0 0 0 7958 41 0 0 25 0 1 0 546333465 63156224 13961 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15419 13961 603 41 0 15378 0
vsize: 61676
[startup+90.0019 s]
Raw data (loadavg): 0.97 0.94 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 17354 0 0 0 8957 42 0 0 25 0 1 0 546333465 64364544 14266 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15714 14266 603 41 0 15673 0
vsize: 62856
[startup+100.003 s]
Raw data (loadavg): 0.97 0.94 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 17575 0 0 0 9956 43 0 0 25 0 1 0 546333465 65429504 14487 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15974 14487 603 41 0 15933 0
vsize: 63896
[startup+110.004 s]
Raw data (loadavg): 0.98 0.94 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 17743 0 0 0 10955 44 0 0 25 0 1 0 546333465 66101248 14655 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16138 14655 603 41 0 16097 0
vsize: 64552
[startup+120.003 s]
Raw data (loadavg): 0.98 0.94 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 18035 0 0 0 11954 45 0 0 25 0 1 0 546333465 67170304 14947 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16399 14947 603 41 0 16358 0
vsize: 65596
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 18207 0 0 0 12953 46 0 0 25 0 1 0 546333465 67969024 15119 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16594 15119 603 41 0 16553 0
vsize: 66376
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 18324 0 0 0 13953 47 0 0 25 0 1 0 546333465 68370432 15236 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16692 15236 603 41 0 16651 0
vsize: 66768
[startup+150.004 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 18470 0 0 0 14952 47 0 0 25 0 1 0 546333465 68902912 15382 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16822 15382 603 41 0 16781 0
vsize: 67288
[startup+160.004 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 18604 0 0 0 15952 48 0 0 25 0 1 0 546333465 69443584 15516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16954 15516 603 41 0 16913 0
vsize: 67816
[startup+170.004 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 18740 0 0 0 16951 49 0 0 25 0 1 0 546333465 70115328 15652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17118 15652 603 41 0 17077 0
vsize: 68472
[startup+180.004 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 18869 0 0 0 17950 49 0 0 25 0 1 0 546333465 70520832 15781 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17217 15781 603 41 0 17176 0
vsize: 68868
[startup+190.004 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 797
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 18969 0 0 0 18950 50 0 0 25 0 1 0 546333465 70955008 15881 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17323 15881 603 41 0 17282 0
vsize: 69292
[startup+200.005 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 799
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 19058 0 0 0 19949 51 0 0 25 0 1 0 546333465 71647232 15970 4294967295 134512640 134672761 3221224624 3221223812 1075347023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17492 15970 603 41 0 17451 0
vsize: 69968
[startup+210.005 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 799
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 19192 0 0 0 20948 52 0 0 25 0 1 0 546333465 72187904 16104 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17624 16104 603 41 0 17583 0
vsize: 70496
[startup+220.005 s]
Raw data (loadavg): 0.99 0.95 0.92 2/55 799
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 19350 0 0 0 21947 53 0 0 25 0 1 0 546333465 72867840 16262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17790 16262 603 41 0 17749 0
vsize: 71160
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 799
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 19586 0 0 0 22947 54 0 0 25 0 1 0 546333465 73809920 16498 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18020 16498 603 41 0 17979 0
vsize: 72080
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 799
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 19759 0 0 0 23946 54 0 0 25 0 1 0 546333465 74473472 16671 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18182 16671 603 41 0 18141 0
vsize: 72728
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 799
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 19919 0 0 0 24946 55 0 0 25 0 1 0 546333465 75141120 16831 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18345 16831 603 41 0 18304 0
vsize: 73380
[startup+260.007 s]
Raw data (loadavg): 1.31 1.02 0.94 3/59 847
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 19997 0 0 0 25946 55 0 0 25 0 1 0 546333465 75407360 16909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18410 16909 603 41 0 18369 0
vsize: 73640
[startup+270.007 s]
Raw data (loadavg): 1.27 1.02 0.94 2/55 854
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20097 0 0 0 26946 55 0 0 25 0 1 0 546333465 75821056 17009 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18511 17009 603 41 0 18470 0
vsize: 74044
[startup+280.007 s]
Raw data (loadavg): 1.22 1.02 0.94 2/55 854
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20191 0 0 0 27945 55 0 0 25 0 1 0 546333465 76226560 17103 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18610 17103 603 41 0 18569 0
vsize: 74440
[startup+290.007 s]
Raw data (loadavg): 1.19 1.02 0.94 2/55 854
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20263 0 0 0 28945 56 0 0 25 0 1 0 546333465 76492800 17175 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18675 17175 603 41 0 18634 0
vsize: 74700
[startup+300.006 s]
Raw data (loadavg): 1.16 1.02 0.94 2/55 854
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20341 0 0 0 29945 56 0 0 25 0 1 0 546333465 76906496 17253 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18776 17253 603 41 0 18735 0
vsize: 75104
[startup+310.006 s]
Raw data (loadavg): 1.13 1.02 0.94 2/55 854
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20412 0 0 0 30945 56 0 0 25 0 1 0 546333465 77176832 17324 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18842 17324 603 41 0 18801 0
vsize: 75368
[startup+320.006 s]
Raw data (loadavg): 1.11 1.02 0.94 2/55 854
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20531 0 0 0 31945 57 0 0 25 0 1 0 546333465 77713408 17443 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18973 17443 603 41 0 18932 0
vsize: 75892
[startup+330.006 s]
Raw data (loadavg): 1.10 1.02 0.94 2/55 854
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20616 0 0 0 32944 57 0 0 25 0 1 0 546333465 77983744 17528 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19039 17528 603 41 0 18998 0
vsize: 76156
[startup+340.006 s]
Raw data (loadavg): 1.08 1.02 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20704 0 0 0 33944 58 0 0 25 0 1 0 546333465 78393344 17616 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19139 17616 603 41 0 19098 0
vsize: 76556
[startup+350.007 s]
Raw data (loadavg): 1.07 1.02 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20755 0 0 0 34944 58 0 0 25 0 1 0 546333465 78524416 17667 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19171 17667 603 41 0 19130 0
vsize: 76684
[startup+360.006 s]
Raw data (loadavg): 1.06 1.02 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20804 0 0 0 35944 58 0 0 25 0 1 0 546333465 78790656 17716 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19236 17716 603 41 0 19195 0
vsize: 76944
[startup+370.006 s]
Raw data (loadavg): 1.05 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20856 0 0 0 36944 59 0 0 25 0 1 0 546333465 78921728 17768 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19268 17768 603 41 0 19227 0
vsize: 77072
[startup+380.007 s]
Raw data (loadavg): 1.04 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 20929 0 0 0 37943 59 0 0 25 0 1 0 546333465 79323136 17841 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19366 17841 603 41 0 19325 0
vsize: 77464
[startup+390.006 s]
Raw data (loadavg): 1.03 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21047 0 0 0 38943 60 0 0 25 0 1 0 546333465 79753216 17959 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19471 17959 603 41 0 19430 0
vsize: 77884
[startup+400.005 s]
Raw data (loadavg): 1.03 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21153 0 0 0 39943 60 0 0 25 0 1 0 546333465 80171008 18065 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19573 18065 603 41 0 19532 0
vsize: 78292
[startup+410.005 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21219 0 0 0 40943 60 0 0 25 0 1 0 546333465 80449536 18131 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19641 18131 603 41 0 19600 0
vsize: 78564
[startup+420.005 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21287 0 0 0 41942 61 0 0 25 0 1 0 546333465 80719872 18199 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19707 18199 603 41 0 19666 0
vsize: 78828
[startup+430.004 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21367 0 0 0 42942 61 0 0 25 0 1 0 546333465 80990208 18279 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19773 18279 603 41 0 19732 0
vsize: 79092
[startup+440.004 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21443 0 0 0 43942 61 0 0 25 0 1 0 546333465 81420288 18355 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19878 18355 603 41 0 19837 0
vsize: 79512
[startup+450.005 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21525 0 0 0 44942 62 0 0 25 0 1 0 546333465 81702912 18437 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19947 18437 603 41 0 19906 0
vsize: 79788
[startup+460.004 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21592 0 0 0 45942 62 0 0 25 0 1 0 546333465 81969152 18504 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20012 18504 603 41 0 19971 0
vsize: 80048
[startup+470.004 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21680 0 0 0 46942 62 0 0 25 0 1 0 546333465 82300928 18592 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20093 18592 603 41 0 20052 0
vsize: 80372
[startup+480.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21742 0 0 0 47942 62 0 0 25 0 1 0 546333465 82567168 18654 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20158 18654 603 41 0 20117 0
vsize: 80632
[startup+490.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 856
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21811 0 0 0 48942 63 0 0 25 0 1 0 546333465 82833408 18723 4294967295 134512640 134672761 3221224624 3221223760 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20223 18723 603 41 0 20182 0
vsize: 80892
[startup+500.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21880 0 0 0 49942 63 0 0 25 0 1 0 546333465 83103744 18792 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20289 18792 603 41 0 20248 0
vsize: 81156
[startup+510.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 21997 0 0 0 50941 63 0 0 25 0 1 0 546333465 83644416 18909 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20421 18909 603 41 0 20380 0
vsize: 81684
[startup+520.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22106 0 0 0 51941 64 0 0 25 0 1 0 546333465 84074496 19018 4294967295 134512640 134672761 3221224624 3221223792 134560931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20526 19018 603 41 0 20485 0
vsize: 82104
[startup+530.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22183 0 0 0 52941 64 0 0 25 0 1 0 546333465 84344832 19095 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20592 19095 603 41 0 20551 0
vsize: 82368
[startup+540.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22237 0 0 0 53941 64 0 0 25 0 1 0 546333465 85143552 19149 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20787 19149 603 41 0 20746 0
vsize: 83148
[startup+550.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22301 0 0 0 54941 64 0 0 25 0 1 0 546333465 85463040 19213 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20865 19213 603 41 0 20824 0
vsize: 83460
[startup+560.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22361 0 0 0 55941 64 0 0 25 0 1 0 546333465 85598208 19273 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20898 19273 603 41 0 20857 0
vsize: 83592
[startup+570.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22433 0 0 0 56941 65 0 0 25 0 1 0 546333465 85999616 19345 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20996 19345 603 41 0 20955 0
vsize: 83984
[startup+580.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 858
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22486 0 0 0 57941 65 0 0 25 0 1 0 546333465 86134784 19398 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21029 19398 603 41 0 20988 0
vsize: 84116
[startup+590.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22541 0 0 0 58941 65 0 0 25 0 1 0 546333465 86405120 19453 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21095 19453 603 41 0 21054 0
vsize: 84380
[startup+600.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22596 0 0 0 59941 65 0 0 25 0 1 0 546333465 86687744 19508 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21164 19508 603 41 0 21123 0
vsize: 84656
[startup+610.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22650 0 0 0 60941 65 0 0 25 0 1 0 546333465 86863872 19562 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21207 19562 603 41 0 21166 0
vsize: 84828
[startup+620.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22721 0 0 0 61941 66 0 0 25 0 1 0 546333465 87134208 19633 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21273 19633 603 41 0 21232 0
vsize: 85092
[startup+630.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22808 0 0 0 62940 66 0 0 25 0 1 0 546333465 87588864 19720 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21384 19720 603 41 0 21343 0
vsize: 85536
[startup+640.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22851 0 0 0 63940 66 0 0 25 0 1 0 546333465 87781376 19763 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21431 19763 603 41 0 21390 0
vsize: 85724
[startup+650.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 22944 0 0 0 64940 67 0 0 25 0 1 0 546333465 88096768 19856 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21508 19856 603 41 0 21467 0
vsize: 86032
[startup+660.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23008 0 0 0 65940 67 0 0 25 0 1 0 546333465 88371200 19920 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21575 19920 603 41 0 21534 0
vsize: 86300
[startup+670.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23067 0 0 0 66940 67 0 0 25 0 1 0 546333465 88641536 19979 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21641 19979 603 41 0 21600 0
vsize: 86564
[startup+680.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23149 0 0 0 67940 67 0 0 25 0 1 0 546333465 88928256 20061 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21711 20061 603 41 0 21670 0
vsize: 86844
[startup+690.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23269 0 0 0 68940 68 0 0 25 0 1 0 546333465 89456640 20181 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21840 20181 603 41 0 21799 0
vsize: 87360
[startup+700.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23319 0 0 0 69940 68 0 0 25 0 1 0 546333465 89624576 20231 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21881 20231 603 41 0 21840 0
vsize: 87524
[startup+710.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23370 0 0 0 70940 68 0 0 25 0 1 0 546333465 89894912 20282 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21947 20282 603 41 0 21906 0
vsize: 87788
[startup+720.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23434 0 0 0 71940 68 0 0 25 0 1 0 546333465 90165248 20346 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22013 20346 603 41 0 21972 0
vsize: 88052
[startup+730.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23503 0 0 0 72940 68 0 0 25 0 1 0 546333465 90435584 20415 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22079 20415 603 41 0 22038 0
vsize: 88316
[startup+740.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23568 0 0 0 73939 69 0 0 25 0 1 0 546333465 90705920 20480 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22145 20480 603 41 0 22104 0
vsize: 88580
[startup+750.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23629 0 0 0 74940 69 0 0 25 0 1 0 546333465 91045888 20541 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22228 20541 603 41 0 22187 0
vsize: 88912
[startup+760.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23691 0 0 0 75939 69 0 0 25 0 1 0 546333465 91181056 20603 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22261 20603 603 41 0 22220 0
vsize: 89044
[startup+770.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23738 0 0 0 76940 69 0 0 25 0 1 0 546333465 91377664 20650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22309 20650 603 41 0 22268 0
vsize: 89236
[startup+780 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23785 0 0 0 77940 69 0 0 25 0 1 0 546333465 91656192 20697 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22377 20697 603 41 0 22336 0
vsize: 89508
[startup+790 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 860
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23864 0 0 0 78940 70 0 0 25 0 1 0 546333465 91971584 20776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22454 20776 603 41 0 22413 0
vsize: 89816
[startup+800 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23932 0 0 0 79940 70 0 0 25 0 1 0 546333465 92344320 20844 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22545 20844 603 41 0 22504 0
vsize: 90180
[startup+810 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 23987 0 0 0 80940 70 0 0 25 0 1 0 546333465 92475392 20899 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22577 20899 603 41 0 22536 0
vsize: 90308
[startup+820 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24051 0 0 0 81939 70 0 0 25 0 1 0 546333465 92741632 20963 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22642 20963 603 41 0 22601 0
vsize: 90568
[startup+829.999 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24111 0 0 0 82939 71 0 0 25 0 1 0 546333465 93057024 21023 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22719 21023 603 41 0 22678 0
vsize: 90876
[startup+839.999 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24186 0 0 0 83939 71 0 0 25 0 1 0 546333465 93380608 21098 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22798 21098 603 41 0 22757 0
vsize: 91192
[startup+849.999 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24251 0 0 0 84940 71 0 0 25 0 1 0 546333465 93511680 21163 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22830 21163 603 41 0 22789 0
vsize: 91320
[startup+860 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24350 0 0 0 85939 71 0 0 25 0 1 0 546333465 93908992 21262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22927 21262 603 41 0 22886 0
vsize: 91708
[startup+869.999 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24423 0 0 0 86939 72 0 0 25 0 1 0 546333465 94175232 21335 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22992 21335 603 41 0 22951 0
vsize: 91968
[startup+879.998 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24491 0 0 0 87939 72 0 0 25 0 1 0 546333465 94441472 21403 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23057 21403 603 41 0 23016 0
vsize: 92228
[startup+889.998 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24551 0 0 0 88938 72 0 0 25 0 1 0 546333465 94707712 21463 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23122 21463 603 41 0 23081 0
vsize: 92488
[startup+899.998 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24607 0 0 0 89938 73 0 0 25 0 1 0 546333465 94978048 21519 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23188 21519 603 41 0 23147 0
vsize: 92752
[startup+909.997 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24644 0 0 0 90938 73 0 0 25 0 1 0 546333465 95113216 21556 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23221 21556 603 41 0 23180 0
vsize: 92884
[startup+919.997 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24725 0 0 0 91938 73 0 0 25 0 1 0 546333465 95510528 21637 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23318 21637 603 41 0 23277 0
vsize: 93272
[startup+929.997 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24783 0 0 0 92938 74 0 0 25 0 1 0 546333465 95801344 21695 4294967295 134512640 134672761 3221224624 3221223840 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23389 21695 603 41 0 23348 0
vsize: 93556
[startup+939.997 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24871 0 0 0 93937 74 0 0 25 0 1 0 546333465 96256000 21783 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23500 21783 603 41 0 23459 0
vsize: 94000
[startup+949.998 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24921 0 0 0 94937 75 0 0 25 0 1 0 546333465 96387072 21833 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23532 21833 603 41 0 23491 0
vsize: 94128
[startup+959.997 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 24978 0 0 0 95937 75 0 0 25 0 1 0 546333465 96661504 21890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23599 21890 603 41 0 23558 0
vsize: 94396
[startup+969.997 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25029 0 0 0 96937 75 0 0 25 0 1 0 546333465 96792576 21941 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23631 21941 603 41 0 23590 0
vsize: 94524
[startup+979.998 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25075 0 0 0 97937 76 0 0 25 0 1 0 546333465 97071104 21987 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23699 21987 603 41 0 23658 0
vsize: 94796
[startup+989.998 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25114 0 0 0 98937 76 0 0 25 0 1 0 546333465 97202176 22026 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23731 22026 603 41 0 23690 0
vsize: 94924
[startup+999.999 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25159 0 0 0 99937 76 0 0 25 0 1 0 546333465 97337344 22071 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23764 22071 603 41 0 23723 0
vsize: 95056
[startup+1010 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25240 0 0 0 100936 77 0 0 25 0 1 0 546333465 97742848 22152 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23863 22152 603 41 0 23822 0
vsize: 95452
[startup+1020 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25274 0 0 0 101936 77 0 0 25 0 1 0 546333465 97873920 22186 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23895 22186 603 41 0 23854 0
vsize: 95580
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25334 0 0 0 102936 77 0 0 25 0 1 0 546333465 98140160 22246 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23960 22246 603 41 0 23919 0
vsize: 95840
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25395 0 0 0 103936 78 0 0 25 0 1 0 546333465 98271232 22307 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23992 22307 603 41 0 23951 0
vsize: 95968
[startup+1050 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25450 0 0 0 104936 78 0 0 25 0 1 0 546333465 98533376 22362 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24056 22362 603 41 0 24015 0
vsize: 96224
[startup+1060 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25509 0 0 0 105936 78 0 0 25 0 1 0 546333465 98799616 22421 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24121 22421 603 41 0 24080 0
vsize: 96484
[startup+1070 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25587 0 0 0 106936 78 0 0 25 0 1 0 546333465 99090432 22499 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24192 22499 603 41 0 24151 0
vsize: 96768
[startup+1080 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25639 0 0 0 107936 78 0 0 25 0 1 0 546333465 99360768 22551 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24258 22551 603 41 0 24217 0
vsize: 97032
[startup+1090 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 862
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25695 0 0 0 108936 79 0 0 25 0 1 0 546333465 99631104 22607 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24324 22607 603 41 0 24283 0
vsize: 97296
[startup+1100 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25761 0 0 0 109936 79 0 0 25 0 1 0 546333465 99893248 22673 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24388 22673 603 41 0 24347 0
vsize: 97552
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25811 0 0 0 110936 79 0 0 25 0 1 0 546333465 100028416 22723 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24421 22723 603 41 0 24380 0
vsize: 97684
[startup+1120 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25858 0 0 0 111935 80 0 0 25 0 1 0 546333465 100163584 22770 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24454 22770 603 41 0 24413 0
vsize: 97816
[startup+1130 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25906 0 0 0 112935 80 0 0 25 0 1 0 546333465 100429824 22818 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24519 22818 603 41 0 24478 0
vsize: 98076
[startup+1140 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25951 0 0 0 113935 80 0 0 25 0 1 0 546333465 100564992 22863 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24552 22863 603 41 0 24511 0
vsize: 98208
[startup+1150 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 25991 0 0 0 114936 80 0 0 25 0 1 0 546333465 100700160 22903 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24585 22903 603 41 0 24544 0
vsize: 98340
[startup+1160 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 26043 0 0 0 115936 80 0 0 25 0 1 0 546333465 101060608 22955 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24673 22955 603 41 0 24632 0
vsize: 98692
[startup+1170 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 26093 0 0 0 116936 80 0 0 25 0 1 0 546333465 101191680 23005 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24705 23005 603 41 0 24664 0
vsize: 98820
[startup+1180 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 26138 0 0 0 117936 80 0 0 25 0 1 0 546333465 101343232 23050 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24742 23050 603 41 0 24701 0
vsize: 98968
[startup+1190 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 26187 0 0 0 118936 80 0 0 25 0 1 0 546333465 101613568 23099 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24808 23099 603 41 0 24767 0
vsize: 99232
[startup+1200 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 864
Raw data (stat): 797 (minisat+) R 796 20838 20837 0 -1 0 26236 0 0 0 119936 81 0 0 25 0 1 0 546333465 101744640 23148 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24840 23148 603 41 0 24799 0
vsize: 99360
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.94 1/55 864
Raw data (stat): 797 (minisat+) Z 796 20838 20837 0 -1 12 26238 0 0 0 119936 85 0 0 25 0 1 0 546333465 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.05
CPU time (s): 1200.22
CPU user time (s): 1199.36
CPU system time (s): 0.855869
CPU usage (%): 100.015
Max. virtual memory (Kb): 99360
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####