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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mkc.opb
MD5SUM087a7cd0fdb8b0bf40fe6b459b39a663
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 67108864000
Number of bits of the biggest number in a constraint 36
Biggest sum of numbers in a constraint 138201238403
Number of bits of the biggest sum of numbers38
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1231.44
Number of variables5383
Total number of constraints8734
Number of constraints which are clauses2977
Number of constraints which are cardinality constraints (but not clauses)5731
Number of constraints which are nor clauses,nor cardinality constraints26
Minimum length of a constraint1
Maximum length of a constraint2952

Trace number 4536

Launcher Data

LAUNCH ON wulflinc11 THE 2005-09-19 18:05:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2990 boxname=wulflinc11 idbench=646 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  087a7cd0fdb8b0bf40fe6b459b39a663  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mkc.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mkc.opb
IDLAUNCH: 2990
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        872884 kB
Buffers:         36044 kB
Cached:          98068 kB
SwapCached:        732 kB
Active:          64392 kB
Inactive:        72320 kB
HighTotal:      131008 kB
HighFree:        31304 kB
LowTotal:       903652 kB
LowFree:        841580 kB
SwapTotal:     2097136 kB
SwapFree:      2095856 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            19508 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:25:41 (client local time) WITH STATUS 0 IN 1208.77 SECONDS
stats: 2990 7 1208.77 0

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: 26932   maxlim: 3837654528   bits: 32/32
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: 1788   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: 1434   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: 513   maxlim: 16431360   bits: 25/24
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: 2322   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: 1580   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: 1564   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: 1694   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: 1572   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: 1626   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 |  414808  1347681 |  138269       0        0     nan |  0.000 % |
c |       101 |  414768  1347547 |  152095      96      320     3.3 |  0.810 % |
c |       251 |  414322  1346219 |  167305     165     2258    13.7 |  0.917 % |
c |       476 |  414274  1346055 |  184036     383    12750    33.3 |  0.926 % |
c |       813 |  414274  1346055 |  202439     720    27406    38.1 |  0.926 % |
c |      1321 |  414248  1345967 |  222683    1226    50215    41.0 |  0.932 % |
c |      2080 |  414248  1345967 |  244951    1985    85036    42.8 |  0.932 % |
c |      3224 |  414182  1345739 |  269447    3120   154835    49.6 |  0.941 % |
c |      4932 |  414132  1345577 |  296391    4822   221395    45.9 |  0.952 % |
c |      7494 |  413647  1343876 |  326031    6902   312123    45.2 |  1.037 % |
c |     11339 |  412829  1341428 |  358634   10337   435369    42.1 |  1.217 % |
c |     17107 |  412665  1340868 |  394497   16060   708534    44.1 |  1.246 % |
c |     25757 |  411601  1337588 |  433947   24148  1030724    42.7 |  1.499 % |
c |     38732 |  409992  1332280 |  477342   34582  1524215    44.1 |  1.827 % |
c |     58194 |  406324  1321483 |  525076   49766  2169223    43.6 |  2.697 % |
c |     87388 |  402636  1312012 |  577583   78532  3221744    41.0 |  3.786 % |
c |    131177 |  401986  1310278 |  635342  122095  4836343    39.6 |  3.962 % |
c |    196862 |  399244  1303526 |  698876  187540  7226500    38.5 |  4.837 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/26623/stat): 26623 (minisat+_script) R 26622 26623 9854 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793688730 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26623/statm): 174 3 169 147 0 27 0
[pid=26623] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=26624
New process pid=26625
New process pid=26626
execve syscall for /bin/sed executable
One traced child (pid=26625) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=26626) exited with status: 0
One traced child (pid=26624) exited with status: 0
New process pid=26627
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mkc.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.95 0.87 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 970 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221219696 134677239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 12136

[startup+20.0049 s]
Raw data (loadavg): 0.94 0.96 0.87 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 1971 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220560 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 12136

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 2971 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220280 134677377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 29.86
Current children cumulated vsize (Kb) 12136

[startup+40.0065 s]
Raw data (loadavg): 0.95 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 3971 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220320 134676301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 39.86
Current children cumulated vsize (Kb) 12136

