Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-momentum3.opb
MD5SUMfd20bcfe4a71405dc1e0ef3cb894b630
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 87370
Biggest coefficient in the objective function 1310720000
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 13573186735
Number of bits of the sum of numbers in the objective function 34
Biggest number in a constraint 10240000000000000927712935936
Number of bits of the biggest number in a constraint 94
Biggest sum of numbers in a constraint 29801266744107043904416645120
Number of bits of the biggest sum of numbers95
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables93400
Total number of constraints70153
Number of constraints which are clauses6081
Number of constraints which are cardinality constraints (but not clauses)7185
Number of constraints which are nor clauses,nor cardinality constraints56887
Minimum length of a constraint1
Maximum length of a constraint1018

Trace number 3929

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        541524 kB
Buffers:         35284 kB
Cached:         428868 kB
SwapCached:        696 kB
Active:         374804 kB
Inactive:        91940 kB
HighTotal:      131008 kB
HighFree:         3752 kB
LowTotal:       903652 kB
LowFree:        537772 kB
SwapTotal:     2097640 kB
SwapFree:      2096372 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5812 kB
Slab:            20652 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 04:09:16 (client local time) WITH STATUS 0 IN 1204.2 SECONDS
stats: 2925 7 1204.2 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 35810] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 30306 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################=====================================================================================================================================================================================================================================================================================================================#################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.s...........s...ss....................s......s......s..s.s.s....s.s...s..........s.....ss.s.......s.s...........s.s.......s.....s.s.sssssssssssssss..........s......ss.sss....................ss...........s...........s.s.........s............s...............s......s.ss....................s.....s.s...s..s...s......s.......s..s...sssss..s.ss..ss..s......s....ss........s..ss.s.s......s..s.....ss.s.ssss.......s.....ss........s.s.......ss......s...........s..ss......s......s......s.s.....s..s..s....s........s........s.sss..................s....s......ss..ssssss.....ss..s.....ssss..s...ss..s.s.sss....s.ss.sssssss.sss..s.ss.....s..ss..s.s...s..s..ss.s.ss.s.....ssss....ssss..s....s..sss..ssss.s..ss.sss......s.ssss..ss...s.....s.sssss.s...s.s........s..ssss.ss...s..sssssssssss.sssssssssssssssssss.s.s.s....s....ss......ss................s.......ss.ss...s....s...s.s.s..s..s..ss......sss.s..ss......s...s...s.s........ss...s.....s.s....s...ss........ss..ssss........ss.sss...s.ss.sss.sss..s..s..s.s..s.s..ssss.ssssss..sssssss.sss.sss..ss..ss..s.....sssssss...ss.ssssssss..ss..sssssss..ss....ssss.ss....ss.s....s.s..s.s.sss.s.s.ssssss.ss.s..s..s.ss.....s.sssssssssssssssss.sssssssss.s.s..s...ssssssss.s.sssss.s.s.sssssssssssssssssssssss.ssss..sss..sssssssss.ssss.sssssssss..ssssss.sssssssssssssssssssssssssssss.s.ssssssssssssssssssssssssssssssss..sss.s.ss.ssss.ss.ssssssssssssssssss.ssssssssssssssssssssssssssssssssssss..ss.s.sssssss.ssssssssssssssssssssssssssssssssssssssssssssssssss..ssssssss.ssssssssssssssssssssssssss..s..ss.sssss...s.s.s.ss.sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.ssssssss.s.ss..ssssssssssssssssssssssssssssssssssssssss.sssssssssssss..s..sss.sssss.ssssssssssssssssssss.sssss..sssssss.sssssssssssssssssssssss.sssssssssss..sssssss.ssssss.ssssssssssssssssssssssssssssssssssssssss.ssssssssssssssssss..sss.sssssssssssss.sss.ssss.ssssssssssssssssssssssssssssssssssssssssssssss.sssssssssssssssssssssssssss.ss.sssssssssssssssssssssss.sss.sssssss.sssssssssssssssssssssssss..ss.s...s....sssssssssssssssssssss.s.s.ssssss.sssssssssssssssssssss.sssssssssssssssss.ssssss.ssssssssssssssssssssssss.ssssssssssssssssssssssssss.ss.sssssssssssssssssssss...s.ssss.ssssssssss............................................................................................s...........s.............................s................................s............s...........................s.......................................................................s......s.........ss.sssssss...........................................s.............s....s.........................................s.....................s...........s........................................s.............................s...s.........s.......s...............................................s......s..........s......s....s....s..................ss....s.......s.......s...s...s...s...s...s.....s..sss.................s....s.............s...............s....................s.......................................................................s...........................................................s......s...........s...............................................................................................................................................s........................s...................................................................................................................................................s.............................................................................................................s..........s..............................................................................................................................................................................................................................................................................................................................................ss..s.s...s.s.....s.....s..s..............s.....s...........................s...s............s...ss.ss..s......................................s...................ss...............s.......s................s...s....................s..................s.......s.s....s..........s....s..............s...................s....s.....s....ssss.........s..s...........s.....s.......s..s...s...........s.........s........s..s.........................s....s.s.s................s.................s..s..s.....s.s....ss.........s...s............s.ss....s.ss..sss...........s........s.s.ss.......s.......s.s.s...s.......ss.s.ss..s.....
c ---[32998]---> BDD-cost:    7
c ---[32997]---> BDD-cost:   10
c ---[32996]---> BDD-cost:   10
c ---[32995]---> BDD-cost:   10
c ---[32994]---> BDD-cost:   10
c ---[32993]---> BDD-cost:   10
c ---[32992]---> BDD-cost:   10
c ---[32991]---> BDD-cost:   10
c ---[32990]---> BDD-cost:   10
c ---[32989]---> BDD-cost:   10
c ---[32988]---> BDD-cost:   10
c ---[32987]---> BDD-cost:   10
c ---[32986]---> BDD-cost:   10
c ---[32985]---> BDD-cost:   10
c ---[32984]---> BDD-cost:   10
c ---[32983]---> BDD-cost:   10
c ---[32982]---> BDD-cost:   10
c ---[32981]---> BDD-cost:   10
c ---[32980]---> BDD-cost:   10
c ---[32979]---> BDD-cost:   10
c ---[32978]---> BDD-cost:   10
c ---[32977]---> BDD-cost:   10
c ---[32976]---> BDD-cost:   10
c ---[32975]---> BDD-cost:   10
c ---[32974]---> BDD-cost:   10
c ---[32973]---> BDD-cost:   10
c ---[32972]---> BDD-cost:   10
c ---[32971]---> BDD-cost:   10
c ---[32970]---> BDD-cost:   10
c ---[32969]---> BDD-cost:   10
c ---[32968]---> BDD-cost:   10
c ---[32967]---> BDD-cost:   10
c ---[32966]---> BDD-cost:   10
c ---[32965]---> BDD-cost:   10
c ---[32964]---> BDD-cost:   10
c ---[32963]---> BDD-cost:   10
c ---[32962]---> BDD-cost:   10
c ---[32961]---> BDD-cost:   10
c ---[32960]---> BDD-cost:   10
c ---[32959]---> BDD-cost:   10
c ---[32958]---> BDD-cost:   10
c ---[32957]---> BDD-cost:   10
c ---[32956]---> BDD-cost:   10
c ---[32954]---> BDD-cost:   10
c ---[32953]---> BDD-cost:   10
c ---[32952]---> BDD-cost:   10
c ---[32951]---> BDD-cost:   10
c ---[32949]---> BDD-cost:   10
c ---[32948]---> BDD-cost:   10
c ---[32947]---> BDD-cost:   10
c ---[32944]---> BDD-cost:   10
c ---[32941]---> BDD-cost:   10
c ---[32940]---> BDD-cost:   10
c ---[32939]---> BDD-cost:   10
c ---[32938]---> BDD-cost:   10
c ---[32937]---> BDD-cost:   10
c ---[32936]---> BDD-cost:   10
c ---[32935]---> BDD-cost:   10
c ---[32933]---> BDD-cost:   10
c ---[32932]---> BDD-cost:   10
c ---[32931]---> BDD-cost:   10
c ---[32930]---> BDD-cost:   10
c ---[32929]---> BDD-cost:   10
c ---[32927]---> BDD-cost:   10
c ---[32924]---> BDD-cost:   10
c ---[32921]---> BDD-cost:   10
c ---[32918]---> BDD-cost:   10
c ---[32916]---> BDD-cost:   10
c ---[32915]---> BDD-cost:   10
c ---[32914]---> BDD-cost:   10
c ---[32913]---> BDD-cost:   10
c ---[32911]---> BDD-cost:   10
c ---[32909]---> BDD-cost:   10
c ---[32908]---> BDD-cost:   10
c ---[32906]---> BDD-cost:   10
c ---[32904]---> BDD-cost:   10
c ---[32903]---> BDD-cost:   10
c ---[32902]---> BDD-cost:   10
c ---[32901]---> BDD-cost:   10
c ---[32900]---> BDD-cost:   10
c ---[32899]---> BDD-cost:   10
c ---[32896]---> BDD-cost:   10
c ---[32895]---> BDD-cost:   10
c ---[32894]---> BDD-cost:   10
c ---[32890]---> BDD-cost:   10
c ---[32889]---> BDD-cost:   10
c ---[32888]---> BDD-cost:   10
c ---[32885]---> BDD-cost:   10
c ---[32884]---> BDD-cost:   10
c ---[32883]---> BDD-cost:   10
c ---[32882]---> BDD-cost:   10
c ---[32881]---> BDD-cost:   10
c ---[32879]---> BDD-cost:   10
c ---[32878]---> BDD-cost:   10
c ---[32877]---> BDD-cost:   10
c ---[32876]---> BDD-cost:   10
c ---[32875]---> BDD-cost:   10
c ---[32874]---> BDD-cost:   10
c ---[32873]---> BDD-cost:   10
c ---[32872]---> BDD-cost:   10
c ---[32871]---> BDD-cost:   10
c ---[32870]---> BDD-cost:   10
c ---[32869]---> BDD-cost:   10
c ---[32868]---> BDD-cost:   10
c ---[32867]---> BDD-cost:   10
c ---[32866]---> BDD-cost:   10
c ---[32865]---> BDD-cost:   10
c ---[32864]---> BDD-cost:   10
c ---[32863]---> BDD-cost:   10
c ---[32861]---> BDD-cost:   10
c ---[32860]---> BDD-cost:   10
c ---[32857]---> BDD-cost:   10
c ---[32855]---> BDD-cost:   10
c ---[32854]---> BDD-cost:   10
c ---[32852]---> BDD-cost:   10
c ---[32848]---> BDD-cost:   10
c ---[32847]---> BDD-cost:   10
c ---[32846]---> BDD-cost:   10
c ---[32845]---> BDD-cost:   10
c ---[32841]---> BDD-cost:   10
c ---[32840]---> BDD-cost:   10
c ---[32839]---> BDD-cost:   10
c ---[32838]---> BDD-cost:   10
c ---[32837]---> BDD-cost:   10
c ---[32836]---> BDD-cost:   10
c ---[32835]---> BDD-cost:   10
c ---[32834]---> BDD-cost:   10
c ---[32833]---> BDD-cost:   10
c ---[32832]---> BDD-cost:   10
c ---[32831]---> BDD-cost:   10
c ---[32830]---> BDD-cost:   10
c ---[32827]---> BDD-cost:   10
c ---[32826]---> BDD-cost:   10
c ---[32825]---> BDD-cost:   10
c ---[32824]---> BDD-cost:   10
c ---[32822]---> BDD-cost:   10
c ---[32821]---> BDD-cost:   10
c ---[32819]---> BDD-cost:   10
c ---[32817]---> BDD-cost:   10
c ---[32816]---> BDD-cost:   10
c ---[32815]---> BDD-cost:   10
c ---[32812]---> BDD-cost:   10
c ---[32811]---> BDD-cost:   10
c ---[32810]---> BDD-cost:   10
c ---[32809]---> BDD-cost:   10
c ---[32807]---> BDD-cost:   10
c ---[32806]---> BDD-cost:   10
c ---[32804]---> BDD-cost:   10
c ---[32803]---> BDD-cost:   10
c ---[32802]---> BDD-cost:   10
c ---[32801]---> BDD-cost:   10
c ---[32798]---> BDD-cost:   10
c ---[26713]---> BDD-cost:    7
c ---[26712]---> BDD-cost:   10
c ---[26711]---> BDD-cost:   10
c ---[26709]---> BDD-cost:    7
c ---[26706]---> BDD-cost:   10
c ---[26704]---> BDD-cost:    7
c ---[26701]---> BDD-cost:    7
c ---[26700]---> BDD-cost:   10
c ---[26699]---> BDD-cost:   10
c ---[26697]---> BDD-cost:    7
c ---[26696]---> BDD-cost:    7
c ---[26695]---> BDD-cost:   10
c ---[26694]---> BDD-cost:   10
c ---[26693]---> BDD-cost:   10
c ---[26692]---> BDD-cost:   10
c ---[26689]---> BDD-cost:   10
c ---[26683]---> BDD-cost:    7
c ---[26682]---> BDD-cost:   10
c ---[26681]---> BDD-cost:   10
c ---[26680]---> BDD-cost:   10
c ---[26678]---> BDD-cost:   10
c ---[26676]---> BDD-cost:   10
c ---[26675]---> BDD-cost:   10
c ---[26673]---> BDD-cost:   10
c ---[26670]---> BDD-cost:   10
c ---[26669]---> BDD-cost:    7
c ---[26668]---> BDD-cost:   10
c ---[26666]---> BDD-cost:   10
c ---[26664]---> BDD-cost:    7
c ---[26660]---> BDD-cost:   10
c ---[26659]---> BDD-cost:   10
c ---[26655]---> BDD-cost:   10
c ---[26654]---> BDD-cost:   10
c ---[26648]---> BDD-cost:   10
c ---[26646]---> BDD-cost:   10
c ---[26645]---> BDD-cost:   10
c ---[26638]---> BDD-cost:   10
c ---[26636]---> BDD-cost:   10
c ---[26635]---> BDD-cost:    7
c ---[26629]---> BDD-cost:   10
c ---[26628]---> BDD-cost:    7
c ---[26627]---> BDD-cost:    7
c ---[26626]---> BDD-cost:    7
c ---[26620]---> BDD-cost:   10
c ---[26618]---> BDD-cost:   10
c ---[26617]---> BDD-cost:    7
c ---[26614]---> BDD-cost:    7
c ---[26609]---> BDD-cost:   10
c ---[26608]---> BDD-cost:    7
c ---[26607]---> BDD-cost:   10
c ---[26601]---> BDD-cost:    7
c ---[26600]---> BDD-cost:    7
c ---[26599]---> BDD-cost:    7
c ---[26598]---> BDD-cost:    7
c ---[26594]---> BDD-cost:    7
c ---[26591]---> BDD-cost:   10
c ---[26588]---> BDD-cost:   10
c ---[26586]---> BDD-cost:   10
c ---[26585]---> BDD-cost:    7
c ---[26581]---> BDD-cost:   10
c ---[26580]---> BDD-cost:   10
c ---[26577]---> BDD-cost:   10
c ---[26574]---> BDD-cost:   10
c ---[26573]---> BDD-cost:   10
c ---[26571]---> BDD-cost:   10
c ---[26570]---> BDD-cost:    7
c ---[26568]---> BDD-cost:   10
c ---[26565]---> BDD-cost:   10
c ---[26563]---> BDD-cost:   10
c ---[26560]---> BDD-cost:    7
c ---[26559]---> BDD-cost:   10
c ---[26558]---> BDD-cost:    7
c ---[26550]---> BDD-cost:   10
c ---[26549]---> BDD-cost:   10
c ---[26546]---> BDD-cost:    7
c ---[26542]---> BDD-cost:   10
c ---[26541]---> BDD-cost:    7
c ---[26539]---> BDD-cost:   10
c ---[26535]---> BDD-cost:    7
c ---[26528]---> BDD-cost:    7
c ---[26527]---> BDD-cost:   10
c ---[26526]---> BDD-cost:    7
c ---[26525]---> BDD-cost:    7
c ---[26524]---> BDD-cost:    7
c ---[26521]---> BDD-cost:   10
c ---[26515]---> BDD-cost:   10
c ---[26514]---> BDD-cost:   10
c ---[26512]---> BDD-cost:   10
c ---[26510]---> BDD-cost:    7
c ---[26509]---> BDD-cost:   10
c ---[26508]---> BDD-cost:    7
c ---[26507]---> BDD-cost:   10
c ---[26506]---> BDD-cost:    7
c ---[26503]---> BDD-cost:   10
c ---[26502]---> BDD-cost:   10
c ---[26501]---> BDD-cost:   10
c ---[26500]---> BDD-cost:    7
c ---[26499]---> BDD-cost:   10
c ---[26497]---> BDD-cost:   10
c ---[26495]---> BDD-cost:    7
c ---[26494]---> BDD-cost:   10
c ---[26493]---> BDD-cost:    7
c ---[26492]---> BDD-cost:   10
c ---[26490]---> BDD-cost:   10
c ---[26488]---> BDD-cost:   10
c ---[26484]---> BDD-cost:   10
c ---[26482]---> BDD-cost:    7
c ---[26480]---> BDD-cost:    7
c ---[26479]---> BDD-cost:    7
c ---[26478]---> BDD-cost:    7
c ---[26475]---> BDD-cost:   10
c ---[26473]---> BDD-cost:   10
c ---[26472]---> BDD-cost:    7
c ---[26471]---> BDD-cost:   10
c ---[26470]---> BDD-cost:    7
c ---[26469]---> BDD-cost:   10
c ---[26465]---> BDD-cost:    7
c ---[26464]---> BDD-cost:   10
c ---[26458]---> BDD-cost:   10
c ---[26456]---> BDD-cost:   10
c ---[26455]---> BDD-cost:   10
c ---[26453]---> BDD-cost:   10
c ---[26450]---> BDD-cost:   10
c ---[26449]---> BDD-cost:    7
c ---[26448]---> BDD-cost:   10
c ---[26445]---> BDD-cost:    7
c ---[26444]---> BDD-cost:    7
c ---[26443]---> BDD-cost:   10
c ---[26438]---> BDD-cost:    7
c ---[26436]---> BDD-cost:   10
c ---[26435]---> BDD-cost:    7
c ---[26431]---> BDD-cost:   10
c ---[26430]---> BDD-cost:   10
c ---[26428]---> BDD-cost:   10
c ---[26425]---> BDD-cost:   10
c ---[26424]---> BDD-cost:   10
c ---[26420]---> BDD-cost:    7
c ---[26418]---> BDD-cost:    7
c ---[26417]---> BDD-cost:   10
c ---[26412]---> BDD-cost:    7
c ---[26409]---> BDD-cost:   10
c ---[26408]---> BDD-cost:    7
c ---[26407]---> BDD-cost:   10
c ---[26404]---> BDD-cost:   10
c ---[26400]---> BDD-cost:    7
c ---[26399]---> BDD-cost:    7
c ---[26394]---> BDD-cost:   10
c ---[26392]---> BDD-cost:   10
c ---[26390]---> BDD-cost:    7
c ---[26389]---> BDD-cost:   10
c ---[26388]---> BDD-cost:   10
c ---[26387]---> BDD-cost:   10
c ---[26386]---> BDD-cost:    7
c ---[26384]---> BDD-cost:   10
c ---[26379]---> BDD-cost:    7
c ---[26378]---> BDD-cost:    7
c ---[26373]---> BDD-cost:    7
c ---[26369]---> BDD-cost:   10
c ---[26368]---> BDD-cost:   10
c ---[26367]---> BDD-cost:    7
c ---[26361]---> BDD-cost:    7
c ---[26360]---> BDD-cost:   10
c ---[26359]---> BDD-cost:   10
c ---[26358]---> BDD-cost:   10
c ---[26357]---> BDD-cost:    7
c ---[26356]---> BDD-cost:   10
c ---[26355]---> BDD-cost:    7
c ---[26354]---> BDD-cost:    7
c ---[26353]---> BDD-cost:    7
c ---[26352]---> BDD-cost:    7
c ---[26349]---> BDD-cost:    7
c ---[26348]---> BDD-cost:    7
c ---[26343]---> BDD-cost:    7
c ---[26342]---> BDD-cost:    7
c ---[26340]---> BDD-cost:    7
c ---[26336]---> BDD-cost:   10
c ---[26335]---> BDD-cost:   10
c ---[26332]---> BDD-cost:    7
c ---[26331]---> BDD-cost:   10
c ---[26330]---> BDD-cost:   10
c ---[26329]---> BDD-cost:    7
c ---[26321]---> BDD-cost:   10
c ---[26320]---> BDD-cost:    7
c ---[26319]---> BDD-cost:    7
c ---[26317]---> BDD-cost:    7
c ---[26315]---> BDD-cost:   10
c ---[26311]---> BDD-cost:   10
c ---[26310]---> BDD-cost:    7
c ---[26309]---> BDD-cost:   10
c ---[26308]---> BDD-cost:   10
c ---[26304]---> BDD-cost:   10
c ---[26302]---> BDD-cost:    7
c ---[26301]---> BDD-cost:   10
c ---[26299]---> BDD-cost:    7
c ---[26297]---> BDD-cost:   10
c ---[26289]---> BDD-cost:    7
c ---[26283]---> BDD-cost:   10
c ---[26279]---> BDD-cost:    7
c ---[26276]---> BDD-cost:    7
c ---[26275]---> BDD-cost:    7
c ---[26274]---> BDD-cost:   10
c ---[26273]---> BDD-cost:    7
c ---[26271]---> BDD-cost:    7
c ---[26269]---> BDD-cost:   10
c ---[26267]---> BDD-cost:    7
c ---[26172]---> BDD-cost:   10
c ---[25957]---> BDD-cost:   11
c ---[25441]---> BDD-cost:   10
c ---[25288]---> BDD-cost:   11
c ---[25084]---> BDD-cost:   10
c ---[25066]---> BDD-cost:    1
c ---[25030]---> BDD-cost:   11
c ---[25023]---> BDD-cost:    5
c ---[25012]---> BDD-cost:    1
c ---[24983]---> BDD-cost:   11
c ---[24954]---> BDD-cost:   11
c ---[24919]---> BDD-cost:   10
c ---[24905]---> BDD-cost:   11
c ---[24898]---> BDD-cost:    9
c ---[24892]---> BDD-cost:   10
c ---[24871]---> BDD-cost:   11
c ---[24855]---> BDD-cost:    8
c ---[24773]---> BDD-cost:   11
c ---[24726]---> BDD-cost:   11
c ---[24716]---> BDD-cost:    1
c ---[24646]---> BDD-cost:    1
c ---[24596]---> BDD-cost:   11
c ---[24587]---> BDD-cost:   11
c ---[24585]---> BDD-cost:    1
c ---[24555]---> BDD-cost:   10
c ---[24456]---> BDD-cost:   11
c ---[24454]---> BDD-cost:    5
c ---[24430]---> BDD-cost:   10
c ---[24429]---> BDD-cost:    1
c ---[24410]---> BDD-cost:    8
c ---[24368]---> BDD-cost:   11
c ---[24355]---> BDD-cost:   10
c ---[24345]---> BDD-cost:    1
c ---[24324]---> BDD-cost:    9
c ---[24319]---> BDD-cost:    8
c ---[24317]---> BDD-cost:    1
c ---[24311]---> BDD-cost:   10
c ---[24300]---> BDD-cost:    2
c ---[24291]---> BDD-cost:   11
c ---[24290]---> BDD-cost:    9
c ---[24269]---> BDD-cost:    1
c ---[24268]---> BDD-cost:    1
c ---[24257]---> BDD-cost:   10
c ---[24237]---> BDD-cost:    2
c ---[24208]---> BDD-cost:   10
c ---[24162]---> BDD-cost:   10
c ---[24161]---> BDD-cost:    2
c ---[24146]---> BDD-cost:   11
c ---[24134]---> BDD-cost:    1
c ---[24124]---> BDD-cost:    1
c ---[24111]---> BDD-cost:   10
c ---[24090]---> BDD-cost:   11
c ---[24068]---> BDD-cost:   10
c ---[24056]---> BDD-cost:    2
c ---[24054]---> BDD-cost:    2
c ---[24053]---> BDD-cost:   10
c ---[23989]---> BDD-cost:   10
c ---[23933]---> BDD-cost:   11
c ---[23932]---> BDD-cost:   10
c ---[23919]---> BDD-cost:   10
c ---[23914]---> BDD-cost:    1
c ---[23894]---> BDD-cost:    2
c ---[23890]---> BDD-cost:   10
c ---[23875]---> BDD-cost:    9
c ---[23828]---> BDD-cost:   10
c ---[23816]---> BDD-cost:   10
c ---[23796]---> BDD-cost:    2
c ---[23789]---> BDD-cost:    2
c ---[23779]---> BDD-cost:   11
c ---[23748]---> BDD-cost:    1
c ---[23716]---> BDD-cost:   11
c ---[23678]---> BDD-cost:   10
c ---[23667]---> BDD-cost:    1
c ---[23648]---> BDD-cost:    1
c ---[23610]---> BDD-cost:    1
c ---[23600]---> BDD-cost:   11
c ---[23593]---> BDD-cost:   10
c ---[23589]---> BDD-cost:    2
c ---[23588]---> BDD-cost:   10
c ---[23569]---> BDD-cost:    9
c ---[23539]---> BDD-cost:   10
c ---[23452]---> BDD-cost:    1
c ---[23444]---> BDD-cost:    1
c ---[23417]---> BDD-cost:   11
c ---[23354]---> BDD-cost:   10
c ---[23327]---> BDD-cost:   10
c ---[23245]---> BDD-cost:   10
c ---[23243]---> BDD-cost:   10
c ---[23220]---> BDD-cost:    9
c ---[23209]---> BDD-cost:    1
c ---[23206]---> BDD-cost:    1
c ---[23201]---> BDD-cost:    2
c ---[23179]---> BDD-cost:   11
c ---[23172]---> BDD-cost:    2
c ---[23168]---> BDD-cost:    2
c ---[23149]---> BDD-cost:   11
c ---[23132]---> BDD-cost:   10
c ---[23131]---> BDD-cost:    9
c ---[23112]---> BDD-cost:    2
c ---[23075]---> BDD-cost:    1
c ---[23070]---> BDD-cost:   10
c ---[23065]---> BDD-cost:   11
c ---[23028]---> BDD-cost:   11
c ---[23008]---> BDD-cost:   11
c ---[22988]---> BDD-cost:    1
c ---[22963]---> BDD-cost:    1
c ---[22962]---> BDD-cost:    1
c ---[22947]---> BDD-cost:    1
c ---[22937]---> BDD-cost:   11
c ---[22935]---> BDD-cost:   12
c ---[22925]---> BDD-cost:   10
c ---[22911]---> BDD-cost:    2
c ---[22909]---> BDD-cost:   10
c ---[22878]---> BDD-cost:    2
c ---[22815]---> BDD-cost:   10
c ---[22800]---> BDD-cost:   10
c ---[22788]---> BDD-cost:   11
c ---[22708]---> BDD-cost:    1
c ---[22692]---> BDD-cost:   11
c ---[22664]---> BDD-cost:    1
c ---[22663]---> BDD-cost:    1
c ---[22616]---> BDD-cost:   11
c ---[22592]---> BDD-cost:    8
c ---[22555]---> BDD-cost:   11
c ---[22532]---> BDD-cost:    1
c ---[22530]---> BDD-cost:    1
c ---[22500]---> BDD-cost:    1
c ---[22472]---> BDD-cost:    1
c ---[22450]---> BDD-cost:   10
c ---[22448]---> BDD-cost:   11
c ---[22355]---> BDD-cost:   11
c ---[22341]---> BDD-cost:    8
c ---[22313]---> BDD-cost:    1
c ---[22312]---> BDD-cost:    1
c ---[22292]---> BDD-cost:   12
c ---[22243]---> BDD-cost:   11
c ---[22224]---> BDD-cost:   10
c ---[22190]---> BDD-cost:   10
c ---[22178]---> BDD-cost:    2
c ---[22160]---> BDD-cost:   10
c ---[22137]---> BDD-cost:    2
c ---[22105]---> BDD-cost:   11
c ---[22073]---> BDD-cost:    8
c ---[22072]---> BDD-cost:    2
c ---[21958]---> BDD-cost:   11
c ---[21928]---> BDD-cost:    1
c ---[21925]---> BDD-cost:   10
c ---[21923]---> BDD-cost:   11
c ---[21874]---> BDD-cost:   10
c ---[21845]---> BDD-cost:   11
c ---[21841]---> BDD-cost:   10
c ---[21737]---> BDD-cost:   11
c ---[21729]---> BDD-cost:    2
c ---[21701]---> BDD-cost:   10
c ---[21691]---> BDD-cost:   10
c ---[21685]---> BDD-cost:   11
c ---[21636]---> BDD-cost:   10
c ---[21606]---> BDD-cost:   11
c ---[21600]---> BDD-cost:    1
c ---[21598]---> BDD-cost:   10
c ---[21593]---> BDD-cost:    1
c ---[21575]---> BDD-co

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/9253/stat): 9253 (minisat+_script) R 9252 9253 20115 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1846790383 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9253/statm): 174 3 169 147 0 27 0
[pid=9253] 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=9254
New process pid=9255
New process pid=9256
execve syscall for /bin/sed executable
One traced child (pid=9255) 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=9256) exited with status: 0
One traced child (pid=9254) exited with status: 0
New process pid=9257
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-momentum3.opb
One traced child (pid=9257) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=9258
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-momentum3.opb

