Some explanations

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

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/lptestset/fome/normalized-mps-v2-13-7-fome11.opb
MD5SUM6ffc5f91e7ad7c6593868bb0012c33e4
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 249428
Biggest coefficient in the objective function 2100440996511744
Number of bits for the biggest coefficient in the objective function 51
Sum of the numbers in the objective function 1724124944012305800
Number of bits of the sum of numbers in the objective function 61
Biggest number in a constraint 52428800000000000
Number of bits of the biggest number in a constraint 56
Biggest sum of numbers in a constraint 4176904799999651840
Number of bits of the biggest sum of numbers62
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables488988
Total number of constraints12168
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints12168
Minimum length of a constraint10
Maximum length of a constraint4560

Trace number 6261

Launcher Data

LAUNCH ON wulflinc17 THE 2005-09-20 05:07:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3437 boxname=wulflinc17 idbench=1093 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6ffc5f91e7ad7c6593868bb0012c33e4  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-fome11.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-fome11.opb
IDLAUNCH: 3437
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        865820 kB
Buffers:         18124 kB
Cached:         122160 kB
SwapCached:        612 kB
Active:          65484 kB
Inactive:        77332 kB
HighTotal:      131008 kB
HighFree:         9184 kB
LowTotal:       903652 kB
LowFree:        856636 kB
SwapTotal:     2097892 kB
SwapFree:      2096676 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            20340 kB
Committed_AS:    64316 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:18:47 (client local time) WITH STATUS 139 IN 646.359 SECONDS
stats: 3437 7 646.359 139

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 24464] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 24310 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssss
c ---[24312]---> BDD-cost:   12
c ---[24311]---> BDD-cost:   10
c ---[24310]---> BDD-cost:    9
c ---[24309]---> BDD-cost:   13
c ---[24307]---> BDD-cost:   11
c ---[24306]---> BDD-cost:   11
c ---[24305]---> BDD-cost:   12
c ---[24304]---> BDD-cost:   11
c ---[24303]---> BDD-cost:    9
c ---[24302]---> BDD-cost:   12
c ---[24301]---> BDD-cost:   11
c ---[24299]---> BDD-cost:   12
c ---[24298]---> BDD-cost:   10
c ---[24297]---> BDD-cost:    9
c ---[24296]---> BDD-cost:   13
c ---[24294]---> BDD-cost:   11
c ---[24293]---> BDD-cost:   11
c ---[24292]---> BDD-cost:   12
c ---[24291]---> BDD-cost:   11
c ---[24290]---> BDD-cost:    9
c ---[24289]---> BDD-cost:   12
c ---[24288]---> BDD-cost:   11
c ---[24286]---> BDD-cost:   96
c ---[24284]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24282]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[24280]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24278]---> BDD-cost:  126
c ---[24276]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[24274]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24272]---> BDD-cost:  126
c ---[24270]---> Adder-cost: 454   maxlim: 2097534   bits: 23/22
c ---[24268]---> BDD-cost:  126
c ---[24266]---> BDD-cost:  126
c ---[24264]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24262]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24260]---> Sorter-cost:  640     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24258]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24256]---> BDD-cost:   96
c ---[24254]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24252]---> BDD-cost:   99
c ---[24250]---> Sorter-cost: 1420     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24248]---> BDD-cost:  126
c ---[24246]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24244]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24242]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24240]---> BDD-cost:  126
c ---[24238]---> Sorter-cost:  564     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24236]---> Sorter-cost: 2008     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24234]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[24232]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24230]---> Sorter-cost:  609     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24228]---> BDD-cost:  126
c ---[24226]---> BDD-cost:  128
c ---[24224]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24222]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24220]---> Sorter-cost:  846     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24218]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24216]---> BDD-cost:  119
c ---[24214]---> BDD-cost:  104
c ---[24212]---> Adder-cost: 346   maxlim: 1048830   bits: 22/21
c ---[24210]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24208]---> Sorter-cost: 1342     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24206]---> BDD-cost:   99
c ---[24204]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24202]---> Adder-cost: 786   maxlim: 7348198   bits: 24/23
c ---[24200]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24198]---> Sorter-cost: 2365     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24196]---> BDD-cost:  104
c ---[24194]---> Sorter-cost:  410     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24192]---> Sorter-cost: 3161     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24190]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24188]---> BDD-cost:  126
c ---[24186]---> BDD-cost:  126
c ---[24184]---> BDD-cost:  154
c ---[24182]---> BDD-cost:  126
c ---[24180]---> Sorter-cost:  646     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24178]---> Sorter-cost: 2300     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24176]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24174]---> BDD-cost:  126
c ---[24172]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24170]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2
c ---[24168]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24166]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24164]---> BDD-cost:   96
c ---[24162]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24160]---> Sorter-cost: 1503     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24158]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24156]---> Sorter-cost: 1142     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24154]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24152]---> BDD-cost:  126
c ---[24150]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24148]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24146]---> BDD-cost:  126
c ---[24144]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24142]---> BDD-cost:  126
c ---[24140]---> Sorter-cost:  650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24138]---> BDD-cost:  172
c ---[24136]---> BDD-cost:  128
c ---[24134]---> Sorter-cost: 2825     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24132]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2
c ---[24130]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[24128]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24126]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[24124]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24122]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[24120]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24118]---> BDD-cost:  172
c ---[24116]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24114]---> BDD-cost:  128
c ---[24112]---> Sorter-cost:  741     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24110]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24108]---> BDD-cost:   99
c ---[24106]---> Sorter-cost: 1239     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24104]---> BDD-cost:  126
c ---[24102]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24100]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24098]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[24096]---> Sorter-cost:  846     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24094]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24092]---> Sorter-cost: 1703     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24090]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24088]---> BDD-cost:  128
c ---[24086]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24084]---> BDD-cost:  158
c ---[24082]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24080]---> Sorter-cost: 2148     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24078]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24076]---> BDD-cost:  126
c ---[24074]---> BDD-cost:  126
c ---[24072]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24070]---> Sorter-cost: 1138     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24068]---> Sorter-cost:  561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24066]---> BDD-cost:  128
c ---[24064]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24062]---> Sorter-cost: 2226     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24060]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24058]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[24056]---> Sorter-cost: 1112     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24054]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24052]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24050]---> Adder-cost: 286   maxlim: 556919   bits: 20/20
c ---[24048]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24046]---> Sorter-cost: 2341     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24044]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24042]---> BDD-cost:  121
c ---[24040]---> BDD-cost:  126
c ---[24038]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24036]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24034]---> Sorter-cost: 1751     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24032]---> Sorter-cost: 1026     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24030]---> BDD-cost:  126
c ---[24028]---> Sorter-cost: 2086     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24026]---> Sorter-cost: 1574     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24024]---> BDD-cost:  172
c ---[24022]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24020]---> Sorter-cost: 2246     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24018]---> Sorter-cost:  832     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24016]---> BDD-cost:  150
c ---[24014]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2
c ---[24012]---> BDD-cost:   96
c ---[24010]---> Sorter-cost: 1197     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24008]---> BDD-cost:   96
c ---[24006]---> Adder-cost: 474   maxlim: 3260410   bits: 23/22
c ---[24004]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24002]---> Sorter-cost:  349     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[24000]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2
c ---[23998]---> Sorter-cost:  454     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[23996]---> BDD-cost:  123
c ---[23994]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[23992]---> Sorter-cost: 2307     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[23990]---> Sorter-cost: 1751     Base: 2 2 2 2 2 2 /oldhome/oroussel/solvers/minisat+_script: line 16:  7261 Segmentation fault      $XDIR/minisat+_bignum_static* "$@"

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/7256/stat): 7256 (minisat+_script) R 7255 7256 19316 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855919316 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7256/statm): 174 9 169 147 0 27 0
[pid=7256] 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=7257
New process pid=7258
New process pid=7259
execve syscall for /bin/sed executable
One traced child (pid=7258) 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=7259) exited with status: 0
One traced child (pid=7257) exited with status: 0
New process pid=7260
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-fome11.opb
One traced child (pid=7260) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=7261
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-fome11.opb

[startup+10.0045 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 12918 0 0 0 866 60 0 0 25 0 1 0 1855919330 50110464 11796 4294967295 134512640 135167914 3221224448 3221222784 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 12234 11796 162 162 0 12072 0
[pid=7261] vsize: 48936
Current children cumulated CPU time (s) 9.32
Current children cumulated vsize (Kb) 51064

[startup+20.0051 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 14806 0 0 0 1844 71 0 0 25 0 1 0 1855919330 74682368 13615 4294967295 134512640 135167914 3221224448 3221221280 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 18233 13616 162 162 0 18071 0
[pid=7261] vsize: 72932
Current children cumulated CPU time (s) 19.21
Current children cumulated vsize (Kb) 75060

[startup+30.0047 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 18129 0 0 0 2804 91 0 0 25 0 1 0 1855919330 86614016 16938 4294967295 134512640 135167914 3221224448 3221222896 134591265 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7261/statm): 21146 16938 162 162 0 20984 0
[pid=7261] vsize: 84584
Current children cumulated CPU time (s) 29.01
Current children cumulated vsize (Kb) 86712

[startup+40.0063 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 21457 0 0 0 3766 109 0 0 25 0 1 0 1855919330 98791424 20208 4294967295 134512640 135167914 3221224448 3221222108 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 24119 20208 162 162 0 23957 0
[pid=7261] vsize: 96476
Current children cumulated CPU time (s) 38.81
Current children cumulated vsize (Kb) 98604

[startup+50.0069 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 25908 0 0 0 4726 128 0 0 25 0 1 0 1855919330 113065984 23901 4294967295 134512640 135167914 3221224448 3221222912 134586989 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 27604 23901 162 162 0 27442 0
[pid=7261] vsize: 110416
Current children cumulated CPU time (s) 48.6
Current children cumulated vsize (Kb) 112544

[startup+60.0075 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 29061 0 0 0 5691 144 0 0 25 0 1 0 1855919330 124952576 26984 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 30506 26984 162 162 0 30344 0
[pid=7261] vsize: 122024
Current children cumulated CPU time (s) 58.41
Current children cumulated vsize (Kb) 124152

[startup+70.0081 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 32093 0 0 0 6648 163 0 0 25 0 1 0 1855919330 136839168 30016 4294967295 134512640 135167914 3221224448 3221223152 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 33408 30016 162 162 0 33246 0
[pid=7261] vsize: 133632
Current children cumulated CPU time (s) 68.17
Current children cumulated vsize (Kb) 135760

[startup+80.0087 s]
Raw data (loadavg): 0.98 0.97 0.99 1/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 35180 0 0 0 7613 179 0 0 25 0 1 0 1855919330 148623360 33103 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 36285 33103 162 162 0 36123 0
[pid=7261] vsize: 145140
Current children cumulated CPU time (s) 77.98
Current children cumulated vsize (Kb) 147268

[startup+90.0093 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 38675 0 0 0 8573 197 0 0 25 0 1 0 1855919330 160899072 36537 4294967295 134512640 135167914 3221224448 3221221872 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 39282 36538 162 162 0 39120 0
[pid=7261] vsize: 157128
Current children cumulated CPU time (s) 87.76
Current children cumulated vsize (Kb) 159256

[startup+100.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 42110 0 0 0 9531 218 0 0 25 0 1 0 1855919330 173314048 39972 4294967295 134512640 135167914 3221224448 3221222240 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 42313 39972 162 162 0 42151 0
[pid=7261] vsize: 169252
Current children cumulated CPU time (s) 97.55
Current children cumulated vsize (Kb) 171380

[startup+110.011 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 45539 0 0 0 10492 235 0 0 25 0 1 0 1855919330 185532416 43241 4294967295 134512640 135167914 3221224448 3221221928 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 45296 43241 162 162 0 45134 0
[pid=7261] vsize: 181184
Current children cumulated CPU time (s) 107.33
Current children cumulated vsize (Kb) 183312

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 48761 0 0 0 11455 251 0 0 25 0 1 0 1855919330 197410816 46363 4294967295 134512640 135167914 3221224448 3221221556 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 48196 46363 162 162 0 48034 0
[pid=7261] vsize: 192784
Current children cumulated CPU time (s) 117.12
Current children cumulated vsize (Kb) 194912

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 51884 0 0 0 12416 268 0 0 25 0 1 0 1855919330 209186816 49415 4294967295 134512640 135167914 3221224448 3221223152 134607966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 51071 49415 162 162 0 50909 0
[pid=7261] vsize: 204284
Current children cumulated CPU time (s) 126.9
Current children cumulated vsize (Kb) 206412

[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 54902 0 0 0 13375 287 0 0 25 0 1 0 1855919330 221028352 52433 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 53962 52433 162 162 0 53800 0
[pid=7261] vsize: 215848
Current children cumulated CPU time (s) 136.68
Current children cumulated vsize (Kb) 217976

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63700 0 0 0 14304 323 0 0 25 0 1 0 1855919330 256786432 61231 4294967295 134512640 135167914 3221224448 3221223184 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 62692 61231 162 162 0 62530 0
[pid=7261] vsize: 250768
Current children cumulated CPU time (s) 146.33
Current children cumulated vsize (Kb) 252896

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63702 0 0 0 15304 323 0 0 25 0 1 0 1855919330 256790528 61233 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 62693 61233 162 162 0 62531 0
[pid=7261] vsize: 250772
Current children cumulated CPU time (s) 156.33
Current children cumulated vsize (Kb) 252900

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63705 0 0 0 16304 323 0 0 25 0 1 0 1855919330 256794624 61236 4294967295 134512640 135167914 3221224448 3221223216 134691286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 62694 61236 162 162 0 62532 0
[pid=7261] vsize: 250776
Current children cumulated CPU time (s) 166.33
Current children cumulated vsize (Kb) 252904

[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63708 0 0 0 17304 323 0 0 25 0 1 0 1855919330 256798720 61239 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 62695 61239 162 162 0 62533 0
[pid=7261] vsize: 250780
Current children cumulated CPU time (s) 176.33
Current children cumulated vsize (Kb) 252908

[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63718 0 0 0 18304 323 0 0 25 0 1 0 1855919330 256811008 61249 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 62698 61249 162 162 0 62536 0
[pid=7261] vsize: 250792
Current children cumulated CPU time (s) 186.33
Current children cumulated vsize (Kb) 252920

[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 63758 0 0 0 19303 324 0 0 25 0 1 0 1855919330 245166080 58423 4294967295 134512640 135167914 3221224448 3221220736 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 59855 58423 162 162 0 59693 0
[pid=7261] vsize: 239420
Current children cumulated CPU time (s) 196.33
Current children cumulated vsize (Kb) 241548

[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 64429 0 0 0 20301 326 0 0 25 0 1 0 1855919330 247914496 59094 4294967295 134512640 135167914 3221224448 3221102044 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 60526 59094 162 162 0 60364 0
[pid=7261] vsize: 242104
Current children cumulated CPU time (s) 206.33
Current children cumulated vsize (Kb) 244232

[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 67752 0 0 0 21275 338 0 0 25 0 1 0 1855919330 258826240 61758 4294967295 134512640 135167914 3221224448 3221092896 134847164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 63190 61758 162 162 0 63028 0
[pid=7261] vsize: 252760
Current children cumulated CPU time (s) 216.19
Current children cumulated vsize (Kb) 254888

[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 70703 0 0 0 22249 350 0 0 25 0 1 0 1855919330 270913536 64709 4294967295 134512640 135167914 3221224448 3221095196 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 66141 64709 162 162 0 65979 0
[pid=7261] vsize: 264564
Current children cumulated CPU time (s) 226.05
Current children cumulated vsize (Kb) 266692

[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 75873 0 0 0 23216 368 0 0 25 0 1 0 1855919330 286691328 68561 4294967295 134512640 135167914 3221224448 3221105904 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 69993 68561 162 162 0 69831 0
[pid=7261] vsize: 279972
Current children cumulated CPU time (s) 235.9
Current children cumulated vsize (Kb) 282100

[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 78907 0 0 0 24187 379 0 0 25 0 1 0 1855919330 299118592 71595 4294967295 134512640 135167914 3221224448 3221104432 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 73027 71595 162 162 0 72865 0
[pid=7261] vsize: 292108
Current children cumulated CPU time (s) 245.72
Current children cumulated vsize (Kb) 294236

[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 81528 0 0 0 25159 392 0 0 25 0 1 0 1855919330 309854208 74216 4294967295 134512640 135167914 3221224448 3221106144 134844697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7261/statm): 75648 74216 162 162 0 75486 0
[pid=7261] vsize: 302592
Current children cumulated CPU time (s) 255.57
Current children cumulated vsize (Kb) 304720

[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.99 1/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 89058 0 0 0 26121 415 0 0 25 0 1 0 1855919330 329895936 79109 4294967295 134512640 135167914 3221224448 3221107884 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 80541 79109 162 162 0 80379 0
[pid=7261] vsize: 322164
Current children cumulated CPU time (s) 265.42
Current children cumulated vsize (Kb) 324292

[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 91793 0 0 0 27092 427 0 0 25 0 1 0 1855919330 341098496 81844 4294967295 134512640 135167914 3221224448 3221108240 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 83276 81844 162 162 0 83114 0
[pid=7261] vsize: 333104
Current children cumulated CPU time (s) 275.25
Current children cumulated vsize (Kb) 335232

[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 94866 0 0 0 28058 442 0 0 25 0 1 0 1855919330 353685504 84917 4294967295 134512640 135167914 3221224448 3221108860 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 86349 84917 162 162 0 86187 0
[pid=7261] vsize: 345396
Current children cumulated CPU time (s) 285.06
Current children cumulated vsize (Kb) 347524

[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 98160 0 0 0 29022 457 0 0 25 0 1 0 1855919330 367177728 88211 4294967295 134512640 135167914 3221224448 3221106012 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 89643 88211 162 162 0 89481 0
[pid=7261] vsize: 358572
Current children cumulated CPU time (s) 294.85
Current children cumulated vsize (Kb) 360700

[startup+310.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 100908 0 0 0 29992 469 0 0 25 0 1 0 1855919330 378433536 90959 4294967295 134512640 135167914 3221224448 3221098716 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 92391 90959 162 162 0 92229 0
[pid=7261] vsize: 369564
Current children cumulated CPU time (s) 304.67
Current children cumulated vsize (Kb) 371692

[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 113348 0 0 0 30947 500 0 0 25 0 1 0 1855919330 429387776 103399 4294967295 134512640 135167914 3221224448 3221113504 134625428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 104831 103399 162 162 0 104669 0
[pid=7261] vsize: 419324
Current children cumulated CPU time (s) 314.53
Current children cumulated vsize (Kb) 421452

[startup+330.023 s]
Raw data (loadavg): 1.07 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 116075 0 0 0 31917 514 0 0 25 0 1 0 1855919330 418959360 100853 4294967295 134512640 135167914 3221224448 3221088832 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 102285 100853 162 162 0 102123 0
[pid=7261] vsize: 409140
Current children cumulated CPU time (s) 324.37
Current children cumulated vsize (Kb) 411268

[startup+340.023 s]
Raw data (loadavg): 1.06 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 118813 0 0 0 32887 526 0 0 25 0 1 0 1855919330 430174208 103591 4294967295 134512640 135167914 3221224448 3221097936 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 105023 103591 162 162 0 104861 0
[pid=7261] vsize: 420092
Current children cumulated CPU time (s) 334.19
Current children cumulated vsize (Kb) 422220

[startup+350.024 s]
Raw data (loadavg): 1.05 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 121792 0 0 0 33856 538 0 0 25 0 1 0 1855919330 442376192 106570 4294967295 134512640 135167914 3221224448 3221121280 134844866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7261/statm): 108002 106570 162 162 0 107840 0
[pid=7261] vsize: 432008
Current children cumulated CPU time (s) 344
Current children cumulated vsize (Kb) 434136

[startup+360.024 s]
Raw data (loadavg): 1.04 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 124435 0 0 0 34825 550 0 0 25 0 1 0 1855919330 453201920 109213 4294967295 134512640 135167914 3221224448 3221108332 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 110645 109213 162 162 0 110483 0
[pid=7261] vsize: 442580
Current children cumulated CPU time (s) 353.81
Current children cumulated vsize (Kb) 444708

[startup+370.025 s]
Raw data (loadavg): 1.04 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 127499 0 0 0 35790 565 0 0 25 0 1 0 1855919330 465752064 112277 4294967295 134512640 135167914 3221224448 3221097212 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 113709 112277 162 162 0 113547 0
[pid=7261] vsize: 454836
Current children cumulated CPU time (s) 363.61
Current children cumulated vsize (Kb) 456964

[startup+380.025 s]
Raw data (loadavg): 1.03 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 130505 0 0 0 36755 578 0 0 25 0 1 0 1855919330 478064640 115283 4294967295 134512640 135167914 3221224448 3221091984 134522325 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 116715 115283 162 162 0 116553 0
[pid=7261] vsize: 466860
Current children cumulated CPU time (s) 373.39
Current children cumulated vsize (Kb) 468988

[startup+390.025 s]
Raw data (loadavg): 1.03 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 133252 0 0 0 37724 590 0 0 25 0 1 0 1855919330 489316352 118030 4294967295 134512640 135167914 3221224448 3221090940 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 119462 118030 162 162 0 119300 0
[pid=7261] vsize: 477848
Current children cumulated CPU time (s) 383.2
Current children cumulated vsize (Kb) 479976

[startup+400.026 s]
Raw data (loadavg): 1.02 0.99 0.99 1/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 136792 0 0 0 38685 605 0 0 25 0 1 0 1855919330 503820288 121570 4294967295 134512640 135167914 3221224448 3221106716 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 123003 121570 162 162 0 122841 0
[pid=7261] vsize: 492012
Current children cumulated CPU time (s) 392.96
Current children cumulated vsize (Kb) 494140

[startup+410.026 s]
Raw data (loadavg): 1.02 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 139637 0 0 0 39657 616 0 0 25 0 1 0 1855919330 515469312 124415 4294967295 134512640 135167914 3221224448 3221097184 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 125847 124415 162 162 0 125685 0
[pid=7261] vsize: 503388
Current children cumulated CPU time (s) 402.79
Current children cumulated vsize (Kb) 505516

[startup+420.027 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 142602 0 0 0 40626 629 0 0 25 0 1 0 1855919330 527613952 127380 4294967295 134512640 135167914 3221224448 3221096112 134845538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7261/statm): 128812 127380 162 162 0 128650 0
[pid=7261] vsize: 515248
Current children cumulated CPU time (s) 412.61
Current children cumulated vsize (Kb) 517376

[startup+430.027 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 166232 0 0 0 41552 687 0 0 25 0 1 0 1855919330 624402432 151010 4294967295 134512640 135167914 3221224448 3221144608 134624949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 152442 151010 162 162 0 152280 0
[pid=7261] vsize: 609768
Current children cumulated CPU time (s) 422.45
Current children cumulated vsize (Kb) 611896

[startup+440.028 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 167129 0 0 0 42541 693 0 0 25 0 1 0 1855919330 584880128 141361 4294967295 134512640 135167914 3221224448 3221092768 134694413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 142793 141361 162 162 0 142631 0
[pid=7261] vsize: 571172
Current children cumulated CPU time (s) 432.4
Current children cumulated vsize (Kb) 573300

[startup+450.029 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 170042 0 0 0 43509 705 0 0 25 0 1 0 1855919330 596811776 144274 4294967295 134512640 135167914 3221224448 3221125032 134846971 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 145706 144274 162 162 0 145544 0
[pid=7261] vsize: 582824
Current children cumulated CPU time (s) 442.2
Current children cumulated vsize (Kb) 584952

[startup+460.029 s]
Raw data (loadavg): 1.01 0.99 0.99 1/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 173011 0 0 0 44474 718 0 0 25 0 1 0 1855919330 608976896 147243 4294967295 134512640 135167914 3221224448 3221087388 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 148676 147243 162 162 0 148514 0
[pid=7261] vsize: 594704
Current children cumulated CPU time (s) 451.98
Current children cumulated vsize (Kb) 596832

[startup+470.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 175810 0 0 0 45441 731 0 0 25 0 1 0 1855919330 620437504 150042 4294967295 134512640 135167914 3221224448 3221100240 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 151474 150042 162 162 0 151312 0
[pid=7261] vsize: 605896
Current children cumulated CPU time (s) 461.78
Current children cumulated vsize (Kb) 608024

[startup+480.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 178700 0 0 0 46409 746 0 0 25 0 1 0 1855919330 632274944 152932 4294967295 134512640 135167914 3221224448 3221110896 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 154364 152932 162 162 0 154202 0
[pid=7261] vsize: 617456
Current children cumulated CPU time (s) 471.61
Current children cumulated vsize (Kb) 619584

[startup+490.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 181446 0 0 0 47379 758 0 0 25 0 1 0 1855919330 643522560 155678 4294967295 134512640 135167914 3221224448 3221093184 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7261/statm): 157110 155678 162 162 0 156948 0
[pid=7261] vsize: 628440
Current children cumulated CPU time (s) 481.43
Current children cumulated vsize (Kb) 630568

[startup+500.031 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 184797 0 0 0 48342 773 0 0 25 0 1 0 1855919330 657248256 159029 4294967295 134512640 135167914 3221224448 3221123552 134843426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 160461 159029 162 162 0 160299 0
[pid=7261] vsize: 641844
Current children cumulated CPU time (s) 491.21
Current children cumulated vsize (Kb) 643972

[startup+510.031 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 187595 0 0 0 49311 786 0 0 25 0 1 0 1855919330 668708864 161827 4294967295 134512640 135167914 3221224448 3221123644 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 163259 161827 162 162 0 163097 0
[pid=7261] vsize: 653036
Current children cumulated CPU time (s) 501.03
Current children cumulated vsize (Kb) 655164

[startup+520.032 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 190649 0 0 0 50278 799 0 0 25 0 1 0 1855919330 681218048 164881 4294967295 134512640 135167914 3221224448 3221109180 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 166313 164881 162 162 0 166151 0
[pid=7261] vsize: 665252
Current children cumulated CPU time (s) 510.83
Current children cumulated vsize (Kb) 667380

[startup+530.032 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 193559 0 0 0 51244 813 0 0 25 0 1 0 1855919330 693137408 167791 4294967295 134512640 135167914 3221224448 3221099456 134849435 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 169223 167791 162 162 0 169061 0
[pid=7261] vsize: 676892
Current children cumulated CPU time (s) 520.63
Current children cumulated vsize (Kb) 679020

[startup+540.032 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 196289 0 0 0 52214 826 0 0 25 0 1 0 1855919330 704319488 170521 4294967295 134512640 135167914 3221224448 3221092864 134694407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 171953 170521 162 162 0 171791 0
[pid=7261] vsize: 687812
Current children cumulated CPU time (s) 530.46
Current children cumulated vsize (Kb) 689940

[startup+550.033 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 199242 0 0 0 53179 842 0 0 25 0 1 0 1855919330 716414976 173474 4294967295 134512640 135167914 3221224448 3221121788 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7261/statm): 174906 173474 162 162 0 174744 0
[pid=7261] vsize: 699624
Current children cumulated CPU time (s) 540.27
Current children cumulated vsize (Kb) 701752

[startup+560.034 s]
Raw data (loadavg): 1.00 0.99 0.99 1/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 201980 0 0 0 54152 854 0 0 25 0 1 0 1855919330 727629824 176212 4294967295 134512640 135167914 3221224448 3221091836 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 177644 176212 162 162 0 177482 0
[pid=7261] vsize: 710576
Current children cumulated CPU time (s) 550.12
Current children cumulated vsize (Kb) 712704

[startup+570.035 s]
Raw data (loadavg): 1.00 0.99 0.99 1/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 204810 0 0 0 55121 868 0 0 25 0 1 0 1855919330 739221504 179042 4294967295 134512640 135167914 3221224448 3221097212 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 180474 179042 162 162 0 180312 0
[pid=7261] vsize: 721896
Current children cumulated CPU time (s) 559.95
Current children cumulated vsize (Kb) 724024

[startup+580.035 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 208200 0 0 0 56083 883 0 0 25 0 1 0 1855919330 753106944 182432 4294967295 134512640 135167914 3221224448 3221110336 134694528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 183864 182432 162 162 0 183702 0
[pid=7261] vsize: 735456
Current children cumulated CPU time (s) 569.72
Current children cumulated vsize (Kb) 737584

[startup+590.035 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 210905 0 0 0 57051 896 0 0 25 0 1 0 1855919330 764186624 185137 4294967295 134512640 135167914 3221224448 3221087676 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 186569 185137 162 162 0 186407 0
[pid=7261] vsize: 746276
Current children cumulated CPU time (s) 579.53
Current children cumulated vsize (Kb) 748404

[startup+600.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 213728 0 0 0 58019 909 0 0 25 0 1 0 1855919330 775749632 187960 4294967295 134512640 135167914 3221224448 3221101948 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 189392 187960 162 162 0 189230 0
[pid=7261] vsize: 757568
Current children cumulated CPU time (s) 589.34
Current children cumulated vsize (Kb) 759696

[startup+610.037 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) T 7256 7256 19316 0 -1 0 216626 0 0 0 58985 922 0 0 25 0 1 0 1855919330 787619840 190858 4294967295 134512640 135167914 3221224448 3221098140 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7261/statm): 192290 190858 162 162 0 192128 0
[pid=7261] vsize: 769160
Current children cumulated CPU time (s) 599.13
Current children cumulated vsize (Kb) 771288

[startup+620.038 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 219345 0 0 0 59955 934 0 0 25 0 1 0 1855919330 798756864 193577 4294967295 134512640 135167914 3221224448 3221102896 134623813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 195009 193577 162 162 0 194847 0
[pid=7261] vsize: 780036
Current children cumulated CPU time (s) 608.95
Current children cumulated vsize (Kb) 782164

[startup+630.038 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 222066 0 0 0 60924 946 0 0 25 0 1 0 1855919330 809902080 196298 4294967295 134512640 135167914 3221224448 3221103408 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 197730 196298 162 162 0 197568 0
[pid=7261] vsize: 790920
Current children cumulated CPU time (s) 618.76
Current children cumulated vsize (Kb) 793048

[startup+640.038 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 225055 0 0 0 61892 958 0 0 25 0 1 0 1855919330 822145024 199287 4294967295 134512640 135167914 3221224448 3221130204 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 200719 199287 162 162 0 200557 0
[pid=7261] vsize: 802876
Current children cumulated CPU time (s) 628.56
Current children cumulated vsize (Kb) 805004

[startup+650.039 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 7261
Raw data (/proc/7256/stat): 7256 (minisat+_script) S 7255 7256 19316 0 -1 0 314 332 0 0 0 1 2 3 17 0 1 0 1855919316 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7256/statm): 532 234 485 147 0 385 0
[pid=7256] vsize: 2128
Raw data (/proc/7261/stat): 7261 (minisat+_bignum) R 7256 7256 19316 0 -1 0 227780 0 0 0 62862 971 0 0 25 0 1 0 1855919330 833306624 202012 4294967295 134512640 135167914 3221224448 3221092352 134695175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7261/statm): 203444 202012 162 162 0 203282 0
[pid=7261] vsize: 813776
Current children cumulated CPU time (s) 638.39
Current children cumulated vsize (Kb) 815904
One traced child (pid=7261) ended because it received signal 11 (SIGSEGV)
One traced child (pid=7256) exited with status: 139
All traced children have exited ! Game is over.

Child status: 139
Real time (s): 658.118
CPU time (s): 646.359
CPU user time (s): 636.122
CPU system time (s): 10.2364
CPU usage (%): 98.2132
Max. virtual memory (cumulated for all children) (Kb): 815904

Verifier Data

ERROR: no interpretation found !