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-fome12.opb
MD5SUMf7d293075cf169ad75cd0116c61aa297
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 498856
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 3448249888024611600
Number of bits of the sum of numbers in the objective function 62
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 variables977976
Total number of constraints24336
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 constraints24336
Minimum length of a constraint10
Maximum length of a constraint4560

Trace number 6268

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        836144 kB
Buffers:          9984 kB
Cached:         160220 kB
SwapCached:        816 kB
Active:          88452 kB
Inactive:        84516 kB
HighTotal:      131008 kB
HighFree:         3780 kB
LowTotal:       903652 kB
LowFree:        832364 kB
SwapTotal:     2097892 kB
SwapFree:      2096608 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            19764 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:21:07 (client local time) WITH STATUS 0 IN 737.043 SECONDS
stats: 3438 7 737.043 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 48924] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 48620 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssss
c ---[48626]---> BDD-cost:   12
c ---[48625]---> BDD-cost:   10
c ---[48624]---> BDD-cost:    9
c ---[48623]---> BDD-cost:   13
c ---[48621]---> BDD-cost:   11
c ---[48620]---> BDD-cost:   11
c ---[48619]---> BDD-cost:   12
c ---[48618]---> BDD-cost:   11
c ---[48617]---> BDD-cost:    9
c ---[48616]---> BDD-cost:   12
c ---[48615]---> BDD-cost:   11
c ---[48613]---> BDD-cost:   12
c ---[48612]---> BDD-cost:   10
c ---[48611]---> BDD-cost:    9
c ---[48610]---> BDD-cost:   13
c ---[48608]---> BDD-cost:   11
c ---[48607]---> BDD-cost:   11
c ---[48606]---> BDD-cost:   12
c ---[48605]---> BDD-cost:   11
c ---[48604]---> BDD-cost:    9
c ---[48603]---> BDD-cost:   12
c ---[48602]---> BDD-cost:   11
c ---[48600]---> BDD-cost:   12
c ---[48599]---> BDD-cost:   10
c ---[48598]---> BDD-cost:    9
c ---[48597]---> BDD-cost:   13
c ---[48595]---> BDD-cost:   11
c ---[48594]---> BDD-cost:   11
c ---[48593]---> BDD-cost:   12
c ---[48592]---> BDD-cost:   11
c ---[48591]---> BDD-cost:    9
c ---[48590]---> BDD-cost:   12
c ---[48589]---> BDD-cost:   11
c ---[48587]---> BDD-cost:   12
c ---[48586]---> BDD-cost:   10
c ---[48585]---> BDD-cost:    9
c ---[48584]---> BDD-cost:   13
c ---[48582]---> BDD-cost:   11
c ---[48581]---> BDD-cost:   11
c ---[48580]---> BDD-cost:   12
c ---[48579]---> BDD-cost:   11
c ---[48578]---> BDD-cost:    9
c ---[48577]---> BDD-cost:   12
c ---[48576]---> BDD-cost:   11
c ---[48574]---> BDD-cost:   96
c ---[48572]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48570]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[48568]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48566]---> BDD-cost:  126
c ---[48564]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[48562]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48560]---> BDD-cost:  126
c ---[48558]---> Adder-cost: 454   maxlim: 2097534   bits: 23/22
c ---[48556]---> BDD-cost:  126
c ---[48554]---> BDD-cost:  126
c ---[48552]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48550]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48548]---> Sorter-cost:  640     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48546]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48544]---> BDD-cost:   96
c ---[48542]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48540]---> BDD-cost:   99
c ---[48538]---> Sorter-cost: 1420     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48536]---> BDD-cost:  126
c ---[48534]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48532]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48530]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48528]---> BDD-cost:  126
c ---[48526]---> Sorter-cost:  564     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48524]---> Sorter-cost: 2008     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48522]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[48520]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48518]---> Sorter-cost:  609     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48516]---> BDD-cost:  126
c ---[48514]---> BDD-cost:  128
c ---[48512]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48510]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48508]---> Sorter-cost:  846     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48506]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48504]---> BDD-cost:  119
c ---[48502]---> BDD-cost:  104
c ---[48500]---> Adder-cost: 346   maxlim: 1048830   bits: 22/21
c ---[48498]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48496]---> Sorter-cost: 1342     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48494]---> BDD-cost:   99
c ---[48492]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48490]---> Adder-cost: 786   maxlim: 7348198   bits: 24/23
c ---[48488]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48486]---> Sorter-cost: 2365     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48484]---> BDD-cost:  104
c ---[48482]---> Sorter-cost:  410     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48480]---> Sorter-cost: 3161     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48478]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48476]---> BDD-cost:  126
c ---[48474]---> BDD-cost:  126
c ---[48472]---> BDD-cost:  154
c ---[48470]---> BDD-cost:  126
c ---[48468]---> Sorter-cost:  646     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48466]---> Sorter-cost: 2300     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48464]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48462]---> BDD-cost:  126
c ---[48460]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48458]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2
c ---[48456]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48454]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48452]---> BDD-cost:   96
c ---[48450]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48448]---> Sorter-cost: 1503     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48446]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48444]---> Sorter-cost: 1142     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48442]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48440]---> BDD-cost:  126
c ---[48438]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48436]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48434]---> BDD-cost:  126
c ---[48432]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48430]---> BDD-cost:  126
c ---[48428]---> Sorter-cost:  650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48426]---> BDD-cost:  172
c ---[48424]---> BDD-cost:  128
c ---[48422]---> Sorter-cost: 2825     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48420]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2
c ---[48418]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[48416]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48414]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[48412]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48410]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[48408]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48406]---> BDD-cost:  172
c ---[48404]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48402]---> BDD-cost:  128
c ---[48400]---> Sorter-cost:  741     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48398]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48396]---> BDD-cost:   99
c ---[48394]---> Sorter-cost: 1239     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48392]---> BDD-cost:  126
c ---[48390]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48388]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48386]---> Sorter-cost: 2075     Base: 2 2 2 2 2 2 2
c ---[48384]---> Sorter-cost:  846     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48382]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48380]---> Sorter-cost: 1703     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48378]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48376]---> BDD-cost:  128
c ---[48374]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48372]---> BDD-cost:  158
c ---[48370]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48368]---> Sorter-cost: 2148     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48366]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48364]---> BDD-cost:  126
c ---[48362]---> BDD-cost:  126
c ---[48360]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48358]---> Sorter-cost: 1138     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48356]---> Sorter-cost:  561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48354]---> BDD-cost:  128
c ---[48352]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48350]---> Sorter-cost: 2226     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48348]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48346]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[48344]---> Sorter-cost: 1112     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48342]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48340]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48338]---> Adder-cost: 286   maxlim: 556919   bits: 20/20
c ---[48336]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48334]---> Sorter-cost: 2341     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48332]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48330]---> BDD-cost:  121
c ---[48328]---> BDD-cost:  126
c ---[48326]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48324]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48322]---> Sorter-cost: 1751     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48320]---> Sorter-cost: 1026     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48318]---> BDD-cost:  126
c ---[48316]---> Sorter-cost: 2086     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48314]---> Sorter-cost: 1574     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48312]---> BDD-cost:  172
c ---[48310]---> Sorter-cost: 1130     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48308]---> Sorter-cost: 2246     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48306]---> Sorter-cost:  832     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48304]---> BDD-cost:  150
c ---[48302]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2
c ---[48300]---> BDD-cost:   96
c ---[48298]---> Sorter-cost: 1197     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48296]---> BDD-cost:   96
c ---[48294]---> Adder-cost: 474   maxlim: 3260410   bits: 23/22
c ---[48292]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48290]---> Sorter-cost:  349     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48288]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2
c ---[48286]---> Sorter-cost:  454     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48284]---> BDD-cost:  123
c ---[48282]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48280]---> Sorter-cost: 2307     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48278]---> Sorter-cost: 1751     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48276]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48274]---> BDD-cost:  150
c ---[48272]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48270]---> BDD-cost:  126
c ---[48268]---> BDD-cost:  118
c ---[48266]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48264]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48262]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48260]---> BDD-cost:  126
c ---[48258]---> BDD-cost:  118
c ---[48256]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48254]---> BDD-cost:   81
c ---[48252]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48250]---> Sorter-cost: 1892     Base: 2 2 2 2 2 2 2
c ---[48248]---> BDD-cost:  145
c ---[48246]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48244]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48242]---> Sorter-cost:  773     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48240]---> Sorter-cost:  749     Base: 2 2 2 2 2 2 2
c ---[48238]---> BDD-cost:  126
c ---[48236]---> Sorter-cost:  819     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[48234]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2

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/7038/stat): 7038 (minisat+_script) R 7037 7038 20728 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855899256 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7038/statm): 174 3 169 147 0 27 0
[pid=7038] 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=7039
New process pid=7040
New process pid=7041
execve syscall for /bin/sed executable
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
One traced child (pid=7040) exited with status: 0
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=7041) exited with status: 0
One traced child (pid=7039) exited with status: 0
New process pid=7042
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fome12.opb
One traced child (pid=7042) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=7043
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-fome12.opb

