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 18099

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        764036 kB
Buffers:         19820 kB
Cached:         226192 kB
SwapCached:        556 kB
Active:          35388 kB
Inactive:       212704 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        763756 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5164 kB
Slab:            16792 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:52:50 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 18608 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.86 0.97 0.92 2/55 1352
Raw data (stat): 1352 (runsolver) R 1351 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545462170 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0007 s]
Raw data (loadavg): 0.88 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 3566 0 0 0 988 10 0 0 25 0 1 0 545462170 10706944 2139 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2139 603 41 0 2573 0
vsize: 10456
[startup+20.0018 s]
Raw data (loadavg): 0.90 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 3566 0 0 0 1988 10 0 0 25 0 1 0 545462170 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+30.0016 s]
Raw data (loadavg): 0.92 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 9283 0 0 0 2975 23 0 0 25 0 1 0 545462170 28151808 6195 4294967295 134512640 134672761 3221224624 3221214960 134542089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6873 6195 603 41 0 6832 0
vsize: 27492
[startup+40.0023 s]
Raw data (loadavg): 0.93 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 16179 0 0 0 3959 38 0 0 25 0 1 0 545462170 59588608 13091 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14548 13091 603 41 0 14507 0
vsize: 58192
[startup+50.0035 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 16550 0 0 0 4958 39 0 0 25 0 1 0 545462170 61059072 13462 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14907 13462 603 41 0 14866 0
vsize: 59628
[startup+60.0043 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 16726 0 0 0 5957 40 0 0 25 0 1 0 545462170 61730816 13638 4294967295 134512640 134672761 3221224624 3221223808 134559561 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.0046 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 16877 0 0 0 6957 40 0 0 25 0 1 0 545462170 62484480 13789 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15255 13789 603 41 0 15214 0
vsize: 61020
[startup+80.0046 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 17046 0 0 0 7956 41 0 0 25 0 1 0 545462170 63156224 13958 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15419 13958 603 41 0 15378 0
vsize: 61676
[startup+90.0055 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 17340 0 0 0 8956 42 0 0 25 0 1 0 545462170 64364544 14252 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15714 14252 603 41 0 15673 0
vsize: 62856
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 17569 0 0 0 9955 42 0 0 25 0 1 0 545462170 65294336 14481 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15941 14481 603 41 0 15900 0
vsize: 63764
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 17735 0 0 0 10955 43 0 0 25 0 1 0 545462170 65966080 14647 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16105 14647 603 41 0 16064 0
vsize: 64420
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 1352
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 18021 0 0 0 11954 43 0 0 25 0 1 0 545462170 67170304 14933 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16399 14933 603 41 0 16358 0
vsize: 65596
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 18204 0 0 0 12954 44 0 0 25 0 1 0 545462170 67969024 15116 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16594 15116 603 41 0 16553 0
vsize: 66376
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 18318 0 0 0 13954 44 0 0 25 0 1 0 545462170 68370432 15230 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16692 15230 603 41 0 16651 0
vsize: 66768
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 18461 0 0 0 14954 45 0 0 25 0 1 0 545462170 68902912 15373 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16822 15373 603 41 0 16781 0
vsize: 67288
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 18596 0 0 0 15954 45 0 0 25 0 1 0 545462170 69443584 15508 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16954 15508 603 41 0 16913 0
vsize: 67816
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 18736 0 0 0 16953 46 0 0 25 0 1 0 545462170 69980160 15648 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17085 15648 603 41 0 17044 0
vsize: 68340
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 18865 0 0 0 17953 46 0 0 25 0 1 0 545462170 70520832 15777 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17217 15777 603 41 0 17176 0
vsize: 68868
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 18963 0 0 0 18953 46 0 0 25 0 1 0 545462170 70955008 15875 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17323 15875 603 41 0 17282 0
vsize: 69292
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 19054 0 0 0 19952 47 0 0 25 0 1 0 545462170 71647232 15966 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17492 15966 603 41 0 17451 0
vsize: 69968
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 19186 0 0 0 20953 47 0 0 25 0 1 0 545462170 72187904 16098 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17624 16098 603 41 0 17583 0
vsize: 70496
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 19346 0 0 0 21952 48 0 0 25 0 1 0 545462170 72867840 16258 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17790 16258 603 41 0 17749 0
vsize: 71160
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 19579 0 0 0 22952 48 0 0 25 0 1 0 545462170 73809920 16491 4294967295 134512640 134672761 3221224624 3221223760 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18020 16491 603 41 0 17979 0
vsize: 72080
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 19755 0 0 0 23952 49 0 0 25 0 1 0 545462170 74473472 16667 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18182 16667 603 41 0 18141 0
vsize: 72728
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 19918 0 0 0 24951 49 0 0 25 0 1 0 545462170 75141120 16830 4294967295 134512640 134672761 3221224624 3221223760 134560652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18345 16830 603 41 0 18304 0
vsize: 73380
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 19998 0 0 0 25951 49 0 0 25 0 1 0 545462170 75407360 16910 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18410 16910 603 41 0 18369 0
vsize: 73640
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20098 0 0 0 26951 49 0 0 25 0 1 0 545462170 75821056 17010 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18511 17010 603 41 0 18470 0
vsize: 74044
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20193 0 0 0 27951 50 0 0 25 0 1 0 545462170 76226560 17105 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18610 17105 603 41 0 18569 0
vsize: 74440
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20270 0 0 0 28951 50 0 0 25 0 1 0 545462170 76640256 17182 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18711 17182 603 41 0 18670 0
vsize: 74844
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20345 0 0 0 29951 50 0 0 25 0 1 0 545462170 76906496 17257 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18776 17257 603 41 0 18735 0
vsize: 75104
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20425 0 0 0 30951 51 0 0 25 0 1 0 545462170 77176832 17337 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18842 17337 603 41 0 18801 0
vsize: 75368
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20541 0 0 0 31951 51 0 0 25 0 1 0 545462170 77713408 17453 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18973 17453 603 41 0 18932 0
vsize: 75892
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20625 0 0 0 32950 51 0 0 25 0 1 0 545462170 77983744 17537 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19039 17537 603 41 0 18998 0
vsize: 76156
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20713 0 0 0 33950 52 0 0 25 0 1 0 545462170 78393344 17625 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19139 17625 603 41 0 19098 0
vsize: 76556
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20763 0 0 0 34950 52 0 0 25 0 1 0 545462170 78659584 17675 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19204 17675 603 41 0 19163 0
vsize: 76816
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20809 0 0 0 35950 52 0 0 25 0 1 0 545462170 78790656 17721 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19236 17721 603 41 0 19195 0
vsize: 76944
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20865 0 0 0 36950 52 0 0 25 0 1 0 545462170 79056896 17777 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19301 17777 603 41 0 19260 0
vsize: 77204
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 20950 0 0 0 37950 53 0 0 25 0 1 0 545462170 79323136 17862 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19366 17862 603 41 0 19325 0
vsize: 77464
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21069 0 0 0 38950 53 0 0 25 0 1 0 545462170 79888384 17981 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19504 17981 603 41 0 19463 0
vsize: 78016
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21167 0 0 0 39950 53 0 0 25 0 1 0 545462170 80310272 18079 4294967295 134512640 134672761 3221224624 3221223792 134560803 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19607 18079 603 41 0 19566 0
vsize: 78428
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21229 0 0 0 40950 53 0 0 25 0 1 0 545462170 80449536 18141 4294967295 134512640 134672761 3221224624 3221223792 134564755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19641 18141 603 41 0 19600 0
vsize: 78564
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1354
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21304 0 0 0 41950 54 0 0 25 0 1 0 545462170 80719872 18216 4294967295 134512640 134672761 3221224624 3221223760 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19707 18216 603 41 0 19666 0
vsize: 78828
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21381 0 0 0 42949 54 0 0 25 0 1 0 545462170 81125376 18293 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19806 18293 603 41 0 19765 0
vsize: 79224
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21474 0 0 0 43949 55 0 0 25 0 1 0 545462170 81567744 18386 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19914 18386 603 41 0 19873 0
vsize: 79656
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21543 0 0 0 44949 55 0 0 25 0 1 0 545462170 81833984 18455 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19979 18455 603 41 0 19938 0
vsize: 79916
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21622 0 0 0 45949 55 0 0 25 0 1 0 545462170 82104320 18534 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20045 18534 603 41 0 20004 0
vsize: 80180
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21695 0 0 0 46949 55 0 0 25 0 1 0 545462170 82436096 18607 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20126 18607 603 41 0 20085 0
vsize: 80504
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21758 0 0 0 47949 55 0 0 25 0 1 0 545462170 82702336 18670 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20191 18670 603 41 0 20150 0
vsize: 80764
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21831 0 0 0 48949 56 0 0 25 0 1 0 545462170 82968576 18743 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20256 18743 603 41 0 20215 0
vsize: 81024
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 21911 0 0 0 49949 56 0 0 25 0 1 0 545462170 83238912 18823 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20322 18823 603 41 0 20281 0
vsize: 81288
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22026 0 0 0 50949 56 0 0 25 0 1 0 545462170 83644416 18938 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20421 18938 603 41 0 20380 0
vsize: 81684
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22166 0 0 0 51949 56 0 0 25 0 1 0 545462170 84344832 19078 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20592 19078 603 41 0 20551 0
vsize: 82368
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22193 0 0 0 52949 56 0 0 25 0 1 0 545462170 84344832 19105 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20592 19105 603 41 0 20551 0
vsize: 82368
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22262 0 0 0 53949 57 0 0 25 0 1 0 545462170 85331968 19174 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20833 19174 603 41 0 20792 0
vsize: 83332
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22322 0 0 0 54949 57 0 0 25 0 1 0 545462170 85463040 19234 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20865 19234 603 41 0 20824 0
vsize: 83460
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22383 0 0 0 55949 57 0 0 25 0 1 0 545462170 85733376 19295 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20931 19295 603 41 0 20890 0
vsize: 83724
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22455 0 0 0 56949 57 0 0 25 0 1 0 545462170 85999616 19367 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20996 19367 603 41 0 20955 0
vsize: 83984
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22513 0 0 0 57949 57 0 0 25 0 1 0 545462170 86269952 19425 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21062 19425 603 41 0 21021 0
vsize: 84248
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22565 0 0 0 58949 57 0 0 25 0 1 0 545462170 86552576 19477 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21131 19477 603 41 0 21090 0
vsize: 84524
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22619 0 0 0 59949 58 0 0 25 0 1 0 545462170 86687744 19531 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21164 19531 603 41 0 21123 0
vsize: 84656
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22684 0 0 0 60949 58 0 0 25 0 1 0 545462170 86999040 19596 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21240 19596 603 41 0 21199 0
vsize: 84960
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22755 0 0 0 61949 58 0 0 25 0 1 0 545462170 87322624 19667 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21319 19667 603 41 0 21278 0
vsize: 85276
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22834 0 0 0 62949 58 0 0 25 0 1 0 545462170 87588864 19746 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21384 19746 603 41 0 21343 0
vsize: 85536
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22891 0 0 0 63949 58 0 0 25 0 1 0 545462170 87912448 19803 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21463 19803 603 41 0 21422 0
vsize: 85852
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 22977 0 0 0 64949 58 0 0 25 0 1 0 545462170 88236032 19889 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21542 19889 603 41 0 21501 0
vsize: 86168
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23033 0 0 0 65949 59 0 0 25 0 1 0 545462170 88506368 19945 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21608 19945 603 41 0 21567 0
vsize: 86432
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23100 0 0 0 66949 59 0 0 25 0 1 0 545462170 88793088 20012 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21678 20012 603 41 0 21637 0
vsize: 86712
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23261 0 0 0 67949 59 0 0 25 0 1 0 545462170 89456640 20173 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21840 20173 603 41 0 21799 0
vsize: 87360
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23293 0 0 0 68949 60 0 0 25 0 1 0 545462170 89624576 20205 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21881 20205 603 41 0 21840 0
vsize: 87524
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23346 0 0 0 69949 60 0 0 25 0 1 0 545462170 89759744 20258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21914 20258 603 41 0 21873 0
vsize: 87656
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23404 0 0 0 70949 60 0 0 25 0 1 0 545462170 90030080 20316 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21980 20316 603 41 0 21939 0
vsize: 87920
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1357
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23468 0 0 0 71949 60 0 0 25 0 1 0 545462170 90300416 20380 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22046 20380 603 41 0 22005 0
vsize: 88184
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23541 0 0 0 72949 60 0 0 25 0 1 0 545462170 90570752 20453 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22112 20453 603 41 0 22071 0
vsize: 88448
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23602 0 0 0 73949 60 0 0 25 0 1 0 545462170 90894336 20514 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22191 20514 603 41 0 22150 0
vsize: 88764
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23674 0 0 0 74949 60 0 0 25 0 1 0 545462170 91181056 20586 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22261 20586 603 41 0 22220 0
vsize: 89044
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23724 0 0 0 75949 60 0 0 25 0 1 0 545462170 91377664 20636 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22309 20636 603 41 0 22268 0
vsize: 89236
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23769 0 0 0 76949 61 0 0 25 0 1 0 545462170 91508736 20681 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22341 20681 603 41 0 22300 0
vsize: 89364
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23830 0 0 0 77949 61 0 0 25 0 1 0 545462170 91791360 20742 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22410 20742 603 41 0 22369 0
vsize: 89640
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23901 0 0 0 78949 61 0 0 25 0 1 0 545462170 92106752 20813 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22487 20813 603 41 0 22446 0
vsize: 89948
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 23958 0 0 0 79949 61 0 0 25 0 1 0 545462170 92344320 20870 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22545 20870 603 41 0 22504 0
vsize: 90180
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24030 0 0 0 80950 61 0 0 25 0 1 0 545462170 92610560 20942 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22610 20942 603 41 0 22569 0
vsize: 90440
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24085 0 0 0 81949 61 0 0 25 0 1 0 545462170 92876800 20997 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22675 20997 603 41 0 22634 0
vsize: 90700
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24152 0 0 0 82949 61 0 0 25 0 1 0 545462170 93192192 21064 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22752 21064 603 41 0 22711 0
vsize: 91008
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24226 0 0 0 83949 62 0 0 25 0 1 0 545462170 93511680 21138 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21138 603 41 0 22789 0
vsize: 91320
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24310 0 0 0 84949 62 0 0 25 0 1 0 545462170 93773824 21222 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22894 21222 603 41 0 22853 0
vsize: 91576
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24404 0 0 0 85949 62 0 0 25 0 1 0 545462170 94175232 21316 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22992 21316 603 41 0 22951 0
vsize: 91968
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24472 0 0 0 86949 63 0 0 25 0 1 0 545462170 94441472 21384 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23057 21385 603 41 0 23016 0
vsize: 92228
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24533 0 0 0 87949 63 0 0 25 0 1 0 545462170 94707712 21445 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23122 21445 603 41 0 23081 0
vsize: 92488
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24600 0 0 0 88949 63 0 0 25 0 1 0 545462170 94978048 21512 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23188 21512 603 41 0 23147 0
vsize: 92752
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24608 0 0 0 89949 63 0 0 25 0 1 0 545462170 94978048 21520 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23188 21520 603 41 0 23147 0
vsize: 92752
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24713 0 0 0 90949 63 0 0 25 0 1 0 545462170 95510528 21625 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23318 21625 603 41 0 23277 0
vsize: 93272
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24760 0 0 0 91949 63 0 0 25 0 1 0 545462170 95666176 21672 4294967295 134512640 134672761 3221224624 3221223808 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23356 21672 603 41 0 23315 0
vsize: 93424
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24837 0 0 0 92949 64 0 0 25 0 1 0 545462170 95936512 21749 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23422 21749 603 41 0 23381 0
vsize: 93688
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24907 0 0 0 93949 64 0 0 25 0 1 0 545462170 96387072 21819 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23532 21819 603 41 0 23491 0
vsize: 94128
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 24966 0 0 0 94949 64 0 0 25 0 1 0 545462170 96522240 21878 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23565 21878 603 41 0 23524 0
vsize: 94260
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25018 0 0 0 95949 64 0 0 25 0 1 0 545462170 96792576 21930 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23631 21930 603 41 0 23590 0
vsize: 94524
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25068 0 0 0 96949 65 0 0 25 0 1 0 545462170 96935936 21980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23666 21980 603 41 0 23625 0
vsize: 94664
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25109 0 0 0 97949 65 0 0 25 0 1 0 545462170 97202176 22021 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23731 22021 603 41 0 23690 0
vsize: 94924
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25152 0 0 0 98949 65 0 0 25 0 1 0 545462170 97337344 22064 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23764 22064 603 41 0 23723 0
vsize: 95056
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25229 0 0 0 99949 65 0 0 25 0 1 0 545462170 97607680 22141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23830 22142 603 41 0 23789 0
vsize: 95320
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25274 0 0 0 100949 65 0 0 25 0 1 0 545462170 97873920 22186 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23895 22186 603 41 0 23854 0
vsize: 95580
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1359
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25324 0 0 0 101949 65 0 0 25 0 1 0 545462170 98009088 22236 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23928 22236 603 41 0 23887 0
vsize: 95712
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25389 0 0 0 102949 65 0 0 25 0 1 0 545462170 98271232 22301 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23992 22301 603 41 0 23951 0
vsize: 95968
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25444 0 0 0 103949 66 0 0 25 0 1 0 545462170 98533376 22356 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24056 22356 603 41 0 24015 0
vsize: 96224
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25503 0 0 0 104949 66 0 0 25 0 1 0 545462170 98799616 22415 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24121 22415 603 41 0 24080 0
vsize: 96484
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25582 0 0 0 105949 66 0 0 25 0 1 0 545462170 99090432 22494 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24192 22494 603 41 0 24151 0
vsize: 96768
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25636 0 0 0 106949 66 0 0 25 0 1 0 545462170 99360768 22548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24258 22548 603 41 0 24217 0
vsize: 97032
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25693 0 0 0 107949 66 0 0 25 0 1 0 545462170 99631104 22605 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24324 22605 603 41 0 24283 0
vsize: 97296
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25756 0 0 0 108949 66 0 0 25 0 1 0 545462170 99762176 22668 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24356 22668 603 41 0 24315 0
vsize: 97424
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25809 0 0 0 109949 66 0 0 25 0 1 0 545462170 100028416 22721 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24421 22721 603 41 0 24380 0
vsize: 97684
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25855 0 0 0 110949 66 0 0 25 0 1 0 545462170 100163584 22767 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24454 22767 603 41 0 24413 0
vsize: 97816
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25905 0 0 0 111949 67 0 0 25 0 1 0 545462170 100429824 22817 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24519 22817 603 41 0 24478 0
vsize: 98076
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25949 0 0 0 112949 67 0 0 25 0 1 0 545462170 100564992 22861 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24552 22861 603 41 0 24511 0
vsize: 98208
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 25990 0 0 0 113949 67 0 0 25 0 1 0 545462170 100700160 22902 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24585 22902 603 41 0 24544 0
vsize: 98340
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 26043 0 0 0 114949 67 0 0 25 0 1 0 545462170 101060608 22955 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24673 22955 603 41 0 24632 0
vsize: 98692
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 26094 0 0 0 115949 68 0 0 25 0 1 0 545462170 101191680 23006 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24705 23006 603 41 0 24664 0
vsize: 98820
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 26139 0 0 0 116949 68 0 0 25 0 1 0 545462170 101343232 23051 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24742 23051 603 41 0 24701 0
vsize: 98968
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 26188 0 0 0 117949 68 0 0 25 0 1 0 545462170 101613568 23100 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24808 23100 603 41 0 24767 0
vsize: 99232
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 26239 0 0 0 118948 68 0 0 25 0 1 0 545462170 101744640 23151 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24840 23151 603 41 0 24799 0
vsize: 99360
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 1361
Raw data (stat): 1352 (minisat+) R 1351 22929 22928 0 -1 0 26283 0 0 0 119949 68 0 0 25 0 1 0 545462170 102006784 23195 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24904 23195 603 41 0 24863 0
vsize: 99616
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.92 1/55 1361
Raw data (stat): 1352 (minisat+) Z 1351 22929 22928 0 -1 12 26285 0 0 0 119949 73 0 0 25 0 1 0 545462170 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.08
CPU time (s): 1200.22
CPU user time (s): 1199.49
CPU system time (s): 0.732888
CPU usage (%): 100.012
Max. virtual memory (Kb): 99616
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####