[startup+10.0044 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 5375 0 0 0 724 28 0 0 25 0 1 0 1846790604 23703552 4899 4294967295 134512640 135167914 3221224448 3221222736 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 5787 4899 162 162 0 5625 0
[pid=9258] vsize: 23148
Current children cumulated CPU time (s) 9.47
Current children cumulated vsize (Kb) 25276

[startup+20.0051 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 7280 0 0 0 1692 43 0 0 25 0 1 0 1846790604 31510528 6804 4294967295 134512640 135167914 3221224448 3221220592 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 7693 6804 162 162 0 7531 0
[pid=9258] vsize: 30772
Current children cumulated CPU time (s) 19.3
Current children cumulated vsize (Kb) 32900

[startup+30.0058 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 8419 0 0 0 2665 55 0 0 25 0 1 0 1846790604 36163584 7943 4294967295 134512640 135167914 3221224448 3221223408 134578783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 8829 7943 162 162 0 8667 0
[pid=9258] vsize: 35316
Current children cumulated CPU time (s) 29.15
Current children cumulated vsize (Kb) 37444

[startup+40.0075 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 9409 0 0 0 3639 66 0 0 25 0 1 0 1846790604 40214528 8933 4294967295 134512640 135167914 3221224448 3221222656 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 9818 8933 162 162 0 9656 0
[pid=9258] vsize: 39272
Current children cumulated CPU time (s) 39
Current children cumulated vsize (Kb) 41400

[startup+50.0092 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 10105 0 0 0 4612 78 0 0 25 0 1 0 1846790604 43065344 9629 4294967295 134512640 135167914 3221224448 3221223136 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 10514 9629 162 162 0 10352 0
[pid=9258] vsize: 42056
Current children cumulated CPU time (s) 48.85
Current children cumulated vsize (Kb) 44184

[startup+60.0099 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 11048 0 0 0 5585 89 0 0 25 0 1 0 1846790604 46927872 10572 4294967295 134512640 135167914 3221224448 3221223264 134849201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 11457 10572 162 162 0 11295 0
[pid=9258] vsize: 45828
Current children cumulated CPU time (s) 58.69
Current children cumulated vsize (Kb) 47956

[startup+70.0106 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 12292 0 0 0 6558 102 0 0 25 0 1 0 1846790604 52023296 11816 4294967295 134512640 135167914 3221224448 3221223164 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 12701 11816 162 162 0 12539 0
[pid=9258] vsize: 50804
Current children cumulated CPU time (s) 68.55
Current children cumulated vsize (Kb) 52932

[startup+80.0113 s]
Raw data (loadavg): 1.01 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 13466 0 0 0 7531 114 0 0 25 0 1 0 1846790604 56832000 12990 4294967295 134512640 135167914 3221224448 3221222620 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 13875 12990 162 162 0 13713 0
[pid=9258] vsize: 55500
Current children cumulated CPU time (s) 78.4
Current children cumulated vsize (Kb) 57628

[startup+90.012 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 14282 0 0 0 8506 125 0 0 25 0 1 0 1846790604 60174336 13806 4294967295 134512640 135167914 3221224448 3221221456 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 14691 13806 162 162 0 14529 0
[pid=9258] vsize: 58764
Current children cumulated CPU time (s) 88.26
Current children cumulated vsize (Kb) 60892

[startup+100.013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 15804 0 0 0 9476 139 0 0 25 0 1 0 1846790604 66408448 15328 4294967295 134512640 135167914 3221224448 3221221892 134610973 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 16213 15328 162 162 0 16051 0
[pid=9258] vsize: 64852
Current children cumulated CPU time (s) 98.1
Current children cumulated vsize (Kb) 66980

[startup+110.013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 17043 0 0 0 10449 151 0 0 25 0 1 0 1846790604 71483392 16567 4294967295 134512640 135167914 3221224448 3221222800 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 17452 16567 162 162 0 17290 0
[pid=9258] vsize: 69808
Current children cumulated CPU time (s) 107.95
Current children cumulated vsize (Kb) 71936

[startup+120.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 18245 0 0 0 11422 163 0 0 25 0 1 0 1846790604 76406784 17769 4294967295 134512640 135167914 3221224448 3221222876 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 18654 17769 162 162 0 18492 0
[pid=9258] vsize: 74616
Current children cumulated CPU time (s) 117.8
Current children cumulated vsize (Kb) 76744

[startup+130.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 19098 0 0 0 12397 174 0 0 25 0 1 0 1846790604 79900672 18622 4294967295 134512640 135167914 3221224448 3221222280 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 19507 18622 162 162 0 19345 0
[pid=9258] vsize: 78028
Current children cumulated CPU time (s) 127.66
Current children cumulated vsize (Kb) 80156

[startup+140.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 19824 0 0 0 13375 184 0 0 25 0 1 0 1846790604 82874368 19348 4294967295 134512640 135167914 3221224448 3221223200 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 20233 19348 162 162 0 20071 0
[pid=9258] vsize: 80932
Current children cumulated CPU time (s) 137.54
Current children cumulated vsize (Kb) 83060

[startup+150.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 20690 0 0 0 14351 196 0 0 25 0 1 0 1846790604 86421504 20214 4294967295 134512640 135167914 3221224448 3221223200 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 21099 20214 162 162 0 20937 0
[pid=9258] vsize: 84396
Current children cumulated CPU time (s) 147.42
Current children cumulated vsize (Kb) 86524

[startup+160.017 s]
Raw data (loadavg): 1.07 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 21892 0 0 0 15320 209 0 0 25 0 1 0 1846790604 91340800 21416 4294967295 134512640 135167914 3221224448 3221223232 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 22300 21416 162 162 0 22138 0
[pid=9258] vsize: 89200
Current children cumulated CPU time (s) 157.24
Current children cumulated vsize (Kb) 91328

[startup+170.017 s]
Raw data (loadavg): 1.06 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 23007 0 0 0 16292 221 0 0 25 0 1 0 1846790604 95907840 22531 4294967295 134512640 135167914 3221224448 3221223312 134569777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 23415 22531 162 162 0 23253 0
[pid=9258] vsize: 93660
Current children cumulated CPU time (s) 167.08
Current children cumulated vsize (Kb) 95788

[startup+180.018 s]
Raw data (loadavg): 1.05 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 24159 0 0 0 17266 232 0 0 25 0 1 0 1846790604 100626432 23683 4294967295 134512640 135167914 3221224448 3221223016 134846979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 24567 23683 162 162 0 24405 0
[pid=9258] vsize: 98268
Current children cumulated CPU time (s) 176.93
Current children cumulated vsize (Kb) 100396

[startup+190.019 s]
Raw data (loadavg): 1.04 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 25129 0 0 0 18237 243 0 0 25 0 1 0 1846790604 104599552 24653 4294967295 134512640 135167914 3221224448 3221222092 134722208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 25537 24653 162 162 0 25375 0
[pid=9258] vsize: 102148
Current children cumulated CPU time (s) 186.75
Current children cumulated vsize (Kb) 104276

[startup+200.02 s]
Raw data (loadavg): 1.04 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 25832 0 0 0 19213 253 0 0 25 0 1 0 1846790604 107479040 25356 4294967295 134512640 135167914 3221224448 3221222640 134695274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 26240 25356 162 162 0 26078 0
[pid=9258] vsize: 104960
Current children cumulated CPU time (s) 196.61
Current children cumulated vsize (Kb) 107088

[startup+210.02 s]
Raw data (loadavg): 1.03 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) T 9253 9253 20115 0 -1 0 26483 0 0 0 20191 263 0 0 25 0 1 0 1846790604 110145536 26007 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9258/statm): 26891 26007 162 162 0 26729 0
[pid=9258] vsize: 107564
Current children cumulated CPU time (s) 206.49
Current children cumulated vsize (Kb) 109692

[startup+220.021 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 27494 0 0 0 21164 275 0 0 25 0 1 0 1846790604 114286592 27018 4294967295 134512640 135167914 3221224448 3221221888 134849113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 27902 27018 162 162 0 27740 0
[pid=9258] vsize: 111608
Current children cumulated CPU time (s) 216.34
Current children cumulated vsize (Kb) 113736

[startup+230.022 s]
Raw data (loadavg): 1.02 1.00 0.96 1/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) T 9253 9253 20115 0 -1 0 28225 0 0 0 22140 286 0 0 25 0 1 0 1846790604 117280768 27749 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9258/statm): 28633 27749 162 162 0 28471 0
[pid=9258] vsize: 114532
Current children cumulated CPU time (s) 226.21
Current children cumulated vsize (Kb) 116660

[startup+240.022 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 29146 0 0 0 23112 299 0 0 25 0 1 0 1846790604 121053184 28670 4294967295 134512640 135167914 3221224448 3221223408 134578907 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 29554 28670 162 162 0 29392 0
[pid=9258] vsize: 118216
Current children cumulated CPU time (s) 236.06
Current children cumulated vsize (Kb) 120344

[startup+250.023 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 30600 0 0 0 24083 313 0 0 25 0 1 0 1846790604 127008768 30124 4294967295 134512640 135167914 3221224448 3221221856 134694398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 31008 30124 162 162 0 30846 0
[pid=9258] vsize: 124032
Current children cumulated CPU time (s) 245.91
Current children cumulated vsize (Kb) 126160

[startup+260.025 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 31157 0 0 0 25060 324 0 0 25 0 1 0 1846790604 129290240 30681 4294967295 134512640 135167914 3221224448 3221223264 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 31565 30681 162 162 0 31403 0
[pid=9258] vsize: 126260
Current children cumulated CPU time (s) 255.79
Current children cumulated vsize (Kb) 128388

[startup+270.024 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) T 9253 9253 20115 0 -1 0 31854 0 0 0 26035 334 0 0 25 0 1 0 1846790604 132145152 31378 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9258/statm): 32262 31378 162 162 0 32100 0
[pid=9258] vsize: 129048
Current children cumulated CPU time (s) 265.64
Current children cumulated vsize (Kb) 131176

[startup+280.026 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 32643 0 0 0 27012 345 0 0 25 0 1 0 1846790604 135376896 32167 4294967295 134512640 135167914 3221224448 3221222832 134608716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 33051 32167 162 162 0 32889 0
[pid=9258] vsize: 132204
Current children cumulated CPU time (s) 275.52
Current children cumulated vsize (Kb) 134332

[startup+290.027 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 33559 0 0 0 27985 358 0 0 25 0 1 0 1846790604 139128832 33083 4294967295 134512640 135167914 3221224448 3221222764 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 33967 33083 162 162 0 33805 0
[pid=9258] vsize: 135868
Current children cumulated CPU time (s) 285.38
Current children cumulated vsize (Kb) 137996

[startup+300.027 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 34485 0 0 0 28961 369 0 0 25 0 1 0 1846790604 142921728 34009 4294967295 134512640 135167914 3221224448 3221222832 134722521 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 34893 34009 162 162 0 34731 0
[pid=9258] vsize: 139572
Current children cumulated CPU time (s) 295.25
Current children cumulated vsize (Kb) 141700

[startup+310.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 35475 0 0 0 29933 381 0 0 25 0 1 0 1846790604 146972672 34999 4294967295 134512640 135167914 3221224448 3221222760 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 35882 34999 162 162 0 35720 0
[pid=9258] vsize: 143528
Current children cumulated CPU time (s) 305.09
Current children cumulated vsize (Kb) 145656

[startup+320.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 36410 0 0 0 30907 391 0 0 25 0 1 0 1846790604 150802432 35934 4294967295 134512640 135167914 3221224448 3221222100 134522324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 36817 35934 162 162 0 36655 0
[pid=9258] vsize: 147268
Current children cumulated CPU time (s) 314.93
Current children cumulated vsize (Kb) 149396

[startup+330.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 37324 0 0 0 31879 405 0 0 25 0 1 0 1846790604 154546176 36848 4294967295 134512640 135167914 3221224448 3221221888 134847173 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 37731 36848 162 162 0 37569 0
[pid=9258] vsize: 150924
Current children cumulated CPU time (s) 324.79
Current children cumulated vsize (Kb) 153052

[startup+340.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 38280 0 0 0 32854 416 0 0 25 0 1 0 1846790604 158461952 37804 4294967295 134512640 135167914 3221224448 3221222816 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 38687 37804 162 162 0 38525 0
[pid=9258] vsize: 154748
Current children cumulated CPU time (s) 334.65
Current children cumulated vsize (Kb) 156876

[startup+350.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 39099 0 0 0 33829 427 0 0 25 0 1 0 1846790604 161816576 38623 4294967295 134512640 135167914 3221224448 3221223280 134849071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 39506 38623 162 162 0 39344 0
[pid=9258] vsize: 158024
Current children cumulated CPU time (s) 344.51
Current children cumulated vsize (Kb) 160152

[startup+360.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 39819 0 0 0 34803 438 0 0 25 0 1 0 1846790604 164765696 39343 4294967295 134512640 135167914 3221224448 3221221924 134581243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 40226 39343 162 162 0 40064 0
[pid=9258] vsize: 160904
Current children cumulated CPU time (s) 354.36
Current children cumulated vsize (Kb) 163032

[startup+370.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 40499 0 0 0 35779 450 0 0 25 0 1 0 1846790604 167550976 40023 4294967295 134512640 135167914 3221224448 3221223292 134691389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 40906 40023 162 162 0 40744 0
[pid=9258] vsize: 163624
Current children cumulated CPU time (s) 364.24
Current children cumulated vsize (Kb) 165752

[startup+380.036 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 41353 0 0 0 36754 462 0 0 25 0 1 0 1846790604 171048960 40877 4294967295 134512640 135167914 3221224448 3221223016 134846924 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 41760 40877 162 162 0 41598 0
[pid=9258] vsize: 167040
Current children cumulated CPU time (s) 374.11
Current children cumulated vsize (Kb) 169168

[startup+390.037 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 42064 0 0 0 37730 473 0 0 25 0 1 0 1846790604 173961216 41588 4294967295 134512640 135167914 3221224448 3221220764 134722218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 42471 41588 162 162 0 42309 0
[pid=9258] vsize: 169884
Current children cumulated CPU time (s) 383.98
Current children cumulated vsize (Kb) 172012

[startup+400.037 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 42949 0 0 0 38705 484 0 0 25 0 1 0 1846790604 177586176 42473 4294967295 134512640 135167914 3221224448 3221221152 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 43356 42473 162 162 0 43194 0
[pid=9258] vsize: 173424
Current children cumulated CPU time (s) 393.84
Current children cumulated vsize (Kb) 175552

[startup+410.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 44036 0 0 0 39676 495 0 0 25 0 1 0 1846790604 182038528 43560 4294967295 134512640 135167914 3221224448 3221223016 134846907 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 44443 43560 162 162 0 44281 0
[pid=9258] vsize: 177772
Current children cumulated CPU time (s) 403.66
Current children cumulated vsize (Kb) 179900

[startup+420.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 45586 0 0 0 40643 510 0 0 25 0 1 0 1846790604 188387328 45110 4294967295 134512640 135167914 3221224448 3221222764 134849259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 45993 45110 162 162 0 45831 0
[pid=9258] vsize: 183972
Current children cumulated CPU time (s) 413.48
Current children cumulated vsize (Kb) 186100

[startup+430.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 46409 0 0 0 41617 522 0 0 25 0 1 0 1846790604 191758336 45933 4294967295 134512640 135167914 3221224448 3221221776 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 46816 45933 162 162 0 46654 0
[pid=9258] vsize: 187264
Current children cumulated CPU time (s) 423.34
Current children cumulated vsize (Kb) 189392

[startup+440.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 47431 0 0 0 42592 532 0 0 25 0 1 0 1846790604 195944448 46955 4294967295 134512640 135167914 3221224448 3221222876 134722660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 47838 46955 162 162 0 47676 0
[pid=9258] vsize: 191352
Current children cumulated CPU time (s) 433.19
Current children cumulated vsize (Kb) 193480

[startup+450.042 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 48454 0 0 0 43563 544 0 0 25 0 1 0 1846790604 200134656 47978 4294967295 134512640 135167914 3221224448 3221223056 134845219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 48861 47978 162 162 0 48699 0
[pid=9258] vsize: 195444
Current children cumulated CPU time (s) 443.02
Current children cumulated vsize (Kb) 197572

[startup+460.042 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 49510 0 0 0 44536 555 0 0 25 0 1 0 1846790604 204455936 49034 4294967295 134512640 135167914 3221224448 3221222672 134847644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 49916 49034 162 162 0 49754 0
[pid=9258] vsize: 199664
Current children cumulated CPU time (s) 452.86
Current children cumulated vsize (Kb) 201792

[startup+470.042 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 50473 0 0 0 45508 568 0 0 17 0 1 0 1846790604 208400384 49997 4294967295 134512640 135167914 3221224448 3221221240 134611868 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 50879 49997 162 162 0 50717 0
[pid=9258] vsize: 203516
Current children cumulated CPU time (s) 462.71
Current children cumulated vsize (Kb) 205644

[startup+480.043 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 51594 0 0 0 46481 581 0 0 25 0 1 0 1846790604 212992000 51118 4294967295 134512640 135167914 3221224448 3221223232 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 52000 51118 162 162 0 51838 0
[pid=9258] vsize: 208000
Current children cumulated CPU time (s) 472.57
Current children cumulated vsize (Kb) 210128

[startup+490.043 s]
Raw data (loadavg): 1.00 1.00 0.96 1/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) T 9253 9253 20115 0 -1 0 52319 0 0 0 47459 591 0 0 25 0 1 0 1846790604 215961600 51843 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9258/statm): 52725 51843 162 162 0 52563 0
[pid=9258] vsize: 210900
Current children cumulated CPU time (s) 482.45
Current children cumulated vsize (Kb) 213028

[startup+500.045 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 52941 0 0 0 48436 604 0 0 25 0 1 0 1846790604 218509312 52465 4294967295 134512640 135167914 3221224448 3221220776 134611856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 53347 52465 162 162 0 53185 0
[pid=9258] vsize: 213388
Current children cumulated CPU time (s) 492.35
Current children cumulated vsize (Kb) 215516

[startup+510.046 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 53370 0 0 0 49414 615 0 0 25 0 1 0 1846790604 220266496 52894 4294967295 134512640 135167914 3221224448 3221222816 134516649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 53776 52894 162 162 0 53614 0
[pid=9258] vsize: 215104
Current children cumulated CPU time (s) 502.24
Current children cumulated vsize (Kb) 217232

[startup+520.047 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 53985 0 0 0 50393 623 0 0 25 0 1 0 1846790604 222785536 53509 4294967295 134512640 135167914 3221224448 3221222784 134845918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 54391 53509 162 162 0 54229 0
[pid=9258] vsize: 217564
Current children cumulated CPU time (s) 512.11
Current children cumulated vsize (Kb) 219692

[startup+530.047 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 54687 0 0 0 51370 635 0 0 25 0 1 0 1846790604 225660928 54211 4294967295 134512640 135167914 3221224448 3221223264 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 55093 54211 162 162 0 54931 0
[pid=9258] vsize: 220372
Current children cumulated CPU time (s) 522
Current children cumulated vsize (Kb) 222500

[startup+540.048 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 55343 0 0 0 52342 647 0 0 25 0 1 0 1846790604 228347904 54867 4294967295 134512640 135167914 3221224448 3221221296 134849110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 55749 54867 162 162 0 55587 0
[pid=9258] vsize: 222996
Current children cumulated CPU time (s) 531.84
Current children cumulated vsize (Kb) 225124

[startup+550.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 55858 0 0 0 53319 657 0 0 25 0 1 0 1846790604 230457344 55382 4294967295 134512640 135167914 3221224448 3221223208 134697560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 56264 55382 162 162 0 56102 0
[pid=9258] vsize: 225056
Current children cumulated CPU time (s) 541.71
Current children cumulated vsize (Kb) 227184

[startup+560.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 56840 0 0 0 54296 668 0 0 25 0 1 0 1846790604 234479616 56364 4294967295 134512640 135167914 3221224448 3221222764 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 57246 56364 162 162 0 57084 0
[pid=9258] vsize: 228984
Current children cumulated CPU time (s) 551.59
Current children cumulated vsize (Kb) 231112

[startup+570.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 57483 0 0 0 55275 678 0 0 25 0 1 0 1846790604 237113344 57007 4294967295 134512640 135167914 3221224448 3221221856 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 57889 57007 162 162 0 57727 0
[pid=9258] vsize: 231556
Current children cumulated CPU time (s) 561.48
Current children cumulated vsize (Kb) 233684

[startup+580.051 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 58110 0 0 0 56252 689 0 0 25 0 1 0 1846790604 239681536 57634 4294967295 134512640 135167914 3221224448 3221223296 134569635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 58516 57634 162 162 0 58354 0
[pid=9258] vsize: 234064
Current children cumulated CPU time (s) 571.36
Current children cumulated vsize (Kb) 236192

[startup+590.053 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 58685 0 0 0 57229 698 0 0 25 0 1 0 1846790604 242036736 58209 4294967295 134512640 135167914 3221224448 3221222704 134845099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 59091 58209 162 162 0 58929 0
[pid=9258] vsize: 236364
Current children cumulated CPU time (s) 581.22
Current children cumulated vsize (Kb) 238492

[startup+600.054 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 59215 0 0 0 58208 707 0 0 25 0 1 0 1846790604 244207616 58739 4294967295 134512640 135167914 3221224448 3221223200 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 59621 58739 162 162 0 59459 0
[pid=9258] vsize: 238484
Current children cumulated CPU time (s) 591.1
Current children cumulated vsize (Kb) 240612

[startup+610.055 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 59773 0 0 0 59187 717 0 0 25 0 1 0 1846790604 246493184 59297 4294967295 134512640 135167914 3221224448 3221221056 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 60179 59297 162 162 0 60017 0
[pid=9258] vsize: 240716
Current children cumulated CPU time (s) 600.99
Current children cumulated vsize (Kb) 242844

[startup+620.055 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 60532 0 0 0 60164 729 0 0 25 0 1 0 1846790604 249602048 60056 4294967295 134512640 135167914 3221224448 3221222784 134696442 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 60938 60056 162 162 0 60776 0
[pid=9258] vsize: 243752
Current children cumulated CPU time (s) 610.88
Current children cumulated vsize (Kb) 245880

[startup+630.056 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 61295 0 0 0 61141 739 0 0 25 0 1 0 1846790604 252727296 60819 4294967295 134512640 135167914 3221224448 3221220608 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 61701 60819 162 162 0 61539 0
[pid=9258] vsize: 246804
Current children cumulated CPU time (s) 620.75
Current children cumulated vsize (Kb) 248932

[startup+640.057 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 62014 0 0 0 62115 752 0 0 25 0 1 0 1846790604 255672320 61538 4294967295 134512640 135167914 3221224448 3221223264 134694495 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 62420 61538 162 162 0 62258 0
[pid=9258] vsize: 249680
Current children cumulated CPU time (s) 630.62
Current children cumulated vsize (Kb) 251808

[startup+650.058 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 62568 0 0 0 63092 763 0 0 25 0 1 0 1846790604 257941504 62092 4294967295 134512640 135167914 3221224448 3221223232 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 62974 62092 162 162 0 62812 0
[pid=9258] vsize: 251896
Current children cumulated CPU time (s) 640.5
Current children cumulated vsize (Kb) 254024

[startup+660.059 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 63067 0 0 0 64070 771 0 0 25 0 1 0 1846790604 259985408 62591 4294967295 134512640 135167914 3221224448 3221221456 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 63473 62591 162 162 0 63311 0
[pid=9258] vsize: 253892
Current children cumulated CPU time (s) 650.36
Current children cumulated vsize (Kb) 256020

[startup+670.06 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 63697 0 0 0 65045 784 0 0 25 0 1 0 1846790604 262565888 63221 4294967295 134512640 135167914 3221224448 3221223296 134569657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 64103 63221 162 162 0 63941 0
[pid=9258] vsize: 256412
Current children cumulated CPU time (s) 660.24
Current children cumulated vsize (Kb) 258540

[startup+680.062 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 64325 0 0 0 66020 796 0 0 25 0 1 0 1846790604 265199616 63849 4294967295 134512640 135167914 3221224448 3221223280 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 64746 63849 162 162 0 64584 0
[pid=9258] vsize: 258984
Current children cumulated CPU time (s) 670.11
Current children cumulated vsize (Kb) 261112

[startup+690.062 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 64837 0 0 0 66996 806 0 0 25 0 1 0 1846790604 267296768 64361 4294967295 134512640 135167914 3221224448 3221221872 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 65258 64361 162 162 0 65096 0
[pid=9258] vsize: 261032
Current children cumulated CPU time (s) 679.97
Current children cumulated vsize (Kb) 263160

[startup+700.063 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 65554 0 0 0 67973 818 0 0 25 0 1 0 1846790604 270233600 65078 4294967295 134512640 135167914 3221224448 3221223200 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 65975 65078 162 162 0 65813 0
[pid=9258] vsize: 263900
Current children cumulated CPU time (s) 689.86
Current children cumulated vsize (Kb) 266028

[startup+710.064 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 66162 0 0 0 68950 829 0 0 25 0 1 0 1846790604 272723968 65686 4294967295 134512640 135167914 3221224448 3221223264 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 66583 65686 162 162 0 66421 0
[pid=9258] vsize: 266332
Current children cumulated CPU time (s) 699.74
Current children cumulated vsize (Kb) 268460

[startup+720.064 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 66652 0 0 0 69927 839 0 0 25 0 1 0 1846790604 274731008 66176 4294967295 134512640 135167914 3221224448 3221223280 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 67073 66176 162 162 0 66911 0
[pid=9258] vsize: 268292
Current children cumulated CPU time (s) 709.61
Current children cumulated vsize (Kb) 270420

[startup+730.065 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 67153 0 0 0 70903 851 0 0 25 0 1 0 1846790604 276783104 66677 4294967295 134512640 135167914 3221224448 3221222428 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 67574 66677 162 162 0 67412 0
[pid=9258] vsize: 270296
Current children cumulated CPU time (s) 719.49
Current children cumulated vsize (Kb) 272424

[startup+740.066 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 67674 0 0 0 71880 860 0 0 25 0 1 0 1846790604 278917120 67198 4294967295 134512640 135167914 3221224448 3221222696 134522321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 68095 67198 162 162 0 67933 0
[pid=9258] vsize: 272380
Current children cumulated CPU time (s) 729.35
Current children cumulated vsize (Kb) 274508

[startup+750.067 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 68225 0 0 0 72859 870 0 0 25 0 1 0 1846790604 281174016 67749 4294967295 134512640 135167914 3221224448 3221223184 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 68646 67749 162 162 0 68484 0
[pid=9258] vsize: 274584
Current children cumulated CPU time (s) 739.24
Current children cumulated vsize (Kb) 276712

[startup+760.068 s]
Raw data (loadavg): 1.00 1.00 0.96 1/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) T 9253 9253 20115 0 -1 0 68834 0 0 0 73834 881 0 0 25 0 1 0 1846790604 283668480 68358 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9258/statm): 69255 68358 162 162 0 69093 0
[pid=9258] vsize: 277020
Current children cumulated CPU time (s) 749.1
Current children cumulated vsize (Kb) 279148

[startup+770.068 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 69462 0 0 0 74810 891 0 0 25 0 1 0 1846790604 286240768 68986 4294967295 134512640 135167914 3221224448 3221222460 134722542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 69883 68986 162 162 0 69721 0
[pid=9258] vsize: 279532
Current children cumulated CPU time (s) 758.96
Current children cumulated vsize (Kb) 281660

[startup+780.068 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 70102 0 0 0 75788 901 0 0 25 0 1 0 1846790604 288862208 69626 4294967295 134512640 135167914 3221224448 3221222736 134843412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 70523 69626 162 162 0 70361 0
[pid=9258] vsize: 282092
Current children cumulated CPU time (s) 768.84
Current children cumulated vsize (Kb) 284220

[startup+790.069 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 70644 0 0 0 76765 912 0 0 25 0 1 0 1846790604 291082240 70168 4294967295 134512640 135167914 3221224448 3221223180 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 71065 70168 162 162 0 70903 0
[pid=9258] vsize: 284260
Current children cumulated CPU time (s) 778.72
Current children cumulated vsize (Kb) 286388

[startup+800.071 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 71240 0 0 0 77743 923 0 0 25 0 1 0 1846790604 293523456 70764 4294967295 134512640 135167914 3221224448 3221223216 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 71661 70764 162 162 0 71499 0
[pid=9258] vsize: 286644
Current children cumulated CPU time (s) 788.61
Current children cumulated vsize (Kb) 288772

[startup+810.071 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 71750 0 0 0 78720 933 0 0 25 0 1 0 1846790604 295612416 71274 4294967295 134512640 135167914 3221224448 3221222832 134691254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 72171 71274 162 162 0 72009 0
[pid=9258] vsize: 288684
Current children cumulated CPU time (s) 798.48
Current children cumulated vsize (Kb) 290812

[startup+820.072 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 72205 0 0 0 79698 943 0 0 25 0 1 0 1846790604 297476096 71729 4294967295 134512640 135167914 3221224448 3221223292 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 72626 71729 162 162 0 72464 0
[pid=9258] vsize: 290504
Current children cumulated CPU time (s) 808.36
Current children cumulated vsize (Kb) 292632

[startup+830.073 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) T 9253 9253 20115 0 -1 0 72723 0 0 0 80675 953 0 0 25 0 1 0 1846790604 299597824 72247 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9258/statm): 73144 72247 162 162 0 72982 0
[pid=9258] vsize: 292576
Current children cumulated CPU time (s) 818.23
Current children cumulated vsize (Kb) 294704

[startup+840.073 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 73280 0 0 0 81650 965 0 0 25 0 1 0 1846790604 301879296 72804 4294967295 134512640 135167914 3221224448 3221222656 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 73701 72804 162 162 0 73539 0
[pid=9258] vsize: 294804
Current children cumulated CPU time (s) 828.1
Current children cumulated vsize (Kb) 296932

[startup+850.074 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 73759 0 0 0 82627 975 0 0 25 0 1 0 1846790604 303841280 73283 4294967295 134512640 135167914 3221224448 3221222672 134847370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 74180 73283 162 162 0 74018 0
[pid=9258] vsize: 296720
Current children cumulated CPU time (s) 837.97
Current children cumulated vsize (Kb) 298848

[startup+860.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 74510 0 0 0 83604 985 0 0 25 0 1 0 1846790604 306917376 74034 4294967295 134512640 135167914 3221224448 3221223216 134694594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 74931 74034 162 162 0 74769 0
[pid=9258] vsize: 299724
Current children cumulated CPU time (s) 847.84
Current children cumulated vsize (Kb) 301852

[startup+870.077 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 75632 0 0 0 84574 998 0 0 25 0 1 0 1846790604 311513088 75156 4294967295 134512640 135167914 3221224448 3221223200 134844691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 76053 75156 162 162 0 75891 0
[pid=9258] vsize: 304212
Current children cumulated CPU time (s) 857.67
Current children cumulated vsize (Kb) 306340

[startup+880.077 s]
Raw data (loadavg): 1.00 1.00 0.96 1/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) T 9253 9253 20115 0 -1 0 76333 0 0 0 85550 1010 0 0 25 0 1 0 1846790604 314384384 75857 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9258/statm): 76754 75857 162 162 0 76592 0
[pid=9258] vsize: 307016
Current children cumulated CPU time (s) 867.55
Current children cumulated vsize (Kb) 309144

[startup+890.078 s]
Raw data (loadavg): 1.00 1.00 0.96 1/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) T 9253 9253 20115 0 -1 0 76848 0 0 0 86528 1019 0 0 25 0 1 0 1846790604 316493824 76372 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9258/statm): 77269 76372 162 162 0 77107 0
[pid=9258] vsize: 309076
Current children cumulated CPU time (s) 877.42
Current children cumulated vsize (Kb) 311204

[startup+900.079 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 77256 0 0 0 87506 1028 0 0 25 0 1 0 1846790604 318164992 76780 4294967295 134512640 135167914 3221224448 3221223232 134722527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 77677 76780 162 162 0 77515 0
[pid=9258] vsize: 310708
Current children cumulated CPU time (s) 887.29
Current children cumulated vsize (Kb) 312836

[startup+910.079 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 77754 0 0 0 88484 1039 0 0 25 0 1 0 1846790604 320200704 77278 4294967295 134512640 135167914 3221224448 3221223252 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 78174 77278 162 162 0 78012 0
[pid=9258] vsize: 312696
Current children cumulated CPU time (s) 897.18
Current children cumulated vsize (Kb) 314824

[startup+920.08 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 78298 0 0 0 89458 1050 0 0 25 0 1 0 1846790604 322428928 77822 4294967295 134512640 135167914 3221224448 3221223232 134691401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 78718 77822 162 162 0 78556 0
[pid=9258] vsize: 314872
Current children cumulated CPU time (s) 907.03
Current children cumulated vsize (Kb) 317000

[startup+930.082 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 79964 0 0 0 90428 1064 0 0 25 0 1 0 1846790604 329252864 79488 4294967295 134512640 135167914 3221224448 3221220880 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 80384 79488 162 162 0 80222 0
[pid=9258] vsize: 321536
Current children cumulated CPU time (s) 916.87
Current children cumulated vsize (Kb) 323664

[startup+940.082 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 81535 0 0 0 91390 1082 0 0 25 0 1 0 1846790604 335613952 81059 4294967295 134512640 135167914 3221224448 3221222752 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 81937 81059 162 162 0 81775 0
[pid=9258] vsize: 327748
Current children cumulated CPU time (s) 926.67
Current children cumulated vsize (Kb) 329876

[startup+950.083 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 83064 0 0 0 92342 1104 0 0 25 0 1 0 1846790604 341540864 82588 4294967295 134512640 135167914 3221224448 3221222872 134693609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 83384 82588 162 162 0 83222 0
[pid=9258] vsize: 333536
Current children cumulated CPU time (s) 936.41
Current children cumulated vsize (Kb) 335664

[startup+960.084 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 85142 0 0 0 93304 1119 0 0 25 0 1 0 1846790604 349945856 84666 4294967295 134512640 135167914 3221224448 3221223136 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 85436 84666 162 162 0 85274 0
[pid=9258] vsize: 341744
Current children cumulated CPU time (s) 946.18
Current children cumulated vsize (Kb) 343872

[startup+970.083 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91217 0 0 0 94254 1145 0 0 25 0 1 0 1846790604 374759424 90741 4294967295 134512640 135167914 3221224448 3221223216 134691286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 91494 90741 162 162 0 91332 0
[pid=9258] vsize: 365976
Current children cumulated CPU time (s) 955.94
Current children cumulated vsize (Kb) 368104

[startup+980.085 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91217 0 0 0 95253 1146 0 0 25 0 1 0 1846790604 374759424 90741 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 91494 90741 162 162 0 91332 0
[pid=9258] vsize: 365976
Current children cumulated CPU time (s) 965.94
Current children cumulated vsize (Kb) 368104

[startup+990.086 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91217 0 0 0 96253 1146 0 0 25 0 1 0 1846790604 374759424 90741 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 91494 90741 162 162 0 91332 0
[pid=9258] vsize: 365976
Current children cumulated CPU time (s) 975.94
Current children cumulated vsize (Kb) 368104

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 97253 1147 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210112 134844697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 985.95
Current children cumulated vsize (Kb) 366104

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 98252 1147 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210876 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 995.94
Current children cumulated vsize (Kb) 366104

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 99252 1147 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210480 134696587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1005.94
Current children cumulated vsize (Kb) 366104

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 100253 1147 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210704 134522732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1015.95
Current children cumulated vsize (Kb) 366104

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 101252 1147 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210672 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1025.94
Current children cumulated vsize (Kb) 366104

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 102252 1148 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211056 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1035.95
Current children cumulated vsize (Kb) 366104

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 103252 1148 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211552 134849068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1045.95
Current children cumulated vsize (Kb) 366104

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 104252 1148 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211168 134843068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1055.95
Current children cumulated vsize (Kb) 366104

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 105251 1149 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210816 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1065.95
Current children cumulated vsize (Kb) 366104

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 106251 1149 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210992 134843139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1075.95
Current children cumulated vsize (Kb) 366104

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 107251 1149 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210728 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1085.95
Current children cumulated vsize (Kb) 366104

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 108251 1150 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211404 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1095.96
Current children cumulated vsize (Kb) 366104

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 109251 1150 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211536 134843001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1105.96
Current children cumulated vsize (Kb) 366104

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 110251 1150 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210752 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1115.96
Current children cumulated vsize (Kb) 366104

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 111251 1150 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211536 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1125.96
Current children cumulated vsize (Kb) 366104

[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 112251 1150 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211560 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1135.96
Current children cumulated vsize (Kb) 366104

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 113250 1150 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211036 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1145.95
Current children cumulated vsize (Kb) 366104

[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 114250 1151 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211312 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1155.96
Current children cumulated vsize (Kb) 366104

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 115249 1152 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221212316 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1165.96
Current children cumulated vsize (Kb) 366104

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 116249 1152 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211616 134630875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1175.96
Current children cumulated vsize (Kb) 366104

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 117249 1153 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221210816 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1185.97
Current children cumulated vsize (Kb) 366104

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 118249 1153 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211936 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1195.97
Current children cumulated vsize (Kb) 366104

[startup+1220.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 119249 1153 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211760 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1205.97
Current children cumulated vsize (Kb) 366104



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1220.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 9258
Raw data (/proc/9253/stat): 9253 (minisat+_script) S 9252 9253 20115 0 -1 0 314 5602 0 0 0 1 167 27 19 0 1 0 1846790383 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9253/statm): 532 234 485 147 0 385 0
[pid=9253] vsize: 2128
Raw data (/proc/9258/stat): 9258 (minisat+_bignum) R 9253 9253 20115 0 -1 0 91312 0 0 0 119249 1153 0 0 25 0 1 0 1846790604 372711424 90288 4294967295 134512640 135167914 3221224448 3221211776 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9258/statm): 90994 90288 162 162 0 90832 0
[pid=9258] vsize: 363976
Current children cumulated CPU time (s) 1205.97
Current children cumulated vsize (Kb) 366104

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

Child status: 0
Real time (s): 1220.28
CPU time (s): 1204.2
CPU user time (s): 1192.49
CPU system time (s): 11.7042
CPU usage (%): 98.6825
Max. virtual memory (cumulated for all children) (Kb): 368104

Verifier Data

ERROR: no interpretation found !