[startup+10.0041 s]
Raw data (loadavg): 0.96 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 12736 0 0 0 848 68 0 0 25 0 1 0 1855899278 66973696 12102 4294967295 134512640 135167914 3221224448 3221223384 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 16351 12102 162 162 0 16189 0
[pid=7043] vsize: 65404
Current children cumulated CPU time (s) 9.28
Current children cumulated vsize (Kb) 67532

[startup+20.0048 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 25598 0 0 0 1736 124 0 0 25 0 1 0 1855899278 99049472 23329 4294967295 134512640 135167914 3221224448 3221222688 134844691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 24182 23329 162 162 0 24020 0
[pid=7043] vsize: 96728
Current children cumulated CPU time (s) 18.72
Current children cumulated vsize (Kb) 98856

[startup+30.0055 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 27458 0 0 0 2714 137 0 0 25 0 1 0 1855899278 142176256 25121 4294967295 134512640 135167914 3221224448 3221222128 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 34711 25121 162 162 0 34549 0
[pid=7043] vsize: 138844
Current children cumulated CPU time (s) 28.63
Current children cumulated vsize (Kb) 140972

[startup+40.0061 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 29289 0 0 0 3692 146 0 0 25 0 1 0 1855899278 148156416 26952 4294967295 134512640 135167914 3221224448 3221221664 134522468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 36171 26952 162 162 0 36009 0
[pid=7043] vsize: 144684
Current children cumulated CPU time (s) 38.5
Current children cumulated vsize (Kb) 146812

[startup+50.0078 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 32183 0 0 0 4657 162 0 0 25 0 1 0 1855899278 158306304 29710 4294967295 134512640 135167914 3221224448 3221222720 134610320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 38649 29710 162 162 0 38487 0
[pid=7043] vsize: 154596
Current children cumulated CPU time (s) 48.31
Current children cumulated vsize (Kb) 156724

[startup+60.0085 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 35387 0 0 0 5618 180 0 0 25 0 1 0 1855899278 170131456 32814 4294967295 134512640 135167914 3221224448 3221221648 134845924 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 41536 32814 162 162 0 41374 0
[pid=7043] vsize: 166144
Current children cumulated CPU time (s) 58.1
Current children cumulated vsize (Kb) 168272

[startup+70.0092 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 38490 0 0 0 6580 197 0 0 25 0 1 0 1855899278 181846016 35844 4294967295 134512640 135167914 3221224448 3221222636 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 44396 35844 162 162 0 44234 0
[pid=7043] vsize: 177584
Current children cumulated CPU time (s) 67.89
Current children cumulated vsize (Kb) 179712

[startup+80.0099 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 41486 0 0 0 7543 213 0 0 25 0 1 0 1855899278 193572864 38840 4294967295 134512640 135167914 3221224448 3221223232 134585000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 47259 38840 162 162 0 47097 0
[pid=7043] vsize: 189036
Current children cumulated CPU time (s) 77.68
Current children cumulated vsize (Kb) 191164

[startup+90.0106 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 44514 0 0 0 8505 231 0 0 25 0 1 0 1855899278 205107200 41868 4294967295 134512640 135167914 3221224448 3221222572 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 50075 41868 162 162 0 49913 0
[pid=7043] vsize: 200300
Current children cumulated CPU time (s) 87.48
Current children cumulated vsize (Kb) 202428

[startup+100.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 48066 0 0 0 9467 249 0 0 25 0 1 0 1855899278 217051136 45216 4294967295 134512640 135167914 3221224448 3221220992 134611946 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 52991 45216 162 162 0 52829 0
[pid=7043] vsize: 211964
Current children cumulated CPU time (s) 97.28
Current children cumulated vsize (Kb) 214092

[startup+110.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 53958 0 0 0 10422 273 0 0 25 0 1 0 1855899278 234168320 49790 4294967295 134512640 135167914 3221224448 3221222192 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 57170 49790 162 162 0 57008 0
[pid=7043] vsize: 228680
Current children cumulated CPU time (s) 107.07
Current children cumulated vsize (Kb) 230808

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 57301 0 0 0 11382 293 0 0 25 0 1 0 1855899278 246120448 52989 4294967295 134512640 135167914 3221224448 3221221584 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 60088 52989 162 162 0 59926 0
[pid=7043] vsize: 240352
Current children cumulated CPU time (s) 116.87
Current children cumulated vsize (Kb) 242480

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 60524 0 0 0 12343 312 0 0 25 0 1 0 1855899278 257974272 56114 4294967295 134512640 135167914 3221224448 3221222864 134843420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 62982 56114 162 162 0 62820 0
[pid=7043] vsize: 251928
Current children cumulated CPU time (s) 126.67
Current children cumulated vsize (Kb) 254056

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 63678 0 0 0 13301 332 0 0 25 0 1 0 1855899278 269852672 59196 4294967295 134512640 135167914 3221224448 3221222768 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 65882 59196 162 162 0 65720 0
[pid=7043] vsize: 263528
Current children cumulated CPU time (s) 136.45
Current children cumulated vsize (Kb) 265656

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 66658 0 0 0 14265 348 0 0 25 0 1 0 1855899278 281497600 62176 4294967295 134512640 135167914 3221224448 3221222896 134590369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 68725 62176 162 162 0 68563 0
[pid=7043] vsize: 274900
Current children cumulated CPU time (s) 146.25
Current children cumulated vsize (Kb) 277028

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 69724 0 0 0 15225 367 0 0 25 0 1 0 1855899278 293195776 65242 4294967295 134512640 135167914 3221224448 3221222656 134720472 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 71581 65242 162 162 0 71419 0
[pid=7043] vsize: 286324
Current children cumulated CPU time (s) 156.04
Current children cumulated vsize (Kb) 288452

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 73305 0 0 0 16183 387 0 0 25 0 1 0 1855899278 305221632 68617 4294967295 134512640 135167914 3221224448 3221222784 134718181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 74517 68617 162 162 0 74355 0
[pid=7043] vsize: 298068
Current children cumulated CPU time (s) 165.82
Current children cumulated vsize (Kb) 300196

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 76704 0 0 0 17146 403 0 0 25 0 1 0 1855899278 317517824 72016 4294967295 134512640 135167914 3221224448 3221222752 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 77519 72016 162 162 0 77357 0
[pid=7043] vsize: 310076
Current children cumulated CPU time (s) 175.61
Current children cumulated vsize (Kb) 312204

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 80073 0 0 0 18108 419 0 0 25 0 1 0 1855899278 329478144 75241 4294967295 134512640 135167914 3221224448 3221223360 134572077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 80439 75241 162 162 0 80277 0
[pid=7043] vsize: 321756
Current children cumulated CPU time (s) 185.39
Current children cumulated vsize (Kb) 323884

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 83265 0 0 0 19069 437 0 0 25 0 1 0 1855899278 341258240 78333 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 83315 78333 162 162 0 83153 0
[pid=7043] vsize: 333260
Current children cumulated CPU time (s) 195.18
Current children cumulated vsize (Kb) 335388

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 86342 0 0 0 20030 454 0 0 25 0 1 0 1855899278 352952320 81338 4294967295 134512640 135167914 3221224448 3221222824 134693601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 86170 81338 162 162 0 86008 0
[pid=7043] vsize: 344680
Current children cumulated CPU time (s) 204.96
Current children cumulated vsize (Kb) 346808

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 89321 0 0 0 20992 471 0 0 25 0 1 0 1855899278 364658688 84317 4294967295 134512640 135167914 3221224448 3221222268 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 89028 84317 162 162 0 88866 0
[pid=7043] vsize: 356112
Current children cumulated CPU time (s) 214.75
Current children cumulated vsize (Kb) 358240

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 92374 0 0 0 21955 487 0 0 25 0 1 0 1855899278 376242176 87370 4294967295 134512640 135167914 3221224448 3221222440 134693601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 91856 87370 162 162 0 91694 0
[pid=7043] vsize: 367424
Current children cumulated CPU time (s) 224.54
Current children cumulated vsize (Kb) 369552

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 95907 0 0 0 22916 506 0 0 25 0 1 0 1855899278 388132864 90704 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 94759 90704 162 162 0 94597 0
[pid=7043] vsize: 379036
Current children cumulated CPU time (s) 234.34
Current children cumulated vsize (Kb) 381164

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 99255 0 0 0 23881 521 0 0 25 0 1 0 1855899278 400240640 94052 4294967295 134512640 135167914 3221224448 3221223192 134566617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 97715 94052 162 162 0 97553 0
[pid=7043] vsize: 390860
Current children cumulated CPU time (s) 244.14
Current children cumulated vsize (Kb) 392988

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 102521 0 0 0 24841 537 0 0 25 0 1 0 1855899278 412147712 97260 4294967295 134512640 135167914 3221224448 3221223352 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 100622 97260 162 162 0 100460 0
[pid=7043] vsize: 402488
Current children cumulated CPU time (s) 253.9
Current children cumulated vsize (Kb) 404616

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 105681 0 0 0 25802 555 0 0 25 0 1 0 1855899278 423800832 100321 4294967295 134512640 135167914 3221224448 3221221840 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 103467 100321 162 162 0 103305 0
[pid=7043] vsize: 413868
Current children cumulated CPU time (s) 263.69
Current children cumulated vsize (Kb) 415996

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 108714 0 0 0 26761 574 0 0 25 0 1 0 1855899278 435240960 103283 4294967295 134512640 135167914 3221224448 3221222640 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 106260 103283 162 162 0 106098 0
[pid=7043] vsize: 425040
Current children cumulated CPU time (s) 273.47
Current children cumulated vsize (Kb) 427168

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 111690 0 0 0 27720 591 0 0 25 0 1 0 1855899278 446894080 106259 4294967295 134512640 135167914 3221224448 3221222780 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 109105 106259 162 162 0 108943 0
[pid=7043] vsize: 436420
Current children cumulated CPU time (s) 283.23
Current children cumulated vsize (Kb) 438548

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127858 0 0 0 28593 654 0 0 19 0 1 0 1855899278 512823296 122427 4294967295 134512640 135167914 3221224448 3221223376 134597487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125201 122427 162 162 0 125039 0
[pid=7043] vsize: 500804
Current children cumulated CPU time (s) 292.59
Current children cumulated vsize (Kb) 502932

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127862 0 0 0 29593 655 0 0 25 0 1 0 1855899278 512827392 122431 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125202 122431 162 162 0 125040 0
[pid=7043] vsize: 500808
Current children cumulated CPU time (s) 302.6
Current children cumulated vsize (Kb) 502936

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127863 0 0 0 30593 655 0 0 25 0 1 0 1855899278 512827392 122432 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125202 122432 162 162 0 125040 0
[pid=7043] vsize: 500808
Current children cumulated CPU time (s) 312.6
Current children cumulated vsize (Kb) 502936

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127866 0 0 0 31592 655 0 0 25 0 1 0 1855899278 512831488 122435 4294967295 134512640 135167914 3221224448 3221223224 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125203 122435 162 162 0 125041 0
[pid=7043] vsize: 500812
Current children cumulated CPU time (s) 322.59
Current children cumulated vsize (Kb) 502940

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127869 0 0 0 32592 655 0 0 25 0 1 0 1855899278 512835584 122438 4294967295 134512640 135167914 3221224448 3221223280 134596387 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125204 122438 162 162 0 125042 0
[pid=7043] vsize: 500816
Current children cumulated CPU time (s) 332.59
Current children cumulated vsize (Kb) 502944

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127872 0 0 0 33592 655 0 0 25 0 1 0 1855899278 512839680 122441 4294967295 134512640 135167914 3221224448 3221223276 134522184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125205 122441 162 162 0 125043 0
[pid=7043] vsize: 500820
Current children cumulated CPU time (s) 342.59
Current children cumulated vsize (Kb) 502948

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127876 0 0 0 34592 656 0 0 25 0 1 0 1855899278 512843776 122445 4294967295 134512640 135167914 3221224448 3221223204 134697054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125206 122445 162 162 0 125044 0
[pid=7043] vsize: 500824
Current children cumulated CPU time (s) 352.6
Current children cumulated vsize (Kb) 502952

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127879 0 0 0 35591 656 0 0 25 0 1 0 1855899278 512847872 122448 4294967295 134512640 135167914 3221224448 3221223212 134697040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125207 122448 162 162 0 125045 0
[pid=7043] vsize: 500828
Current children cumulated CPU time (s) 362.59
Current children cumulated vsize (Kb) 502956

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127885 0 0 0 36591 657 0 0 25 0 1 0 1855899278 512856064 122454 4294967295 134512640 135167914 3221224448 3221223204 134697076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 125209 122454 162 162 0 125047 0
[pid=7043] vsize: 500836
Current children cumulated CPU time (s) 372.6
Current children cumulated vsize (Kb) 502964

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127906 0 0 0 37589 658 0 0 25 0 1 0 1855899278 489418752 116744 4294967295 134512640 135167914 3221224448 3221223132 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 119487 116744 162 162 0 119325 0
[pid=7043] vsize: 477948
Current children cumulated CPU time (s) 382.59
Current children cumulated vsize (Kb) 480076

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127941 0 0 0 38589 658 0 0 25 0 1 0 1855899278 489504768 116779 4294967295 134512640 135167914 3221224448 3221203296 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 119508 116779 162 162 0 119346 0
[pid=7043] vsize: 478032
Current children cumulated CPU time (s) 392.59
Current children cumulated vsize (Kb) 480160

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127953 0 0 0 39589 659 0 0 25 0 1 0 1855899278 489553920 116791 4294967295 134512640 135167914 3221224448 3221099776 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 119520 116791 162 162 0 119358 0
[pid=7043] vsize: 478080
Current children cumulated CPU time (s) 402.6
Current children cumulated vsize (Kb) 480208

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 127953 0 0 0 40589 659 0 0 25 0 1 0 1855899278 489553920 116791 4294967295 134512640 135167914 3221224448 3221101268 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 119520 116791 162 162 0 119358 0
[pid=7043] vsize: 478080
Current children cumulated CPU time (s) 412.6
Current children cumulated vsize (Kb) 480208

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 130592 0 0 0 41556 672 0 0 25 0 1 0 1855899278 500363264 119430 4294967295 134512640 135167914 3221224448 3221107016 134621274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 122159 119430 162 162 0 121997 0
[pid=7043] vsize: 488636
Current children cumulated CPU time (s) 422.4
Current children cumulated vsize (Kb) 490764

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 134494 0 0 0 42534 685 0 0 25 0 1 0 1855899278 516345856 123332 4294967295 134512640 135167914 3221224448 3221110400 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 126061 123332 162 162 0 125899 0
[pid=7043] vsize: 504244
Current children cumulated CPU time (s) 432.31
Current children cumulated vsize (Kb) 506372

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 137520 0 0 0 43498 701 0 0 25 0 1 0 1855899278 528740352 126358 4294967295 134512640 135167914 3221224448 3221102208 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 129087 126358 162 162 0 128925 0
[pid=7043] vsize: 516348
Current children cumulated CPU time (s) 442.11
Current children cumulated vsize (Kb) 518476

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 140100 0 0 0 44467 714 0 0 25 0 1 0 1855899278 539308032 128938 4294967295 134512640 135167914 3221224448 3221103776 134695185 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 131667 128938 162 162 0 131505 0
[pid=7043] vsize: 526668
Current children cumulated CPU time (s) 451.93
Current children cumulated vsize (Kb) 528796

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 147600 0 0 0 45427 737 0 0 25 0 1 0 1855899278 559226880 133801 4294967295 134512640 135167914 3221224448 3221141824 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 136530 133801 162 162 0 136368 0
[pid=7043] vsize: 546120
Current children cumulated CPU time (s) 461.76
Current children cumulated vsize (Kb) 548248

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 150294 0 0 0 46399 748 0 0 25 0 1 0 1855899278 570261504 136495 4294967295 134512640 135167914 3221224448 3221087856 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 139224 136495 162 162 0 139062 0
[pid=7043] vsize: 556896
Current children cumulated CPU time (s) 471.59
Current children cumulated vsize (Kb) 559024

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 153295 0 0 0 47366 764 0 0 25 0 1 0 1855899278 582553600 139496 4294967295 134512640 135167914 3221224448 3221114304 134624000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 142225 139496 162 162 0 142063 0
[pid=7043] vsize: 568900
Current children cumulated CPU time (s) 481.42
Current children cumulated vsize (Kb) 571028

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 156559 0 0 0 48326 782 0 0 25 0 1 0 1855899278 595922944 142760 4294967295 134512640 135167914 3221224448 3221102844 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 145489 142760 162 162 0 145327 0
[pid=7043] vsize: 581956
Current children cumulated CPU time (s) 491.2
Current children cumulated vsize (Kb) 584084

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 159303 0 0 0 49296 795 0 0 25 0 1 0 1855899278 607162368 145504 4294967295 134512640 135167914 3221224448 3221097968 134624032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 148233 145504 162 162 0 148071 0
[pid=7043] vsize: 592932
Current children cumulated CPU time (s) 501.03
Current children cumulated vsize (Kb) 595060

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 171877 0 0 0 50247 830 0 0 25 0 1 0 1855899278 658665472 158078 4294967295 134512640 135167914 3221224448 3221113392 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 160807 158078 162 162 0 160645 0
[pid=7043] vsize: 643228
Current children cumulated CPU time (s) 510.89
Current children cumulated vsize (Kb) 645356

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 174406 0 0 0 51218 843 0 0 25 0 1 0 1855899278 647426048 155334 4294967295 134512640 135167914 3221224448 3221097628 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 158063 155334 162 162 0 157901 0
[pid=7043] vsize: 632252
Current children cumulated CPU time (s) 520.73
Current children cumulated vsize (Kb) 634380

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 177084 0 0 0 52190 855 0 0 25 0 1 0 1855899278 658395136 158012 4294967295 134512640 135167914 3221224448 3221090236 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 160741 158012 162 162 0 160579 0
[pid=7043] vsize: 642964
Current children cumulated CPU time (s) 530.57
Current children cumulated vsize (Kb) 645092

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 179950 0 0 0 53158 869 0 0 25 0 1 0 1855899278 670134272 160878 4294967295 134512640 135167914 3221224448 3221111880 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 163607 160878 162 162 0 163445 0
[pid=7043] vsize: 654428
Current children cumulated CPU time (s) 540.39
Current children cumulated vsize (Kb) 656556

[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 182668 0 0 0 54126 882 0 0 25 0 1 0 1855899278 681267200 163596 4294967295 134512640 135167914 3221224448 3221091440 134849071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 166325 163596 162 162 0 166163 0
[pid=7043] vsize: 665300
Current children cumulated CPU time (s) 550.2
Current children cumulated vsize (Kb) 667428

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 185686 0 0 0 55092 896 0 0 25 0 1 0 1855899278 693628928 166614 4294967295 134512640 135167914 3221224448 3221092064 134849438 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 169343 166614 162 162 0 169181 0
[pid=7043] vsize: 677372
Current children cumulated CPU time (s) 560
Current children cumulated vsize (Kb) 679500

[startup+580.05 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 188557 0 0 0 56057 911 0 0 25 0 1 0 1855899278 705388544 169485 4294967295 134512640 135167914 3221224448 3221102508 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 172214 169485 162 162 0 172052 0
[pid=7043] vsize: 688856
Current children cumulated CPU time (s) 569.8
Current children cumulated vsize (Kb) 690984

[startup+590.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 191314 0 0 0 57024 922 0 0 25 0 1 0 1855899278 716681216 172242 4294967295 134512640 135167914 3221224448 3221112256 134694428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 174971 172242 162 162 0 174809 0
[pid=7043] vsize: 699884
Current children cumulated CPU time (s) 579.58
Current children cumulated vsize (Kb) 702012

[startup+600.051 s]
Raw data (loadavg): 1.07 0.99 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 194614 0 0 0 57988 937 0 0 25 0 1 0 1855899278 730198016 175542 4294967295 134512640 135167914 3221224448 3221140892 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 178271 175542 162 162 0 178109 0
[pid=7043] vsize: 713084
Current children cumulated CPU time (s) 589.37
Current children cumulated vsize (Kb) 715212

[startup+610.052 s]
Raw data (loadavg): 1.06 0.99 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 197657 0 0 0 58953 952 0 0 25 0 1 0 1855899278 742662144 178585 4294967295 134512640 135167914 3221224448 3221093212 134722208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 181314 178585 162 162 0 181152 0
[pid=7043] vsize: 725256
Current children cumulated CPU time (s) 599.17
Current children cumulated vsize (Kb) 727384

[startup+620.052 s]
Raw data (loadavg): 1.05 0.99 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 200572 0 0 0 59921 967 0 0 25 0 1 0 1855899278 754601984 181500 4294967295 134512640 135167914 3221224448 3221120608 134696017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 184229 181500 162 162 0 184067 0
[pid=7043] vsize: 736916
Current children cumulated CPU time (s) 609
Current children cumulated vsize (Kb) 739044

[startup+630.052 s]
Raw data (loadavg): 1.04 0.99 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 203351 0 0 0 60889 978 0 0 25 0 1 0 1855899278 765984768 184279 4294967295 134512640 135167914 3221224448 3221120448 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 187008 184279 162 162 0 186846 0
[pid=7043] vsize: 748032
Current children cumulated CPU time (s) 618.79
Current children cumulated vsize (Kb) 750160

[startup+640.053 s]
Raw data (loadavg): 1.04 0.99 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 225018 0 0 0 61828 1037 0 0 25 0 1 0 1855899278 811536384 195400 4294967295 134512640 135167914 3221224448 3221101532 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 198129 195400 162 162 0 197967 0
[pid=7043] vsize: 792516
Current children cumulated CPU time (s) 628.77
Current children cumulated vsize (Kb) 794644

[startup+650.053 s]
Raw data (loadavg): 1.03 0.99 0.94 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 227712 0 0 0 62799 1050 0 0 25 0 1 0 1855899278 822571008 198094 4294967295 134512640 135167914 3221224448 3221122588 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 200823 198094 162 162 0 200661 0
[pid=7043] vsize: 803292
Current children cumulated CPU time (s) 638.61
Current children cumulated vsize (Kb) 805420

[startup+660.053 s]
Raw data (loadavg): 1.11 1.00 0.95 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 230745 0 0 0 63764 1065 0 0 25 0 1 0 1855899278 834994176 201127 4294967295 134512640 135167914 3221224448 3221109008 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 203856 201127 162 162 0 203694 0
[pid=7043] vsize: 815424
Current children cumulated CPU time (s) 648.41
Current children cumulated vsize (Kb) 817552

[startup+670.053 s]
Raw data (loadavg): 1.16 1.02 0.95 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 233553 0 0 0 64733 1077 0 0 25 0 1 0 1855899278 846495744 203935 4294967295 134512640 135167914 3221224448 3221104380 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 206664 203935 162 162 0 206502 0
[pid=7043] vsize: 826656
Current children cumulated CPU time (s) 658.22
Current children cumulated vsize (Kb) 828784

[startup+680.054 s]
Raw data (loadavg): 1.14 1.02 0.95 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 236371 0 0 0 65703 1089 0 0 25 0 1 0 1855899278 858038272 206753 4294967295 134512640 135167914 3221224448 3221104640 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 209482 206753 162 162 0 209320 0
[pid=7043] vsize: 837928
Current children cumulated CPU time (s) 668.04
Current children cumulated vsize (Kb) 840056

[startup+690.055 s]
Raw data (loadavg): 1.12 1.02 0.95 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 239151 0 0 0 66673 1103 0 0 25 0 1 0 1855899278 869425152 209469 4294967295 134512640 135167914 3221224448 3221106556 134694480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 212262 209469 162 162 0 212100 0
[pid=7043] vsize: 849048
Current children cumulated CPU time (s) 677.88
Current children cumulated vsize (Kb) 851176

[startup+700.054 s]
Raw data (loadavg): 1.10 1.02 0.95 1/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 242160 0 3 0 67629 1121 0 0 25 0 1 0 1855899278 881717248 212276 4294967295 134512640 135167914 3221224448 3221143484 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 215263 212276 162 162 0 215101 0
[pid=7043] vsize: 861052
Current children cumulated CPU time (s) 687.62
Current children cumulated vsize (Kb) 863180

[startup+710.055 s]
Raw data (loadavg): 1.16 1.03 0.96 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 245306 0 12 0 68586 1136 0 0 25 0 1 0 1855899278 894345216 214935 4294967295 134512640 135167914 3221224448 3221106208 134694428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 218346 214935 162 162 0 218184 0
[pid=7043] vsize: 873384
Current children cumulated CPU time (s) 697.34
Current children cumulated vsize (Kb) 875512

[startup+720.056 s]
Raw data (loadavg): 1.13 1.03 0.96 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 248308 0 58 0 69509 1152 0 0 25 0 1 0 1855899278 906272768 217146 4294967295 134512640 135167914 3221224448 3221099712 134694383 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 221258 217146 162 162 0 221096 0
[pid=7043] vsize: 885032
Current children cumulated CPU time (s) 706.73
Current children cumulated vsize (Kb) 887160

[startup+730.056 s]
Raw data (loadavg): 1.11 1.03 0.96 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 251046 0 67 0 70467 1166 0 0 25 0 1 0 1855899278 917372928 219001 4294967295 134512640 135167914 3221224448 3221093984 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7043/statm): 223968 219001 162 162 0 223806 0
[pid=7043] vsize: 895872
Current children cumulated CPU time (s) 716.45
Current children cumulated vsize (Kb) 898000

[startup+740.057 s]
Raw data (loadavg): 1.09 1.03 0.96 2/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) R 7038 7038 20728 0 -1 0 253939 0 91 0 71412 1180 0 0 23 0 1 0 1855899278 928702464 220732 4294967295 134512640 135167914 3221224448 3221095008 134694428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7043/statm): 226734 220732 162 162 0 226572 0
[pid=7043] vsize: 906936
Current children cumulated CPU time (s) 726.04
Current children cumulated vsize (Kb) 909064

[startup+750.057 s]
Raw data (loadavg): 1.08 1.03 0.96 1/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) D 7038 7038 20728 0 -1 0 256328 0 231 0 72191 1191 0 0 18 0 1 0 1855899278 937459712 216937 4294967295 134512640 135167914 3221224448 3221112256 134694389 0 0 5 16386 3222515881 0 0 17 0 0 0
Raw data (/proc/7043/statm): 228872 216937 162 162 0 228710 0
[pid=7043] vsize: 915488
Current children cumulated CPU time (s) 733.94
Current children cumulated vsize (Kb) 917616



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+754.658 s]
Raw data (loadavg): 1.07 1.03 0.96 1/57 7043
Raw data (/proc/7038/stat): 7038 (minisat+_script) S 7037 7038 20728 0 -1 0 314 332 0 0 0 1 6 5 17 0 1 0 1855899256 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7038/statm): 532 234 485 147 0 385 0
[pid=7038] vsize: 2128
Raw data (/proc/7043/stat): 7043 (minisat+_bignum) T 7038 7038 20728 0 -1 0 257914 0 303 0 72462 1199 0 0 21 0 1 0 1855899278 941543424 218572 4294967295 134512640 135167914 3221224448 3221092060 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7043/statm): 229869 218572 162 162 0 229707 0
[pid=7043] vsize: 919476
Current children cumulated CPU time (s) 736.73
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 755.087
CPU time (s): 737.043
CPU user time (s): 724.626
CPU system time (s): 12.4171
CPU usage (%): 97.6103
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !