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 15397

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        516808 kB
Buffers:         33880 kB
Cached:         460560 kB
SwapCached:         56 kB
Active:          34636 kB
Inactive:       462604 kB
HighTotal:      131008 kB
HighFree:        40516 kB
LowTotal:       903652 kB
LowFree:        476292 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            15060 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:36:18 (client local time) WITH STATUS 0 IN 1200.47 SECONDS
stats: 17706 7 1200.47 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3225 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[3223]---> Adder-cost: 26498   maxlim: 479706816   bits: 29/29
c ---[3222]---> BDD-cost: 2265
c ---[3221]---> BDD-cost:   25
c ---[3210]---> BDD-cost:   23
c ---[3199]---> BDD-cost:    9
c ---[3188]---> BDD-cost:   21
c ---[3177]---> BDD-cost:   27
c ---[3138]---> BDD-cost:  461
c ---[3135]---> BDD-cost:    5
c ---[3114]---> Adder-cost: 1804   maxlim: 2264275   bits: 22/22
c ---[3113]---> BDD-cost:   29
c ---[3102]---> BDD-cost:   19
c ---[3091]---> BDD-cost:    7
c ---[3080]---> BDD-cost:    5
c ---[3069]---> BDD-cost:    5
c ---[3058]---> BDD-cost:    5
c ---[3037]---> BDD-cost:   29
c ---[3026]---> BDD-cost:   27
c ---[3015]---> BDD-cost:   27
c ---[3004]---> BDD-cost: 3790
c ---[3003]---> BDD-cost:    5
c ---[2992]---> BDD-cost:    5
c ---[2981]---> BDD-cost:   29
c ---[2970]---> BDD-cost:   27
c ---[2959]---> BDD-cost:   11
c ---[2948]---> BDD-cost:    9
c ---[2930]---> BDD-cost:  485
c ---[2927]---> BDD-cost:   19
c ---[2916]---> BDD-cost:   19
c ---[2905]---> BDD-cost:   27
c ---[2894]---> BDD-cost: 1005
c ---[2893]---> BDD-cost:   19
c ---[2872]---> BDD-cost:   21
c ---[2839]---> BDD-cost:   19
c ---[2828]---> BDD-cost:   19
c ---[2796]---> BDD-cost:   21
c ---[2785]---> Sorter-cost:17311     Base: 5 2 5 2 3 2 2 2 2 2
c ---[2784]---> BDD-cost:    3
c ---[2773]---> BDD-cost:   29
c ---[2752]---> BDD-cost:   29
c ---[2741]---> BDD-cost:   27
c ---[2730]---> BDD-cost:   29
c ---[2711]---> BDD-cost:  461
c ---[2699]---> BDD-cost:    3
c ---[2688]---> BDD-cost:   13
c ---[2677]---> Adder-cost: 1438   maxlim: 1767687   bits: 21/21
c ---[2665]---> BDD-cost:    3
c ---[2654]---> BDD-cost:    3
c ---[2632]---> BDD-cost:    3
c ---[2621]---> BDD-cost:    3
c ---[2610]---> BDD-cost:   21
c ---[2589]---> BDD-cost:   23
c ---[2568]---> Adder-cost: 1090   maxlim: 131883   bits: 18/18
c ---[2567]---> BDD-cost:    3
c ---[2524]---> BDD-cost:    3
c ---[2505]---> BDD-cost:  461
c ---[2503]---> BDD-cost:   23
c ---[2472]---> BDD-cost:   29
c ---[2461]---> Sorter-cost:10972     Base: 2 5 5 3 11 3 2
c ---[2460]---> BDD-cost:   29
c ---[2438]---> BDD-cost:    3
c ---[2367]---> BDD-cost:   27
c ---[2356]---> BDD-cost: 1027
c ---[2355]---> BDD-cost:   29
c ---[2324]---> BDD-cost:    3
c ---[2305]---> BDD-cost:  461
c ---[2283]---> BDD-cost:    3
c ---[2261]---> BDD-cost:    3
c ---[2250]---> BDD-cost:  196
c ---[2239]---> BDD-cost:    5
c ---[2218]---> BDD-cost:   11
c ---[2207]---> BDD-cost:    7
c ---[2196]---> BDD-cost:   15
c ---[2166]---> BDD-cost:   19
c ---[2143]---> Adder-cost: 477   maxlim: 2053920   bits: 22/21
c ---[2142]---> BDD-cost:   81
c ---[2141]---> BDD-cost:   19
c ---[2130]---> BDD-cost:   19
c ---[2119]---> BDD-cost:   17
c ---[2108]---> BDD-cost:   17
c ---[2099]---> BDD-cost:  527
c ---[2097]---> BDD-cost:   19
c ---[2086]---> BDD-cost:   19
c ---[2075]---> BDD-cost:   19
c ---[2033]---> BDD-cost:  171
c ---[2011]---> BDD-cost:   19
c ---[2000]---> BDD-cost:   17
c ---[1989]---> BDD-cost:   19
c ---[1978]---> BDD-cost:   19
c ---[1967]---> BDD-cost:   19
c ---[1946]---> BDD-cost:   21
c ---[1935]---> BDD-cost:   19
c ---[1924]---> BDD-cost:  131
c ---[1923]---> BDD-cost:   17
c ---[1912]---> BDD-cost:   19
c ---[1880]---> BDD-cost:    3
c ---[1869]---> BDD-cost:   15
c ---[1865]---> BDD-cost:  551
c ---[1858]---> BDD-cost:   13
c ---[1848]---> BDD-cost:   19
c ---[1827]---> BDD-cost:   19
c ---[1816]---> BDD-cost:   74
c ---[1815]---> BDD-cost:   19
c ---[1794]---> BDD-cost:   19
c ---[1773]---> BDD-cost:   19
c ---[1752]---> BDD-cost:   19
c ---[1741]---> BDD-cost:   19
c ---[1712]---> BDD-cost:   51
c ---[1711]---> BDD-cost:   15
c ---[1693]---> BDD-cost:   19
c ---[1672]---> BDD-cost:    3
c ---[1661]---> BDD-cost:   15
c ---[1650]---> BDD-cost:   19
c ---[1639]---> BDD-cost:   19
c ---[1628]---> BDD-cost:   19
c ---[1627]---> BDD-cost:  488
c ---[1612]---> BDD-cost:   29
c ---[1611]---> BDD-cost:   17
c ---[1602]---> BDD-cost:   19
c ---[1594]---> BDD-cost:   19
c ---[1577]---> BDD-cost:   19
c ---[1558]---> BDD-cost:   19
c ---[1547]---> BDD-cost:   15
c ---[1526]---> BDD-cost:   17
c ---[1518]---> BDD-cost:    3
c ---[1513]---> BDD-cost:   17
c ---[1482]---> BDD-cost:    7
c ---[1462]---> BDD-cost:  335
c ---[1451]---> BDD-cost:    3
c ---[1430]---> BDD-cost:   17
c ---[1339]---> BDD-cost:   17
c ---[1338]---> BDD-cost:   11
c ---[1327]---> BDD-cost:    7
c ---[1316]---> BDD-cost:  416
c ---[1306]---> BDD-cost:   17
c ---[1295]---> BDD-cost:    5
c ---[1284]---> BDD-cost:    3
c ---[1273]---> BDD-cost:    3
c ---[1262]---> BDD-cost:    7
c ---[1251]---> BDD-cost:    7
c ---[1240]---> BDD-cost:   19
c ---[1229]---> BDD-cost:   19
c ---[1218]---> BDD-cost:   19
c ---[1207]---> BDD-cost:    5
c ---[1196]---> BDD-cost:   17
c ---[1185]---> BDD-cost:   19
c ---[1163]---> BDD-cost:   29
c ---[1152]---> BDD-cost:   29
c ---[1141]---> BDD-cost:   29
c ---[1130]---> BDD-cost:   29
c ---[1128]---> BDD-cost:  260
c ---[1119]---> Adder-cost: 2340   maxlim: 3201964   bits: 22/22
c ---[1118]---> BDD-cost:   21
c ---[1117]---> BDD-cost:   29
c ---[1106]---> BDD-cost:   23
c ---[1095]---> BDD-cost:   17
c ---[1084]---> BDD-cost:   17
c ---[1073]---> BDD-cost:   17
c ---[1062]---> BDD-cost:    7
c ---[1051]---> BDD-cost:    7
c ---[1019]---> BDD-cost:   21
c ---[1008]---> BDD-cost:   29
c ---[1007]---> BDD-cost:    7
c ---[ 996]---> BDD-cost:    5
c ---[ 988]---> BDD-cost:  212
c ---[ 985]---> BDD-cost:    5
c ---[ 974]---> BDD-cost:    5
c ---[ 963]---> BDD-cost:    7
c ---[ 952]---> BDD-cost:    9
c ---[ 931]---> BDD-cost:    5
c ---[ 920]---> BDD-cost:   21
c ---[ 909]---> BDD-cost:   17
c ---[ 891]---> BDD-cost:  161
c ---[ 888]---> BDD-cost:   27
c ---[ 877]---> BDD-cost:   17
c ---[ 866]---> BDD-cost:   17
c ---[ 855]---> BDD-cost:   27
c ---[ 844]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   65
c ---[ 813]---> BDD-cost:   27
c ---[ 802]---> BDD-cost:   19
c ---[ 790]---> BDD-cost:   29
c ---[ 780]---> BDD-cost:   32
c ---[ 779]---> BDD-cost:   23
c ---[ 761]---> BDD-cost:   50
c ---[ 739]---> BDD-cost:   38
c ---[ 738]---> BDD-cost:   21
c ---[ 727]---> BDD-cost:   23
c ---[ 719]---> BDD-cost:   26
c ---[ 704]---> BDD-cost:   17
c ---[ 695]---> BDD-cost:   21
c ---[ 689]---> BDD-cost:   17
c ---[ 684]---> BDD-cost:   11
c ---[ 683]---> BDD-cost:   23
c ---[ 678]---> BDD-cost:   14
c ---[ 672]---> BDD-cost:   11
c ---[ 669]---> BDD-cost:   19
c ---[ 666]---> BDD-cost:   19
c ---[ 664]---> BDD-cost:   29
c ---[ 663]---> BDD-cost:   29
c ---[ 662]---> BDD-cost:   19
c ---[ 661]---> BDD-cost:   29
c ---[ 660]---> BDD-cost:   29
c ---[ 659]---> BDD-cost:   23
c ---[ 658]---> BDD-cost:   25
c ---[ 657]---> BDD-cost:   29
c ---[ 656]---> BDD-cost:   27
c ---[ 655]---> BDD-cost:   19
c ---[ 654]---> BDD-cost:   19
c ---[ 653]---> BDD-cost:   19
c ---[ 652]---> BDD-cost:   19
c ---[ 651]---> BDD-cost:   19
c ---[ 650]---> BDD-cost:   17
c ---[ 649]---> BDD-cost:   19
c ---[ 648]---> BDD-cost:    9
c ---[ 647]---> BDD-cost:   19
c ---[ 644]---> BDD-cost:   23
c ---[ 643]---> BDD-cost:   27
c ---[ 642]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:   19
c ---[ 640]---> BDD-cost:    3
c ---[ 639]---> BDD-cost:   25
c ---[ 637]---> BDD-cost:   23
c ---[ 636]---> BDD-cost:   27
c ---[ 635]---> BDD-cost:   21
c ---[ 634]---> BDD-cost:   15
c ---[ 633]---> BDD-cost:   15
c ---[ 628]---> BDD-cost:    3
c ---[ 627]---> BDD-cost: 1925
c ---[ 626]---> BDD-cost:    5
c ---[ 625]---> BDD-cost:   29
c ---[ 624]---> BDD-cost:   29
c ---[ 623]---> BDD-cost:   29
c ---[ 622]---> BDD-cost:   29
c ---[ 621]---> BDD-cost:   19
c ---[ 620]---> BDD-cost:   21
c ---[ 619]---> BDD-cost:   19
c ---[ 618]---> BDD-cost:   19
c ---[ 616]---> BDD-cost:   19
c ---[ 615]---> BDD-cost:   19
c ---[ 614]---> BDD-cost:   17
c ---[ 613]---> BDD-cost:   19
c ---[ 612]---> BDD-cost:   15
c ---[ 611]---> BDD-cost:   27
c ---[ 610]---> BDD-cost:    3
c ---[ 609]---> BDD-cost:    9
c ---[ 608]---> BDD-cost:    9
c ---[ 607]---> BDD-cost:    7
c ---[ 606]---> BDD-cost:   19
c ---[ 604]---> BDD-cost:   29
c ---[ 603]---> BDD-cost:   23
c ---[ 602]---> BDD-cost:   21
c ---[ 601]---> BDD-cost:   27
c ---[ 600]---> BDD-cost:   23
c ---[ 598]---> BDD-cost:   23
c ---[ 597]---> BDD-cost:   19
c ---[ 596]---> BDD-cost:   29
c ---[ 595]---> BDD-cost:   27
c ---[ 594]---> BDD-cost:   23
c ---[ 593]---> BDD-cost:   25
c ---[ 592]---> BDD-cost:   19
c ---[ 591]---> BDD-cost:   23
c ---[ 590]---> BDD-cost:   27
c ---[ 584]---> BDD-cost:   23
c ---[ 581]---> BDD-cost:   23
c ---[ 580]---> BDD-cost:   19
c ---[ 579]---> BDD-cost:  659
c ---[ 575]---> BDD-cost:   29
c ---[ 554]---> BDD-cost:   19
c ---[ 543]---> Adder-cost: 1584   maxlim: 1898736   bits: 21/21
c ---[ 542]---> BDD-cost:   19
c ---[ 477]---> BDD-cost:   29
c ---[ 466]---> BDD-cost:   23
c ---[ 444]---> BDD-cost:   15
c ---[ 433]---> Adder-cost: 1568   maxlim: 1898736   bits: 21/21
c ---[ 422]---> BDD-cost:   23
c ---[ 400]---> BDD-cost:    5
c ---[ 378]---> BDD-cost:   27
c ---[ 367]---> BDD-cost:   11
c ---[ 356]---> BDD-cost:   29
c ---[ 345]---> BDD-cost:   19
c ---[ 324]---> Adder-cost: 1704   maxlim: 2180627   bits: 22/22
c ---[ 312]---> BDD-cost:   21
c ---[ 279]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:   29
c ---[ 260]---> BDD-cost:  305
c ---[ 246]---> BDD-cost:   29
c ---[ 235]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:   29
c ---[ 213]---> Adder-cost: 1576   maxlim: 1898736   bits: 21/21
c ---[ 212]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   15
c ---[ 190]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   23
c ---[ 158]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:  461
c ---[ 115]---> BDD-cost:    5
c ---[ 105]---> Adder-cost: 1630   maxlim: 1978736   bits: 21/21
c ---[  83]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   27
c ---[  61]---> BDD-cost:    5
c ---[  40]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  461410  1485049 |  153803       0        0     nan |  0.000 % |
c |       100 |  461043  1483794 |  169183      46      131     2.8 |  0.779 % |
c |       250 |  460895  1483378 |  186101     179     1632     9.1 |  0.814 % |
c |       475 |  460881  1483332 |  204711     368     5358    14.6 |  0.816 % |
c |       812 |  460881  1483332 |  225182     705    15475    22.0 |  0.816 % |
c |      1319 |  460881  1483332 |  247701    1212    43424    35.8 |  0.816 % |
c |      2078 |  460881  1483332 |  272471    1971    68179    34.6 |  0.816 % |
c |      3217 |  460584  1482289 |  299718    1725    32091    18.6 |  0.871 % |
c |      4925 |  460364  1481511 |  329690    3355    98483    29.4 |  0.914 % |
c |      7488 |  460268  1481193 |  362659    5904   228276    38.7 |  0.936 % |
c |     11332 |  458920  1477448 |  398925    9128   392619    43.0 |  1.277 % |
c |     17098 |  458259  1475233 |  438817   14574   596570    40.9 |  1.408 % |
c |     25748 |  456823  1471181 |  482699   22288   901893    40.5 |  1.778 % |
c |     38722 |  451079  1454518 |  530969   33212  1356238    40.8 |  3.257 % |
c |     58184 |  447142  1442999 |  584066   49694  1984102    39.9 |  4.187 % |
c |     87376 |  437672  1419569 |  642473   77699  3119799    40.2 |  7.179 % |
c |    131166 |  434055  1409723 |  706720  118805  5264900    44.3 |  8.167 % |
c |    196851 |  432908  1406485 |  777392  184232  7678843    41.7 |  8.461 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.98 0.92 2/54 4563
Raw data (stat): 4563 (runsolver) R 4562 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483901732 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0008 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 3566 0 0 0 989 9 0 0 25 0 1 0 483901732 10706944 2139 4294967295 134512640 134672761 3221224560 3221222256 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.0097 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 3566 0 0 0 1990 9 0 0 25 0 1 0 483901732 10706944 2139 4294967295 134512640 134672761 3221224560 3221222112 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+30.0109 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 9425 0 0 0 2977 23 0 0 25 0 1 0 483901732 28606464 6337 4294967295 134512640 134672761 3221224560 3221216592 134565208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6984 6337 603 41 0 6943 0
vsize: 27936
[startup+40.0113 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 16371 0 0 0 3958 41 0 0 25 0 1 0 483901732 59797504 13268 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14599 13268 603 41 0 14558 0
vsize: 58396
[startup+50.0112 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 16525 0 0 0 4958 41 0 0 25 0 1 0 483901732 60334080 13422 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14730 13422 603 41 0 14689 0
vsize: 58920
[startup+60.012 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 16759 0 0 0 5957 42 0 0 25 0 1 0 483901732 61296640 13656 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14965 13656 603 41 0 14924 0
vsize: 59860
[startup+70.0132 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 16874 0 0 0 6957 42 0 0 25 0 1 0 483901732 61698048 13771 4294967295 134512640 134672761 3221224560 3221223696 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15063 13771 603 41 0 15022 0
vsize: 60252
[startup+80.0146 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 16894 0 0 0 7957 42 0 0 25 0 1 0 483901732 61833216 13791 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15096 13791 603 41 0 15055 0
vsize: 60384
[startup+90.0145 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 17057 0 0 0 8957 43 0 0 25 0 1 0 483901732 62500864 13954 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 13954 603 41 0 15218 0
vsize: 61036
[startup+100.014 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 17174 0 0 0 9956 43 0 0 25 0 1 0 483901732 62906368 14071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15358 14071 603 41 0 15317 0
vsize: 61432
[startup+110.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 17365 0 0 0 10956 44 0 0 25 0 1 0 483901732 63700992 14262 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15552 14262 603 41 0 15511 0
vsize: 62208
[startup+120.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 17456 0 0 0 11956 44 0 0 25 0 1 0 483901732 64098304 14353 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15649 14353 603 41 0 15608 0
vsize: 62596
[startup+130.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 17644 0 0 0 12955 45 0 0 25 0 1 0 483901732 64905216 14541 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15846 14541 603 41 0 15805 0
vsize: 63384
[startup+140.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 17695 0 0 0 13955 45 0 0 25 0 1 0 483901732 65040384 14592 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15879 14592 603 41 0 15838 0
vsize: 63516
[startup+150.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 17813 0 0 0 14955 45 0 0 25 0 1 0 483901732 65581056 14710 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16011 14710 603 41 0 15970 0
vsize: 64044
[startup+160.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 17922 0 0 0 15955 45 0 0 25 0 1 0 483901732 65986560 14819 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16110 14819 603 41 0 16069 0
vsize: 64440
[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18013 0 0 0 16955 46 0 0 25 0 1 0 483901732 66387968 14910 4294967295 134512640 134672761 3221224560 3221223732 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16208 14910 603 41 0 16167 0
vsize: 64832
[startup+180.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18092 0 0 0 17955 46 0 0 25 0 1 0 483901732 66654208 14989 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16273 14989 603 41 0 16232 0
vsize: 65092
[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18135 0 0 0 18955 46 0 0 25 0 1 0 483901732 66916352 15032 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16337 15032 603 41 0 16296 0
vsize: 65348
[startup+200.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18198 0 0 0 19955 46 0 0 25 0 1 0 483901732 67186688 15095 4294967295 134512640 134672761 3221224560 3221223760 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16403 15095 603 41 0 16362 0
vsize: 65612
[startup+210.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18284 0 0 0 20955 46 0 0 25 0 1 0 483901732 67588096 15181 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16501 15181 603 41 0 16460 0
vsize: 66004
[startup+220.121 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18334 0 0 0 21966 46 0 0 25 0 1 0 483901732 67719168 15231 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16533 15231 603 41 0 16492 0
vsize: 66132
[startup+230.122 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18489 0 0 0 22966 46 0 0 25 0 1 0 483901732 68386816 15386 4294967295 134512640 134672761 3221224560 3221223732 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16696 15386 603 41 0 16655 0
vsize: 66784
[startup+240.122 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18581 0 0 0 23965 47 0 0 25 0 1 0 483901732 68788224 15478 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16794 15478 603 41 0 16753 0
vsize: 67176
[startup+250.122 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18640 0 0 0 24965 47 0 0 25 0 1 0 483901732 69062656 15537 4294967295 134512640 134672761 3221224560 3221223716 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16861 15537 603 41 0 16820 0
vsize: 67444
[startup+260.123 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18665 0 0 0 25966 47 0 0 25 0 1 0 483901732 69062656 15562 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16861 15562 603 41 0 16820 0
vsize: 67444
[startup+270.122 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18711 0 0 0 26966 47 0 0 25 0 1 0 483901732 69332992 15608 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16927 15608 603 41 0 16886 0
vsize: 67708
[startup+280.123 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18841 0 0 0 27966 47 0 0 25 0 1 0 483901732 69873664 15738 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17059 15738 603 41 0 17018 0
vsize: 68236
[startup+290.123 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 18971 0 0 0 28965 48 0 0 25 0 1 0 483901732 70275072 15868 4294967295 134512640 134672761 3221224560 3221223776 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17157 15868 603 41 0 17116 0
vsize: 68628
[startup+300.123 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 19168 0 0 0 29965 49 0 0 25 0 1 0 483901732 71077888 16065 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17353 16065 603 41 0 17312 0
vsize: 69412
[startup+310.124 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 19206 0 0 0 30965 49 0 0 25 0 1 0 483901732 71208960 16103 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17385 16103 603 41 0 17344 0
vsize: 69540
[startup+320.125 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 19278 0 0 0 31965 49 0 0 25 0 1 0 483901732 71606272 16175 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17482 16175 603 41 0 17441 0
vsize: 69928
[startup+330.125 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 19393 0 0 0 32965 49 0 0 25 0 1 0 483901732 72011776 16290 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17581 16290 603 41 0 17540 0
vsize: 70324
[startup+340.126 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 19597 0 0 0 33964 50 0 0 25 0 1 0 483901732 72810496 16494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17776 16494 603 41 0 17735 0
vsize: 71104
[startup+350.126 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 19848 0 0 0 34963 51 0 0 25 0 1 0 483901732 74133504 16745 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18099 16745 603 41 0 18058 0
vsize: 72396
[startup+360.127 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 19949 0 0 0 35963 52 0 0 25 0 1 0 483901732 74526720 16846 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18195 16847 603 41 0 18154 0
vsize: 72780
[startup+370.128 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 20045 0 0 0 36963 52 0 0 25 0 1 0 483901732 74924032 16942 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18292 16942 603 41 0 18251 0
vsize: 73168
[startup+380.129 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 20128 0 0 0 37963 52 0 0 25 0 1 0 483901732 75190272 17025 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18357 17025 603 41 0 18316 0
vsize: 73428
[startup+390.128 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 20292 0 0 0 38963 53 0 0 25 0 1 0 483901732 75857920 17189 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18520 17189 603 41 0 18479 0
vsize: 74080
[startup+400.128 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 20456 0 0 0 39962 53 0 0 25 0 1 0 483901732 76525568 17353 4294967295 134512640 134672761 3221224560 3221223748 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18683 17353 603 41 0 18642 0
vsize: 74732
[startup+410.129 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 20602 0 0 0 40962 54 0 0 25 0 1 0 483901732 77193216 17499 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18846 17499 603 41 0 18805 0
vsize: 75384
[startup+420.129 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 20741 0 0 0 41962 54 0 0 25 0 1 0 483901732 77733888 17638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18978 17638 603 41 0 18937 0
vsize: 75912
[startup+430.13 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 20977 0 0 0 42961 55 0 0 25 0 1 0 483901732 78667776 17874 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19206 17874 603 41 0 19165 0
vsize: 76824
[startup+440.131 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 21035 0 0 0 43962 55 0 0 25 0 1 0 483901732 78934016 17932 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19271 17932 603 41 0 19230 0
vsize: 77084
[startup+450.13 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 21073 0 0 0 44962 55 0 0 25 0 1 0 483901732 79065088 17970 4294967295 134512640 134672761 3221224560 3221223776 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19303 17970 603 41 0 19262 0
vsize: 77212
[startup+460.131 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 21170 0 0 0 45962 55 0 0 25 0 1 0 483901732 79470592 18067 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19402 18067 603 41 0 19361 0
vsize: 77608
[startup+470.132 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 21588 0 0 0 46961 56 0 0 25 0 1 0 483901732 81104896 18485 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19801 18485 603 41 0 19760 0
vsize: 79204
[startup+480.133 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 21658 0 0 0 47961 56 0 0 25 0 1 0 483901732 81371136 18555 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19866 18555 603 41 0 19825 0
vsize: 79464
[startup+490.133 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 21795 0 0 0 48961 57 0 0 25 0 1 0 483901732 81903616 18692 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19996 18692 603 41 0 19955 0
vsize: 79984
[startup+500.132 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 21983 0 0 0 49960 57 0 0 25 0 1 0 483901732 82702336 18880 4294967295 134512640 134672761 3221224560 3221223696 134565078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20191 18880 603 41 0 20150 0
vsize: 80764
[startup+510.133 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 22095 0 0 0 50960 58 0 0 25 0 1 0 483901732 83103744 18992 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20289 18992 603 41 0 20248 0
vsize: 81156
[startup+520.133 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 22166 0 0 0 51960 58 0 0 25 0 1 0 483901732 83505152 19063 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20387 19063 603 41 0 20346 0
vsize: 81548
[startup+530.134 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 22428 0 0 0 52959 59 0 0 25 0 1 0 483901732 84447232 19325 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20617 19325 603 41 0 20576 0
vsize: 82468
[startup+540.135 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 22868 0 0 0 53958 60 0 0 25 0 1 0 483901732 86315008 19765 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21073 19765 603 41 0 21032 0
vsize: 84292
[startup+550.135 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 22982 0 0 0 54957 61 0 0 25 0 1 0 483901732 86716416 19879 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21171 19879 603 41 0 21130 0
vsize: 84684
[startup+560.135 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 23143 0 0 0 55957 61 0 0 25 0 1 0 483901732 87388160 20040 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21335 20040 603 41 0 21294 0
vsize: 85340
[startup+570.136 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 23289 0 0 0 56957 61 0 0 25 0 1 0 483901732 87924736 20186 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21466 20186 603 41 0 21425 0
vsize: 85864
[startup+580.137 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 23395 0 0 0 57957 62 0 0 25 0 1 0 483901732 88850432 20292 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21692 20292 603 41 0 21651 0
vsize: 86768
[startup+590.137 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 23475 0 0 0 58957 62 0 0 25 0 1 0 483901732 89251840 20372 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21790 20372 603 41 0 21749 0
vsize: 87160
[startup+600.137 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 23589 0 0 0 59957 62 0 0 25 0 1 0 483901732 89649152 20486 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21887 20486 603 41 0 21846 0
vsize: 87548
[startup+610.138 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 23734 0 0 0 60957 62 0 0 25 0 1 0 483901732 90324992 20631 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22052 20631 603 41 0 22011 0
vsize: 88208
[startup+620.139 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 23824 0 0 0 61957 63 0 0 25 0 1 0 483901732 90595328 20721 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22118 20721 603 41 0 22077 0
vsize: 88472
[startup+630.139 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 23938 0 0 0 62956 63 0 0 25 0 1 0 483901732 91140096 20835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22251 20835 603 41 0 22210 0
vsize: 89004
[startup+640.14 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 24059 0 0 0 63956 64 0 0 25 0 1 0 483901732 91541504 20956 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22349 20956 603 41 0 22308 0
vsize: 89396
[startup+650.144 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 24152 0 0 0 64957 64 0 0 25 0 1 0 483901732 91938816 21049 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22446 21049 603 41 0 22405 0
vsize: 89784
[startup+660.145 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 24280 0 0 0 65957 64 0 0 25 0 1 0 483901732 92475392 21177 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22577 21177 603 41 0 22536 0
vsize: 90308
[startup+670.145 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 24381 0 0 0 66956 65 0 0 25 0 1 0 483901732 92876800 21278 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22675 21278 603 41 0 22634 0
vsize: 90700
[startup+680.146 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 24517 0 0 0 67956 65 0 0 25 0 1 0 483901732 93417472 21414 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22807 21414 603 41 0 22766 0
vsize: 91228
[startup+690.146 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 24623 0 0 0 68956 66 0 0 25 0 1 0 483901732 93822976 21520 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22906 21520 603 41 0 22865 0
vsize: 91624
[startup+700.146 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 24699 0 0 0 69956 66 0 0 25 0 1 0 483901732 94101504 21596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22974 21596 603 41 0 22933 0
vsize: 91896
[startup+710.147 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 24815 0 0 0 70956 66 0 0 25 0 1 0 483901732 94650368 21712 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23108 21712 603 41 0 23067 0
vsize: 92432
[startup+720.239 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25013 0 0 0 71964 67 0 0 25 0 1 0 483901732 95477760 21910 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23310 21910 603 41 0 23269 0
vsize: 93240
[startup+730.24 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25142 0 0 0 72964 67 0 0 25 0 1 0 483901732 96010240 22039 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23440 22039 603 41 0 23399 0
vsize: 93760
[startup+740.24 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25244 0 0 0 73965 67 0 0 25 0 1 0 483901732 96415744 22141 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23539 22141 603 41 0 23498 0
vsize: 94156
[startup+750.24 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25378 0 0 0 74965 67 0 0 25 0 1 0 483901732 96956416 22275 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23671 22275 603 41 0 23630 0
vsize: 94684
[startup+760.24 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25466 0 0 0 75964 68 0 0 25 0 1 0 483901732 97234944 22363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23739 22363 603 41 0 23698 0
vsize: 94956
[startup+770.24 s]
Raw data (loadavg): 0.99 0.98 0.92 3/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25532 0 0 0 76964 68 0 0 25 0 1 0 483901732 97505280 22429 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23805 22429 603 41 0 23764 0
vsize: 95220
[startup+780.243 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25613 0 0 0 77965 68 0 0 25 0 1 0 483901732 97771520 22510 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23870 22510 603 41 0 23829 0
vsize: 95480
[startup+790.244 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25725 0 0 0 78964 69 0 0 25 0 1 0 483901732 98324480 22622 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24005 22622 603 41 0 23964 0
vsize: 96020
[startup+800.243 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25807 0 0 0 79964 69 0 0 25 0 1 0 483901732 98603008 22704 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24073 22704 603 41 0 24032 0
vsize: 96292
[startup+810.244 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25889 0 0 0 80964 69 0 0 25 0 1 0 483901732 99004416 22786 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24171 22786 603 41 0 24130 0
vsize: 96684
[startup+820.244 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 25964 0 0 0 81964 69 0 0 25 0 1 0 483901732 99287040 22861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24240 22861 603 41 0 24199 0
vsize: 96960
[startup+830.245 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26026 0 0 0 82964 69 0 0 25 0 1 0 483901732 99557376 22923 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24306 22923 603 41 0 24265 0
vsize: 97224
[startup+840.245 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26090 0 0 0 83963 70 0 0 25 0 1 0 483901732 99840000 22987 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24375 22987 603 41 0 24334 0
vsize: 97500
[startup+850.246 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26166 0 0 0 84963 70 0 0 25 0 1 0 483901732 100126720 23063 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24445 23063 603 41 0 24404 0
vsize: 97780
[startup+860.246 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26254 0 0 0 85963 70 0 0 25 0 1 0 483901732 100405248 23151 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24513 23151 603 41 0 24472 0
vsize: 98052
[startup+870.246 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26301 0 0 0 86963 70 0 0 25 0 1 0 483901732 100667392 23198 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24577 23198 603 41 0 24536 0
vsize: 98308
[startup+880.247 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26371 0 0 0 87963 71 0 0 25 0 1 0 483901732 100929536 23268 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24641 23268 603 41 0 24600 0
vsize: 98564
[startup+890.247 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26455 0 0 0 88963 71 0 0 25 0 1 0 483901732 101195776 23352 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24706 23352 603 41 0 24665 0
vsize: 98824
[startup+900.246 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26560 0 0 0 89963 71 0 0 25 0 1 0 483901732 101732352 23457 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24837 23457 603 41 0 24796 0
vsize: 99348
[startup+910.247 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26609 0 0 0 90963 71 0 0 25 0 1 0 483901732 101863424 23506 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24869 23506 603 41 0 24828 0
vsize: 99476
[startup+920.247 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26641 0 0 0 91963 71 0 0 25 0 1 0 483901732 101994496 23538 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24901 23538 603 41 0 24860 0
vsize: 99604
[startup+930.248 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26690 0 0 0 92963 72 0 0 25 0 1 0 483901732 102264832 23587 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24967 23587 603 41 0 24926 0
vsize: 99868
[startup+940.249 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26749 0 0 0 93964 72 0 0 25 0 1 0 483901732 102395904 23646 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24999 23646 603 41 0 24958 0
vsize: 99996
[startup+950.249 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26812 0 0 0 94963 72 0 0 25 0 1 0 483901732 102666240 23709 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25065 23709 603 41 0 25024 0
vsize: 100260
[startup+960.25 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 26895 0 0 0 95963 72 0 0 25 0 1 0 483901732 103075840 23792 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25165 23792 603 41 0 25124 0
vsize: 100660
[startup+970.25 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27030 0 0 0 96963 73 0 0 25 0 1 0 483901732 103616512 23927 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25297 23927 603 41 0 25256 0
vsize: 101188
[startup+980.251 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27150 0 0 0 97963 73 0 0 25 0 1 0 483901732 104148992 24047 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25427 24047 603 41 0 25386 0
vsize: 101708
[startup+990.255 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27239 0 0 0 98964 73 0 0 25 0 1 0 483901732 104419328 24136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25493 24136 603 41 0 25452 0
vsize: 101972
[startup+1000.25 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27294 0 0 0 99964 73 0 0 25 0 1 0 483901732 104689664 24191 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25559 24191 603 41 0 25518 0
vsize: 102236
[startup+1010.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27359 0 0 0 100964 73 0 0 25 0 1 0 483901732 104960000 24256 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25625 24256 603 41 0 25584 0
vsize: 102500
[startup+1020.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27446 0 0 0 101963 74 0 0 25 0 1 0 483901732 105365504 24343 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25724 24343 603 41 0 25683 0
vsize: 102896
[startup+1030.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27526 0 0 0 102963 74 0 0 25 0 1 0 483901732 105631744 24423 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25789 24423 603 41 0 25748 0
vsize: 103156
[startup+1040.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27568 0 0 0 103963 74 0 0 25 0 1 0 483901732 105766912 24465 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25822 24465 603 41 0 25781 0
vsize: 103288
[startup+1050.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27627 0 0 0 104963 75 0 0 25 0 1 0 483901732 106041344 24524 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25889 24524 603 41 0 25848 0
vsize: 103556
[startup+1060.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27678 0 0 0 105964 75 0 0 25 0 1 0 483901732 106176512 24575 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25922 24575 603 41 0 25881 0
vsize: 103688
[startup+1070.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27752 0 0 0 106963 75 0 0 25 0 1 0 483901732 106573824 24649 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26019 24649 603 41 0 25978 0
vsize: 104076
[startup+1080.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27841 0 0 0 107964 75 0 0 25 0 1 0 483901732 106864640 24738 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26090 24738 603 41 0 26049 0
vsize: 104360
[startup+1090.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27899 0 0 0 108964 75 0 0 25 0 1 0 483901732 107130880 24796 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26155 24796 603 41 0 26114 0
vsize: 104620
[startup+1100.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 27951 0 0 0 109964 75 0 0 25 0 1 0 483901732 107397120 24848 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26220 24848 603 41 0 26179 0
vsize: 104880
[startup+1110.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28008 0 0 0 110964 75 0 0 25 0 1 0 483901732 107528192 24905 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26252 24905 603 41 0 26211 0
vsize: 105008
[startup+1120.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28069 0 0 0 111964 76 0 0 25 0 1 0 483901732 107794432 24966 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26317 24966 603 41 0 26276 0
vsize: 105268
[startup+1130.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28166 0 0 0 112964 76 0 0 25 0 1 0 483901732 108199936 25063 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26416 25063 603 41 0 26375 0
vsize: 105664
[startup+1140.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28237 0 0 0 113964 76 0 0 25 0 1 0 483901732 108486656 25134 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26486 25134 603 41 0 26445 0
vsize: 105944
[startup+1150.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28248 0 0 0 114964 76 0 0 25 0 1 0 483901732 108621824 25145 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26519 25145 603 41 0 26478 0
vsize: 106076
[startup+1160.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28302 0 0 0 115964 76 0 0 25 0 1 0 483901732 108756992 25199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26552 25199 603 41 0 26511 0
vsize: 106208
[startup+1170.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28367 0 0 0 116964 76 0 0 25 0 1 0 483901732 109027328 25264 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26618 25264 603 41 0 26577 0
vsize: 106472
[startup+1180.26 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28460 0 0 0 117964 76 0 0 25 0 1 0 483901732 109428736 25357 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26716 25357 603 41 0 26675 0
vsize: 106864
[startup+1190.27 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28551 0 0 0 118965 76 0 0 25 0 1 0 483901732 109830144 25448 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26814 25448 603 41 0 26773 0
vsize: 107256
[startup+1200.27 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 4563
Raw data (stat): 4563 (minisat+) R 4562 10720 10719 0 -1 0 28634 0 0 0 119965 77 0 0 25 0 1 0 483901732 110129152 25531 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26887 25531 603 41 0 26846 0
vsize: 107548
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.32 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 4563
Raw data (stat): 4563 (minisat+) Z 4562 10720 10719 0 -1 12 28636 0 0 0 119965 81 0 0 25 0 1 0 483901732 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.32
CPU time (s): 1200.47
CPU user time (s): 1199.65
CPU system time (s): 0.818875
CPU usage (%): 100.013
Max. virtual memory (Kb): 107548
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####