PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/een/normalized-p0548.opb
MD5SUM	422c0da7d5380a26c4dac413428db5c9
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	14670
Optimality of the best value was proved	NO
Number of terms in the objective function	416
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	96797
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	96797
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1230.14
Number of variables	527
Total number of constraints	156
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	116
Minimum length of a constraint	2
Maximum length of a constraint	134
Trace number 7154

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-14 21:41:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5237 boxname=wulflinc4 idbench=403 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  422c0da7d5380a26c4dac413428db5c9  /oldhome/oroussel/tmp/wulflinc4/normalized-p0548.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc4/normalized-p0548.opb /oldhome/oroussel/tmp/wulflinc4/normalized-p0548.opb
IDLAUNCH: 5237
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 2
cpu MHz		: 451.169
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:        871892 kB
Buffers:         36880 kB
Cached:         105920 kB
SwapCached:          0 kB
Active:          63232 kB
Inactive:        82384 kB
HighTotal:      131008 kB
HighFree:        21364 kB
LowTotal:       903652 kB
LowFree:        850528 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11624 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 22:01:19 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 5237 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................ss.ssssss.s.s.
c ---[ 125]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    3
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:    3
c ---[ 117]---> BDD-cost:    3
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    3
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    3
c ---[ 110]---> BDD-cost:    3
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    3
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:    3
c ---[ 105]---> BDD-cost:    3
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    5
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    6
c ---[  98]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   19
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:    4
c ---[  89]---> BDD-cost:   24
c ---[  88]---> BDD-cost:   14
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   28
c ---[  85]---> BDD-cost:   13
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:   25
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   19
c ---[  72]---> BDD-cost:   24
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:   27
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   56
c ---[  64]---> BDD-cost:   50
c ---[  63]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   33
c ---[  60]---> BDD-cost:   12
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   34
c ---[  56]---> BDD-cost:   33
c ---[  55]---> BDD-cost:   23
c ---[  54]---> BDD-cost:   75
c ---[  53]---> BDD-cost:   24
c ---[  52]---> BDD-cost:   37
c ---[  51]---> BDD-cost:   37
c ---[  50]---> BDD-cost:   95
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  115
c ---[  46]---> BDD-cost:  120
c ---[  45]---> BDD-cost:  104
c ---[  44]---> BDD-cost:   29
c ---[  43]---> BDD-cost:   51
c ---[  42]---> BDD-cost:   35
c ---[  41]---> BDD-cost:   24
c ---[  39]---> BDD-cost:   61
c ---[  38]---> BDD-cost:  109
c ---[  37]---> BDD-cost:  153
c ---[  36]---> BDD-cost:  120
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   25
c ---[  33]---> BDD-cost:  121
c ---[  32]---> BDD-cost:   32
c ---[  31]---> BDD-cost:   70
c ---[  30]---> BDD-cost:   56
c ---[  29]---> BDD-cost:   78
c ---[  28]---> BDD-cost:   84
c ---[  27]---> BDD-cost:   36
c ---[  26]---> BDD-cost:   91
c ---[  25]---> BDD-cost:   42
c ---[  23]---> BDD-cost:   39
c ---[  22]---> BDD-cost:  128
c ---[  21]---> BDD-cost:   61
c ---[  19]---> BDD-cost:   85
c ---[  18]---> BDD-cost:   55
c ---[  17]---> BDD-cost:   79
c ---[  16]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  15]---> BDD-cost:   26
c ---[  14]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  13]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   49
c ---[  10]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    2
c ---[   5]---> BDD-cost:    4
c ---[   4]---> BDD-cost:    7
c ---[   3]---> BDD-cost:    5
c ---[   2]---> BDD-cost:   11
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   20
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ===========================#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 19972
Raw data (stat): 19972 (runsolver) R 19971 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429685135 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 2160 0 0 0 993 5 0 0 25 0 1 0 429685135 10665984 2107 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2604 2107 603 41 0 2563 0
vsize: 10416
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 2415 0 0 0 1993 6 0 0 25 0 1 0 429685135 11624448 2362 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2838 2362 603 41 0 2797 0
vsize: 11352
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 2536 0 0 0 2992 6 0 0 25 0 1 0 429685135 12120064 2483 4294967295 134512640 134672761 3221224576 3221223760 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2959 2483 603 41 0 2918 0
vsize: 11836
[startup+40.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 2582 0 0 0 3992 6 0 0 25 0 1 0 429685135 12353536 2529 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3016 2529 603 41 0 2975 0
vsize: 12064
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 2893 0 0 0 4992 7 0 0 25 0 1 0 429685135 13553664 2839 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3309 2839 603 41 0 3268 0
vsize: 13236
[startup+60.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 3008 0 0 0 5991 8 0 0 25 0 1 0 429685135 14012416 2953 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3421 2953 603 41 0 3380 0
vsize: 13684
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 3095 0 0 0 6991 8 0 0 25 0 1 0 429685135 14413824 3040 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3519 3040 603 41 0 3478 0
vsize: 14076
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 3164 0 0 0 7991 8 0 0 25 0 1 0 429685135 14655488 3109 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3578 3109 603 41 0 3537 0
vsize: 14312
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 3235 0 0 0 8991 9 0 0 25 0 1 0 429685135 14913536 3180 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3641 3180 603 41 0 3600 0
vsize: 14564
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 3361 0 0 0 9991 9 0 0 25 0 1 0 429685135 15458304 3306 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3774 3306 603 41 0 3733 0
vsize: 15096
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 3634 0 0 0 10990 10 0 0 25 0 1 0 429685135 16568320 3578 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4045 3578 603 41 0 4004 0
vsize: 16180
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 3638 0 0 0 11990 10 0 0 25 0 1 0 429685135 16568320 3582 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4045 3582 603 41 0 4004 0
vsize: 16180
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 3967 0 0 0 12989 11 0 0 25 0 1 0 429685135 18018304 3911 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4399 3911 603 41 0 4358 0
vsize: 17596
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4038 0 0 0 13989 11 0 0 25 0 1 0 429685135 18239488 3982 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4453 3982 603 41 0 4412 0
vsize: 17812
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4039 0 0 0 14990 11 0 0 25 0 1 0 429685135 18239488 3983 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4453 3983 603 41 0 4412 0
vsize: 17812
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4073 0 0 0 15990 11 0 0 25 0 1 0 429685135 18419712 4017 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4497 4017 603 41 0 4456 0
vsize: 17988
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4073 0 0 0 16990 11 0 0 25 0 1 0 429685135 18419712 4017 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4497 4017 603 41 0 4456 0
vsize: 17988
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4143 0 0 0 17990 12 0 0 25 0 1 0 429685135 18702336 4086 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4566 4086 603 41 0 4525 0
vsize: 18264
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4143 0 0 0 18990 12 0 0 25 0 1 0 429685135 18702336 4086 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4566 4086 603 41 0 4525 0
vsize: 18264
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4143 0 0 0 19990 12 0 0 25 0 1 0 429685135 18702336 4086 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4566 4086 603 41 0 4525 0
vsize: 18264
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4167 0 0 0 20990 12 0 0 25 0 1 0 429685135 18800640 4110 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4590 4110 603 41 0 4549 0
vsize: 18360
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4168 0 0 0 21991 12 0 0 25 0 1 0 429685135 18800640 4111 4294967295 134512640 134672761 3221224576 3221223732 134614480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4590 4111 603 41 0 4549 0
vsize: 18360
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4171 0 0 0 22991 12 0 0 25 0 1 0 429685135 18948096 4114 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4626 4114 603 41 0 4585 0
vsize: 18504
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4202 0 0 0 23991 12 0 0 25 0 1 0 429685135 18948096 4145 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4626 4145 603 41 0 4585 0
vsize: 18504
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4236 0 0 0 24991 12 0 0 25 0 1 0 429685135 19210240 4179 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4179 603 41 0 4649 0
vsize: 18760
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4273 0 0 0 25991 12 0 0 25 0 1 0 429685135 19210240 4182 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4182 603 41 0 4649 0
vsize: 18760
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4273 0 0 0 26991 12 0 0 25 0 1 0 429685135 19210240 4182 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4182 603 41 0 4649 0
vsize: 18760
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4273 0 0 0 27991 12 0 0 25 0 1 0 429685135 19210240 4182 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4182 603 41 0 4649 0
vsize: 18760
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4307 0 0 0 28992 12 0 0 25 0 1 0 429685135 19210240 4182 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4182 603 41 0 4649 0
vsize: 18760
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4307 0 0 0 29992 12 0 0 25 0 1 0 429685135 19210240 4182 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4182 603 41 0 4649 0
vsize: 18760
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4308 0 0 0 30992 12 0 0 25 0 1 0 429685135 19210240 4183 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4183 603 41 0 4649 0
vsize: 18760
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4372 0 0 0 31992 12 0 0 25 0 1 0 429685135 19591168 4247 4294967295 134512640 134672761 3221224576 3221223632 134644266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4247 603 41 0 4742 0
vsize: 19132
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4372 0 0 0 32992 12 0 0 25 0 1 0 429685135 19329024 4213 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4719 4213 603 41 0 4678 0
vsize: 18876
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4372 0 0 0 33992 12 0 0 25 0 1 0 429685135 19329024 4213 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4719 4213 603 41 0 4678 0
vsize: 18876
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4373 0 0 0 34992 12 0 0 25 0 1 0 429685135 19329024 4214 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4719 4214 603 41 0 4678 0
vsize: 18876
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4458 0 0 0 35992 12 0 0 25 0 1 0 429685135 19537920 4265 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4770 4265 603 41 0 4729 0
vsize: 19080
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4458 0 0 0 36993 12 0 0 25 0 1 0 429685135 19537920 4265 4294967295 134512640 134672761 3221224576 3221223760 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4770 4265 603 41 0 4729 0
vsize: 19080
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4458 0 0 0 37993 12 0 0 25 0 1 0 429685135 19537920 4265 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4770 4265 603 41 0 4729 0
vsize: 19080
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4469 0 0 0 38993 12 0 0 25 0 1 0 429685135 19570688 4273 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4778 4273 603 41 0 4737 0
vsize: 19112
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4469 0 0 0 39993 12 0 0 25 0 1 0 429685135 19570688 4273 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4778 4273 603 41 0 4737 0
vsize: 19112
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4469 0 0 0 40993 12 0 0 25 0 1 0 429685135 19570688 4273 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4778 4273 603 41 0 4737 0
vsize: 19112
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4499 0 0 0 41993 13 0 0 25 0 1 0 429685135 19636224 4296 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4794 4296 603 41 0 4753 0
vsize: 19176
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4499 0 0 0 42994 13 0 0 25 0 1 0 429685135 19636224 4296 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4794 4296 603 41 0 4753 0
vsize: 19176
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4499 0 0 0 43994 13 0 0 25 0 1 0 429685135 19636224 4296 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4794 4296 603 41 0 4753 0
vsize: 19176
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4499 0 0 0 44994 13 0 0 25 0 1 0 429685135 19636224 4296 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4794 4296 603 41 0 4753 0
vsize: 19176
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4560 0 0 0 45994 13 0 0 25 0 1 0 429685135 19734528 4320 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4818 4320 603 41 0 4777 0
vsize: 19272
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4560 0 0 0 46994 13 0 0 25 0 1 0 429685135 19734528 4320 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4818 4320 603 41 0 4777 0
vsize: 19272
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4560 0 0 0 47995 13 0 0 25 0 1 0 429685135 19734528 4320 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4818 4320 603 41 0 4777 0
vsize: 19272
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4560 0 0 0 48995 13 0 0 25 0 1 0 429685135 19734528 4320 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4818 4320 603 41 0 4777 0
vsize: 19272
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4575 0 0 0 49995 13 0 0 25 0 1 0 429685135 19767296 4328 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4826 4328 603 41 0 4785 0
vsize: 19304
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4575 0 0 0 50995 13 0 0 25 0 1 0 429685135 19767296 4328 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4826 4328 603 41 0 4785 0
vsize: 19304
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4575 0 0 0 51995 13 0 0 25 0 1 0 429685135 19767296 4328 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4826 4328 603 41 0 4785 0
vsize: 19304
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4612 0 0 0 52995 13 0 0 25 0 1 0 429685135 20029440 4365 4294967295 134512640 134672761 3221224576 3221223632 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4365 603 41 0 4849 0
vsize: 19560
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4612 0 0 0 53996 13 0 0 25 0 1 0 429685135 19767296 4328 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4826 4328 603 41 0 4785 0
vsize: 19304
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4612 0 0 0 54996 13 0 0 25 0 1 0 429685135 19767296 4328 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4826 4328 603 41 0 4785 0
vsize: 19304
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4612 0 0 0 55996 13 0 0 25 0 1 0 429685135 19767296 4328 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4826 4328 603 41 0 4785 0
vsize: 19304
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4629 0 0 0 56996 13 0 0 25 0 1 0 429685135 19800064 4338 4294967295 134512640 134672761 3221224576 3221223616 134612871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4834 4338 603 41 0 4793 0
vsize: 19336
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4629 0 0 0 57996 13 0 0 25 0 1 0 429685135 19800064 4338 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4834 4338 603 41 0 4793 0
vsize: 19336
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4629 0 0 0 58997 13 0 0 25 0 1 0 429685135 19800064 4338 4294967295 134512640 134672761 3221224576 3221223760 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4834 4338 603 41 0 4793 0
vsize: 19336
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4629 0 0 0 59997 13 0 0 25 0 1 0 429685135 19800064 4338 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4834 4338 603 41 0 4793 0
vsize: 19336
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4703 0 0 0 60997 13 0 0 25 0 1 0 429685135 20078592 4406 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4902 4406 603 41 0 4861 0
vsize: 19608
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4703 0 0 0 61997 13 0 0 25 0 1 0 429685135 20078592 4406 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4902 4406 603 41 0 4861 0
vsize: 19608
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4703 0 0 0 62997 13 0 0 25 0 1 0 429685135 20078592 4406 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4902 4406 603 41 0 4861 0
vsize: 19608
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4705 0 0 0 63997 13 0 0 25 0 1 0 429685135 20209664 4408 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4408 603 41 0 4893 0
vsize: 19736
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4837 0 0 0 64997 14 0 0 25 0 1 0 429685135 20475904 4503 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4999 4503 603 41 0 4958 0
vsize: 19996
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 4837 0 0 0 65997 14 0 0 25 0 1 0 429685135 20475904 4503 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4999 4503 603 41 0 4958 0
vsize: 19996
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 5273 0 0 0 66996 15 0 0 25 0 1 0 429685135 22327296 4939 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5451 4939 603 41 0 5410 0
vsize: 21804
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 5629 0 0 0 67995 16 0 0 25 0 1 0 429685135 23535616 5254 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5746 5254 603 41 0 5705 0
vsize: 22984
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 5629 0 0 0 68995 16 0 0 25 0 1 0 429685135 23535616 5254 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5746 5254 603 41 0 5705 0
vsize: 22984
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 5629 0 0 0 69995 16 0 0 25 0 1 0 429685135 23535616 5254 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5746 5254 603 41 0 5705 0
vsize: 22984
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 5629 0 0 0 70996 16 0 0 25 0 1 0 429685135 23535616 5254 4294967295 134512640 134672761 3221224576 3221223616 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5746 5254 603 41 0 5705 0
vsize: 22984
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6047 0 0 0 71995 17 0 0 25 0 1 0 429685135 25374720 5672 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6195 5672 603 41 0 6154 0
vsize: 24780
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6095 0 0 0 72995 17 0 0 25 0 1 0 429685135 25415680 5709 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6205 5709 603 41 0 6164 0
vsize: 24820
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6096 0 0 0 73995 17 0 0 25 0 1 0 429685135 25415680 5710 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6205 5710 603 41 0 6164 0
vsize: 24820
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6096 0 0 0 74995 17 0 0 25 0 1 0 429685135 25415680 5710 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6205 5710 603 41 0 6164 0
vsize: 24820
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6096 0 0 0 75995 17 0 0 25 0 1 0 429685135 25415680 5710 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6205 5710 603 41 0 6164 0
vsize: 24820
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6417 0 0 0 76995 18 0 0 25 0 1 0 429685135 26570752 5990 4294967295 134512640 134672761 3221224576 3221223776 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6487 5990 603 41 0 6446 0
vsize: 25948
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6417 0 0 0 77995 18 0 0 25 0 1 0 429685135 26570752 5990 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6487 5990 603 41 0 6446 0
vsize: 25948
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6417 0 0 0 78995 18 0 0 25 0 1 0 429685135 26570752 5990 4294967295 134512640 134672761 3221224576 3221223528 1075347133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6487 5990 603 41 0 6446 0
vsize: 25948
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6417 0 0 0 79995 18 0 0 25 0 1 0 429685135 26570752 5990 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6487 5990 603 41 0 6446 0
vsize: 25948
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6417 0 0 0 80995 18 0 0 25 0 1 0 429685135 26570752 5990 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6487 5990 603 41 0 6446 0
vsize: 25948
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6439 0 0 0 81995 18 0 0 25 0 1 0 429685135 26615808 6001 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6498 6001 603 41 0 6457 0
vsize: 25992
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6439 0 0 0 82995 18 0 0 25 0 1 0 429685135 26615808 6001 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6498 6001 603 41 0 6457 0
vsize: 25992
[startup+840.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6439 0 0 0 83996 18 0 0 25 0 1 0 429685135 26615808 6001 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6498 6001 603 41 0 6457 0
vsize: 25992
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6439 0 0 0 84996 18 0 0 25 0 1 0 429685135 26615808 6001 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6498 6001 603 41 0 6457 0
vsize: 25992
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6777 0 0 0 85995 20 0 0 25 0 1 0 429685135 27967488 6329 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6828 6329 603 41 0 6787 0
vsize: 27312
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6777 0 0 0 86995 20 0 0 25 0 1 0 429685135 27967488 6329 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6828 6329 603 41 0 6787 0
vsize: 27312
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6777 0 0 0 87995 20 0 0 25 0 1 0 429685135 27967488 6329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6828 6329 603 41 0 6787 0
vsize: 27312
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6777 0 0 0 88995 20 0 0 25 0 1 0 429685135 27967488 6329 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6828 6329 603 41 0 6787 0
vsize: 27312
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6777 0 0 0 89995 20 0 0 25 0 1 0 429685135 27967488 6329 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6828 6329 603 41 0 6787 0
vsize: 27312
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6974 0 0 0 90996 20 0 0 25 0 1 0 429685135 28905472 6526 4294967295 134512640 134672761 3221224576 3221223632 134644275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7057 6526 603 41 0 7016 0
vsize: 28228
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6974 0 0 0 91996 20 0 0 25 0 1 0 429685135 28643328 6485 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6993 6485 603 41 0 6952 0
vsize: 27972
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6974 0 0 0 92996 20 0 0 25 0 1 0 429685135 28643328 6485 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6993 6485 603 41 0 6952 0
vsize: 27972
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6974 0 0 0 93996 20 0 0 25 0 1 0 429685135 28643328 6485 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6993 6485 603 41 0 6952 0
vsize: 27972
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 6974 0 0 0 94996 20 0 0 25 0 1 0 429685135 28643328 6485 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6993 6485 603 41 0 6952 0
vsize: 27972
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7131 0 0 0 95996 20 0 0 25 0 1 0 429685135 29298688 6642 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7153 6642 603 41 0 7112 0
vsize: 28612
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7298 0 0 0 96996 20 0 0 25 0 1 0 429685135 29806592 6768 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7277 6768 603 41 0 7236 0
vsize: 29108
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7298 0 0 0 97996 20 0 0 25 0 1 0 429685135 29806592 6768 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7277 6768 603 41 0 7236 0
vsize: 29108
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7298 0 0 0 98996 20 0 0 25 0 1 0 429685135 29806592 6768 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7277 6768 603 41 0 7236 0
vsize: 29108
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7298 0 0 0 99997 20 0 0 25 0 1 0 429685135 29806592 6768 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7277 6768 603 41 0 7236 0
vsize: 29108
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7298 0 0 0 100997 20 0 0 25 0 1 0 429685135 29806592 6768 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7277 6768 603 41 0 7236 0
vsize: 29108
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7316 0 0 0 101997 21 0 0 25 0 1 0 429685135 29839360 6776 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7285 6776 603 41 0 7244 0
vsize: 29140
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7316 0 0 0 102997 21 0 0 25 0 1 0 429685135 29839360 6776 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7285 6776 603 41 0 7244 0
vsize: 29140
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7316 0 0 0 103997 21 0 0 25 0 1 0 429685135 29839360 6776 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7285 6776 603 41 0 7244 0
vsize: 29140
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7316 0 0 0 104997 21 0 0 25 0 1 0 429685135 29839360 6776 4294967295 134512640 134672761 3221224576 3221223700 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7285 6776 603 41 0 7244 0
vsize: 29140
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7317 0 0 0 105997 21 0 0 25 0 1 0 429685135 29839360 6777 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7285 6777 603 41 0 7244 0
vsize: 29140
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7354 0 0 0 106998 21 0 0 25 0 1 0 429685135 29904896 6800 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6800 603 41 0 7260 0
vsize: 29204
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7354 0 0 0 107998 21 0 0 25 0 1 0 429685135 29904896 6800 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6800 603 41 0 7260 0
vsize: 29204
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7356 0 0 0 108998 21 0 0 25 0 1 0 429685135 29904896 6802 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6802 603 41 0 7260 0
vsize: 29204
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7356 0 0 0 109998 21 0 0 25 0 1 0 429685135 29904896 6802 4294967295 134512640 134672761 3221224576 3221223760 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6802 603 41 0 7260 0
vsize: 29204
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7356 0 0 0 110998 21 0 0 25 0 1 0 429685135 29904896 6802 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7301 6802 603 41 0 7260 0
vsize: 29204
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19972
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7425 0 0 0 111998 21 0 0 25 0 1 0 429685135 30003200 6826 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7325 6826 603 41 0 7284 0
vsize: 29300
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 3/59 20024
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7425 0 0 0 112998 21 0 0 25 0 1 0 429685135 30003200 6826 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7325 6826 603 41 0 7284 0
vsize: 29300
[startup+1140.04 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 20025
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7425 0 0 0 113998 21 0 0 25 0 1 0 429685135 30003200 6826 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7325 6826 603 41 0 7284 0
vsize: 29300
[startup+1150.04 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 20025
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7425 0 0 0 114998 21 0 0 25 0 1 0 429685135 30003200 6826 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7325 6826 603 41 0 7284 0
vsize: 29300
[startup+1160.04 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 20025
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7425 0 0 0 115998 21 0 0 25 0 1 0 429685135 30003200 6826 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7325 6826 603 41 0 7284 0
vsize: 29300
[startup+1170.04 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 20025
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7425 0 0 0 116998 21 0 0 25 0 1 0 429685135 30003200 6826 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7325 6826 603 41 0 7284 0
vsize: 29300
[startup+1180.04 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 20025
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7455 0 0 0 117999 22 0 0 25 0 1 0 429685135 30068736 6842 4294967295 134512640 134672761 3221224576 3221223616 134614330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7341 6842 603 41 0 7300 0
vsize: 29364
[startup+1190.04 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 20025
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7455 0 0 0 118999 22 0 0 25 0 1 0 429685135 30068736 6842 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7341 6842 603 41 0 7300 0
vsize: 29364
[startup+1200.04 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 20027
Raw data (stat): 19972 (minisat+) R 19971 5897 5896 0 -1 0 7455 0 0 0 119999 22 0 0 25 0 1 0 429685135 30068736 6842 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7341 6842 603 41 0 7300 0
vsize: 29364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.05 1.00 0.92 1/54 20027
Raw data (stat): 19972 (minisat+) Z 19971 5897 5896 0 -1 12 7455 0 0 0 119999 23 0 0 25 0 1 0 429685135 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.23
CPU user time (s): 1199.99
CPU system time (s): 0.235964
CPU usage (%): 100.014
Max. virtual memory (Kb): 29364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####