[startup+50.0073 s]
Raw data (loadavg): 0.96 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 4971 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220752 134676532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 49.86
Current children cumulated vsize (Kb) 12136

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 5971 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 59.86
Current children cumulated vsize (Kb) 12136

[startup+70.0089 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 6972 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220576 134676598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 69.87
Current children cumulated vsize (Kb) 12136

[startup+80.0097 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 7972 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221221880 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 79.87
Current children cumulated vsize (Kb) 12136

[startup+90.0105 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 8972 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220644 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 89.87
Current children cumulated vsize (Kb) 12136

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 9973 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 99.88
Current children cumulated vsize (Kb) 12136

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 10973 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221221344 134676341 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 109.88
Current children cumulated vsize (Kb) 12136

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 11973 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220380 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 119.88
Current children cumulated vsize (Kb) 12136

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 12973 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 129.88
Current children cumulated vsize (Kb) 12136

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 13974 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 139.89
Current children cumulated vsize (Kb) 12136

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 14974 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221221084 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 149.89
Current children cumulated vsize (Kb) 12136

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 15974 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 159.89
Current children cumulated vsize (Kb) 12136

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 16974 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220224 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 169.89
Current children cumulated vsize (Kb) 12136

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 17975 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220564 134600159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 179.9
Current children cumulated vsize (Kb) 12136

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 18975 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 189.9
Current children cumulated vsize (Kb) 12136

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 19975 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221221808 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 199.9
Current children cumulated vsize (Kb) 12136

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 20975 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 209.9
Current children cumulated vsize (Kb) 12136

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 21975 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 219.9
Current children cumulated vsize (Kb) 12136

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 22976 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 229.91
Current children cumulated vsize (Kb) 12136

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 23976 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 239.91
Current children cumulated vsize (Kb) 12136

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 24976 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221221360 134677078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 249.91
Current children cumulated vsize (Kb) 12136

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 25976 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220848 134677021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 259.91
Current children cumulated vsize (Kb) 12136

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 26977 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 269.92
Current children cumulated vsize (Kb) 12136

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 27977 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 279.92
Current children cumulated vsize (Kb) 12136

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 28977 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220752 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 289.92
Current children cumulated vsize (Kb) 12136

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 29977 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220556 134677150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 299.92
Current children cumulated vsize (Kb) 12136

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 30978 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 309.93
Current children cumulated vsize (Kb) 12136

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 31978 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221220400 134676598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 319.93
Current children cumulated vsize (Kb) 12136

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 32978 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221221700 134677085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 329.93
Current children cumulated vsize (Kb) 12136

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 3780 0 0 0 33979 14 0 0 25 0 1 0 1793688735 10252288 2291 4294967295 134512640 135094434 3221224432 3221221632 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 2503 2291 145 145 0 2358 0
[pid=26627] vsize: 10012
Current children cumulated CPU time (s) 339.94
Current children cumulated vsize (Kb) 12136

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 8687 0 0 0 34956 31 0 0 25 0 1 0 1793688735 25751552 5918 4294967295 134512640 135094434 3221224432 3221221868 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 6287 5918 145 145 0 6142 0
[pid=26627] vsize: 25148
Current children cumulated CPU time (s) 349.88
Current children cumulated vsize (Kb) 27272

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 8897 0 0 0 35955 31 0 0 25 0 1 0 1793688735 25751552 5918 4294967295 134512640 135094434 3221224432 3221221808 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 6287 5918 145 145 0 6142 0
[pid=26627] vsize: 25148
Current children cumulated CPU time (s) 359.87
Current children cumulated vsize (Kb) 27272

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 9065 0 0 0 36954 32 0 0 25 0 1 0 1793688735 25751552 5918 4294967295 134512640 135094434 3221224432 3221221632 134601168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 6287 5918 145 145 0 6142 0
[pid=26627] vsize: 25148
Current children cumulated CPU time (s) 369.87
Current children cumulated vsize (Kb) 27272

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 16091 0 0 0 37893 62 0 0 25 0 1 0 1793688735 57106432 12909 4294967295 134512640 135094434 3221224432 3221223056 134562146 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 13942 12909 145 145 0 13797 0
[pid=26627] vsize: 55768
Current children cumulated CPU time (s) 379.56
Current children cumulated vsize (Kb) 57892

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 16416 0 0 0 38887 65 0 0 25 0 1 0 1793688735 58441728 13234 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 14268 13234 145 145 0 14123 0
[pid=26627] vsize: 57072
Current children cumulated CPU time (s) 389.53
Current children cumulated vsize (Kb) 59196

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 16535 0 0 0 39885 66 0 0 25 0 1 0 1793688735 58912768 13353 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 14383 13353 145 145 0 14238 0
[pid=26627] vsize: 57532
Current children cumulated CPU time (s) 399.52
Current children cumulated vsize (Kb) 59656

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 16937 0 0 0 40880 69 0 0 25 0 1 0 1793688735 60473344 13755 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 14764 13755 145 145 0 14619 0
[pid=26627] vsize: 59056
Current children cumulated CPU time (s) 409.5
Current children cumulated vsize (Kb) 61180

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 17183 0 0 0 41875 71 0 0 25 0 1 0 1793688735 61509632 14001 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 15017 14001 145 145 0 14872 0
[pid=26627] vsize: 60068
Current children cumulated CPU time (s) 419.47
Current children cumulated vsize (Kb) 62192

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 17314 0 0 0 42872 73 0 0 25 0 1 0 1793688735 62009344 14132 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 15139 14132 145 145 0 14994 0
[pid=26627] vsize: 60556
Current children cumulated CPU time (s) 429.46
Current children cumulated vsize (Kb) 62680

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 17634 0 0 0 43866 76 0 0 25 0 1 0 1793688735 63291392 14452 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 15452 14452 145 145 0 15307 0
[pid=26627] vsize: 61808
Current children cumulated CPU time (s) 439.43
Current children cumulated vsize (Kb) 63932

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 17864 0 0 0 44862 78 0 0 25 0 1 0 1793688735 64217088 14682 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 15678 14682 145 145 0 15533 0
[pid=26627] vsize: 62712
Current children cumulated CPU time (s) 449.41
Current children cumulated vsize (Kb) 64836

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 17906 0 0 0 45861 79 0 0 25 0 1 0 1793688735 64389120 14724 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 15720 14724 145 145 0 15575 0
[pid=26627] vsize: 62880
Current children cumulated CPU time (s) 459.41
Current children cumulated vsize (Kb) 65004

[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18018 0 0 0 46859 80 0 0 25 0 1 0 1793688735 64970752 14836 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 15862 14836 145 145 0 15717 0
[pid=26627] vsize: 63448
Current children cumulated CPU time (s) 469.4
Current children cumulated vsize (Kb) 65572

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18146 0 0 0 47857 80 0 0 25 0 1 0 1793688735 65486848 14964 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 15988 14964 145 145 0 15843 0
[pid=26627] vsize: 63952
Current children cumulated CPU time (s) 479.38
Current children cumulated vsize (Kb) 66076

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18296 0 0 0 48855 82 0 0 25 0 1 0 1793688735 66084864 15114 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 16134 15114 145 145 0 15989 0
[pid=26627] vsize: 64536
Current children cumulated CPU time (s) 489.38
Current children cumulated vsize (Kb) 66660

[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18406 0 0 0 49853 83 0 0 25 0 1 0 1793688735 66527232 15224 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 16242 15224 145 145 0 16097 0
[pid=26627] vsize: 64968
Current children cumulated CPU time (s) 499.37
Current children cumulated vsize (Kb) 67092

[startup+510.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18469 0 0 0 50852 84 0 0 25 0 1 0 1793688735 66781184 15287 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 16304 15287 145 145 0 16159 0
[pid=26627] vsize: 65216
Current children cumulated CPU time (s) 509.37
Current children cumulated vsize (Kb) 67340

[startup+520.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18469 0 0 0 51851 84 0 0 25 0 1 0 1793688735 66781184 15287 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 16304 15287 145 145 0 16159 0
[pid=26627] vsize: 65216
Current children cumulated CPU time (s) 519.36
Current children cumulated vsize (Kb) 67340

[startup+530.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18626 0 0 0 52849 85 0 0 25 0 1 0 1793688735 67407872 15444 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 16457 15444 145 145 0 16312 0
[pid=26627] vsize: 65828
Current children cumulated CPU time (s) 529.35
Current children cumulated vsize (Kb) 67952

[startup+540.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18703 0 0 0 53848 86 0 0 25 0 1 0 1793688735 67719168 15521 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 16533 15521 145 145 0 16388 0
[pid=26627] vsize: 66132
Current children cumulated CPU time (s) 539.35
Current children cumulated vsize (Kb) 68256

[startup+550.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18883 0 0 0 54845 87 0 0 25 0 1 0 1793688735 68440064 15701 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 16709 15701 145 145 0 16564 0
[pid=26627] vsize: 66836
Current children cumulated CPU time (s) 549.33
Current children cumulated vsize (Kb) 68960

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 18948 0 0 0 55844 87 0 0 25 0 1 0 1793688735 68702208 15766 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 16773 15766 145 145 0 16628 0
[pid=26627] vsize: 67092
Current children cumulated CPU time (s) 559.32
Current children cumulated vsize (Kb) 69216

[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 19056 0 0 0 56843 88 0 0 25 0 1 0 1793688735 69136384 15874 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 16879 15874 145 145 0 16734 0
[pid=26627] vsize: 67516
Current children cumulated CPU time (s) 569.32
Current children cumulated vsize (Kb) 69640

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 19175 0 0 0 57840 89 0 0 25 0 1 0 1793688735 69615616 15993 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 16996 15993 145 145 0 16851 0
[pid=26627] vsize: 67984
Current children cumulated CPU time (s) 579.3
Current children cumulated vsize (Kb) 70108

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 19583 0 0 0 58834 91 0 0 25 0 1 0 1793688735 71507968 16401 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 17458 16401 145 145 0 17313 0
[pid=26627] vsize: 69832
Current children cumulated CPU time (s) 589.26
Current children cumulated vsize (Kb) 71956

[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 19914 0 0 0 59828 94 0 0 25 0 1 0 1793688735 72835072 16732 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 17782 16732 145 145 0 17637 0
[pid=26627] vsize: 71128
Current children cumulated CPU time (s) 599.23
Current children cumulated vsize (Kb) 73252

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 20154 0 0 0 60824 95 0 0 25 0 1 0 1793688735 73797632 16972 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 18017 16972 145 145 0 17872 0
[pid=26627] vsize: 72068
Current children cumulated CPU time (s) 609.2
Current children cumulated vsize (Kb) 74192

[startup+620.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 20425 0 0 0 61820 97 0 0 25 0 1 0 1793688735 74887168 17243 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 18283 17243 145 145 0 18138 0
[pid=26627] vsize: 73132
Current children cumulated CPU time (s) 619.18
Current children cumulated vsize (Kb) 75256

[startup+630.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 20533 0 0 0 62818 98 0 0 25 0 1 0 1793688735 75317248 17351 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 18388 17351 145 145 0 18243 0
[pid=26627] vsize: 73552
Current children cumulated CPU time (s) 629.17
Current children cumulated vsize (Kb) 75676

[startup+640.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 20650 0 0 0 63816 98 0 0 25 0 1 0 1793688735 75792384 17468 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 18504 17468 145 145 0 18359 0
[pid=26627] vsize: 74016
Current children cumulated CPU time (s) 639.15
Current children cumulated vsize (Kb) 76140

[startup+650.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 20859 0 0 0 64813 100 0 0 25 0 1 0 1793688735 76627968 17677 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 18708 17677 145 145 0 18563 0
[pid=26627] vsize: 74832
Current children cumulated CPU time (s) 649.14
Current children cumulated vsize (Kb) 76956

[startup+660.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 21034 0 0 0 65810 101 0 0 25 0 1 0 1793688735 77332480 17852 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 18880 17852 145 145 0 18735 0
[pid=26627] vsize: 75520
Current children cumulated CPU time (s) 659.12
Current children cumulated vsize (Kb) 77644

[startup+670.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 21258 0 0 0 66807 102 0 0 25 0 1 0 1793688735 78254080 18076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 19105 18076 145 145 0 18960 0
[pid=26627] vsize: 76420
Current children cumulated CPU time (s) 669.1
Current children cumulated vsize (Kb) 78544

[startup+680.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 21424 0 0 0 67804 104 0 0 25 0 1 0 1793688735 78938112 18242 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 19272 18242 145 145 0 19127 0
[pid=26627] vsize: 77088
Current children cumulated CPU time (s) 679.09
Current children cumulated vsize (Kb) 79212

[startup+690.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 21575 0 0 0 68802 105 0 0 25 0 1 0 1793688735 79552512 18393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 19422 18393 145 145 0 19277 0
[pid=26627] vsize: 77688
Current children cumulated CPU time (s) 689.08
Current children cumulated vsize (Kb) 79812

[startup+700.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 21670 0 0 0 69801 105 0 0 25 0 1 0 1793688735 79933440 18488 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 19515 18488 145 145 0 19370 0
[pid=26627] vsize: 78060
Current children cumulated CPU time (s) 699.07
Current children cumulated vsize (Kb) 80184

[startup+710.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 21792 0 0 0 70799 107 0 0 25 0 1 0 1793688735 80429056 18610 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 19636 18610 145 145 0 19491 0
[pid=26627] vsize: 78544
Current children cumulated CPU time (s) 709.07
Current children cumulated vsize (Kb) 80668

[startup+720.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 21951 0 0 0 71796 108 0 0 25 0 1 0 1793688735 81068032 18769 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 19792 18769 145 145 0 19647 0
[pid=26627] vsize: 79168
Current children cumulated CPU time (s) 719.05
Current children cumulated vsize (Kb) 81292

[startup+730.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 22092 0 0 0 72794 109 0 0 25 0 1 0 1793688735 81633280 18910 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 19930 18910 145 145 0 19785 0
[pid=26627] vsize: 79720
Current children cumulated CPU time (s) 729.04
Current children cumulated vsize (Kb) 81844

[startup+740.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 22269 0 0 0 73791 110 0 0 25 0 1 0 1793688735 82362368 19087 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 20108 19087 145 145 0 19963 0
[pid=26627] vsize: 80432
Current children cumulated CPU time (s) 739.02
Current children cumulated vsize (Kb) 82556

[startup+750.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 22396 0 0 0 74789 111 0 0 25 0 1 0 1793688735 82874368 19214 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 20233 19214 145 145 0 20088 0
[pid=26627] vsize: 80932
Current children cumulated CPU time (s) 749.01
Current children cumulated vsize (Kb) 83056

[startup+760.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 22536 0 0 0 75787 112 0 0 25 0 1 0 1793688735 83435520 19354 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 20370 19354 145 145 0 20225 0
[pid=26627] vsize: 81480
Current children cumulated CPU time (s) 759
Current children cumulated vsize (Kb) 83604

[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 22631 0 0 0 76786 112 0 0 25 0 1 0 1793688735 83820544 19449 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 20464 19449 145 145 0 20319 0
[pid=26627] vsize: 81856
Current children cumulated CPU time (s) 768.99
Current children cumulated vsize (Kb) 83980

[startup+780.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 22803 0 0 0 77784 113 0 0 25 0 1 0 1793688735 85065728 19621 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 20768 19621 145 145 0 20623 0
[pid=26627] vsize: 83072
Current children cumulated CPU time (s) 778.98
Current children cumulated vsize (Kb) 85196

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 22956 0 0 0 78781 114 0 0 25 0 1 0 1793688735 85676032 19774 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 20917 19774 145 145 0 20772 0
[pid=26627] vsize: 83668
Current children cumulated CPU time (s) 788.96
Current children cumulated vsize (Kb) 85792

[startup+800.075 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23077 0 0 0 79779 115 0 0 25 0 1 0 1793688735 86163456 19895 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21036 19895 145 145 0 20891 0
[pid=26627] vsize: 84144
Current children cumulated CPU time (s) 798.95
Current children cumulated vsize (Kb) 86268

[startup+810.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23193 0 0 0 80777 116 0 0 25 0 1 0 1793688735 86622208 20011 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21148 20011 145 145 0 21003 0
[pid=26627] vsize: 84592
Current children cumulated CPU time (s) 808.94
Current children cumulated vsize (Kb) 86716

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23309 0 0 0 81775 117 0 0 25 0 1 0 1793688735 87093248 20127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21263 20127 145 145 0 21118 0
[pid=26627] vsize: 85052
Current children cumulated CPU time (s) 818.93
Current children cumulated vsize (Kb) 87176

[startup+830.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23446 0 0 0 82772 118 0 0 25 0 1 0 1793688735 87670784 20264 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21404 20264 145 145 0 21259 0
[pid=26627] vsize: 85616
Current children cumulated CPU time (s) 828.91
Current children cumulated vsize (Kb) 87740

[startup+840.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23537 0 0 0 83771 118 0 0 25 0 1 0 1793688735 88031232 20355 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21492 20355 145 145 0 21347 0
[pid=26627] vsize: 85968
Current children cumulated CPU time (s) 838.9
Current children cumulated vsize (Kb) 88092

[startup+850.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23642 0 0 0 84770 119 0 0 25 0 1 0 1793688735 88469504 20460 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21599 20460 145 145 0 21454 0
[pid=26627] vsize: 86396
Current children cumulated CPU time (s) 848.9
Current children cumulated vsize (Kb) 88520

[startup+860.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23768 0 0 0 85768 119 0 0 25 0 1 0 1793688735 88993792 20586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21727 20586 145 145 0 21582 0
[pid=26627] vsize: 86908
Current children cumulated CPU time (s) 858.88
Current children cumulated vsize (Kb) 89032

[startup+870.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23862 0 0 0 86766 120 0 0 25 0 1 0 1793688735 89362432 20680 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21817 20680 145 145 0 21672 0
[pid=26627] vsize: 87268
Current children cumulated CPU time (s) 868.87
Current children cumulated vsize (Kb) 89392

[startup+880.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 23940 0 0 0 87765 121 0 0 25 0 1 0 1793688735 89690112 20758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21897 20758 145 145 0 21752 0
[pid=26627] vsize: 87588
Current children cumulated CPU time (s) 878.87
Current children cumulated vsize (Kb) 89712

[startup+890.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24031 0 0 0 88764 122 0 0 25 0 1 0 1793688735 90071040 20849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 21990 20849 145 145 0 21845 0
[pid=26627] vsize: 87960
Current children cumulated CPU time (s) 888.87
Current children cumulated vsize (Kb) 90084

[startup+900.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24110 0 0 0 89763 122 0 0 25 0 1 0 1793688735 90382336 20928 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22066 20928 145 145 0 21921 0
[pid=26627] vsize: 88264
Current children cumulated CPU time (s) 898.86
Current children cumulated vsize (Kb) 90388

[startup+910.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24207 0 0 0 90762 123 0 0 25 0 1 0 1793688735 90779648 21025 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22163 21025 145 145 0 22018 0
[pid=26627] vsize: 88652
Current children cumulated CPU time (s) 908.86
Current children cumulated vsize (Kb) 90776

[startup+920.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24317 0 0 0 91760 123 0 0 25 0 1 0 1793688735 91226112 21135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22272 21135 145 145 0 22127 0
[pid=26627] vsize: 89088
Current children cumulated CPU time (s) 918.84
Current children cumulated vsize (Kb) 91212

[startup+930.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24410 0 0 0 92758 124 0 0 25 0 1 0 1793688735 91594752 21228 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22362 21228 145 145 0 22217 0
[pid=26627] vsize: 89448
Current children cumulated CPU time (s) 928.83
Current children cumulated vsize (Kb) 91572

[startup+940.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24485 0 0 0 93758 125 0 0 25 0 1 0 1793688735 91918336 21303 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22441 21303 145 145 0 22296 0
[pid=26627] vsize: 89764
Current children cumulated CPU time (s) 938.84
Current children cumulated vsize (Kb) 91888

[startup+950.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24588 0 0 0 94756 125 0 0 25 0 1 0 1793688735 92327936 21406 4294967295 134512640 135094434 3221224432 3221223088 134558094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22541 21406 145 145 0 22396 0
[pid=26627] vsize: 90164
Current children cumulated CPU time (s) 948.82
Current children cumulated vsize (Kb) 92288

[startup+960.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24666 0 0 0 95755 126 0 0 25 0 1 0 1793688735 92635136 21484 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22616 21484 145 145 0 22471 0
[pid=26627] vsize: 90464
Current children cumulated CPU time (s) 958.82
Current children cumulated vsize (Kb) 92588

[startup+970.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24738 0 0 0 96754 126 0 0 25 0 1 0 1793688735 92962816 21556 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22696 21556 145 145 0 22551 0
[pid=26627] vsize: 90784
Current children cumulated CPU time (s) 968.81
Current children cumulated vsize (Kb) 92908

[startup+980.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24835 0 0 0 97754 127 0 0 25 0 1 0 1793688735 93347840 21653 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22790 21653 145 145 0 22645 0
[pid=26627] vsize: 91160
Current children cumulated CPU time (s) 978.82
Current children cumulated vsize (Kb) 93284

[startup+990.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24911 0 0 0 98753 128 0 0 25 0 1 0 1793688735 93671424 21729 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22869 21729 145 145 0 22724 0
[pid=26627] vsize: 91476
Current children cumulated CPU time (s) 988.82
Current children cumulated vsize (Kb) 93600

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 24961 0 0 0 99752 128 0 0 25 0 1 0 1793688735 93872128 21779 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22918 21779 145 145 0 22773 0
[pid=26627] vsize: 91672
Current children cumulated CPU time (s) 998.81
Current children cumulated vsize (Kb) 93796

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25014 0 0 0 100751 128 0 0 25 0 1 0 1793688735 94085120 21832 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 22970 21832 145 145 0 22825 0
[pid=26627] vsize: 91880
Current children cumulated CPU time (s) 1008.8
Current children cumulated vsize (Kb) 94004

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25071 0 0 0 101751 128 0 0 25 0 1 0 1793688735 94310400 21889 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23025 21889 145 145 0 22880 0
[pid=26627] vsize: 92100
Current children cumulated CPU time (s) 1018.8
Current children cumulated vsize (Kb) 94224

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25138 0 0 0 102750 129 0 0 25 0 1 0 1793688735 94601216 21956 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23096 21956 145 145 0 22951 0
[pid=26627] vsize: 92384
Current children cumulated CPU time (s) 1028.8
Current children cumulated vsize (Kb) 94508

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25211 0 0 0 103749 129 0 0 25 0 1 0 1793688735 94896128 22029 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23168 22029 145 145 0 23023 0
[pid=26627] vsize: 92672
Current children cumulated CPU time (s) 1038.79
Current children cumulated vsize (Kb) 94796

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25277 0 0 0 104748 130 0 0 25 0 1 0 1793688735 95170560 22095 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23235 22095 145 145 0 23090 0
[pid=26627] vsize: 92940
Current children cumulated CPU time (s) 1048.79
Current children cumulated vsize (Kb) 95064

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25343 0 0 0 105747 130 0 0 25 0 1 0 1793688735 95469568 22161 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23308 22161 145 145 0 23163 0
[pid=26627] vsize: 93232
Current children cumulated CPU time (s) 1058.78
Current children cumulated vsize (Kb) 95356

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25404 0 0 0 106745 131 0 0 25 0 1 0 1793688735 95711232 22222 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26627/statm): 23367 22222 145 145 0 23222 0
[pid=26627] vsize: 93468
Current children cumulated CPU time (s) 1068.77
Current children cumulated vsize (Kb) 95592

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25468 0 0 0 107744 132 0 0 25 0 1 0 1793688735 96002048 22286 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23438 22286 145 145 0 23293 0
[pid=26627] vsize: 93752
Current children cumulated CPU time (s) 1078.77
Current children cumulated vsize (Kb) 95876

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25543 0 0 0 108743 132 0 0 25 0 1 0 1793688735 96292864 22361 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23509 22361 145 145 0 23364 0
[pid=26627] vsize: 94036
Current children cumulated CPU time (s) 1088.76
Current children cumulated vsize (Kb) 96160

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25610 0 0 0 109743 132 0 0 25 0 1 0 1793688735 96559104 22428 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23574 22428 145 145 0 23429 0
[pid=26627] vsize: 94296
Current children cumulated CPU time (s) 1098.76
Current children cumulated vsize (Kb) 96420

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25678 0 0 0 110742 133 0 0 25 0 1 0 1793688735 96833536 22496 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23641 22496 145 145 0 23496 0
[pid=26627] vsize: 94564
Current children cumulated CPU time (s) 1108.76
Current children cumulated vsize (Kb) 96688

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25754 0 0 0 111742 133 0 0 25 0 1 0 1793688735 97169408 22572 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23723 22572 145 145 0 23578 0
[pid=26627] vsize: 94892
Current children cumulated CPU time (s) 1118.76
Current children cumulated vsize (Kb) 97016

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25815 0 0 0 112742 133 0 0 25 0 1 0 1793688735 97419264 22633 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23784 22633 145 145 0 23639 0
[pid=26627] vsize: 95136
Current children cumulated CPU time (s) 1128.76
Current children cumulated vsize (Kb) 97260

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25877 0 0 0 113740 134 0 0 25 0 1 0 1793688735 97669120 22695 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23845 22695 145 145 0 23700 0
[pid=26627] vsize: 95380
Current children cumulated CPU time (s) 1138.75
Current children cumulated vsize (Kb) 97504

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25935 0 0 0 114739 134 0 0 25 0 1 0 1793688735 97910784 22753 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23904 22753 145 145 0 23759 0
[pid=26627] vsize: 95616
Current children cumulated CPU time (s) 1148.74
Current children cumulated vsize (Kb) 97740

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 25986 0 0 0 115739 135 0 0 25 0 1 0 1793688735 98111488 22804 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 23953 22804 145 145 0 23808 0
[pid=26627] vsize: 95812
Current children cumulated CPU time (s) 1158.75
Current children cumulated vsize (Kb) 97936

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 26036 0 0 0 116738 135 0 0 25 0 1 0 1793688735 98316288 22854 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 24003 22854 145 145 0 23858 0
[pid=26627] vsize: 96012
Current children cumulated CPU time (s) 1168.74
Current children cumulated vsize (Kb) 98136

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 26086 0 0 0 117738 136 0 0 25 0 1 0 1793688735 98557952 22904 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 24062 22904 145 145 0 23917 0
[pid=26627] vsize: 96248
Current children cumulated CPU time (s) 1178.75
Current children cumulated vsize (Kb) 98372

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 26178 0 0 0 118736 136 0 0 25 0 1 0 1793688735 98926592 22996 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 24152 22996 145 145 0 24007 0
[pid=26627] vsize: 96608
Current children cumulated CPU time (s) 1188.73
Current children cumulated vsize (Kb) 98732

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 26272 0 0 0 119735 137 0 0 25 0 1 0 1793688735 99315712 23090 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 24247 23090 145 145 0 24102 0
[pid=26627] vsize: 96988
Current children cumulated CPU time (s) 1198.73
Current children cumulated vsize (Kb) 99112

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 26332 0 0 0 120734 137 0 0 25 0 1 0 1793688735 99565568 23150 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 24308 23150 145 145 0 24163 0
[pid=26627] vsize: 97232
Current children cumulated CPU time (s) 1208.72
Current children cumulated vsize (Kb) 99356



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 26627
Raw data (/proc/26623/stat): 26623 (minisat+_script) S 26622 26623 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793688730 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26623/statm): 531 226 485 147 0 384 0
[pid=26623] vsize: 2124
Raw data (/proc/26627/stat): 26627 (minisat+_64-bit) R 26623 26623 9854 0 -1 0 26332 0 0 0 120734 137 0 0 25 0 1 0 1793688735 99565568 23150 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26627/statm): 24308 23150 145 145 0 24163 0
[pid=26627] vsize: 97232
Current children cumulated CPU time (s) 1208.72
Current children cumulated vsize (Kb) 99356

Sending SIGTERM to -26623
Sleeping 2 seconds
One traced child (pid=26623) ended because it received signal 15 (SIGTERM)
One traced child (pid=26627) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.77
CPU user time (s): 1207.35
CPU system time (s): 1.42278
CPU usage (%): 99.8851
Max. virtual memory (cumulated for all children) (Kb): 99356

Verifier Data

ERROR: no interpretation found !