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-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos15.opb
MD5SUMb9f2d6d55f20df770e36766d58f8055f
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2677095900004446
Optimality of the best value was proved NO
Number of terms in the objective function 7040
Biggest coefficient in the objective function 524288000000000000
Number of bits for the biggest coefficient in the objective function 59
Sum of the numbers in the objective function 75579061049066668032
Number of bits of the sum of numbers in the objective function 67
Biggest number in a constraint 524288000000000000
Number of bits of the biggest number in a constraint 59
Biggest sum of numbers in a constraint 75579061049066668032
Number of bits of the biggest sum of numbers67
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1224.25
Number of variables11840
Total number of constraints792
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)160
Number of constraints which are nor clauses,nor cardinality constraints632
Minimum length of a constraint1
Maximum length of a constraint100

Trace number 6295

Launcher Data

LAUNCH ON wulflinc11 THE 2005-09-20 05:15:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3450 boxname=wulflinc11 idbench=1106 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b9f2d6d55f20df770e36766d58f8055f  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-neos15.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-neos15.opb
IDLAUNCH: 3450
/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:        869296 kB
Buffers:         27852 kB
Cached:         110836 kB
SwapCached:        916 kB
Active:          42620 kB
Inactive:        98684 kB
HighTotal:      131008 kB
HighFree:        20468 kB
LowTotal:       903652 kB
LowFree:        848828 kB
SwapTotal:     2097136 kB
SwapFree:      2095640 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            18516 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:36:09 (client local time) WITH STATUS 0 IN 1207.78 SECONDS
stats: 3450 7 1207.78 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 796] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 872 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    7
c ---[ 869]---> BDD-cost:    7
c ---[ 868]---> BDD-cost:    7
c ---[ 867]---> BDD-cost:    7
c ---[ 866]---> BDD-cost:    7
c ---[ 865]---> BDD-cost:    7
c ---[ 864]---> BDD-cost:    7
c ---[ 863]---> BDD-cost:    7
c ---[ 862]---> BDD-cost:    7
c ---[ 861]---> BDD-cost:    7
c ---[ 860]---> BDD-cost:    7
c ---[ 859]---> BDD-cost:    7
c ---[ 858]---> BDD-cost:    7
c ---[ 857]---> BDD-cost:    7
c ---[ 856]---> BDD-cost:    7
c ---[ 855]---> BDD-cost:    7
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    7
c ---[ 852]---> BDD-cost:    7
c ---[ 851]---> BDD-cost:    7
c ---[ 850]---> BDD-cost:    7
c ---[ 849]---> BDD-cost:    7
c ---[ 848]---> BDD-cost:    7
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    7
c ---[ 845]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:    7
c ---[ 843]---> BDD-cost:    7
c ---[ 842]---> BDD-cost:    7
c ---[ 841]---> BDD-cost:    7
c ---[ 840]---> BDD-cost:    7
c ---[ 839]---> BDD-cost:    7
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    7
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    7
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:    7
c ---[ 832]---> BDD-cost:    7
c ---[ 831]---> BDD-cost:    7
c ---[ 830]---> BDD-cost:    7
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    7
c ---[ 827]---> BDD-cost:    7
c ---[ 826]---> BDD-cost:    7
c ---[ 825]---> BDD-cost:    7
c ---[ 824]---> BDD-cost:    7
c ---[ 823]---> BDD-cost:    7
c ---[ 822]---> BDD-cost:    7
c ---[ 821]---> BDD-cost:    7
c ---[ 820]---> BDD-cost:    7
c ---[ 819]---> BDD-cost:    7
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    7
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    7
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    7
c ---[ 810]---> BDD-cost:    7
c ---[ 809]---> BDD-cost:    7
c ---[ 808]---> BDD-cost:    7
c ---[ 807]---> BDD-cost:    7
c ---[ 806]---> BDD-cost:    7
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    7
c ---[ 803]---> BDD-cost:    7
c ---[ 802]---> BDD-cost:    7
c ---[ 801]---> BDD-cost:    7
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:    7
c ---[ 796]---> BDD-cost:    7
c ---[ 795]---> BDD-cost:    7
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    7
c ---[ 792]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:   54
c ---[ 788]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 776]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 770]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> BDD-cost:   62
c ---[ 740]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 738]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 736]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 732]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 730]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 728]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 726]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 724]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 720]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 718]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 716]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 710]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 708]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 702]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 698]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 694]---> BDD-cost:   58
c ---[ 692]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 688]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 684]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 680]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 678]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 676]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 670]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 668]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 662]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 656]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 650]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 648]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 646]---> BDD-cost:   64
c ---[ 644]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 640]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 638]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 636]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 632]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 628]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 622]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 620]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 618]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 614]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 610]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 606]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 602]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 598]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 596]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 594]---> Sorter-cost: 1139     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 584]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 554]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 552]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost: 1139     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 536]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 508]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost: 1139     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 476]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> BDD-cost:  152
c ---[ 452]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  709     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 410]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 408]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost: 1099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 358]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost: 1099     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 307]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 295]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 287]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 281]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 279]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 277]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 275]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 273]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 271]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 269]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 267]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 265]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 263]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1137     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 261]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 259]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 257]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 250]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 246]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 242]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 240]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 239]---> BDD-cost:   27
c ---[ 238]---> BDD-cost:   27
c ---[ 237]---> BDD-cost:   27
c ---[ 236]---> BDD-cost:   27
c ---[ 235]---> BDD-cost:   27
c ---[ 234]---> BDD-cost:   27
c ---[ 233]---> BDD-cost:   27
c ---[ 232]---> BDD-cost:   27
c ---[ 231]---> BDD-cost:   27
c ---[ 230]---> BDD-cost:   27
c ---[ 229]---> BDD-cost:   27
c ---[ 228]---> BDD-cost:   27
c ---[ 227]---> BDD-cost:   27
c ---[ 226]---> BDD-cost:   27
c ---[ 225]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:   27
c ---[ 223]---> BDD-cost:   27
c ---[ 222]---> BDD-cost:   27
c ---[ 221]---> BDD-cost:   27
c ---[ 220]---> BDD-cost:   27
c ---[ 219]---> BDD-cost:   27
c ---[ 218]---> BDD-cost:   27
c ---[ 217]---> BDD-cost:   27
c ---[ 216]---> BDD-cost:   27
c ---[ 215]---> BDD-cost:   27
c ---[ 214]---> BDD-cost:   27
c ---[ 213]---> BDD-cost:   27
c ---[ 212]---> BDD-cost:   27
c ---[ 211]---> BDD-cost:   27
c ---[ 210]---> BDD-cost:   27
c ---[ 209]---> BDD-cost:   27
c ---[ 208]---> BDD-cost:   27
c ---[ 207]---> BDD-cost:   27
c ---[ 206]---> BDD-cost:   27
c ---[ 205]---> BDD-cost:   27
c ---[ 204]---> BDD-cost:   27
c ---[ 203]---> BDD-cost:   27
c ---[ 202]---> BDD-cost:   27
c ---[ 201]---> BDD-cost:   27
c ---[ 200]---> BDD-cost:   27
c ---[ 199]---> BDD-cost:   27
c ---[ 198]---> BDD-cost:   27
c ---[ 197]---> BDD-cost:   27
c ---[ 196]---> BDD-cost:   27
c ---[ 195]---> BDD-cost:   27
c ---[ 194]---> BDD-cost:   27
c ---[ 193]---> BDD-cost:   27
c ---[ 192]---> BDD-cost:   27
c ---[ 191]---> BDD-cost:   27
c ---[ 190]---> BDD-cost:   27
c ---[ 189]---> BDD-cost:   27
c ---[ 188]---> BDD-cost:   27
c ---[ 187]---> BDD-cost:   27
c ---[ 186]---> BDD-cost:   27
c ---[ 185]---> BDD-cost:   27
c ---[ 184]---> BDD-cost:   27
c ---[ 183]---> BDD-cost:   27
c ---[ 182]---> BDD-cost:   27
c ---[ 181]---> BDD-cost:   27
c ---[ 180]---> BDD-cost:   27
c ---[ 179]---> BDD-cost:   27
c ---[ 178]---> BDD-cost:   27
c ---[ 177]---> BDD-cost:   27
c ---[ 176]---> BDD-cost:   27
c ---[ 175]---> BDD-cost:   27
c ---[ 174]---> BDD-cost:   27
c ---[ 173]---> BDD-cost:   27
c ---[ 172]---> BDD-cost:   27
c ---[ 171]---> BDD-cost:   27
c ---[ 170]---> BDD-cost:   27
c ---[ 169]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:   27
c ---[ 167]---> BDD-cost:   27
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   27
c ---[ 164]---> BDD-cost:   27
c ---[ 163]---> BDD-cost:   27
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:   27
c ---[ 160]---> BDD-cost:   27
c ---[ 159]---> BDD-cost:   27
c ---[ 158]---> BDD-cost:   27
c ---[ 157]---> BDD-cost:   27
c ---[ 156]---> BDD-cost:   27
c ---[ 155]---> BDD-cost:   27
c ---[ 154]---> BDD-cost:   27
c ---[ 153]---> BDD-cost:   27
c ---[ 152]---> BDD-cost:   27
c ---[ 151]---> BDD-cost:   27
c ---[ 150]---> BDD-cost:   27
c ---[ 149]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   27
c ---[ 147]---> BDD-cost:   27
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   27
c ---[ 144]---> BDD-cost:   27
c ---[ 143]---> BDD-cost:   27
c ---[ 142]---> BDD-cost:   27
c ---[ 141]---> BDD-cost:   27
c ---[ 140]---> BDD-cost:   27
c ---[ 139]---> BDD-cost:   27
c ---[ 138]---> BDD-cost:   27
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   27
c ---[ 131]---> BDD-cost:   27
c ---[ 130]---> BDD-cost:   27
c ---[ 129]---> BDD-cost:   27
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   27
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> Sorter-cost: 1006     Base: 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 117]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 116]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 115]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 114]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 113]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 112]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 111]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 110]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 109]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 108]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 107]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 106]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 105]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 104]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 103]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 102]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 101]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[ 100]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  99]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  98]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  97]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  96]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  95]---> Sorter-cost: 1006     Base: 2 2 2 2 2 2 3 5 2 2 2 2 2 2
c ---[  94]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  93]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  92]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  91]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  90]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  89]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  88]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  87]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  86]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  85]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  84]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  83]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  82]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  81]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  80]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  79]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  78]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  77]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  76]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  75]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  74]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  73]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  72]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  71]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  70]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  69]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  68]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  67]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  66]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  65]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  64]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  63]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  62]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  61]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  60]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  59]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  58]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  57]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  56]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  55]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  54]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  53]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  52]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  51]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  50]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  49]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  48]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  47]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  46]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  45]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  44]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  43]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  42]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  41]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  40]---> Sorter-cost: 1111     Base: 2 2 2 2 2 2 2 2 3 5 2 2 2 2
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   27
c ---[  34]---> BDD-cost:   27
c ---[  33]---> BDD-cost:   27
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   27
c ---[  28]---> BDD-cost:   27
c ---[  27]---> BDD-cost:   27
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   27
c ---[  22]---> BDD-cost:   27
c ---[  21]---> BDD-cost:   27
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   27
c ---[  16]---> BDD-cost:   27
c ---[  15]---> BDD-cost:   27
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   27
c ---[  10]---> BDD-cost:   27
c ---[   9]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   27
c ---[   4]---> BDD-cost:   27
c ---[   3]---> BDD-cost:   27
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  853042  2009753 |  284347       0        0     nan |  0.000 % |
c |       100 |  852883  2009401 |  312781      76      292     3.8 |  3.322 % |
c |       250 |  852770  2009148 |  344059     219     1189     5.4 |  3.332 % |
c |       475 |  852539  2008636 |  378465     406     1949     4.8 |  3.353 % |
c |       812 |  852118  2007701 |  416312     693     3395     4.9 |  3.393 % |
c |      1318 |  851489  2006302 |  457943    1126     5424     4.8 |  3.452 % |
c |      2077 |  850689  2004528 |  503738    1777     8929     5.0 |  3.527 % |
c |      3217 |  849673  2002266 |  554111    2792    17049     6.1 |  3.622 % |
c |      4928 |  847706  1997893 |  609523    4225    28125     6.7 |  3.809 % |
c |      7490 |  845652  1993313 |  670475    6514    53861     8.3 |  3.998 % |
c |     11334 |  844004  1989637 |  737522   10128   143591    14.2 |  4.151 % |
c |     17106 |  842906  1987194 |  811275   15724   274904    17.5 |  4.254 % |
c |     25758 |  841242  1983471 |  892402   24121   533926    22.1 |  4.408 % |
c |     38732 |  840062  1980823 |  981642   36953   996615    27.0 |  4.514 % |
c |     58193 |  839698  1980001 | 1079807   56359  1883281    33.4 |  4.545 % |
c |     87385 |  838319  1976916 | 1187787   85402  3271132    38.3 |  4.670 % |
c |    131177 |  836633  1973146 | 1306566  128980  5314764    41.2 |  4.822 % |
c |    196862 |  834781  1969006 | 1437223  194463  9021600    46.4 |  4.988 % |

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/637/stat): 637 (minisat+_script) R 636 637 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797712049 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/637/statm): 174 3 169 147 0 27 0
[pid=637] 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=638
New process pid=639
New process pid=640
execve syscall for /bin/sed executable
One traced child (pid=639) 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=640) exited with status: 0
One traced child (pid=638) exited with status: 0
New process pid=641
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-13-7-neos15.opb
One traced child (pid=641) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=642
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-neos15.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 2289 0 0 0 973 10 0 0 25 0 1 0 1797712056 9871360 2080 4294967295 134512640 135167914 3221224448 3221221632 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 2410 2080 162 162 0 2248 0
[pid=642] vsize: 9640
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 11768

[startup+20.0046 s]
Raw data (loadavg): 0.94 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 4314 0 0 0 1961 18 0 0 25 0 1 0 1797712056 16158720 3610 4294967295 134512640 135167914 3221224448 3221222520 134693815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 3945 3610 162 162 0 3783 0
[pid=642] vsize: 15780
Current children cumulated CPU time (s) 19.8
Current children cumulated vsize (Kb) 17908

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 4875 0 0 0 2957 20 0 0 25 0 1 0 1797712056 20766720 4171 4294967295 134512640 135167914 3221224448 3221221792 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 5070 4171 162 162 0 4908 0
[pid=642] vsize: 20280
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 22408

[startup+40.0072 s]
Raw data (loadavg): 0.95 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 5070 0 0 0 3956 21 0 0 25 0 1 0 1797712056 21270528 4366 4294967295 134512640 135167914 3221224448 3221221992 134693776 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 5193 4366 162 162 0 5031 0
[pid=642] vsize: 20772
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 22900

[startup+50.008 s]
Raw data (loadavg): 0.96 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 5265 0 0 0 4955 21 0 0 25 0 1 0 1797712056 21778432 4561 4294967295 134512640 135167914 3221224448 3221221904 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 5317 4561 162 162 0 5155 0
[pid=642] vsize: 21268
Current children cumulated CPU time (s) 49.77
Current children cumulated vsize (Kb) 23396

[startup+60.0088 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 6779 0 0 0 5950 25 0 0 25 0 1 0 1797712056 24985600 5416 4294967295 134512640 135167914 3221224448 3221221964 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/642/statm): 6100 5416 162 162 0 5938 0
[pid=642] vsize: 24400
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 26528

[startup+70.0096 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26582 0 0 0 6789 108 0 0 25 0 1 0 1797712056 122445824 25212 4294967295 134512640 135167914 3221224448 3221223156 134558145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/642/statm): 29894 25212 162 162 0 29732 0
[pid=642] vsize: 119576
Current children cumulated CPU time (s) 68.98
Current children cumulated vsize (Kb) 121704

[startup+80.0113 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26591 0 0 0 7789 108 0 0 25 0 1 0 1797712056 122474496 25221 4294967295 134512640 135167914 3221224448 3221223200 134563673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 29901 25221 162 162 0 29739 0
[pid=642] vsize: 119604
Current children cumulated CPU time (s) 78.98
Current children cumulated vsize (Kb) 121732

[startup+90.0121 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26612 0 0 0 8789 109 0 0 25 0 1 0 1797712056 122560512 25242 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 29922 25242 162 162 0 29760 0
[pid=642] vsize: 119688
Current children cumulated CPU time (s) 88.99
Current children cumulated vsize (Kb) 121816

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26639 0 0 0 9788 109 0 0 25 0 1 0 1797712056 122642432 25269 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/642/statm): 29942 25269 162 162 0 29780 0
[pid=642] vsize: 119768
Current children cumulated CPU time (s) 98.98
Current children cumulated vsize (Kb) 121896

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26667 0 0 0 10788 109 0 0 25 0 1 0 1797712056 122720256 25297 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 29961 25297 162 162 0 29799 0
[pid=642] vsize: 119844
Current children cumulated CPU time (s) 108.98
Current children cumulated vsize (Kb) 121972

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26690 0 0 0 11788 109 0 0 25 0 1 0 1797712056 122789888 25320 4294967295 134512640 135167914 3221224448 3221223156 134558106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 29978 25320 162 162 0 29816 0
[pid=642] vsize: 119912
Current children cumulated CPU time (s) 118.98
Current children cumulated vsize (Kb) 122040

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26715 0 0 0 12787 109 0 0 25 0 1 0 1797712056 122875904 25345 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 29999 25345 162 162 0 29837 0
[pid=642] vsize: 119996
Current children cumulated CPU time (s) 128.97
Current children cumulated vsize (Kb) 122124

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26720 0 0 0 13787 109 0 0 25 0 1 0 1797712056 122896384 25350 4294967295 134512640 135167914 3221224448 3221223156 134558175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30004 25350 162 162 0 29842 0
[pid=642] vsize: 120016
Current children cumulated CPU time (s) 138.97
Current children cumulated vsize (Kb) 122144

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26725 0 0 0 14787 109 0 0 25 0 1 0 1797712056 122916864 25355 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30009 25355 162 162 0 29847 0
[pid=642] vsize: 120036
Current children cumulated CPU time (s) 148.97
Current children cumulated vsize (Kb) 122164

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26749 0 0 0 15787 110 0 0 25 0 1 0 1797712056 122961920 25379 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30020 25379 162 162 0 29858 0
[pid=642] vsize: 120080
Current children cumulated CPU time (s) 158.98
Current children cumulated vsize (Kb) 122208

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26781 0 0 0 16787 110 0 0 25 0 1 0 1797712056 123064320 25411 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30045 25411 162 162 0 29883 0
[pid=642] vsize: 120180
Current children cumulated CPU time (s) 168.98
Current children cumulated vsize (Kb) 122308

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26801 0 0 0 17787 110 0 0 25 0 1 0 1797712056 123142144 25431 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30064 25431 162 162 0 29902 0
[pid=642] vsize: 120256
Current children cumulated CPU time (s) 178.98
Current children cumulated vsize (Kb) 122384

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26811 0 0 0 18787 110 0 0 25 0 1 0 1797712056 123179008 25441 4294967295 134512640 135167914 3221224448 3221223184 134559387 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30073 25441 162 162 0 29911 0
[pid=642] vsize: 120292
Current children cumulated CPU time (s) 188.98
Current children cumulated vsize (Kb) 122420

[startup+200.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26825 0 0 0 19787 110 0 0 25 0 1 0 1797712056 123215872 25455 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30082 25455 162 162 0 29920 0
[pid=642] vsize: 120328
Current children cumulated CPU time (s) 198.98
Current children cumulated vsize (Kb) 122456

[startup+210.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26848 0 0 0 20787 111 0 0 25 0 1 0 1797712056 123301888 25478 4294967295 134512640 135167914 3221224448 3221223156 134558136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30103 25478 162 162 0 29941 0
[pid=642] vsize: 120412
Current children cumulated CPU time (s) 208.99
Current children cumulated vsize (Kb) 122540

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26856 0 0 0 21787 111 0 0 25 0 1 0 1797712056 123334656 25486 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30111 25486 162 162 0 29949 0
[pid=642] vsize: 120444
Current children cumulated CPU time (s) 218.99
Current children cumulated vsize (Kb) 122572

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26958 0 0 0 22785 111 0 0 25 0 1 0 1797712056 123772928 25588 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30218 25588 162 162 0 30056 0
[pid=642] vsize: 120872
Current children cumulated CPU time (s) 228.97
Current children cumulated vsize (Kb) 123000

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26966 0 0 0 23785 111 0 0 25 0 1 0 1797712056 123805696 25596 4294967295 134512640 135167914 3221224448 3221223156 134558131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30226 25596 162 162 0 30064 0
[pid=642] vsize: 120904
Current children cumulated CPU time (s) 238.97
Current children cumulated vsize (Kb) 123032

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26977 0 0 0 24786 111 0 0 25 0 1 0 1797712056 123846656 25607 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30236 25607 162 162 0 30074 0
[pid=642] vsize: 120944
Current children cumulated CPU time (s) 248.98
Current children cumulated vsize (Kb) 123072

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 26994 0 0 0 25786 111 0 0 25 0 1 0 1797712056 123916288 25624 4294967295 134512640 135167914 3221224448 3221223156 134558155 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30253 25624 162 162 0 30091 0
[pid=642] vsize: 121012
Current children cumulated CPU time (s) 258.98
Current children cumulated vsize (Kb) 123140

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27161 0 0 0 26783 113 0 0 25 0 1 0 1797712056 124583936 25791 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30416 25791 162 162 0 30254 0
[pid=642] vsize: 121664
Current children cumulated CPU time (s) 268.97
Current children cumulated vsize (Kb) 123792

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27184 0 0 0 27783 113 0 0 25 0 1 0 1797712056 124739584 25814 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30454 25814 162 162 0 30292 0
[pid=642] vsize: 121816
Current children cumulated CPU time (s) 278.97
Current children cumulated vsize (Kb) 123944

[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27201 0 0 0 28783 113 0 0 25 0 1 0 1797712056 124805120 25831 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30470 25831 162 162 0 30308 0
[pid=642] vsize: 121880
Current children cumulated CPU time (s) 288.97
Current children cumulated vsize (Kb) 124008

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27238 0 0 0 29783 113 0 0 25 0 1 0 1797712056 124948480 25868 4294967295 134512640 135167914 3221224448 3221223156 134558175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30505 25868 162 162 0 30343 0
[pid=642] vsize: 122020
Current children cumulated CPU time (s) 298.97
Current children cumulated vsize (Kb) 124148

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27346 0 0 0 30781 114 0 0 25 0 1 0 1797712056 125382656 25976 4294967295 134512640 135167914 3221224448 3221223156 134558186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30611 25976 162 162 0 30449 0
[pid=642] vsize: 122444
Current children cumulated CPU time (s) 308.96
Current children cumulated vsize (Kb) 124572

[startup+320.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27496 0 0 0 31778 115 0 0 25 0 1 0 1797712056 125984768 26126 4294967295 134512640 135167914 3221224448 3221223152 134563058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30758 26126 162 162 0 30596 0
[pid=642] vsize: 123032
Current children cumulated CPU time (s) 318.94
Current children cumulated vsize (Kb) 125160

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27714 0 0 0 32775 116 0 0 25 0 1 0 1797712056 126861312 26344 4294967295 134512640 135167914 3221224448 3221223152 134562549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30972 26344 162 162 0 30810 0
[pid=642] vsize: 123888
Current children cumulated CPU time (s) 328.92
Current children cumulated vsize (Kb) 126016

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27729 0 0 0 33775 116 0 0 25 0 1 0 1797712056 126918656 26359 4294967295 134512640 135167914 3221224448 3221223156 134558186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 30986 26359 162 162 0 30824 0
[pid=642] vsize: 123944
Current children cumulated CPU time (s) 338.92
Current children cumulated vsize (Kb) 126072

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 27766 0 0 0 34775 116 0 0 25 0 1 0 1797712056 127066112 26396 4294967295 134512640 135167914 3221224448 3221223136 134566738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 31022 26396 162 162 0 30860 0
[pid=642] vsize: 124088
Current children cumulated CPU time (s) 348.92
Current children cumulated vsize (Kb) 126216

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 28058 0 0 0 35768 118 0 0 25 0 1 0 1797712056 128372736 26688 4294967295 134512640 135167914 3221224448 3221223152 134562516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/642/statm): 31341 26688 162 162 0 31179 0
[pid=642] vsize: 125364
Current children cumulated CPU time (s) 358.87
Current children cumulated vsize (Kb) 127492

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 28409 0 0 0 36761 121 0 0 25 0 1 0 1797712056 129789952 27039 4294967295 134512640 135167914 3221224448 3221223152 134562663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 31687 27039 162 162 0 31525 0
[pid=642] vsize: 126748
Current children cumulated CPU time (s) 368.83
Current children cumulated vsize (Kb) 128876

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 28636 0 0 0 37757 123 0 0 25 0 1 0 1797712056 130703360 27266 4294967295 134512640 135167914 3221224448 3221223156 134558157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 31910 27266 162 162 0 31748 0
[pid=642] vsize: 127640
Current children cumulated CPU time (s) 378.81
Current children cumulated vsize (Kb) 129768

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 28862 0 0 0 38752 125 0 0 25 0 1 0 1797712056 131608576 27492 4294967295 134512640 135167914 3221224448 3221223136 134566757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 32131 27492 162 162 0 31969 0
[pid=642] vsize: 128524
Current children cumulated CPU time (s) 388.78
Current children cumulated vsize (Kb) 130652

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 29102 0 0 0 39749 126 0 0 25 0 1 0 1797712056 132575232 27732 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 32367 27732 162 162 0 32205 0
[pid=642] vsize: 129468
Current children cumulated CPU time (s) 398.76
Current children cumulated vsize (Kb) 131596

[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 29353 0 0 0 40744 129 0 0 25 0 1 0 1797712056 133591040 27983 4294967295 134512640 135167914 3221224448 3221223132 134562295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 32615 27983 162 162 0 32453 0
[pid=642] vsize: 130460
Current children cumulated CPU time (s) 408.74
Current children cumulated vsize (Kb) 132588

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 29628 0 0 0 41740 131 0 0 25 0 1 0 1797712056 134701056 28258 4294967295 134512640 135167914 3221224448 3221223088 134561836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 32886 28258 162 162 0 32724 0
[pid=642] vsize: 131544
Current children cumulated CPU time (s) 418.72
Current children cumulated vsize (Kb) 133672

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 29773 0 0 0 42737 131 0 0 25 0 1 0 1797712056 135544832 28403 4294967295 134512640 135167914 3221224448 3221223200 134563673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 33092 28403 162 162 0 32930 0
[pid=642] vsize: 132368
Current children cumulated CPU time (s) 428.69
Current children cumulated vsize (Kb) 134496

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) T 637 637 9854 0 -1 0 29911 0 0 0 43735 132 0 0 25 0 1 0 1797712056 136101888 28541 4294967295 134512640 135167914 3221224448 3221222860 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/642/statm): 33228 28541 162 162 0 33066 0
[pid=642] vsize: 132912
Current children cumulated CPU time (s) 438.68
Current children cumulated vsize (Kb) 135040

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 30044 0 0 0 44734 133 0 0 25 0 1 0 1797712056 136642560 28674 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 33360 28674 162 162 0 33198 0
[pid=642] vsize: 133440
Current children cumulated CPU time (s) 448.68
Current children cumulated vsize (Kb) 135568

[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 30308 0 0 0 45729 135 0 0 25 0 1 0 1797712056 137707520 28938 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 33620 28938 162 162 0 33458 0
[pid=642] vsize: 134480
Current children cumulated CPU time (s) 458.65
Current children cumulated vsize (Kb) 136608

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 30570 0 0 0 46724 138 0 0 25 0 1 0 1797712056 138776576 29200 4294967295 134512640 135167914 3221224448 3221223156 134558171 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 33881 29200 162 162 0 33719 0
[pid=642] vsize: 135524
Current children cumulated CPU time (s) 468.63
Current children cumulated vsize (Kb) 137652

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 30629 0 0 0 47723 138 0 0 25 0 1 0 1797712056 139014144 29259 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 33939 29259 162 162 0 33777 0
[pid=642] vsize: 135756
Current children cumulated CPU time (s) 478.62
Current children cumulated vsize (Kb) 137884

[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 30671 0 0 0 48723 138 0 0 25 0 1 0 1797712056 139190272 29301 4294967295 134512640 135167914 3221224448 3221223108 134567766 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 33982 29301 162 162 0 33820 0
[pid=642] vsize: 135928
Current children cumulated CPU time (s) 488.62
Current children cumulated vsize (Kb) 138056

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 30762 0 0 0 49722 139 0 0 25 0 1 0 1797712056 139554816 29392 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 34071 29392 162 162 0 33909 0
[pid=642] vsize: 136284
Current children cumulated CPU time (s) 498.62
Current children cumulated vsize (Kb) 138412

[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 30959 0 0 0 50717 140 0 0 25 0 1 0 1797712056 140345344 29589 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 34264 29589 162 162 0 34102 0
[pid=642] vsize: 137056
Current children cumulated CPU time (s) 508.58
Current children cumulated vsize (Kb) 139184

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 31079 0 0 0 51716 141 0 0 25 0 1 0 1797712056 140828672 29709 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 34382 29709 162 162 0 34220 0
[pid=642] vsize: 137528
Current children cumulated CPU time (s) 518.58
Current children cumulated vsize (Kb) 139656

[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 31194 0 0 0 52714 142 0 0 25 0 1 0 1797712056 141279232 29824 4294967295 134512640 135167914 3221224448 3221223152 134562834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 34492 29824 162 162 0 34330 0
[pid=642] vsize: 137968
Current children cumulated CPU time (s) 528.57
Current children cumulated vsize (Kb) 140096

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 31378 0 0 0 53711 143 0 0 25 0 1 0 1797712056 142016512 30008 4294967295 134512640 135167914 3221224448 3221223120 134562352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 34672 30008 162 162 0 34510 0
[pid=642] vsize: 138688
Current children cumulated CPU time (s) 538.55
Current children cumulated vsize (Kb) 140816

[startup+550.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 31459 0 0 0 54710 144 0 0 25 0 1 0 1797712056 142340096 30089 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 34751 30089 162 162 0 34589 0
[pid=642] vsize: 139004
Current children cumulated CPU time (s) 548.55
Current children cumulated vsize (Kb) 141132

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 31484 0 0 0 55709 144 0 0 25 0 1 0 1797712056 142438400 30114 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 34775 30114 162 162 0 34613 0
[pid=642] vsize: 139100
Current children cumulated CPU time (s) 558.54
Current children cumulated vsize (Kb) 141228

[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 31640 0 0 0 56707 145 0 0 25 0 1 0 1797712056 143060992 30270 4294967295 134512640 135167914 3221224448 3221223152 134562604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 34927 30270 162 162 0 34765 0
[pid=642] vsize: 139708
Current children cumulated CPU time (s) 568.53
Current children cumulated vsize (Kb) 141836

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) T 637 637 9854 0 -1 0 31833 0 0 0 57705 146 0 0 25 0 1 0 1797712056 143835136 30463 4294967295 134512640 135167914 3221224448 3221222860 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/642/statm): 35116 30463 162 162 0 34954 0
[pid=642] vsize: 140464
Current children cumulated CPU time (s) 578.52
Current children cumulated vsize (Kb) 142592

[startup+590.053 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) T 637 637 9854 0 -1 0 31971 0 0 0 58703 147 0 0 25 0 1 0 1797712056 144392192 30601 4294967295 134512640 135167914 3221224448 3221222876 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/642/statm): 35252 30601 162 162 0 35090 0
[pid=642] vsize: 141008
Current children cumulated CPU time (s) 588.51
Current children cumulated vsize (Kb) 143136

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 32178 0 0 0 59699 148 0 0 25 0 1 0 1797712056 145231872 30808 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 35457 30808 162 162 0 35295 0
[pid=642] vsize: 141828
Current children cumulated CPU time (s) 598.48
Current children cumulated vsize (Kb) 143956

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 32467 0 0 0 60693 150 0 0 25 0 1 0 1797712056 146399232 31097 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 35742 31097 162 162 0 35580 0
[pid=642] vsize: 142968
Current children cumulated CPU time (s) 608.44
Current children cumulated vsize (Kb) 145096

[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 32817 0 0 0 61687 153 0 0 25 0 1 0 1797712056 147820544 31447 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 36089 31447 162 162 0 35927 0
[pid=642] vsize: 144356
Current children cumulated CPU time (s) 618.41
Current children cumulated vsize (Kb) 146484

[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 33053 0 0 0 62684 155 0 0 25 0 1 0 1797712056 148770816 31683 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 36321 31683 162 162 0 36159 0
[pid=642] vsize: 145284
Current children cumulated CPU time (s) 628.4
Current children cumulated vsize (Kb) 147412

[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 33176 0 0 0 63682 156 0 0 25 0 1 0 1797712056 149282816 31806 4294967295 134512640 135167914 3221224448 3221223152 134562549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 36446 31806 162 162 0 36284 0
[pid=642] vsize: 145784
Current children cumulated CPU time (s) 638.39
Current children cumulated vsize (Kb) 147912

[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 33374 0 0 0 64679 157 0 0 25 0 1 0 1797712056 150069248 32004 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 36638 32004 162 162 0 36476 0
[pid=642] vsize: 146552
Current children cumulated CPU time (s) 648.37
Current children cumulated vsize (Kb) 148680

[startup+660.059 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 33436 0 0 0 65677 158 0 0 25 0 1 0 1797712056 150319104 32066 4294967295 134512640 135167914 3221224448 3221223152 134562672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 36699 32066 162 162 0 36537 0
[pid=642] vsize: 146796
Current children cumulated CPU time (s) 658.36
Current children cumulated vsize (Kb) 148924

[startup+670.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 33565 0 0 0 66675 159 0 0 25 0 1 0 1797712056 151363584 32195 4294967295 134512640 135167914 3221224448 3221223180 134558088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 36954 32195 162 162 0 36792 0
[pid=642] vsize: 147816
Current children cumulated CPU time (s) 668.35
Current children cumulated vsize (Kb) 149944

[startup+680.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 33763 0 0 0 67672 161 0 0 25 0 1 0 1797712056 152150016 32393 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37146 32393 162 162 0 36984 0
[pid=642] vsize: 148584
Current children cumulated CPU time (s) 678.34
Current children cumulated vsize (Kb) 150712

[startup+690.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 33858 0 0 0 68669 161 0 0 25 0 1 0 1797712056 152530944 32488 4294967295 134512640 135167914 3221224448 3221223156 134558150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37239 32488 162 162 0 37077 0
[pid=642] vsize: 148956
Current children cumulated CPU time (s) 688.31
Current children cumulated vsize (Kb) 151084

[startup+700.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 33946 0 0 0 69668 162 0 0 25 0 1 0 1797712056 152895488 32576 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37328 32576 162 162 0 37166 0
[pid=642] vsize: 149312
Current children cumulated CPU time (s) 698.31
Current children cumulated vsize (Kb) 151440

[startup+710.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34001 0 0 0 70668 162 0 0 25 0 1 0 1797712056 153120768 32631 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37383 32631 162 162 0 37221 0
[pid=642] vsize: 149532
Current children cumulated CPU time (s) 708.31
Current children cumulated vsize (Kb) 151660

[startup+720.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34050 0 0 0 71668 162 0 0 25 0 1 0 1797712056 153321472 32680 4294967295 134512640 135167914 3221224448 3221223152 134562601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37432 32680 162 162 0 37270 0
[pid=642] vsize: 149728
Current children cumulated CPU time (s) 718.31
Current children cumulated vsize (Kb) 151856

[startup+730.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34224 0 0 0 72665 163 0 0 25 0 1 0 1797712056 154013696 32854 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37601 32854 162 162 0 37439 0
[pid=642] vsize: 150404
Current children cumulated CPU time (s) 728.29
Current children cumulated vsize (Kb) 152532

[startup+740.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34472 0 0 0 73660 165 0 0 25 0 1 0 1797712056 155017216 33102 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37846 33102 162 162 0 37684 0
[pid=642] vsize: 151384
Current children cumulated CPU time (s) 738.26
Current children cumulated vsize (Kb) 153512

[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34567 0 0 0 74658 166 0 0 25 0 1 0 1797712056 155398144 33197 4294967295 134512640 135167914 3221224448 3221223152 134562782 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37939 33197 162 162 0 37777 0
[pid=642] vsize: 151756
Current children cumulated CPU time (s) 748.25
Current children cumulated vsize (Kb) 153884

[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34615 0 0 0 75657 167 0 0 25 0 1 0 1797712056 155598848 33245 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 37988 33245 162 162 0 37826 0
[pid=642] vsize: 151952
Current children cumulated CPU time (s) 758.25
Current children cumulated vsize (Kb) 154080

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34669 0 0 0 76657 167 0 0 25 0 1 0 1797712056 155824128 33299 4294967295 134512640 135167914 3221224448 3221223152 134562522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 38043 33299 162 162 0 37881 0
[pid=642] vsize: 152172
Current children cumulated CPU time (s) 768.25
Current children cumulated vsize (Kb) 154300

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34672 0 0 0 77657 167 0 0 25 0 1 0 1797712056 155836416 33302 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 38046 33302 162 162 0 37884 0
[pid=642] vsize: 152184
Current children cumulated CPU time (s) 778.25
Current children cumulated vsize (Kb) 154312

[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34757 0 0 0 78656 168 0 0 25 0 1 0 1797712056 156155904 33387 4294967295 134512640 135167914 3221224448 3221223152 134563082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 38124 33387 162 162 0 37962 0
[pid=642] vsize: 152496
Current children cumulated CPU time (s) 788.25
Current children cumulated vsize (Kb) 154624

[startup+800.069 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 34856 0 0 0 79654 168 0 0 25 0 1 0 1797712056 156553216 33486 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 38221 33486 162 162 0 38059 0
[pid=642] vsize: 152884
Current children cumulated CPU time (s) 798.23
Current children cumulated vsize (Kb) 155012

[startup+810.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 35062 0 0 0 80650 170 0 0 25 0 1 0 1797712056 157384704 33692 4294967295 134512640 135167914 3221224448 3221223152 134562905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 38424 33692 162 162 0 38262 0
[pid=642] vsize: 153696
Current children cumulated CPU time (s) 808.21
Current children cumulated vsize (Kb) 155824

[startup+820.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 35310 0 0 0 81645 172 0 0 25 0 1 0 1797712056 158396416 33940 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 38671 33940 162 162 0 38509 0
[pid=642] vsize: 154684
Current children cumulated CPU time (s) 818.18
Current children cumulated vsize (Kb) 156812

[startup+830.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 35567 0 0 0 82641 175 0 0 25 0 1 0 1797712056 159432704 34197 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 38924 34197 162 162 0 38762 0
[pid=642] vsize: 155696
Current children cumulated CPU time (s) 828.17
Current children cumulated vsize (Kb) 157824

[startup+840.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 35820 0 0 0 83637 177 0 0 25 0 1 0 1797712056 160456704 34450 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 39174 34450 162 162 0 39012 0
[pid=642] vsize: 156696
Current children cumulated CPU time (s) 838.15
Current children cumulated vsize (Kb) 158824

[startup+850.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 36051 0 0 0 84633 178 0 0 25 0 1 0 1797712056 161419264 34681 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 39409 34681 162 162 0 39247 0
[pid=642] vsize: 157636
Current children cumulated CPU time (s) 848.12
Current children cumulated vsize (Kb) 159764

[startup+860.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 36278 0 0 0 85629 180 0 0 25 0 1 0 1797712056 162336768 34908 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 39633 34908 162 162 0 39471 0
[pid=642] vsize: 158532
Current children cumulated CPU time (s) 858.1
Current children cumulated vsize (Kb) 160660

[startup+870.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 36521 0 0 0 86626 181 0 0 25 0 1 0 1797712056 163323904 35151 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 39874 35151 162 162 0 39712 0
[pid=642] vsize: 159496
Current children cumulated CPU time (s) 868.08
Current children cumulated vsize (Kb) 161624

[startup+880.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 36769 0 0 0 87622 183 0 0 25 0 1 0 1797712056 164327424 35399 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 40119 35399 162 162 0 39957 0
[pid=642] vsize: 160476
Current children cumulated CPU time (s) 878.06
Current children cumulated vsize (Kb) 162604

[startup+890.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 36998 0 0 0 88619 185 0 0 25 0 1 0 1797712056 165249024 35628 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 40344 35628 162 162 0 40182 0
[pid=642] vsize: 161376
Current children cumulated CPU time (s) 888.05
Current children cumulated vsize (Kb) 163504

[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 37260 0 0 0 89612 187 0 0 25 0 1 0 1797712056 166313984 35890 4294967295 134512640 135167914 3221224448 3221223152 134562652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 40604 35890 162 162 0 40442 0
[pid=642] vsize: 162416
Current children cumulated CPU time (s) 898
Current children cumulated vsize (Kb) 164544

[startup+910.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 37536 0 0 0 90608 188 0 0 25 0 1 0 1797712056 167432192 36166 4294967295 134512640 135167914 3221224448 3221223120 134562341 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 40877 36166 162 162 0 40715 0
[pid=642] vsize: 163508
Current children cumulated CPU time (s) 907.97
Current children cumulated vsize (Kb) 165636

[startup+920.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 37784 0 0 0 91605 190 0 0 25 0 1 0 1797712056 168476672 36414 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/642/statm): 41132 36414 162 162 0 40970 0
[pid=642] vsize: 164528
Current children cumulated CPU time (s) 917.96
Current children cumulated vsize (Kb) 166656

[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 37919 0 0 0 92603 192 0 0 25 0 1 0 1797712056 169021440 36549 4294967295 134512640 135167914 3221224448 3221223152 134562675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 41265 36549 162 162 0 41103 0
[pid=642] vsize: 165060
Current children cumulated CPU time (s) 927.96
Current children cumulated vsize (Kb) 167188

[startup+940.082 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 37975 0 0 0 93602 192 0 0 25 0 1 0 1797712056 169271296 36605 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 41326 36605 162 162 0 41164 0
[pid=642] vsize: 165304
Current children cumulated CPU time (s) 937.95
Current children cumulated vsize (Kb) 167432

[startup+950.083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 38055 0 0 0 94602 192 0 0 25 0 1 0 1797712056 169631744 36685 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 41414 36685 162 162 0 41252 0
[pid=642] vsize: 165656
Current children cumulated CPU time (s) 947.95
Current children cumulated vsize (Kb) 167784

[startup+960.085 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 38304 0 0 0 95597 194 0 0 25 0 1 0 1797712056 170627072 36934 4294967295 134512640 135167914 3221224448 3221223152 134562905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 41657 36934 162 162 0 41495 0
[pid=642] vsize: 166628
Current children cumulated CPU time (s) 957.92
Current children cumulated vsize (Kb) 168756

[startup+970.085 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 38467 0 0 0 96594 196 0 0 25 0 1 0 1797712056 171274240 37097 4294967295 134512640 135167914 3221224448 3221223152 134562556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 41815 37097 162 162 0 41653 0
[pid=642] vsize: 167260
Current children cumulated CPU time (s) 967.91
Current children cumulated vsize (Kb) 169388

[startup+980.086 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 38690 0 0 0 97590 198 0 0 25 0 1 0 1797712056 172171264 37320 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42034 37320 162 162 0 41872 0
[pid=642] vsize: 168136
Current children cumulated CPU time (s) 977.89
Current children cumulated vsize (Kb) 170264

[startup+990.087 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 38883 0 0 0 98587 198 0 0 25 0 1 0 1797712056 172945408 37513 4294967295 134512640 135167914 3221224448 3221223152 134562604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42223 37513 162 162 0 42061 0
[pid=642] vsize: 168892
Current children cumulated CPU time (s) 987.86
Current children cumulated vsize (Kb) 171020

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 38984 0 0 0 99585 199 0 0 25 0 1 0 1797712056 173355008 37614 4294967295 134512640 135167914 3221224448 3221223184 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42323 37614 162 162 0 42161 0
[pid=642] vsize: 169292
Current children cumulated CPU time (s) 997.85
Current children cumulated vsize (Kb) 171420

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39145 0 0 0 100583 200 0 0 25 0 1 0 1797712056 173993984 37775 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42479 37775 162 162 0 42317 0
[pid=642] vsize: 169916
Current children cumulated CPU time (s) 1007.84
Current children cumulated vsize (Kb) 172044

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39256 0 0 0 101581 202 0 0 25 0 1 0 1797712056 174440448 37886 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42588 37886 162 162 0 42426 0
[pid=642] vsize: 170352
Current children cumulated CPU time (s) 1017.84
Current children cumulated vsize (Kb) 172480

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39458 0 0 0 102578 203 0 0 25 0 1 0 1797712056 175255552 38088 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42787 38088 162 162 0 42625 0
[pid=642] vsize: 171148
Current children cumulated CPU time (s) 1027.82
Current children cumulated vsize (Kb) 173276

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39477 0 0 0 103578 203 0 0 25 0 1 0 1797712056 175329280 38107 4294967295 134512640 135167914 3221224448 3221223152 134566303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42805 38107 162 162 0 42643 0
[pid=642] vsize: 171220
Current children cumulated CPU time (s) 1037.82
Current children cumulated vsize (Kb) 173348

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39530 0 0 0 104577 203 0 0 25 0 1 0 1797712056 175538176 38160 4294967295 134512640 135167914 3221224448 3221223152 134562864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42856 38160 162 162 0 42694 0
[pid=642] vsize: 171424
Current children cumulated CPU time (s) 1047.81
Current children cumulated vsize (Kb) 173552

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39634 0 0 0 105576 204 0 0 25 0 1 0 1797712056 175968256 38264 4294967295 134512640 135167914 3221224448 3221223120 134562306 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 42961 38264 162 162 0 42799 0
[pid=642] vsize: 171844
Current children cumulated CPU time (s) 1057.81
Current children cumulated vsize (Kb) 173972

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39686 0 0 0 106576 204 0 0 25 0 1 0 1797712056 176177152 38316 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43012 38316 162 162 0 42850 0
[pid=642] vsize: 172048
Current children cumulated CPU time (s) 1067.81
Current children cumulated vsize (Kb) 174176

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39779 0 0 0 107574 205 0 0 25 0 1 0 1797712056 176545792 38409 4294967295 134512640 135167914 3221224448 3221223152 134562669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43102 38409 162 162 0 42940 0
[pid=642] vsize: 172408
Current children cumulated CPU time (s) 1077.8
Current children cumulated vsize (Kb) 174536

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 39965 0 0 0 108571 206 0 0 25 0 1 0 1797712056 177291264 38595 4294967295 134512640 135167914 3221224448 3221223152 134562905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43284 38595 162 162 0 43122 0
[pid=642] vsize: 173136
Current children cumulated CPU time (s) 1087.78
Current children cumulated vsize (Kb) 175264

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40107 0 0 0 109569 207 0 0 25 0 1 0 1797712056 177864704 38737 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43424 38737 162 162 0 43262 0
[pid=642] vsize: 173696
Current children cumulated CPU time (s) 1097.77
Current children cumulated vsize (Kb) 175824

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40136 0 0 0 110568 207 0 0 25 0 1 0 1797712056 177983488 38766 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43453 38766 162 162 0 43291 0
[pid=642] vsize: 173812
Current children cumulated CPU time (s) 1107.76
Current children cumulated vsize (Kb) 175940

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40142 0 0 0 111569 207 0 0 25 0 1 0 1797712056 178008064 38772 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43459 38772 162 162 0 43297 0
[pid=642] vsize: 173836
Current children cumulated CPU time (s) 1117.77
Current children cumulated vsize (Kb) 175964

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40174 0 0 0 112568 208 0 0 25 0 1 0 1797712056 178130944 38804 4294967295 134512640 135167914 3221224448 3221223172 134558092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43489 38804 162 162 0 43327 0
[pid=642] vsize: 173956
Current children cumulated CPU time (s) 1127.77
Current children cumulated vsize (Kb) 176084

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40176 0 0 0 113568 208 0 0 25 0 1 0 1797712056 178139136 38806 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43491 38806 162 162 0 43329 0
[pid=642] vsize: 173964
Current children cumulated CPU time (s) 1137.77
Current children cumulated vsize (Kb) 176092

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40195 0 0 0 114568 208 0 0 25 0 1 0 1797712056 178216960 38825 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43510 38825 162 162 0 43348 0
[pid=642] vsize: 174040
Current children cumulated CPU time (s) 1147.77
Current children cumulated vsize (Kb) 176168

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40227 0 0 0 115568 208 0 0 25 0 1 0 1797712056 178339840 38857 4294967295 134512640 135167914 3221224448 3221223156 134558150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43540 38857 162 162 0 43378 0
[pid=642] vsize: 174160
Current children cumulated CPU time (s) 1157.77
Current children cumulated vsize (Kb) 176288

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40333 0 0 0 116567 209 0 0 25 0 1 0 1797712056 178753536 38963 4294967295 134512640 135167914 3221224448 3221223152 134562669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43641 38963 162 162 0 43479 0
[pid=642] vsize: 174564
Current children cumulated CPU time (s) 1167.77
Current children cumulated vsize (Kb) 176692

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40477 0 0 0 117565 209 0 0 25 0 1 0 1797712056 179335168 39107 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43783 39107 162 162 0 43621 0
[pid=642] vsize: 175132
Current children cumulated CPU time (s) 1177.75
Current children cumulated vsize (Kb) 177260

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40627 0 0 0 118562 210 0 0 25 0 1 0 1797712056 179941376 39257 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/642/statm): 43931 39257 162 162 0 43769 0
[pid=642] vsize: 175724
Current children cumulated CPU time (s) 1187.73
Current children cumulated vsize (Kb) 177852

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40765 0 0 0 119559 212 0 0 25 0 1 0 1797712056 180502528 39395 4294967295 134512640 135167914 3221224448 3221223152 134562604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/642/statm): 44068 39395 162 162 0 43906 0
[pid=642] vsize: 176272
Current children cumulated CPU time (s) 1197.72
Current children cumulated vsize (Kb) 178400

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40913 0 0 0 120557 213 0 0 25 0 1 0 1797712056 181100544 39543 4294967295 134512640 135167914 3221224448 3221223152 134562601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/642/statm): 44214 39543 162 162 0 44052 0
[pid=642] vsize: 176856
Current children cumulated CPU time (s) 1207.71
Current children cumulated vsize (Kb) 178984



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 642
Raw data (/proc/637/stat): 637 (minisat+_script) S 636 637 9854 0 -1 0 314 332 0 0 0 1 0 0 21 0 1 0 1797712049 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/637/statm): 532 234 485 147 0 385 0
[pid=637] vsize: 2128
Raw data (/proc/642/stat): 642 (minisat+_bignum) R 637 637 9854 0 -1 0 40913 0 0 0 120557 213 0 0 25 0 1 0 1797712056 181100544 39543 4294967295 134512640 135167914 3221224448 3221223152 134562601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/642/statm): 44214 39543 162 162 0 44052 0
[pid=642] vsize: 176856
Current children cumulated CPU time (s) 1207.71
Current children cumulated vsize (Kb) 178984

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

Child status: 0
Real time (s): 1210.19
CPU time (s): 1207.78
CPU user time (s): 1205.57
CPU system time (s): 2.20766
CPU usage (%): 99.8011
Max. virtual memory (cumulated for all children) (Kb): 178984

Verifier Data

ERROR: no interpretation found !